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

(0) Obligation:

Clauses:

f(0, Y, Z) :- ','(!, eq(Z, 0)).
f(X, Y, Z) :- ','(p(X, P), ','(f(P, Y, U), f(U, Y, Z))).
p(0, 0).
p(s(X), X).
eq(X, X).

Query: f(g,a,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: f(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: f(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(!_1, eq(T10, 0)) | f(0, T2, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX5 is free\nX6 is free\nf(T1, T2, T3) !=? f(0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: eq(T10, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: eq(T10, 0), SCOPE: 2, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(p(T23, X24), ','(f(X24, T26, X25), f(X25, T26, T27)))\n\nT23 is ground\nX5 is free\nX6 is free\nX24 is free\nX25 is free\nf(T23, T2, T3) !=? f(0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(p(T23, X24), ','(f(X24, T26, X25), f(X25, T26, T27))), SCOPE: 3, CLAUSE: 2 | ','(p(T23, X24), ','(f(X24, T26, X25), f(X25, T26, T27))), SCOPE: 3, CLAUSE: 3\n\nT23 is ground\nX5 is free\nX6 is free\nX24 is free\nX25 is free\nf(T23, T2, T3) !=? f(0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(p(T23, X24), ','(f(X24, T26, X25), f(X25, T26, T27))), SCOPE: 3, CLAUSE: 3\n\nT23 is ground\nX5 is free\nX6 is free\nX24 is free\nX25 is free\nf(T23, T2, T3) !=? f(0, X5, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(f(T31, T26, X25), f(X25, T26, T27))\n\nT31 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: f(T31, T26, X25)\n\nT31 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: f(T33, T34, T35)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: f(T31, T26, X25), SCOPE: 4, CLAUSE: 0 | f(T31, T26, X25), SCOPE: 4, CLAUSE: 1\n\nT31 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(!_4, eq(X46, 0)) | f(0, T26, X25), SCOPE: 4, CLAUSE: 1\n\nX25 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: f(T31, T26, X25), SCOPE: 4, CLAUSE: 1\n\nT31 is ground\nX25 is free\nX44 is free\nX45 is free\nf(T31, T26, X25) !=? f(0, X44, X45)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: eq(X46, 0)\n\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: eq(X46, 0), SCOPE: 5, CLAUSE: 4\n\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(p(T46, X69), ','(f(X69, T48, X70), f(X70, T48, X71)))\n\nT46 is ground\nX25 is free\nX44 is free\nX45 is free\nX71 is free\nX69 is free\nX70 is free\nf(T46, T26, X25) !=? f(0, X44, X45)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(p(T46, X69), ','(f(X69, T48, X70), f(X70, T48, X71))), SCOPE: 6, CLAUSE: 2 | ','(p(T46, X69), ','(f(X69, T48, X70), f(X70, T48, X71))), SCOPE: 6, CLAUSE: 3\n\nT46 is ground\nX25 is free\nX44 is free\nX45 is free\nX71 is free\nX69 is free\nX70 is free\nf(T46, T26, X25) !=? f(0, X44, X45)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(p(T46, X69), ','(f(X69, T48, X70), f(X70, T48, X71))), SCOPE: 6, CLAUSE: 3\n\nT46 is ground\nX25 is free\nX44 is free\nX45 is free\nX71 is free\nX69 is free\nX70 is free\nf(T46, T26, X25) !=? f(0, X44, X45)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(f(T52, T48, X70), f(X70, T48, X71))\n\nT52 is ground\nX71 is free\nX70 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: f(T52, T48, X70)\n\nT52 is ground\nX70 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: f(T54, T55, X71)\n\nT54 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 91 [arrowhead = none ];
91 -> 5;

92 [label="EVAL with clause\nf(0, X5, X6) :- ','(!_1, eq(X6, 0)).\nand substitutionT1 -> 0,\nT2 -> T8,\nX5 -> T8,\nT3 -> T10,\nX6 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 92 [arrowhead = none ];
92 -> 9;

93 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 93 [arrowhead = none ];
93 -> 12;

94 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 94 [arrowhead = none ];
94 -> 13;

95 [label="ONLY EVAL with clause\nf(X21, X22, X23) :- ','(p(X21, X24), ','(f(X24, X22, X25), f(X25, X22, X23))).\nand substitutionT1 -> T23,\nX21 -> T23,\nT2 -> T26,\nX22 -> T26,\nT3 -> T27,\nX23 -> T27,\nT24 -> T26,\nT25 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 95 [arrowhead = none ];
95 -> 32;

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

97 [label="EVAL with clause\neq(X9, X9).\nand substitutionT10 -> 0,\nX9 -> 0,\nT13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 97 [arrowhead = none ];
97 -> 22;

98 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 98 [arrowhead = none ];
98 -> 26;

99 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 99 [arrowhead = none ];
99 -> 27;

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

101 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(T23, T2, T3), f(0, X5, X6))", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 101 [arrowhead = none ];
101 -> 40;

102 [label="EVAL with clause\np(s(X31), X31).\nand substitutionX31 -> T31,\nT23 -> s(T31),\nX24 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 102 [arrowhead = none ];
102 -> 41;

103 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 103 [arrowhead = none ];
103 -> 42;

104 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
41 -> 104 [arrowhead = none ];
104 -> 47;

105 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT33 is ground\nreplacements:X25 -> T33,\nT26 -> T34,\nT27 -> T35", fontsize=14, style = filled, fillcolor = violet];
41 -> 105 [arrowhead = none ];
105 -> 48;

106 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
47 -> 106 [arrowhead = none ];
106 -> 51;

107 [label="INSTANCE with matching:\nT1 -> T33\nT2 -> T34\nT3 -> T35", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 107 [arrowhead = none , style=dashed];
107 -> 3[style=dashed];

108 [label="EVAL with clause\nf(0, X44, X45) :- ','(!_4, eq(X45, 0)).\nand substitutionT31 -> 0,\nT26 -> T39,\nX44 -> T39,\nX25 -> X46,\nX45 -> X46", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 108 [arrowhead = none ];
108 -> 60;

109 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 109 [arrowhead = none ];
109 -> 65;

110 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 110 [arrowhead = none ];
110 -> 72;

111 [label="ONLY EVAL with clause\nf(X66, X67, X68) :- ','(p(X66, X69), ','(f(X69, X67, X70), f(X70, X67, X68))).\nand substitutionT31 -> T46,\nX66 -> T46,\nT26 -> T48,\nX67 -> T48,\nX25 -> X71,\nX68 -> X71,\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 111 [arrowhead = none ];
111 -> 84;

112 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 112 [arrowhead = none ];
112 -> 73;

113 [label="ONLY EVAL with clause\neq(X51, X51).\nand substitutionX46 -> 0,\nX51 -> 0,\nX52 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 113 [arrowhead = none ];
113 -> 78;

114 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 114 [arrowhead = none ];
114 -> 79;

115 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
84 -> 115 [arrowhead = none ];
115 -> 85;

116 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (f(T46, T26, X25), f(0, X44, X45))", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 116 [arrowhead = none ];
116 -> 86;

117 [label="EVAL with clause\np(s(X77), X77).\nand substitutionX77 -> T52,\nT46 -> s(T52),\nX69 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 117 [arrowhead = none ];
117 -> 87;

118 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 118 [arrowhead = none ];
118 -> 88;

119 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
87 -> 119 [arrowhead = none ];
119 -> 89;

120 [label="SPLIT 2\nnew knowledge:\nT52 is ground\nT54 is ground\nreplacements:X70 -> T54,\nT48 -> T55", fontsize=14, style = filled, fillcolor = violet];
87 -> 120 [arrowhead = none ];
120 -> 90;

121 [label="INSTANCE with matching:\nT31 -> T52\nT26 -> T48\nX25 -> X70", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 121 [arrowhead = none , style=dashed];
121 -> 47[style=dashed];

122 [label="INSTANCE with matching:\nT31 -> T54\nT26 -> T55\nX25 -> X71", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 122 [arrowhead = none , style=dashed];
122 -> 47[style=dashed];

}

(2) Obligation:

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

f3_in(0) → f3_out1(0)
f3_in(s(T31)) → U1(f41_in(T31), s(T31))
U1(f41_out1(X25, T27), s(T31)) → f3_out1(T27)
f47_in(0) → f47_out1(0)
f47_in(s(T52)) → U2(f87_in(T52), s(T52))
U2(f87_out1(X70, X71), s(T52)) → f47_out1(X71)
f41_in(T31) → U3(f47_in(T31), T31)
U3(f47_out1(T33), T31) → U4(f3_in(T33), T31, T33)
U4(f3_out1(T35), T31, T33) → f41_out1(T33, T35)
f87_in(T52) → U5(f47_in(T52), T52)
U5(f47_out1(T54), T52) → U6(f47_in(T54), T52, T54)
U6(f47_out1(X71), T52, T54) → f87_out1(T54, X71)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
f3_in(x1)  =  f3_in(x1)
0  =  0
f3_out1(x1)  =  f3_out1(x1)
s(x1)  =  s(x1)
U1(x1, x2)  =  U1(x1, x2)
f41_in(x1)  =  f41_in(x1)
f41_out1(x1, x2)  =  f41_out1(x1, x2)
f47_in(x1)  =  f47_in(x1)
f47_out1(x1)  =  x1
U2(x1, x2)  =  U2(x1, x2)
f87_in(x1)  =  f87_in(x1)
f87_out1(x1, x2)  =  f87_out1(x1, x2)
U3(x1, x2)  =  U3(x1, x2)
U4(x1, x2, x3)  =  U4(x1, x2, x3)
U5(x1, x2)  =  U5(x1, x2)
U6(x1, x2, x3)  =  U6(x1, x2, x3)

Recursive path order with status [RPO].
Quasi-Precedence:

[s₁, f41_in1] > [f3_in1, U3₂] > 0 > f87_out12
[s₁, f41_in1] > [f3_in1, U3₂] > [f3_out11, U1₂] > f41_out12 > f87_out12
[s₁, f41_in1] > [f3_in1, U3₂] > U4₃ > f41_out12 > f87_out12
[s₁, f41_in1] > f87_in1 > U5₂ > [f47_in1, U2₂] > f87_out12
[s₁, f41_in1] > f87_in1 > U5₂ > U6₃ > f87_out12

Status:

f3_in1: multiset
0: multiset
f3_out11: multiset
s₁: [1]
U1₂: multiset
f41_in1: [1]
f41_out12: multiset
f47_in1: [1]
U2₂: [1,2]
f87_in1: multiset
f87_out12: [1,2]
U3₂: multiset
U4₃: multiset
U5₂: [1,2]
U6₃: [1,2,3]

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

f3_in(0) → f3_out1(0)
f3_in(s(T31)) → U1(f41_in(T31), s(T31))
U1(f41_out1(X25, T27), s(T31)) → f3_out1(T27)
f47_in(0) → f47_out1(0)
f47_in(s(T52)) → U2(f87_in(T52), s(T52))
U2(f87_out1(X70, X71), s(T52)) → f47_out1(X71)
f41_in(T31) → U3(f47_in(T31), T31)
U3(f47_out1(T33), T31) → U4(f3_in(T33), T31, T33)
U4(f3_out1(T35), T31, T33) → f41_out1(T33, T35)
f87_in(T52) → U5(f47_in(T52), T52)
U5(f47_out1(T54), T52) → U6(f47_in(T54), T52, T54)
U6(f47_out1(X71), T52, T54) → f87_out1(T54, X71)

(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