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

(0) Obligation:

Clauses:

m(X, 0, Z) :- ','(!, =(Z, X)).
m(0, Y, Z) :- ','(!, =(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
q(X, Y, Z) :- m(X, Y, Z).
q(X, Y, Z).
=(X, X).

Query: q(g,g,a)

(1) BuiltinConflictTransformerProof (EQUIVALENT transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

m(X, 0, Z) :- ','(!, user_defined_=(Z, X)).
m(0, Y, Z) :- ','(!, user_defined_=(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(X), X).
q(X, Y, Z) :- m(X, Y, Z).
q(X, Y, Z).
user_defined_=(X, X).

Query: q(g,g,a)

(3) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: q(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: q(T1, T2, T3), SCOPE: 1, CLAUSE: 5 | q(T1, T2, T3), SCOPE: 1, CLAUSE: 6\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: m(T7, T8, T10) | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: m(T7, T8, T10), SCOPE: 2, CLAUSE: 0 | m(T7, T8, T10), SCOPE: 2, CLAUSE: 1 | m(T7, T8, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(!_2, user_defined_=(T17, T15)) | m(T15, 0, T10), SCOPE: 2, CLAUSE: 1 | m(T15, 0, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(T15, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: m(T7, T8, T10), SCOPE: 2, CLAUSE: 1 | m(T7, T8, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: user_defined_=(T17, T15) | q(T15, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: user_defined_=(T17, T15)\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: q(T15, 0, T3), SCOPE: 1, CLAUSE: 6\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: user_defined_=(T17, T15), SCOPE: 3, CLAUSE: 7\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(!_2, user_defined_=(T33, 0)) | m(0, T31, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(0, T31, T3), SCOPE: 1, CLAUSE: 6\n\nT31 is ground\nX11 is free\nX12 is free\nm(0, T31, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: m(T7, T8, T10), SCOPE: 2, CLAUSE: 2 | ?_2 | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nX29 is free\nX30 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)\nm(T7, T8, T10) !=? m(0, X29, X30)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: user_defined_=(T33, 0) | q(0, T31, T3), SCOPE: 1, CLAUSE: 6\n\nT31 is ground\nX11 is free\nX12 is free\nm(0, T31, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: user_defined_=(T33, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: q(0, T31, T3), SCOPE: 1, CLAUSE: 6\n\nT31 is ground\nX11 is free\nX12 is free\nm(0, T31, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: user_defined_=(T33, 0), SCOPE: 4, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: m(T7, T8, T10), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nX29 is free\nX30 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)\nm(T7, T8, T10) !=? m(0, X29, X30)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ?_2 | q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nX29 is free\nX30 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)\nm(T7, T8, T10) !=? m(0, X29, X30)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(p(T59, X68), ','(p(T60, X69), m(X68, X69, T62)))\n\nT59 is ground\nT60 is ground\nX11 is free\nX12 is free\nX29 is free\nX30 is free\nX68 is free\nX69 is free\nm(T59, T60, T10) !=? m(X11, 0, X12)\nm(T59, T60, T10) !=? m(0, X29, X30)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(p(T59, X68), ','(p(T60, X69), m(X68, X69, T62))), SCOPE: 5, CLAUSE: 3 | ','(p(T59, X68), ','(p(T60, X69), m(X68, X69, T62))), SCOPE: 5, CLAUSE: 4\n\nT59 is ground\nT60 is ground\nX11 is free\nX12 is free\nX29 is free\nX30 is free\nX68 is free\nX69 is free\nm(T59, T60, T10) !=? m(X11, 0, X12)\nm(T59, T60, T10) !=? m(0, X29, X30)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(p(T59, X68), ','(p(T60, X69), m(X68, X69, T62))), SCOPE: 5, CLAUSE: 4\n\nT59 is ground\nT60 is ground\nX11 is free\nX12 is free\nX29 is free\nX30 is free\nX68 is free\nX69 is free\nm(T59, T60, T10) !=? m(X11, 0, X12)\nm(T59, T60, T10) !=? m(0, X29, X30)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(p(T60, X69), m(T66, X69, T62))\n\nT60 is ground\nT66 is ground\nX11 is free\nX12 is free\nX69 is free\nm(s(T66), T60, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(p(T60, X69), m(T66, X69, T62)), SCOPE: 6, CLAUSE: 3 | ','(p(T60, X69), m(T66, X69, T62)), SCOPE: 6, CLAUSE: 4\n\nT60 is ground\nT66 is ground\nX11 is free\nX12 is free\nX69 is free\nm(s(T66), T60, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(p(T60, X69), m(T66, X69, T62)), SCOPE: 6, CLAUSE: 4\n\nT60 is ground\nT66 is ground\nX11 is free\nX12 is free\nX69 is free\nm(s(T66), T60, T10) !=? m(X11, 0, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="B: m(T66, T71, T62)\n\nT66 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: m(T66, T71, T62), SCOPE: 7, CLAUSE: 0 | m(T66, T71, T62), SCOPE: 7, CLAUSE: 1 | m(T66, T71, T62), SCOPE: 7, CLAUSE: 2\n\nT66 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(!_7, user_defined_=(T80, T78)) | m(T78, 0, T62), SCOPE: 7, CLAUSE: 1 | m(T78, 0, T62), SCOPE: 7, CLAUSE: 2\n\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: m(T66, T71, T62), SCOPE: 7, CLAUSE: 1 | m(T66, T71, T62), SCOPE: 7, CLAUSE: 2\n\nT66 is ground\nT71 is ground\nX87 is free\nX88 is free\nm(T66, T71, T62) !=? m(X87, 0, X88)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: user_defined_=(T80, T78)\n\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: user_defined_=(T80, T78), SCOPE: 8, CLAUSE: 7\n\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(!_7, user_defined_=(T90, 0)) | m(0, T88, T62), SCOPE: 7, CLAUSE: 2\n\nT88 is ground\nX87 is free\nX88 is free\nm(0, T88, T62) !=? m(X87, 0, X88)", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: m(T66, T71, T62), SCOPE: 7, CLAUSE: 2\n\nT66 is ground\nT71 is ground\nX87 is free\nX88 is free\nX96 is free\nX97 is free\nm(T66, T71, T62) !=? m(X87, 0, X88)\nm(T66, T71, T62) !=? m(0, X96, X97)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: user_defined_=(T90, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: user_defined_=(T90, 0), SCOPE: 9, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(p(T102, X115), ','(p(T103, X116), m(X115, X116, T105)))\n\nT102 is ground\nT103 is ground\nX87 is free\nX88 is free\nX96 is free\nX97 is free\nX115 is free\nX116 is free\nm(T102, T103, T62) !=? m(X87, 0, X88)\nm(T102, T103, T62) !=? m(0, X96, X97)", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(p(T102, X115), ','(p(T103, X116), m(X115, X116, T105))), SCOPE: 10, CLAUSE: 3 | ','(p(T102, X115), ','(p(T103, X116), m(X115, X116, T105))), SCOPE: 10, CLAUSE: 4\n\nT102 is ground\nT103 is ground\nX87 is free\nX88 is free\nX96 is free\nX97 is free\nX115 is free\nX116 is free\nm(T102, T103, T62) !=? m(X87, 0, X88)\nm(T102, T103, T62) !=? m(0, X96, X97)", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(p(T102, X115), ','(p(T103, X116), m(X115, X116, T105))), SCOPE: 10, CLAUSE: 4\n\nT102 is ground\nT103 is ground\nX87 is free\nX88 is free\nX96 is free\nX97 is free\nX115 is free\nX116 is free\nm(T102, T103, T62) !=? m(X87, 0, X88)\nm(T102, T103, T62) !=? m(0, X96, X97)", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(p(T103, X116), m(T109, X116, T105))\n\nT103 is ground\nT109 is ground\nX87 is free\nX88 is free\nX116 is free\nm(s(T109), T103, T62) !=? m(X87, 0, X88)", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(p(T103, X116), m(T109, X116, T105)), SCOPE: 11, CLAUSE: 3 | ','(p(T103, X116), m(T109, X116, T105)), SCOPE: 11, CLAUSE: 4\n\nT103 is ground\nT109 is ground\nX87 is free\nX88 is free\nX116 is free\nm(s(T109), T103, T62) !=? m(X87, 0, X88)", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(p(T103, X116), m(T109, X116, T105)), SCOPE: 11, CLAUSE: 4\n\nT103 is ground\nT109 is ground\nX87 is free\nX88 is free\nX116 is free\nm(s(T109), T103, T62) !=? m(X87, 0, X88)", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: m(T109, T114, T105)\n\nT109 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: q(T7, T8, T3), SCOPE: 1, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX11 is free\nX12 is free\nX29 is free\nX30 is free\nm(T7, T8, T10) !=? m(X11, 0, X12)\nm(T7, T8, T10) !=? m(0, X29, X30)", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 160 [arrowhead = none ];
160 -> 5;

161 [label="ONLY EVAL with clause\nq(X4, X5, X6) :- m(X4, X5, X6).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T8,\nX5 -> T8,\nT3 -> T10,\nX6 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 161 [arrowhead = none ];
161 -> 8;

162 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 162 [arrowhead = none ];
162 -> 11;

163 [label="EVAL with clause\nm(X11, 0, X12) :- ','(!_2, user_defined_=(X12, X11)).\nand substitutionT7 -> T15,\nX11 -> T15,\nT8 -> 0,\nT10 -> T17,\nX12 -> T17,\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 163 [arrowhead = none ];
163 -> 13;

164 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 164 [arrowhead = none ];
164 -> 15;

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

166 [label="EVAL with clause\nm(0, X29, X30) :- ','(!_2, user_defined_=(X30, 0)).\nand substitutionT7 -> 0,\nT8 -> T31,\nX29 -> T31,\nT10 -> T33,\nX30 -> T33,\nT32 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 166 [arrowhead = none ];
166 -> 48;

167 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 167 [arrowhead = none ];
167 -> 49;

168 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 168 [arrowhead = none ];
168 -> 21;

169 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 169 [arrowhead = none ];
169 -> 23;

170 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
21 -> 170 [arrowhead = none ];
170 -> 25;

171 [label="ONLY EVAL with clause\nq(X22, X23, X24).\nand substitutionT15 -> T25,\nX22 -> T25,\nX23 -> 0,\nT3 -> T26,\nX24 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 171 [arrowhead = none ];
171 -> 40;

172 [label="EVAL with clause\nuser_defined_=(X15, X15).\nand substitutionT17 -> T20,\nX15 -> T20,\nT15 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 172 [arrowhead = none ];
172 -> 26;

173 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 173 [arrowhead = none ];
173 -> 28;

174 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 174 [arrowhead = none ];
174 -> 30;

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

176 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 176 [arrowhead = none ];
176 -> 53;

177 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
49 -> 177 [arrowhead = none ];
177 -> 82;

178 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
49 -> 178 [arrowhead = none ];
178 -> 83;

179 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 179 [arrowhead = none ];
179 -> 54;

180 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
53 -> 180 [arrowhead = none ];
180 -> 56;

181 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
54 -> 181 [arrowhead = none ];
181 -> 57;

182 [label="ONLY EVAL with clause\nq(X40, X41, X42).\nand substitutionX40 -> 0,\nT31 -> T41,\nX41 -> T41,\nT3 -> T42,\nX42 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 182 [arrowhead = none ];
182 -> 71;

183 [label="EVAL with clause\nuser_defined_=(X33, X33).\nand substitutionT33 -> 0,\nX33 -> 0,\nT36 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 183 [arrowhead = none ];
183 -> 62;

184 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 184 [arrowhead = none ];
184 -> 63;

185 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 185 [arrowhead = none ];
185 -> 65;

186 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 186 [arrowhead = none ];
186 -> 72;

187 [label="ONLY EVAL with clause\nm(X65, X66, X67) :- ','(p(X65, X68), ','(p(X66, X69), m(X68, X69, X67))).\nand substitutionT7 -> T59,\nX65 -> T59,\nT8 -> T60,\nX66 -> T60,\nT10 -> T62,\nX67 -> T62,\nT61 -> T62", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 187 [arrowhead = none ];
187 -> 88;

188 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 188 [arrowhead = none ];
188 -> 157;

189 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
88 -> 189 [arrowhead = none ];
189 -> 90;

190 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T59, T60, T10), m(0, X29, X30))", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 190 [arrowhead = none ];
190 -> 92;

191 [label="EVAL with clause\np(s(X75), X75).\nand substitutionX75 -> T66,\nT59 -> s(T66),\nX68 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 191 [arrowhead = none ];
191 -> 101;

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

193 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
101 -> 193 [arrowhead = none ];
193 -> 110;

194 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(T66), T60, T10), m(X11, 0, X12))", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 194 [arrowhead = none ];
194 -> 111;

195 [label="EVAL with clause\np(s(X80), X80).\nand substitutionX80 -> T71,\nT60 -> s(T71),\nX69 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 195 [arrowhead = none ];
195 -> 113;

196 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 196 [arrowhead = none ];
196 -> 120;

197 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
113 -> 197 [arrowhead = none ];
197 -> 121;

198 [label="EVAL with clause\nm(X87, 0, X88) :- ','(!_7, user_defined_=(X88, X87)).\nand substitutionT66 -> T78,\nX87 -> T78,\nT71 -> 0,\nT62 -> T80,\nX88 -> T80,\nT79 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 198 [arrowhead = none ];
198 -> 122;

199 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
121 -> 199 [arrowhead = none ];
199 -> 123;

200 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 200 [arrowhead = none ];
200 -> 124;

201 [label="EVAL with clause\nm(0, X96, X97) :- ','(!_7, user_defined_=(X97, 0)).\nand substitutionT66 -> 0,\nT71 -> T88,\nX96 -> T88,\nT62 -> T90,\nX97 -> T90,\nT89 -> T90", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 201 [arrowhead = none ];
201 -> 129;

202 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 202 [arrowhead = none ];
202 -> 130;

203 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
124 -> 203 [arrowhead = none ];
203 -> 125;

204 [label="EVAL with clause\nuser_defined_=(X91, X91).\nand substitutionT80 -> T83,\nX91 -> T83,\nT78 -> T83", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 204 [arrowhead = none ];
204 -> 126;

205 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 205 [arrowhead = none ];
205 -> 127;

206 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 206 [arrowhead = none ];
206 -> 128;

207 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 207 [arrowhead = none ];
207 -> 131;

208 [label="ONLY EVAL with clause\nm(X112, X113, X114) :- ','(p(X112, X115), ','(p(X113, X116), m(X115, X116, X114))).\nand substitutionT66 -> T102,\nX112 -> T102,\nT71 -> T103,\nX113 -> T103,\nT62 -> T105,\nX114 -> T105,\nT104 -> T105", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 208 [arrowhead = none ];
208 -> 144;

209 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
131 -> 209 [arrowhead = none ];
209 -> 132;

210 [label="EVAL with clause\nuser_defined_=(X100, X100).\nand substitutionT90 -> 0,\nX100 -> 0,\nT93 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 210 [arrowhead = none ];
210 -> 133;

211 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 211 [arrowhead = none ];
211 -> 139;

212 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 212 [arrowhead = none ];
212 -> 142;

213 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
144 -> 213 [arrowhead = none ];
213 -> 149;

214 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T102, T103, T62), m(0, X96, X97))", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 214 [arrowhead = none ];
214 -> 150;

215 [label="EVAL with clause\np(s(X122), X122).\nand substitutionX122 -> T109,\nT102 -> s(T109),\nX115 -> T109", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 215 [arrowhead = none ];
215 -> 151;

216 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
150 -> 216 [arrowhead = none ];
216 -> 152;

217 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
151 -> 217 [arrowhead = none ];
217 -> 153;

218 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(T109), T103, T62), m(X87, 0, X88))", fontsize=14, style = filled, fillcolor = lightgreen];
153 -> 218 [arrowhead = none ];
218 -> 154;

219 [label="EVAL with clause\np(s(X127), X127).\nand substitutionX127 -> T114,\nT103 -> s(T114),\nX116 -> T114", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 219 [arrowhead = none ];
219 -> 155;

220 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 220 [arrowhead = none ];
220 -> 156;

221 [label="INSTANCE with matching:\nT66 -> T109\nT71 -> T114\nT62 -> T105", fontsize=14, style = filled, fillcolor = lightgrey];
155 -> 221 [arrowhead = none , style=dashed];
221 -> 113[style=dashed];

222 [label="ONLY EVAL with clause\nq(X136, X137, X138).\nand substitutionT7 -> T123,\nX136 -> T123,\nT8 -> T124,\nX137 -> T124,\nT3 -> T125,\nX138 -> T125", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 222 [arrowhead = none ];
222 -> 158;

223 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 223 [arrowhead = none ];
223 -> 159;

}

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

qA_in_gga(T20, 0, T20) → qA_out_gga(T20, 0, T20)
qA_in_gga(T25, 0, T26) → qA_out_gga(T25, 0, T26)
qA_in_gga(0, T31, 0) → qA_out_gga(0, T31, 0)
qA_in_gga(0, T41, T42) → qA_out_gga(0, T41, T42)
qA_in_gga(s(T66), s(T71), T62) → U1_gga(T66, T71, T62, mB_in_gga(T66, T71, T62))
mB_in_gga(T83, 0, T83) → mB_out_gga(T83, 0, T83)
mB_in_gga(0, T88, 0) → mB_out_gga(0, T88, 0)
mB_in_gga(s(T109), s(T114), T105) → U2_gga(T109, T114, T105, mB_in_gga(T109, T114, T105))
U2_gga(T109, T114, T105, mB_out_gga(T109, T114, T105)) → mB_out_gga(s(T109), s(T114), T105)
U1_gga(T66, T71, T62, mB_out_gga(T66, T71, T62)) → qA_out_gga(s(T66), s(T71), T62)
qA_in_gga(T123, T124, T125) → qA_out_gga(T123, T124, T125)

The argument filtering Pi contains the following mapping:
qA_in_gga(x1, x2, x3)  =  qA_in_gga(x1, x2)
0  =  0
qA_out_gga(x1, x2, x3)  =  qA_out_gga(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

QA_IN_GGA(s(T66), s(T71), T62) → U1_GGA(T66, T71, T62, mB_in_gga(T66, T71, T62))
QA_IN_GGA(s(T66), s(T71), T62) → MB_IN_GGA(T66, T71, T62)
MB_IN_GGA(s(T109), s(T114), T105) → U2_GGA(T109, T114, T105, mB_in_gga(T109, T114, T105))
MB_IN_GGA(s(T109), s(T114), T105) → MB_IN_GGA(T109, T114, T105)

The TRS R consists of the following rules:

qA_in_gga(T20, 0, T20) → qA_out_gga(T20, 0, T20)
qA_in_gga(T25, 0, T26) → qA_out_gga(T25, 0, T26)
qA_in_gga(0, T31, 0) → qA_out_gga(0, T31, 0)
qA_in_gga(0, T41, T42) → qA_out_gga(0, T41, T42)
qA_in_gga(s(T66), s(T71), T62) → U1_gga(T66, T71, T62, mB_in_gga(T66, T71, T62))
mB_in_gga(T83, 0, T83) → mB_out_gga(T83, 0, T83)
mB_in_gga(0, T88, 0) → mB_out_gga(0, T88, 0)
mB_in_gga(s(T109), s(T114), T105) → U2_gga(T109, T114, T105, mB_in_gga(T109, T114, T105))
U2_gga(T109, T114, T105, mB_out_gga(T109, T114, T105)) → mB_out_gga(s(T109), s(T114), T105)
U1_gga(T66, T71, T62, mB_out_gga(T66, T71, T62)) → qA_out_gga(s(T66), s(T71), T62)
qA_in_gga(T123, T124, T125) → qA_out_gga(T123, T124, T125)

The argument filtering Pi contains the following mapping:
qA_in_gga(x1, x2, x3)  =  qA_in_gga(x1, x2)
0  =  0
qA_out_gga(x1, x2, x3)  =  qA_out_gga(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
QA_IN_GGA(x1, x2, x3)  =  QA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
MB_IN_GGA(x1, x2, x3)  =  MB_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QA_IN_GGA(s(T66), s(T71), T62) → U1_GGA(T66, T71, T62, mB_in_gga(T66, T71, T62))
QA_IN_GGA(s(T66), s(T71), T62) → MB_IN_GGA(T66, T71, T62)
MB_IN_GGA(s(T109), s(T114), T105) → U2_GGA(T109, T114, T105, mB_in_gga(T109, T114, T105))
MB_IN_GGA(s(T109), s(T114), T105) → MB_IN_GGA(T109, T114, T105)

The TRS R consists of the following rules:

qA_in_gga(T20, 0, T20) → qA_out_gga(T20, 0, T20)
qA_in_gga(T25, 0, T26) → qA_out_gga(T25, 0, T26)
qA_in_gga(0, T31, 0) → qA_out_gga(0, T31, 0)
qA_in_gga(0, T41, T42) → qA_out_gga(0, T41, T42)
qA_in_gga(s(T66), s(T71), T62) → U1_gga(T66, T71, T62, mB_in_gga(T66, T71, T62))
mB_in_gga(T83, 0, T83) → mB_out_gga(T83, 0, T83)
mB_in_gga(0, T88, 0) → mB_out_gga(0, T88, 0)
mB_in_gga(s(T109), s(T114), T105) → U2_gga(T109, T114, T105, mB_in_gga(T109, T114, T105))
U2_gga(T109, T114, T105, mB_out_gga(T109, T114, T105)) → mB_out_gga(s(T109), s(T114), T105)
U1_gga(T66, T71, T62, mB_out_gga(T66, T71, T62)) → qA_out_gga(s(T66), s(T71), T62)
qA_in_gga(T123, T124, T125) → qA_out_gga(T123, T124, T125)

The argument filtering Pi contains the following mapping:
qA_in_gga(x1, x2, x3)  =  qA_in_gga(x1, x2)
0  =  0
qA_out_gga(x1, x2, x3)  =  qA_out_gga(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
QA_IN_GGA(x1, x2, x3)  =  QA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
MB_IN_GGA(x1, x2, x3)  =  MB_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MB_IN_GGA(s(T109), s(T114), T105) → MB_IN_GGA(T109, T114, T105)

The TRS R consists of the following rules:

qA_in_gga(T20, 0, T20) → qA_out_gga(T20, 0, T20)
qA_in_gga(T25, 0, T26) → qA_out_gga(T25, 0, T26)
qA_in_gga(0, T31, 0) → qA_out_gga(0, T31, 0)
qA_in_gga(0, T41, T42) → qA_out_gga(0, T41, T42)
qA_in_gga(s(T66), s(T71), T62) → U1_gga(T66, T71, T62, mB_in_gga(T66, T71, T62))
mB_in_gga(T83, 0, T83) → mB_out_gga(T83, 0, T83)
mB_in_gga(0, T88, 0) → mB_out_gga(0, T88, 0)
mB_in_gga(s(T109), s(T114), T105) → U2_gga(T109, T114, T105, mB_in_gga(T109, T114, T105))
U2_gga(T109, T114, T105, mB_out_gga(T109, T114, T105)) → mB_out_gga(s(T109), s(T114), T105)
U1_gga(T66, T71, T62, mB_out_gga(T66, T71, T62)) → qA_out_gga(s(T66), s(T71), T62)
qA_in_gga(T123, T124, T125) → qA_out_gga(T123, T124, T125)

The argument filtering Pi contains the following mapping:
qA_in_gga(x1, x2, x3)  =  qA_in_gga(x1, x2)
0  =  0
qA_out_gga(x1, x2, x3)  =  qA_out_gga(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
mB_in_gga(x1, x2, x3)  =  mB_in_gga(x1, x2)
mB_out_gga(x1, x2, x3)  =  mB_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
MB_IN_GGA(x1, x2, x3)  =  MB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(9) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(10) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MB_IN_GGA(s(T109), s(T114), T105) → MB_IN_GGA(T109, T114, T105)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MB_IN_GGA(x1, x2, x3)  =  MB_IN_GGA(x1, x2)

We have to consider all (P,R,Pi)-chains

(11) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MB_IN_GGA(s(T109), s(T114)) → MB_IN_GGA(T109, T114)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(13) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MB_IN_GGA(s(T109), s(T114)) → MB_IN_GGA(T109, T114)
  The graph contains the following edges 1 > 1, 2 > 2

(14) YES