Left Termination of the query pattern
f(a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

f(X) :- ','(p(X), q(X)).
p(a) :- !.
p(X) :- p(Y).
q(b).

Query: f(a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: f(T1)\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: f(T1), SCOPE: 1, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(p(T4), q(T4))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(p(T4), q(T4)), SCOPE: 2, CLAUSE: 1 | ','(p(T4), q(T4)), SCOPE: 2, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(!_2, q(a)) | ','(p(T4), q(T4)), SCOPE: 2, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(p(T4), q(T4)), SCOPE: 2, CLAUSE: 2\n\np(T4) !=? p(a)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: q(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: q(a), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(p(X7), q(T9))\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: p(X7)\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: q(T9)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: p(X7), SCOPE: 4, CLAUSE: 1 | p(X7), SCOPE: 4, CLAUSE: 2\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: !_4 | p(X7), SCOPE: 4, CLAUSE: 2\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: q(T9), SCOPE: 5, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 51 [arrowhead = none ];
51 -> 4;

52 [label="ONLY EVAL with clause\nf(X2) :- ','(p(X2), q(X2)).\nand substitutionT1 -> T4,\nX2 -> T4,\nT3 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 52 [arrowhead = none ];
52 -> 7;

53 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 53 [arrowhead = none ];
53 -> 10;

54 [label="EVAL with clause\np(a) :- !_2.\nand substitutionT4 -> a", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 54 [arrowhead = none ];
54 -> 12;

55 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 55 [arrowhead = none ];
55 -> 14;

56 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 56 [arrowhead = none ];
56 -> 17;

57 [label="ONLY EVAL with clause\np(X6) :- p(X7).\nand substitutionT4 -> T9,\nX6 -> T9,\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 57 [arrowhead = none ];
57 -> 24;

58 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 58 [arrowhead = none ];
58 -> 18;

59 [label="BACKTRACK\nfor clause: q(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 59 [arrowhead = none ];
59 -> 20;

60 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
24 -> 60 [arrowhead = none ];
60 -> 31;

61 [label="SPLIT 2\nreplacements:X7 -> T10", fontsize=14, style = filled, fillcolor = violet];
24 -> 61 [arrowhead = none ];
61 -> 33;

62 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
31 -> 62 [arrowhead = none ];
62 -> 35;

63 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
33 -> 63 [arrowhead = none ];
63 -> 43;

64 [label="ONLY EVAL with clause\np(a) :- !_4.\nand substitutionX7 -> a", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 64 [arrowhead = none ];
64 -> 37;

65 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 65 [arrowhead = none ];
65 -> 39;

66 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 66 [arrowhead = none ];
66 -> 41;

67 [label="EVAL with clause\nq(b).\nand substitutionT9 -> b", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 67 [arrowhead = none ];
67 -> 46;

68 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 68 [arrowhead = none ];
68 -> 48;

69 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 69 [arrowhead = none ];
69 -> 50;

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1_in → U1(f24_in)
U1(f24_out1(T9)) → f1_out1(T9)
f31_in → f31_out1
f33_in → f33_out1(b)
f24_in → U2(f31_in)
U2(f31_out1) → U3(f33_in)
U3(f33_out1(T9)) → f24_out1(T9)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Knuth-Bendix order [KBO] with precedence:

f1_in > U1₁ > f1_out11 > f24_in > U2₁ > U3₁ > b > f33_in > f33_out11 > f31_in > f31_out1 > f24_out11

and weight map:

f1_in=5
f24_in=4
f31_in=2
f31_out1=1
f33_in=2
b=1
U1_1=1
f24_out1_1=2
f1_out1_1=3
f33_out1_1=1
U2_1=2
U3_1=1

The variable weight is 1With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f1_in → U1(f24_in)
U1(f24_out1(T9)) → f1_out1(T9)
f31_in → f31_out1
f33_in → f33_out1(b)
f24_in → U2(f31_in)
U2(f31_out1) → U3(f33_in)
U3(f33_out1(T9)) → f24_out1(T9)

(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) YES