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

(0) Obligation:

Clauses:

mul(X1, 0, Z) :- ','(!, eq(Z, 0)).
mul(X, Y, Z) :- ','(p(Y, P), ','(mul(X, P, V), add(X, V, Z))).
add(X, 0, Z) :- ','(!, eq(Z, X)).
add(X, Y, Z) :- ','(p(Y, V), ','(add(X, V, W), p(Z, W))).
p(0, 0).
p(s(X), X).
eq(X, X).

Query: mul(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: mul(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: mul(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | mul(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(!_1, eq(T8, 0)) | mul(T6, 0, T3), SCOPE: 1, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: mul(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nX4 is free\nX5 is free\nmul(T1, T2, T3) !=? mul(X4, 0, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: eq(T8, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: eq(T8, 0), SCOPE: 2, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(p(T16, X15), ','(mul(T15, X15, X16), add(T15, X16, T18)))\n\nT15 is ground\nT16 is ground\nX4 is free\nX5 is free\nX15 is free\nX16 is free\nmul(T15, T16, T3) !=? mul(X4, 0, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(p(T16, X15), ','(mul(T15, X15, X16), add(T15, X16, T18))), SCOPE: 3, CLAUSE: 4 | ','(p(T16, X15), ','(mul(T15, X15, X16), add(T15, X16, T18))), SCOPE: 3, CLAUSE: 5\n\nT15 is ground\nT16 is ground\nX4 is free\nX5 is free\nX15 is free\nX16 is free\nmul(T15, T16, T3) !=? mul(X4, 0, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(p(T16, X15), ','(mul(T15, X15, X16), add(T15, X16, T18))), SCOPE: 3, CLAUSE: 5\n\nT15 is ground\nT16 is ground\nX4 is free\nX5 is free\nX15 is free\nX16 is free\nmul(T15, T16, T3) !=? mul(X4, 0, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="B: ','(mul(T15, T21, X16), add(T15, X16, T18))\n\nT15 is ground\nT21 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="C: mul(T15, T21, X16)\n\nT15 is ground\nT21 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="G: add(T15, T23, T18)\n\nT15 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: mul(T15, T21, X16), SCOPE: 4, CLAUSE: 0 | mul(T15, T21, X16), SCOPE: 4, CLAUSE: 1\n\nT15 is ground\nT21 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(!_4, eq(X34, 0)) | mul(T27, 0, X16), SCOPE: 4, CLAUSE: 1\n\nT27 is ground\nX16 is free\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: mul(T15, T21, X16), SCOPE: 4, CLAUSE: 1\n\nT15 is ground\nT21 is ground\nX16 is free\nX32 is free\nX33 is free\nmul(T15, T21, X16) !=? mul(X32, 0, X33)", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: eq(X34, 0)\n\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: eq(X34, 0), SCOPE: 5, CLAUSE: 6\n\nX34 is free", 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];
77 [label="77: ','(p(T34, X57), ','(mul(T33, X57, X58), add(T33, X58, X59)))\n\nT33 is ground\nT34 is ground\nX16 is free\nX32 is free\nX33 is free\nX59 is free\nX57 is free\nX58 is free\nmul(T33, T34, X16) !=? mul(X32, 0, X33)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(p(T34, X57), ','(mul(T33, X57, X58), add(T33, X58, X59))), SCOPE: 6, CLAUSE: 4 | ','(p(T34, X57), ','(mul(T33, X57, X58), add(T33, X58, X59))), SCOPE: 6, CLAUSE: 5\n\nT33 is ground\nT34 is ground\nX16 is free\nX32 is free\nX33 is free\nX59 is free\nX57 is free\nX58 is free\nmul(T33, T34, X16) !=? mul(X32, 0, X33)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(p(T34, X57), ','(mul(T33, X57, X58), add(T33, X58, X59))), SCOPE: 6, CLAUSE: 5\n\nT33 is ground\nT34 is ground\nX16 is free\nX32 is free\nX33 is free\nX59 is free\nX57 is free\nX58 is free\nmul(T33, T34, X16) !=? mul(X32, 0, X33)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="D: ','(mul(T33, T38, X58), add(T33, X58, X59))\n\nT33 is ground\nT38 is ground\nX59 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: mul(T33, T38, X58)\n\nT33 is ground\nT38 is ground\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="E: add(T33, T40, X59)\n\nT33 is ground\nT40 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: add(T33, T40, X59), SCOPE: 7, CLAUSE: 2 | add(T33, T40, X59), SCOPE: 7, CLAUSE: 3\n\nT33 is ground\nT40 is ground\nX59 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(!_7, eq(X83, T45)) | add(T45, 0, X59), SCOPE: 7, CLAUSE: 3\n\nT45 is ground\nX59 is free\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: add(T33, T40, X59), SCOPE: 7, CLAUSE: 3\n\nT33 is ground\nT40 is ground\nX59 is free\nX81 is free\nX82 is free\nadd(T33, T40, X59) !=? add(X81, 0, X82)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: eq(X83, T45)\n\nT45 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: eq(X83, T45), SCOPE: 8, CLAUSE: 6\n\nT45 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(p(T55, X106), ','(add(T54, X106, X107), p(X108, X107)))\n\nT54 is ground\nT55 is ground\nX59 is free\nX81 is free\nX82 is free\nX108 is free\nX106 is free\nX107 is free\nadd(T54, T55, X59) !=? add(X81, 0, X82)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(p(T55, X106), ','(add(T54, X106, X107), p(X108, X107))), SCOPE: 9, CLAUSE: 4 | ','(p(T55, X106), ','(add(T54, X106, X107), p(X108, X107))), SCOPE: 9, CLAUSE: 5\n\nT54 is ground\nT55 is ground\nX59 is free\nX81 is free\nX82 is free\nX108 is free\nX106 is free\nX107 is free\nadd(T54, T55, X59) !=? add(X81, 0, X82)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(p(T55, X106), ','(add(T54, X106, X107), p(X108, X107))), SCOPE: 9, CLAUSE: 5\n\nT54 is ground\nT55 is ground\nX59 is free\nX81 is free\nX82 is free\nX108 is free\nX106 is free\nX107 is free\nadd(T54, T55, X59) !=? add(X81, 0, X82)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="F: ','(add(T54, T59, X107), p(X108, X107))\n\nT54 is ground\nT59 is ground\nX108 is free\nX107 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: add(T54, T59, X107)\n\nT54 is ground\nT59 is ground\nX107 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="I: p(X108, T61)\n\nT61 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: p(X108, T61), SCOPE: 10, CLAUSE: 4 | p(X108, T61), SCOPE: 10, CLAUSE: 5\n\nT61 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: p(X108, T61), SCOPE: 10, CLAUSE: 4\n\nT61 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: p(X108, T61), SCOPE: 10, CLAUSE: 5\n\nT61 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: add(T15, T23, T18), SCOPE: 11, CLAUSE: 2 | add(T15, T23, T18), SCOPE: 11, CLAUSE: 3\n\nT15 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(!_11, eq(T74, T72)) | add(T72, 0, T18), SCOPE: 11, CLAUSE: 3\n\nT72 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: add(T15, T23, T18), SCOPE: 11, CLAUSE: 3\n\nT15 is ground\nT23 is ground\nX133 is free\nX134 is free\nadd(T15, T23, T18) !=? add(X133, 0, X134)", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: eq(T74, T72)\n\nT72 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: eq(T74, T72), SCOPE: 12, CLAUSE: 6\n\nT72 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(p(T87, X152), ','(add(T86, X152, X153), p(T89, X153)))\n\nT86 is ground\nT87 is ground\nX133 is free\nX134 is free\nX152 is free\nX153 is free\nadd(T86, T87, T18) !=? add(X133, 0, X134)", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(p(T87, X152), ','(add(T86, X152, X153), p(T89, X153))), SCOPE: 13, CLAUSE: 4 | ','(p(T87, X152), ','(add(T86, X152, X153), p(T89, X153))), SCOPE: 13, CLAUSE: 5\n\nT86 is ground\nT87 is ground\nX133 is free\nX134 is free\nX152 is free\nX153 is free\nadd(T86, T87, T18) !=? add(X133, 0, X134)", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(p(T87, X152), ','(add(T86, X152, X153), p(T89, X153))), SCOPE: 13, CLAUSE: 5\n\nT86 is ground\nT87 is ground\nX133 is free\nX134 is free\nX152 is free\nX153 is free\nadd(T86, T87, T18) !=? add(X133, 0, X134)", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="H: ','(add(T86, T93, X153), p(T89, X153))\n\nT86 is ground\nT93 is ground\nX153 is free", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: add(T86, T93, X153)\n\nT86 is ground\nT93 is ground\nX153 is free", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="J: p(T89, T95)\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: p(T89, T95), SCOPE: 14, CLAUSE: 4 | p(T89, T95), SCOPE: 14, CLAUSE: 5\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: p(T89, T95), SCOPE: 14, CLAUSE: 4\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: p(T89, T95), SCOPE: 14, CLAUSE: 5\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 229 [arrowhead = none ];
229 -> 2;

230 [label="EVAL with clause\nmul(X4, 0, X5) :- ','(!_1, eq(X5, 0)).\nand substitutionT1 -> T6,\nX4 -> T6,\nT2 -> 0,\nT3 -> T8,\nX5 -> T8,\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 230 [arrowhead = none ];
230 -> 8;

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

232 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 232 [arrowhead = none ];
232 -> 15;

233 [label="ONLY EVAL with clause\nmul(X12, X13, X14) :- ','(p(X13, X15), ','(mul(X12, X15, X16), add(X12, X16, X14))).\nand substitutionT1 -> T15,\nX12 -> T15,\nT2 -> T16,\nX13 -> T16,\nT3 -> T18,\nX14 -> T18,\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 233 [arrowhead = none ];
233 -> 28;

234 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
15 -> 234 [arrowhead = none ];
234 -> 16;

235 [label="EVAL with clause\neq(X8, X8).\nand substitutionT8 -> 0,\nX8 -> 0,\nT11 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 235 [arrowhead = none ];
235 -> 19;

236 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 236 [arrowhead = none ];
236 -> 22;

237 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 237 [arrowhead = none ];
237 -> 23;

238 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
28 -> 238 [arrowhead = none ];
238 -> 29;

239 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (mul(T15, T16, T3), mul(X4, 0, X5))", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 239 [arrowhead = none ];
239 -> 30;

240 [label="EVAL with clause\np(s(X19), X19).\nand substitutionX19 -> T21,\nT16 -> s(T21),\nX15 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 240 [arrowhead = none ];
240 -> 36;

241 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 241 [arrowhead = none ];
241 -> 37;

242 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
36 -> 242 [arrowhead = none ];
242 -> 43;

243 [label="SPLIT 2\nnew knowledge:\nT15 is ground\nT21 is ground\nT23 is ground\nreplacements:X16 -> T23", fontsize=14, style = filled, fillcolor = violet];
36 -> 243 [arrowhead = none ];
243 -> 44;

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

245 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
44 -> 245 [arrowhead = none ];
245 -> 174;

246 [label="EVAL with clause\nmul(X32, 0, X33) :- ','(!_4, eq(X33, 0)).\nand substitutionT15 -> T27,\nX32 -> T27,\nT21 -> 0,\nX16 -> X34,\nX33 -> X34", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 246 [arrowhead = none ];
246 -> 59;

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

248 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 248 [arrowhead = none ];
248 -> 64;

249 [label="ONLY EVAL with clause\nmul(X54, X55, X56) :- ','(p(X55, X57), ','(mul(X54, X57, X58), add(X54, X58, X56))).\nand substitutionT15 -> T33,\nX54 -> T33,\nT21 -> T34,\nX55 -> T34,\nX16 -> X59,\nX56 -> X59", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 249 [arrowhead = none ];
249 -> 77;

250 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
64 -> 250 [arrowhead = none ];
250 -> 65;

251 [label="ONLY EVAL with clause\neq(X39, X39).\nand substitutionX34 -> 0,\nX39 -> 0,\nX40 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 251 [arrowhead = none ];
251 -> 71;

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

253 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
77 -> 253 [arrowhead = none ];
253 -> 79;

254 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (mul(T33, T34, X16), mul(X32, 0, X33))", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 254 [arrowhead = none ];
254 -> 80;

255 [label="EVAL with clause\np(s(X65), X65).\nand substitutionX65 -> T38,\nT34 -> s(T38),\nX57 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 255 [arrowhead = none ];
255 -> 81;

256 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 256 [arrowhead = none ];
256 -> 83;

257 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
81 -> 257 [arrowhead = none ];
257 -> 90;

258 [label="SPLIT 2\nnew knowledge:\nT33 is ground\nT38 is ground\nT40 is ground\nreplacements:X58 -> T40", fontsize=14, style = filled, fillcolor = violet];
81 -> 258 [arrowhead = none ];
258 -> 91;

259 [label="INSTANCE with matching:\nT15 -> T33\nT21 -> T38\nX16 -> X58", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 259 [arrowhead = none , style=dashed];
259 -> 43[style=dashed];

260 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 260 [arrowhead = none ];
260 -> 92;

261 [label="EVAL with clause\nadd(X81, 0, X82) :- ','(!_7, eq(X82, X81)).\nand substitutionT33 -> T45,\nX81 -> T45,\nT40 -> 0,\nX59 -> X83,\nX82 -> X83", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 261 [arrowhead = none ];
261 -> 93;

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

263 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 263 [arrowhead = none ];
263 -> 95;

264 [label="ONLY EVAL with clause\nadd(X103, X104, X105) :- ','(p(X104, X106), ','(add(X103, X106, X107), p(X105, X107))).\nand substitutionT33 -> T54,\nX103 -> T54,\nT40 -> T55,\nX104 -> T55,\nX59 -> X108,\nX105 -> X108", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 264 [arrowhead = none ];
264 -> 111;

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

266 [label="ONLY EVAL with clause\neq(X88, X88).\nand substitutionX83 -> T48,\nX88 -> T48,\nT45 -> T48,\nX89 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 266 [arrowhead = none ];
266 -> 97;

267 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 267 [arrowhead = none ];
267 -> 98;

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

269 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (add(T54, T55, X59), add(X81, 0, X82))", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 269 [arrowhead = none ];
269 -> 116;

270 [label="EVAL with clause\np(s(X114), X114).\nand substitutionX114 -> T59,\nT55 -> s(T59),\nX106 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 270 [arrowhead = none ];
270 -> 121;

271 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 271 [arrowhead = none ];
271 -> 124;

272 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
121 -> 272 [arrowhead = none ];
272 -> 130;

273 [label="SPLIT 2\nnew knowledge:\nT54 is ground\nT59 is ground\nT61 is ground\nreplacements:X107 -> T61", fontsize=14, style = filled, fillcolor = violet];
121 -> 273 [arrowhead = none ];
273 -> 131;

274 [label="INSTANCE with matching:\nT33 -> T54\nT40 -> T59\nX59 -> X107", fontsize=14, style = filled, fillcolor = lightgrey];
130 -> 274 [arrowhead = none , style=dashed];
274 -> 91[style=dashed];

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

276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
156 -> 276 [arrowhead = none ];
276 -> 159;

277 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
156 -> 277 [arrowhead = none ];
277 -> 160;

278 [label="EVAL with clause\np(0, 0).\nand substitutionX108 -> 0,\nT61 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
159 -> 278 [arrowhead = none ];
278 -> 161;

279 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
159 -> 279 [arrowhead = none ];
279 -> 162;

280 [label="ONLY EVAL with clause\np(s(X125), X125).\nand substitutionX125 -> T65,\nX108 -> s(T65),\nT61 -> T65,\nX126 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 280 [arrowhead = none ];
280 -> 167;

281 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
161 -> 281 [arrowhead = none ];
281 -> 164;

282 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
167 -> 282 [arrowhead = none ];
282 -> 168;

283 [label="EVAL with clause\nadd(X133, 0, X134) :- ','(!_11, eq(X134, X133)).\nand substitutionT15 -> T72,\nX133 -> T72,\nT23 -> 0,\nT18 -> T74,\nX134 -> T74,\nT73 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 283 [arrowhead = none ];
283 -> 179;

284 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
174 -> 284 [arrowhead = none ];
284 -> 182;

285 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
179 -> 285 [arrowhead = none ];
285 -> 183;

286 [label="ONLY EVAL with clause\nadd(X149, X150, X151) :- ','(p(X150, X152), ','(add(X149, X152, X153), p(X151, X153))).\nand substitutionT15 -> T86,\nX149 -> T86,\nT23 -> T87,\nX150 -> T87,\nT18 -> T89,\nX151 -> T89,\nT88 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 286 [arrowhead = none ];
286 -> 213;

287 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
183 -> 287 [arrowhead = none ];
287 -> 184;

288 [label="EVAL with clause\neq(X137, X137).\nand substitutionT74 -> T77,\nX137 -> T77,\nT72 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 288 [arrowhead = none ];
288 -> 185;

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

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

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

292 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (add(T86, T87, T18), add(X133, 0, X134))", fontsize=14, style = filled, fillcolor = lightgreen];
214 -> 292 [arrowhead = none ];
292 -> 215;

293 [label="EVAL with clause\np(s(X159), X159).\nand substitutionX159 -> T93,\nT87 -> s(T93),\nX152 -> T93", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 293 [arrowhead = none ];
293 -> 216;

294 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
215 -> 294 [arrowhead = none ];
294 -> 217;

295 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
216 -> 295 [arrowhead = none ];
295 -> 218;

296 [label="SPLIT 2\nnew knowledge:\nT86 is ground\nT93 is ground\nT95 is ground\nreplacements:X153 -> T95", fontsize=14, style = filled, fillcolor = violet];
216 -> 296 [arrowhead = none ];
296 -> 219;

297 [label="INSTANCE with matching:\nT33 -> T86\nT40 -> T93\nX59 -> X153", fontsize=14, style = filled, fillcolor = lightgrey];
218 -> 297 [arrowhead = none , style=dashed];
297 -> 91[style=dashed];

298 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
219 -> 298 [arrowhead = none ];
298 -> 220;

299 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
220 -> 299 [arrowhead = none ];
299 -> 221;

300 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
220 -> 300 [arrowhead = none ];
300 -> 222;

301 [label="EVAL with clause\np(0, 0).\nand substitutionT89 -> 0,\nT95 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
221 -> 301 [arrowhead = none ];
301 -> 223;

302 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
221 -> 302 [arrowhead = none ];
302 -> 224;

303 [label="EVAL with clause\np(s(X168), X168).\nand substitutionX168 -> T99,\nT89 -> s(T99),\nT95 -> T99", fontsize=14, style = filled, fillcolor = lightblue];
222 -> 303 [arrowhead = none ];
303 -> 226;

304 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
222 -> 304 [arrowhead = none ];
304 -> 227;

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

306 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
226 -> 306 [arrowhead = none ];
306 -> 228;

}

(2) Obligation:

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

mulA_in_gga(T6, 0, 0) → mulA_out_gga(T6, 0, 0)
mulA_in_gga(T15, s(T21), T18) → U1_gga(T15, T21, T18, pB_in_ggaa(T15, T21, X16, T18))
pB_in_ggaa(T15, T21, T23, T18) → U5_ggaa(T15, T21, T23, T18, mulC_in_gga(T15, T21, T23))
mulC_in_gga(T27, 0, 0) → mulC_out_gga(T27, 0, 0)
mulC_in_gga(T33, s(T38), X59) → U2_gga(T33, T38, X59, pD_in_ggaa(T33, T38, X58, X59))
pD_in_ggaa(T33, T38, T40, X59) → U7_ggaa(T33, T38, T40, X59, mulC_in_gga(T33, T38, T40))
U7_ggaa(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → U8_ggaa(T33, T38, T40, X59, addE_in_gga(T33, T40, X59))
addE_in_gga(T48, 0, T48) → addE_out_gga(T48, 0, T48)
addE_in_gga(T54, s(T59), X108) → U3_gga(T54, T59, X108, pF_in_ggaa(T54, T59, X107, X108))
pF_in_ggaa(T54, T59, T61, X108) → U9_ggaa(T54, T59, T61, X108, addE_in_gga(T54, T59, T61))
U9_ggaa(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → U10_ggaa(T54, T59, T61, X108, pI_in_ag(X108, T61))
pI_in_ag(0, 0) → pI_out_ag(0, 0)
pI_in_ag(s(T65), T65) → pI_out_ag(s(T65), T65)
U10_ggaa(T54, T59, T61, X108, pI_out_ag(X108, T61)) → pF_out_ggaa(T54, T59, T61, X108)
U3_gga(T54, T59, X108, pF_out_ggaa(T54, T59, X107, X108)) → addE_out_gga(T54, s(T59), X108)
U8_ggaa(T33, T38, T40, X59, addE_out_gga(T33, T40, X59)) → pD_out_ggaa(T33, T38, T40, X59)
U2_gga(T33, T38, X59, pD_out_ggaa(T33, T38, X58, X59)) → mulC_out_gga(T33, s(T38), X59)
U5_ggaa(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → U6_ggaa(T15, T21, T23, T18, addG_in_gga(T15, T23, T18))
addG_in_gga(T77, 0, T77) → addG_out_gga(T77, 0, T77)
addG_in_gga(T86, s(T93), T89) → U4_gga(T86, T93, T89, pH_in_ggaa(T86, T93, X153, T89))
pH_in_ggaa(T86, T93, T95, T89) → U11_ggaa(T86, T93, T95, T89, addE_in_gga(T86, T93, T95))
U11_ggaa(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → U12_ggaa(T86, T93, T95, T89, pJ_in_ag(T89, T95))
pJ_in_ag(0, 0) → pJ_out_ag(0, 0)
pJ_in_ag(s(T99), T99) → pJ_out_ag(s(T99), T99)
U12_ggaa(T86, T93, T95, T89, pJ_out_ag(T89, T95)) → pH_out_ggaa(T86, T93, T95, T89)
U4_gga(T86, T93, T89, pH_out_ggaa(T86, T93, X153, T89)) → addG_out_gga(T86, s(T93), T89)
U6_ggaa(T15, T21, T23, T18, addG_out_gga(T15, T23, T18)) → pB_out_ggaa(T15, T21, T23, T18)
U1_gga(T15, T21, T18, pB_out_ggaa(T15, T21, X16, T18)) → mulA_out_gga(T15, s(T21), T18)

The argument filtering Pi contains the following mapping:
mulA_in_gga(x1, x2, x3)  =  mulA_in_gga(x1, x2)
0  =  0
mulA_out_gga(x1, x2, x3)  =  mulA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x5)
mulC_in_gga(x1, x2, x3)  =  mulC_in_gga(x1, x2)
mulC_out_gga(x1, x2, x3)  =  mulC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
addE_in_gga(x1, x2, x3)  =  addE_in_gga(x1, x2)
addE_out_gga(x1, x2, x3)  =  addE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
pI_in_ag(x1, x2)  =  pI_in_ag(x2)
pI_out_ag(x1, x2)  =  pI_out_ag(x1, x2)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x1, x2, x3, x5)
addG_in_gga(x1, x2, x3)  =  addG_in_gga(x1, x2)
addG_out_gga(x1, x2, x3)  =  addG_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
pJ_in_ag(x1, x2)  =  pJ_in_ag(x2)
pJ_out_ag(x1, x2)  =  pJ_out_ag(x1, x2)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)

(3) 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:

MULA_IN_GGA(T15, s(T21), T18) → U1_GGA(T15, T21, T18, pB_in_ggaa(T15, T21, X16, T18))
MULA_IN_GGA(T15, s(T21), T18) → PB_IN_GGAA(T15, T21, X16, T18)
PB_IN_GGAA(T15, T21, T23, T18) → U5_GGAA(T15, T21, T23, T18, mulC_in_gga(T15, T21, T23))
PB_IN_GGAA(T15, T21, T23, T18) → MULC_IN_GGA(T15, T21, T23)
MULC_IN_GGA(T33, s(T38), X59) → U2_GGA(T33, T38, X59, pD_in_ggaa(T33, T38, X58, X59))
MULC_IN_GGA(T33, s(T38), X59) → PD_IN_GGAA(T33, T38, X58, X59)
PD_IN_GGAA(T33, T38, T40, X59) → U7_GGAA(T33, T38, T40, X59, mulC_in_gga(T33, T38, T40))
PD_IN_GGAA(T33, T38, T40, X59) → MULC_IN_GGA(T33, T38, T40)
U7_GGAA(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → U8_GGAA(T33, T38, T40, X59, addE_in_gga(T33, T40, X59))
U7_GGAA(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → ADDE_IN_GGA(T33, T40, X59)
ADDE_IN_GGA(T54, s(T59), X108) → U3_GGA(T54, T59, X108, pF_in_ggaa(T54, T59, X107, X108))
ADDE_IN_GGA(T54, s(T59), X108) → PF_IN_GGAA(T54, T59, X107, X108)
PF_IN_GGAA(T54, T59, T61, X108) → U9_GGAA(T54, T59, T61, X108, addE_in_gga(T54, T59, T61))
PF_IN_GGAA(T54, T59, T61, X108) → ADDE_IN_GGA(T54, T59, T61)
U9_GGAA(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → U10_GGAA(T54, T59, T61, X108, pI_in_ag(X108, T61))
U9_GGAA(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → PI_IN_AG(X108, T61)
U5_GGAA(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → U6_GGAA(T15, T21, T23, T18, addG_in_gga(T15, T23, T18))
U5_GGAA(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → ADDG_IN_GGA(T15, T23, T18)
ADDG_IN_GGA(T86, s(T93), T89) → U4_GGA(T86, T93, T89, pH_in_ggaa(T86, T93, X153, T89))
ADDG_IN_GGA(T86, s(T93), T89) → PH_IN_GGAA(T86, T93, X153, T89)
PH_IN_GGAA(T86, T93, T95, T89) → U11_GGAA(T86, T93, T95, T89, addE_in_gga(T86, T93, T95))
PH_IN_GGAA(T86, T93, T95, T89) → ADDE_IN_GGA(T86, T93, T95)
U11_GGAA(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → U12_GGAA(T86, T93, T95, T89, pJ_in_ag(T89, T95))
U11_GGAA(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → PJ_IN_AG(T89, T95)

The TRS R consists of the following rules:

mulA_in_gga(T6, 0, 0) → mulA_out_gga(T6, 0, 0)
mulA_in_gga(T15, s(T21), T18) → U1_gga(T15, T21, T18, pB_in_ggaa(T15, T21, X16, T18))
pB_in_ggaa(T15, T21, T23, T18) → U5_ggaa(T15, T21, T23, T18, mulC_in_gga(T15, T21, T23))
mulC_in_gga(T27, 0, 0) → mulC_out_gga(T27, 0, 0)
mulC_in_gga(T33, s(T38), X59) → U2_gga(T33, T38, X59, pD_in_ggaa(T33, T38, X58, X59))
pD_in_ggaa(T33, T38, T40, X59) → U7_ggaa(T33, T38, T40, X59, mulC_in_gga(T33, T38, T40))
U7_ggaa(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → U8_ggaa(T33, T38, T40, X59, addE_in_gga(T33, T40, X59))
addE_in_gga(T48, 0, T48) → addE_out_gga(T48, 0, T48)
addE_in_gga(T54, s(T59), X108) → U3_gga(T54, T59, X108, pF_in_ggaa(T54, T59, X107, X108))
pF_in_ggaa(T54, T59, T61, X108) → U9_ggaa(T54, T59, T61, X108, addE_in_gga(T54, T59, T61))
U9_ggaa(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → U10_ggaa(T54, T59, T61, X108, pI_in_ag(X108, T61))
pI_in_ag(0, 0) → pI_out_ag(0, 0)
pI_in_ag(s(T65), T65) → pI_out_ag(s(T65), T65)
U10_ggaa(T54, T59, T61, X108, pI_out_ag(X108, T61)) → pF_out_ggaa(T54, T59, T61, X108)
U3_gga(T54, T59, X108, pF_out_ggaa(T54, T59, X107, X108)) → addE_out_gga(T54, s(T59), X108)
U8_ggaa(T33, T38, T40, X59, addE_out_gga(T33, T40, X59)) → pD_out_ggaa(T33, T38, T40, X59)
U2_gga(T33, T38, X59, pD_out_ggaa(T33, T38, X58, X59)) → mulC_out_gga(T33, s(T38), X59)
U5_ggaa(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → U6_ggaa(T15, T21, T23, T18, addG_in_gga(T15, T23, T18))
addG_in_gga(T77, 0, T77) → addG_out_gga(T77, 0, T77)
addG_in_gga(T86, s(T93), T89) → U4_gga(T86, T93, T89, pH_in_ggaa(T86, T93, X153, T89))
pH_in_ggaa(T86, T93, T95, T89) → U11_ggaa(T86, T93, T95, T89, addE_in_gga(T86, T93, T95))
U11_ggaa(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → U12_ggaa(T86, T93, T95, T89, pJ_in_ag(T89, T95))
pJ_in_ag(0, 0) → pJ_out_ag(0, 0)
pJ_in_ag(s(T99), T99) → pJ_out_ag(s(T99), T99)
U12_ggaa(T86, T93, T95, T89, pJ_out_ag(T89, T95)) → pH_out_ggaa(T86, T93, T95, T89)
U4_gga(T86, T93, T89, pH_out_ggaa(T86, T93, X153, T89)) → addG_out_gga(T86, s(T93), T89)
U6_ggaa(T15, T21, T23, T18, addG_out_gga(T15, T23, T18)) → pB_out_ggaa(T15, T21, T23, T18)
U1_gga(T15, T21, T18, pB_out_ggaa(T15, T21, X16, T18)) → mulA_out_gga(T15, s(T21), T18)

The argument filtering Pi contains the following mapping:
mulA_in_gga(x1, x2, x3)  =  mulA_in_gga(x1, x2)
0  =  0
mulA_out_gga(x1, x2, x3)  =  mulA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x5)
mulC_in_gga(x1, x2, x3)  =  mulC_in_gga(x1, x2)
mulC_out_gga(x1, x2, x3)  =  mulC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
addE_in_gga(x1, x2, x3)  =  addE_in_gga(x1, x2)
addE_out_gga(x1, x2, x3)  =  addE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
pI_in_ag(x1, x2)  =  pI_in_ag(x2)
pI_out_ag(x1, x2)  =  pI_out_ag(x1, x2)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x1, x2, x3, x5)
addG_in_gga(x1, x2, x3)  =  addG_in_gga(x1, x2)
addG_out_gga(x1, x2, x3)  =  addG_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
pJ_in_ag(x1, x2)  =  pJ_in_ag(x2)
pJ_out_ag(x1, x2)  =  pJ_out_ag(x1, x2)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
MULA_IN_GGA(x1, x2, x3)  =  MULA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U5_GGAA(x1, x2, x3, x4, x5)  =  U5_GGAA(x1, x2, x5)
MULC_IN_GGA(x1, x2, x3)  =  MULC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x1, x2, x5)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x1, x2, x3, x5)
ADDE_IN_GGA(x1, x2, x3)  =  ADDE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PF_IN_GGAA(x1, x2, x3, x4)  =  PF_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4, x5)  =  U9_GGAA(x1, x2, x5)
U10_GGAA(x1, x2, x3, x4, x5)  =  U10_GGAA(x1, x2, x3, x5)
PI_IN_AG(x1, x2)  =  PI_IN_AG(x2)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x1, x2, x3, x5)
ADDG_IN_GGA(x1, x2, x3)  =  ADDG_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
PJ_IN_AG(x1, x2)  =  PJ_IN_AG(x2)

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

(4) Obligation:

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

MULA_IN_GGA(T15, s(T21), T18) → U1_GGA(T15, T21, T18, pB_in_ggaa(T15, T21, X16, T18))
MULA_IN_GGA(T15, s(T21), T18) → PB_IN_GGAA(T15, T21, X16, T18)
PB_IN_GGAA(T15, T21, T23, T18) → U5_GGAA(T15, T21, T23, T18, mulC_in_gga(T15, T21, T23))
PB_IN_GGAA(T15, T21, T23, T18) → MULC_IN_GGA(T15, T21, T23)
MULC_IN_GGA(T33, s(T38), X59) → U2_GGA(T33, T38, X59, pD_in_ggaa(T33, T38, X58, X59))
MULC_IN_GGA(T33, s(T38), X59) → PD_IN_GGAA(T33, T38, X58, X59)
PD_IN_GGAA(T33, T38, T40, X59) → U7_GGAA(T33, T38, T40, X59, mulC_in_gga(T33, T38, T40))
PD_IN_GGAA(T33, T38, T40, X59) → MULC_IN_GGA(T33, T38, T40)
U7_GGAA(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → U8_GGAA(T33, T38, T40, X59, addE_in_gga(T33, T40, X59))
U7_GGAA(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → ADDE_IN_GGA(T33, T40, X59)
ADDE_IN_GGA(T54, s(T59), X108) → U3_GGA(T54, T59, X108, pF_in_ggaa(T54, T59, X107, X108))
ADDE_IN_GGA(T54, s(T59), X108) → PF_IN_GGAA(T54, T59, X107, X108)
PF_IN_GGAA(T54, T59, T61, X108) → U9_GGAA(T54, T59, T61, X108, addE_in_gga(T54, T59, T61))
PF_IN_GGAA(T54, T59, T61, X108) → ADDE_IN_GGA(T54, T59, T61)
U9_GGAA(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → U10_GGAA(T54, T59, T61, X108, pI_in_ag(X108, T61))
U9_GGAA(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → PI_IN_AG(X108, T61)
U5_GGAA(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → U6_GGAA(T15, T21, T23, T18, addG_in_gga(T15, T23, T18))
U5_GGAA(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → ADDG_IN_GGA(T15, T23, T18)
ADDG_IN_GGA(T86, s(T93), T89) → U4_GGA(T86, T93, T89, pH_in_ggaa(T86, T93, X153, T89))
ADDG_IN_GGA(T86, s(T93), T89) → PH_IN_GGAA(T86, T93, X153, T89)
PH_IN_GGAA(T86, T93, T95, T89) → U11_GGAA(T86, T93, T95, T89, addE_in_gga(T86, T93, T95))
PH_IN_GGAA(T86, T93, T95, T89) → ADDE_IN_GGA(T86, T93, T95)
U11_GGAA(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → U12_GGAA(T86, T93, T95, T89, pJ_in_ag(T89, T95))
U11_GGAA(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → PJ_IN_AG(T89, T95)

The TRS R consists of the following rules:

mulA_in_gga(T6, 0, 0) → mulA_out_gga(T6, 0, 0)
mulA_in_gga(T15, s(T21), T18) → U1_gga(T15, T21, T18, pB_in_ggaa(T15, T21, X16, T18))
pB_in_ggaa(T15, T21, T23, T18) → U5_ggaa(T15, T21, T23, T18, mulC_in_gga(T15, T21, T23))
mulC_in_gga(T27, 0, 0) → mulC_out_gga(T27, 0, 0)
mulC_in_gga(T33, s(T38), X59) → U2_gga(T33, T38, X59, pD_in_ggaa(T33, T38, X58, X59))
pD_in_ggaa(T33, T38, T40, X59) → U7_ggaa(T33, T38, T40, X59, mulC_in_gga(T33, T38, T40))
U7_ggaa(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → U8_ggaa(T33, T38, T40, X59, addE_in_gga(T33, T40, X59))
addE_in_gga(T48, 0, T48) → addE_out_gga(T48, 0, T48)
addE_in_gga(T54, s(T59), X108) → U3_gga(T54, T59, X108, pF_in_ggaa(T54, T59, X107, X108))
pF_in_ggaa(T54, T59, T61, X108) → U9_ggaa(T54, T59, T61, X108, addE_in_gga(T54, T59, T61))
U9_ggaa(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → U10_ggaa(T54, T59, T61, X108, pI_in_ag(X108, T61))
pI_in_ag(0, 0) → pI_out_ag(0, 0)
pI_in_ag(s(T65), T65) → pI_out_ag(s(T65), T65)
U10_ggaa(T54, T59, T61, X108, pI_out_ag(X108, T61)) → pF_out_ggaa(T54, T59, T61, X108)
U3_gga(T54, T59, X108, pF_out_ggaa(T54, T59, X107, X108)) → addE_out_gga(T54, s(T59), X108)
U8_ggaa(T33, T38, T40, X59, addE_out_gga(T33, T40, X59)) → pD_out_ggaa(T33, T38, T40, X59)
U2_gga(T33, T38, X59, pD_out_ggaa(T33, T38, X58, X59)) → mulC_out_gga(T33, s(T38), X59)
U5_ggaa(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → U6_ggaa(T15, T21, T23, T18, addG_in_gga(T15, T23, T18))
addG_in_gga(T77, 0, T77) → addG_out_gga(T77, 0, T77)
addG_in_gga(T86, s(T93), T89) → U4_gga(T86, T93, T89, pH_in_ggaa(T86, T93, X153, T89))
pH_in_ggaa(T86, T93, T95, T89) → U11_ggaa(T86, T93, T95, T89, addE_in_gga(T86, T93, T95))
U11_ggaa(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → U12_ggaa(T86, T93, T95, T89, pJ_in_ag(T89, T95))
pJ_in_ag(0, 0) → pJ_out_ag(0, 0)
pJ_in_ag(s(T99), T99) → pJ_out_ag(s(T99), T99)
U12_ggaa(T86, T93, T95, T89, pJ_out_ag(T89, T95)) → pH_out_ggaa(T86, T93, T95, T89)
U4_gga(T86, T93, T89, pH_out_ggaa(T86, T93, X153, T89)) → addG_out_gga(T86, s(T93), T89)
U6_ggaa(T15, T21, T23, T18, addG_out_gga(T15, T23, T18)) → pB_out_ggaa(T15, T21, T23, T18)
U1_gga(T15, T21, T18, pB_out_ggaa(T15, T21, X16, T18)) → mulA_out_gga(T15, s(T21), T18)

The argument filtering Pi contains the following mapping:
mulA_in_gga(x1, x2, x3)  =  mulA_in_gga(x1, x2)
0  =  0
mulA_out_gga(x1, x2, x3)  =  mulA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x5)
mulC_in_gga(x1, x2, x3)  =  mulC_in_gga(x1, x2)
mulC_out_gga(x1, x2, x3)  =  mulC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
addE_in_gga(x1, x2, x3)  =  addE_in_gga(x1, x2)
addE_out_gga(x1, x2, x3)  =  addE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
pI_in_ag(x1, x2)  =  pI_in_ag(x2)
pI_out_ag(x1, x2)  =  pI_out_ag(x1, x2)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x1, x2, x3, x5)
addG_in_gga(x1, x2, x3)  =  addG_in_gga(x1, x2)
addG_out_gga(x1, x2, x3)  =  addG_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
pJ_in_ag(x1, x2)  =  pJ_in_ag(x2)
pJ_out_ag(x1, x2)  =  pJ_out_ag(x1, x2)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
MULA_IN_GGA(x1, x2, x3)  =  MULA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U5_GGAA(x1, x2, x3, x4, x5)  =  U5_GGAA(x1, x2, x5)
MULC_IN_GGA(x1, x2, x3)  =  MULC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x1, x2, x5)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x1, x2, x3, x5)
ADDE_IN_GGA(x1, x2, x3)  =  ADDE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PF_IN_GGAA(x1, x2, x3, x4)  =  PF_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4, x5)  =  U9_GGAA(x1, x2, x5)
U10_GGAA(x1, x2, x3, x4, x5)  =  U10_GGAA(x1, x2, x3, x5)
PI_IN_AG(x1, x2)  =  PI_IN_AG(x2)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x1, x2, x3, x5)
ADDG_IN_GGA(x1, x2, x3)  =  ADDG_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
PJ_IN_AG(x1, x2)  =  PJ_IN_AG(x2)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 20 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

ADDE_IN_GGA(T54, s(T59), X108) → PF_IN_GGAA(T54, T59, X107, X108)
PF_IN_GGAA(T54, T59, T61, X108) → ADDE_IN_GGA(T54, T59, T61)

The TRS R consists of the following rules:

mulA_in_gga(T6, 0, 0) → mulA_out_gga(T6, 0, 0)
mulA_in_gga(T15, s(T21), T18) → U1_gga(T15, T21, T18, pB_in_ggaa(T15, T21, X16, T18))
pB_in_ggaa(T15, T21, T23, T18) → U5_ggaa(T15, T21, T23, T18, mulC_in_gga(T15, T21, T23))
mulC_in_gga(T27, 0, 0) → mulC_out_gga(T27, 0, 0)
mulC_in_gga(T33, s(T38), X59) → U2_gga(T33, T38, X59, pD_in_ggaa(T33, T38, X58, X59))
pD_in_ggaa(T33, T38, T40, X59) → U7_ggaa(T33, T38, T40, X59, mulC_in_gga(T33, T38, T40))
U7_ggaa(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → U8_ggaa(T33, T38, T40, X59, addE_in_gga(T33, T40, X59))
addE_in_gga(T48, 0, T48) → addE_out_gga(T48, 0, T48)
addE_in_gga(T54, s(T59), X108) → U3_gga(T54, T59, X108, pF_in_ggaa(T54, T59, X107, X108))
pF_in_ggaa(T54, T59, T61, X108) → U9_ggaa(T54, T59, T61, X108, addE_in_gga(T54, T59, T61))
U9_ggaa(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → U10_ggaa(T54, T59, T61, X108, pI_in_ag(X108, T61))
pI_in_ag(0, 0) → pI_out_ag(0, 0)
pI_in_ag(s(T65), T65) → pI_out_ag(s(T65), T65)
U10_ggaa(T54, T59, T61, X108, pI_out_ag(X108, T61)) → pF_out_ggaa(T54, T59, T61, X108)
U3_gga(T54, T59, X108, pF_out_ggaa(T54, T59, X107, X108)) → addE_out_gga(T54, s(T59), X108)
U8_ggaa(T33, T38, T40, X59, addE_out_gga(T33, T40, X59)) → pD_out_ggaa(T33, T38, T40, X59)
U2_gga(T33, T38, X59, pD_out_ggaa(T33, T38, X58, X59)) → mulC_out_gga(T33, s(T38), X59)
U5_ggaa(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → U6_ggaa(T15, T21, T23, T18, addG_in_gga(T15, T23, T18))
addG_in_gga(T77, 0, T77) → addG_out_gga(T77, 0, T77)
addG_in_gga(T86, s(T93), T89) → U4_gga(T86, T93, T89, pH_in_ggaa(T86, T93, X153, T89))
pH_in_ggaa(T86, T93, T95, T89) → U11_ggaa(T86, T93, T95, T89, addE_in_gga(T86, T93, T95))
U11_ggaa(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → U12_ggaa(T86, T93, T95, T89, pJ_in_ag(T89, T95))
pJ_in_ag(0, 0) → pJ_out_ag(0, 0)
pJ_in_ag(s(T99), T99) → pJ_out_ag(s(T99), T99)
U12_ggaa(T86, T93, T95, T89, pJ_out_ag(T89, T95)) → pH_out_ggaa(T86, T93, T95, T89)
U4_gga(T86, T93, T89, pH_out_ggaa(T86, T93, X153, T89)) → addG_out_gga(T86, s(T93), T89)
U6_ggaa(T15, T21, T23, T18, addG_out_gga(T15, T23, T18)) → pB_out_ggaa(T15, T21, T23, T18)
U1_gga(T15, T21, T18, pB_out_ggaa(T15, T21, X16, T18)) → mulA_out_gga(T15, s(T21), T18)

The argument filtering Pi contains the following mapping:
mulA_in_gga(x1, x2, x3)  =  mulA_in_gga(x1, x2)
0  =  0
mulA_out_gga(x1, x2, x3)  =  mulA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x5)
mulC_in_gga(x1, x2, x3)  =  mulC_in_gga(x1, x2)
mulC_out_gga(x1, x2, x3)  =  mulC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
addE_in_gga(x1, x2, x3)  =  addE_in_gga(x1, x2)
addE_out_gga(x1, x2, x3)  =  addE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
pI_in_ag(x1, x2)  =  pI_in_ag(x2)
pI_out_ag(x1, x2)  =  pI_out_ag(x1, x2)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x1, x2, x3, x5)
addG_in_gga(x1, x2, x3)  =  addG_in_gga(x1, x2)
addG_out_gga(x1, x2, x3)  =  addG_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
pJ_in_ag(x1, x2)  =  pJ_in_ag(x2)
pJ_out_ag(x1, x2)  =  pJ_out_ag(x1, x2)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
ADDE_IN_GGA(x1, x2, x3)  =  ADDE_IN_GGA(x1, x2)
PF_IN_GGAA(x1, x2, x3, x4)  =  PF_IN_GGAA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

ADDE_IN_GGA(T54, s(T59), X108) → PF_IN_GGAA(T54, T59, X107, X108)
PF_IN_GGAA(T54, T59, T61, X108) → ADDE_IN_GGA(T54, T59, T61)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

ADDE_IN_GGA(T54, s(T59)) → PF_IN_GGAA(T54, T59)
PF_IN_GGAA(T54, T59) → ADDE_IN_GGA(T54, T59)

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

(12) 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:

• PF_IN_GGAA(T54, T59) → ADDE_IN_GGA(T54, T59)
  The graph contains the following edges 1 >= 1, 2 >= 2

• ADDE_IN_GGA(T54, s(T59)) → PF_IN_GGAA(T54, T59)
  The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

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

MULC_IN_GGA(T33, s(T38), X59) → PD_IN_GGAA(T33, T38, X58, X59)
PD_IN_GGAA(T33, T38, T40, X59) → MULC_IN_GGA(T33, T38, T40)

The TRS R consists of the following rules:

mulA_in_gga(T6, 0, 0) → mulA_out_gga(T6, 0, 0)
mulA_in_gga(T15, s(T21), T18) → U1_gga(T15, T21, T18, pB_in_ggaa(T15, T21, X16, T18))
pB_in_ggaa(T15, T21, T23, T18) → U5_ggaa(T15, T21, T23, T18, mulC_in_gga(T15, T21, T23))
mulC_in_gga(T27, 0, 0) → mulC_out_gga(T27, 0, 0)
mulC_in_gga(T33, s(T38), X59) → U2_gga(T33, T38, X59, pD_in_ggaa(T33, T38, X58, X59))
pD_in_ggaa(T33, T38, T40, X59) → U7_ggaa(T33, T38, T40, X59, mulC_in_gga(T33, T38, T40))
U7_ggaa(T33, T38, T40, X59, mulC_out_gga(T33, T38, T40)) → U8_ggaa(T33, T38, T40, X59, addE_in_gga(T33, T40, X59))
addE_in_gga(T48, 0, T48) → addE_out_gga(T48, 0, T48)
addE_in_gga(T54, s(T59), X108) → U3_gga(T54, T59, X108, pF_in_ggaa(T54, T59, X107, X108))
pF_in_ggaa(T54, T59, T61, X108) → U9_ggaa(T54, T59, T61, X108, addE_in_gga(T54, T59, T61))
U9_ggaa(T54, T59, T61, X108, addE_out_gga(T54, T59, T61)) → U10_ggaa(T54, T59, T61, X108, pI_in_ag(X108, T61))
pI_in_ag(0, 0) → pI_out_ag(0, 0)
pI_in_ag(s(T65), T65) → pI_out_ag(s(T65), T65)
U10_ggaa(T54, T59, T61, X108, pI_out_ag(X108, T61)) → pF_out_ggaa(T54, T59, T61, X108)
U3_gga(T54, T59, X108, pF_out_ggaa(T54, T59, X107, X108)) → addE_out_gga(T54, s(T59), X108)
U8_ggaa(T33, T38, T40, X59, addE_out_gga(T33, T40, X59)) → pD_out_ggaa(T33, T38, T40, X59)
U2_gga(T33, T38, X59, pD_out_ggaa(T33, T38, X58, X59)) → mulC_out_gga(T33, s(T38), X59)
U5_ggaa(T15, T21, T23, T18, mulC_out_gga(T15, T21, T23)) → U6_ggaa(T15, T21, T23, T18, addG_in_gga(T15, T23, T18))
addG_in_gga(T77, 0, T77) → addG_out_gga(T77, 0, T77)
addG_in_gga(T86, s(T93), T89) → U4_gga(T86, T93, T89, pH_in_ggaa(T86, T93, X153, T89))
pH_in_ggaa(T86, T93, T95, T89) → U11_ggaa(T86, T93, T95, T89, addE_in_gga(T86, T93, T95))
U11_ggaa(T86, T93, T95, T89, addE_out_gga(T86, T93, T95)) → U12_ggaa(T86, T93, T95, T89, pJ_in_ag(T89, T95))
pJ_in_ag(0, 0) → pJ_out_ag(0, 0)
pJ_in_ag(s(T99), T99) → pJ_out_ag(s(T99), T99)
U12_ggaa(T86, T93, T95, T89, pJ_out_ag(T89, T95)) → pH_out_ggaa(T86, T93, T95, T89)
U4_gga(T86, T93, T89, pH_out_ggaa(T86, T93, X153, T89)) → addG_out_gga(T86, s(T93), T89)
U6_ggaa(T15, T21, T23, T18, addG_out_gga(T15, T23, T18)) → pB_out_ggaa(T15, T21, T23, T18)
U1_gga(T15, T21, T18, pB_out_ggaa(T15, T21, X16, T18)) → mulA_out_gga(T15, s(T21), T18)

The argument filtering Pi contains the following mapping:
mulA_in_gga(x1, x2, x3)  =  mulA_in_gga(x1, x2)
0  =  0
mulA_out_gga(x1, x2, x3)  =  mulA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U5_ggaa(x1, x2, x3, x4, x5)  =  U5_ggaa(x1, x2, x5)
mulC_in_gga(x1, x2, x3)  =  mulC_in_gga(x1, x2)
mulC_out_gga(x1, x2, x3)  =  mulC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pD_in_ggaa(x1, x2, x3, x4)  =  pD_in_ggaa(x1, x2)
U7_ggaa(x1, x2, x3, x4, x5)  =  U7_ggaa(x1, x2, x5)
U8_ggaa(x1, x2, x3, x4, x5)  =  U8_ggaa(x1, x2, x3, x5)
addE_in_gga(x1, x2, x3)  =  addE_in_gga(x1, x2)
addE_out_gga(x1, x2, x3)  =  addE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pF_in_ggaa(x1, x2, x3, x4)  =  pF_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
pI_in_ag(x1, x2)  =  pI_in_ag(x2)
pI_out_ag(x1, x2)  =  pI_out_ag(x1, x2)
pF_out_ggaa(x1, x2, x3, x4)  =  pF_out_ggaa(x1, x2, x3, x4)
pD_out_ggaa(x1, x2, x3, x4)  =  pD_out_ggaa(x1, x2, x3, x4)
U6_ggaa(x1, x2, x3, x4, x5)  =  U6_ggaa(x1, x2, x3, x5)
addG_in_gga(x1, x2, x3)  =  addG_in_gga(x1, x2)
addG_out_gga(x1, x2, x3)  =  addG_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
pJ_in_ag(x1, x2)  =  pJ_in_ag(x2)
pJ_out_ag(x1, x2)  =  pJ_out_ag(x1, x2)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
MULC_IN_GGA(x1, x2, x3)  =  MULC_IN_GGA(x1, x2)
PD_IN_GGAA(x1, x2, x3, x4)  =  PD_IN_GGAA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

MULC_IN_GGA(T33, s(T38), X59) → PD_IN_GGAA(T33, T38, X58, X59)
PD_IN_GGAA(T33, T38, T40, X59) → MULC_IN_GGA(T33, T38, T40)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

MULC_IN_GGA(T33, s(T38)) → PD_IN_GGAA(T33, T38)
PD_IN_GGAA(T33, T38) → MULC_IN_GGA(T33, T38)

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

(19) 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:

• PD_IN_GGAA(T33, T38) → MULC_IN_GGA(T33, T38)
  The graph contains the following edges 1 >= 1, 2 >= 2

• MULC_IN_GGA(T33, s(T38)) → PD_IN_GGAA(T33, T38)
  The graph contains the following edges 1 >= 1, 2 > 2

(20) YES