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

(0) Obligation:

Clauses:

convert([], X1, Z) :- ','(!, eq(Z, 0)).
convert(X, Y, Z) :- ','(head(X, 0), ','(!, ','(tail(X, T), ','(convert(T, Y, U), times(U, Y, Z))))).
convert(X, Y, Z) :- ','(head(X, H), ','(p(H, P), ','(tail(X, T), ','(convert(.(P, T), Y, U), ','(p(Z, U), !))))).
times(0, Y, Z) :- ','(!, eq(Z, 0)).
times(X, Y, Z) :- ','(p(X, P), ','(times(P, Y, U), plus(Y, U, Z))).
plus(0, Y, Z) :- ','(!, eq(Y, Z)).
plus(X, Y, Z) :- ','(p(X, P), ','(plus(P, Y, U), ','(p(Z, U), !))).
head([], X2).
head(.(H, X3), H).
tail([], []).
tail(.(X4, Xs), Xs).
p(s(X), X).
p(0, 0).
eq(X, X).

Queries:

convert(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: convert(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: convert(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | convert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | convert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(!_1, eq(T8, 0)) | convert([], T6, T3), SCOPE: 1, CLAUSE: 1 | convert([], T6, T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: convert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | convert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nconvert(T1, T2, T3) !=? convert([], X7, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: eq(T8, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: eq(T8, 0), SCOPE: 2, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(head(T15, 0), ','(!_1, ','(tail(T15, X21), ','(convert(X21, T16, X22), times(X22, T16, T18))))) | convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX21 is free; \nX22 is free; \nconvert(T15, T16, T3) !=? convert([], X7, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(head(T15, 0), ','(!_1, ','(tail(T15, X21), ','(convert(X21, T16, X22), times(X22, T16, T18))))), SCOPE: 3, CLAUSE: 7 | ','(head(T15, 0), ','(!_1, ','(tail(T15, X21), ','(convert(X21, T16, X22), times(X22, T16, T18))))), SCOPE: 3, CLAUSE: 8 | ?_3 | convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX21 is free; \nX22 is free; \nconvert(T15, T16, T3) !=? convert([], X7, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(head(T15, 0), ','(!_1, ','(tail(T15, X21), ','(convert(X21, T16, X22), times(X22, T16, T18))))), SCOPE: 3, CLAUSE: 8 | ?_3 | convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX21 is free; \nX22 is free; \nconvert(T15, T16, T3) !=? convert([], X7, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(!_1, ','(tail(.(0, T24), X21), ','(convert(X21, T16, X22), times(X22, T16, T18)))) | ?_3 | convert(.(0, T24), T16, T3), SCOPE: 1, CLAUSE: 2\n\nT16 is ground\nT24 is ground\nX21 is free; \nX22 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ?_3 | convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nconvert(T15, T16, T3) !=? convert([], X7, X8)\nhead(T15, 0) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(tail(.(0, T24), X21), ','(convert(X21, T16, X22), times(X22, T16, T18)))\n\nT16 is ground\nT24 is ground\nX21 is free; \nX22 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(tail(.(0, T24), X21), ','(convert(X21, T16, X22), times(X22, T16, T18))), SCOPE: 4, CLAUSE: 9 | ','(tail(.(0, T24), X21), ','(convert(X21, T16, X22), times(X22, T16, T18))), SCOPE: 4, CLAUSE: 10\n\nT16 is ground\nT24 is ground\nX21 is free; \nX22 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(tail(.(0, T24), X21), ','(convert(X21, T16, X22), times(X22, T16, T18))), SCOPE: 4, CLAUSE: 10\n\nT16 is ground\nT24 is ground\nX21 is free; \nX22 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(convert(T29, T16, X22), times(X22, T16, T18))\n\nT16 is ground\nT29 is ground\nX22 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: convert(T29, T16, X22)\n\nT16 is ground\nT29 is ground\nX22 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: times(T31, T16, T18)\n\nT16 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: convert(T29, T16, X22), SCOPE: 5, CLAUSE: 0 | convert(T29, T16, X22), SCOPE: 5, CLAUSE: 1 | convert(T29, T16, X22), SCOPE: 5, CLAUSE: 2\n\nT16 is ground\nT29 is ground\nX22 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(!_5, eq(X58, 0)) | convert([], T35, X22), SCOPE: 5, CLAUSE: 1 | convert([], T35, X22), SCOPE: 5, CLAUSE: 2\n\nT35 is ground\nX22 is free; \nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: convert(T29, T16, X22), SCOPE: 5, CLAUSE: 1 | convert(T29, T16, X22), SCOPE: 5, CLAUSE: 2\n\nT16 is ground\nT29 is ground\nX22 is free; \nconvert(T29, T16, X22) !=? convert([], X56, X57)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: eq(X58, 0)\n\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: eq(X58, 0), SCOPE: 6, CLAUSE: 13\n\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(head(T40, 0), ','(!_5, ','(tail(T40, X80), ','(convert(X80, T41, X81), times(X81, T41, X82))))) | convert(T40, T41, X22), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX22 is free; \nX82 is free; \nX80 is free; \nX81 is free; \nconvert(T40, T41, X22) !=? convert([], X56, X57)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(head(T40, 0), ','(!_5, ','(tail(T40, X80), ','(convert(X80, T41, X81), times(X81, T41, X82))))), SCOPE: 7, CLAUSE: 7 | ','(head(T40, 0), ','(!_5, ','(tail(T40, X80), ','(convert(X80, T41, X81), times(X81, T41, X82))))), SCOPE: 7, CLAUSE: 8 | ?_7 | convert(T40, T41, X22), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX22 is free; \nX82 is free; \nX80 is free; \nX81 is free; \nconvert(T40, T41, X22) !=? convert([], X56, X57)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(head(T40, 0), ','(!_5, ','(tail(T40, X80), ','(convert(X80, T41, X81), times(X81, T41, X82))))), SCOPE: 7, CLAUSE: 8 | ?_7 | convert(T40, T41, X22), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX22 is free; \nX82 is free; \nX80 is free; \nX81 is free; \nconvert(T40, T41, X22) !=? convert([], X56, X57)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(!_5, ','(tail(.(0, T47), X80), ','(convert(X80, T41, X81), times(X81, T41, X82)))) | ?_7 | convert(.(0, T47), T41, X22), SCOPE: 5, CLAUSE: 2\n\nT41 is ground\nT47 is ground\nX22 is free; \nX82 is free; \nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ?_7 | convert(T40, T41, X22), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX22 is free; \nconvert(T40, T41, X22) !=? convert([], X56, X57)\nhead(T40, 0) !=? head(.(X88, X89), X88)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(tail(.(0, T47), X80), ','(convert(X80, T41, X81), times(X81, T41, X82)))\n\nT41 is ground\nT47 is ground\nX82 is free; \nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(tail(.(0, T47), X80), ','(convert(X80, T41, X81), times(X81, T41, X82))), SCOPE: 8, CLAUSE: 9 | ','(tail(.(0, T47), X80), ','(convert(X80, T41, X81), times(X81, T41, X82))), SCOPE: 8, CLAUSE: 10\n\nT41 is ground\nT47 is ground\nX82 is free; \nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(tail(.(0, T47), X80), ','(convert(X80, T41, X81), times(X81, T41, X82))), SCOPE: 8, CLAUSE: 10\n\nT41 is ground\nT47 is ground\nX82 is free; \nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(convert(T52, T41, X81), times(X81, T41, X82))\n\nT41 is ground\nT52 is ground\nX82 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: convert(T52, T41, X81)\n\nT41 is ground\nT52 is ground\nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: times(T54, T41, X82)\n\nT41 is ground\nT54 is ground\nX82 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: times(T54, T41, X82), SCOPE: 9, CLAUSE: 3 | times(T54, T41, X82), SCOPE: 9, CLAUSE: 4\n\nT41 is ground\nT54 is ground\nX82 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(!_9, eq(X121, 0)) | times(0, T59, X82), SCOPE: 9, CLAUSE: 4\n\nT59 is ground\nX82 is free; \nX121 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: times(T54, T41, X82), SCOPE: 9, CLAUSE: 4\n\nT41 is ground\nT54 is ground\nX82 is free; \ntimes(T54, T41, X82) !=? times(0, X119, X120)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: eq(X121, 0)\n\nX121 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: eq(X121, 0), SCOPE: 10, CLAUSE: 13\n\nX121 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(p(T65, X146), ','(times(X146, T66, X147), plus(T66, X147, X148)))\n\nT65 is ground\nT66 is ground\nX148 is free; \nX146 is free; \nX147 is free; \ntimes(T65, T66, X82) !=? times(0, X119, X120)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(p(T65, X146), ','(times(X146, T66, X147), plus(T66, X147, X148))), SCOPE: 11, CLAUSE: 11 | ','(p(T65, X146), ','(times(X146, T66, X147), plus(T66, X147, X148))), SCOPE: 11, CLAUSE: 12\n\nT65 is ground\nT66 is ground\nX148 is free; \nX146 is free; \nX147 is free; \ntimes(T65, T66, X82) !=? times(0, X119, X120)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(p(T65, X146), ','(times(X146, T66, X147), plus(T66, X147, X148))), SCOPE: 11, CLAUSE: 11\n\nT65 is ground\nT66 is ground\nX148 is free; \nX146 is free; \nX147 is free; \ntimes(T65, T66, X82) !=? times(0, X119, X120)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(p(T65, X146), ','(times(X146, T66, X147), plus(T66, X147, X148))), SCOPE: 11, CLAUSE: 12\n\nT65 is ground\nT66 is ground\nX148 is free; \nX146 is free; \nX147 is free; \ntimes(T65, T66, X82) !=? times(0, X119, X120)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(times(T72, T66, X147), plus(T66, X147, X148))\n\nT66 is ground\nT72 is ground\nX148 is free; \nX147 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: times(T72, T66, X147)\n\nT66 is ground\nT72 is ground\nX147 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: plus(T66, T74, X148)\n\nT66 is ground\nT74 is ground\nX148 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: plus(T66, T74, X148), SCOPE: 12, CLAUSE: 5 | plus(T66, T74, X148), SCOPE: 12, CLAUSE: 6\n\nT66 is ground\nT74 is ground\nX148 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(!_12, eq(T79, X175)) | plus(0, T79, X148), SCOPE: 12, CLAUSE: 6\n\nT79 is ground\nX148 is free; \nX175 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: plus(T66, T74, X148), SCOPE: 12, CLAUSE: 6\n\nT66 is ground\nT74 is ground\nX148 is free; \nplus(T66, T74, X148) !=? plus(0, X173, X174)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: eq(T79, X175)\n\nT79 is ground\nX175 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: eq(T79, X175), SCOPE: 13, CLAUSE: 13\n\nT79 is ground\nX175 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(p(T88, X197), ','(plus(X197, T89, X198), ','(p(X199, X198), !_12)))\n\nT88 is ground\nT89 is ground\nX199 is free; \nX197 is free; \nX198 is free; \nplus(T88, T89, X148) !=? plus(0, X173, X174)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(p(T88, X197), ','(plus(X197, T89, X198), ','(p(X199, X198), !_12))), SCOPE: 14, CLAUSE: 11 | ','(p(T88, X197), ','(plus(X197, T89, X198), ','(p(X199, X198), !_12))), SCOPE: 14, CLAUSE: 12\n\nT88 is ground\nT89 is ground\nX199 is free; \nX197 is free; \nX198 is free; \nplus(T88, T89, X148) !=? plus(0, X173, X174)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(plus(T93, T89, X198), ','(p(X199, X198), !_12)) | ','(p(s(T93), X197), ','(plus(X197, T89, X198), ','(p(X199, X198), !_12))), SCOPE: 14, CLAUSE: 12\n\nT89 is ground\nT93 is ground\nX199 is free; \nX197 is free; \nX198 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(p(T88, X197), ','(plus(X197, T89, X198), ','(p(X199, X198), !_12))), SCOPE: 14, CLAUSE: 12\n\nT88 is ground\nT89 is ground\nX199 is free; \nX197 is free; \nX198 is free; \nplus(T88, T89, X148) !=? plus(0, X173, X174)\np(T88, X197) !=? p(s(X205), X205)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(plus(T93, T89, X198), ','(p(X199, X198), !_12))\n\nT89 is ground\nT93 is ground\nX199 is free; \nX198 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(p(s(T93), X197), ','(plus(X197, T89, X198), ','(p(X199, X198), !_12))), SCOPE: 14, CLAUSE: 12\n\nT89 is ground\nT93 is ground\nX199 is free; \nX197 is free; \nX198 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: plus(T93, T89, X198)\n\nT89 is ground\nT93 is ground\nX198 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(p(X199, T96), !_12)\n\nT96 is ground\nX199 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(p(X199, T96), !_12), SCOPE: 15, CLAUSE: 11 | ','(p(X199, T96), !_12), SCOPE: 15, CLAUSE: 12\n\nT96 is ground\nX199 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: !_12 | ','(p(X199, T100), !_12), SCOPE: 15, CLAUSE: 12\n\nT100 is ground\nX199 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];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: convert(T40, T41, X22), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX22 is free; \nconvert(T40, T41, X22) !=? convert([], X56, X57)\nhead(T40, 0) !=? head(.(X88, X89), X88)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(head(T106, X247), ','(p(X247, X248), ','(tail(T106, X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))))\n\nT106 is ground\nT107 is ground\nX251 is free; \nX247 is free; \nX248 is free; \nX249 is free; \nX250 is free; \nconvert(T106, T107, X22) !=? convert([], X56, X57)\nhead(T106, 0) !=? head(.(X88, X89), X88)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(head(T106, X247), ','(p(X247, X248), ','(tail(T106, X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5))))), SCOPE: 16, CLAUSE: 7 | ','(head(T106, X247), ','(p(X247, X248), ','(tail(T106, X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5))))), SCOPE: 16, CLAUSE: 8\n\nT106 is ground\nT107 is ground\nX251 is free; \nX247 is free; \nX248 is free; \nX249 is free; \nX250 is free; \nconvert(T106, T107, X22) !=? convert([], X56, X57)\nhead(T106, 0) !=? head(.(X88, X89), X88)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(head(T106, X247), ','(p(X247, X248), ','(tail(T106, X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5))))), SCOPE: 16, CLAUSE: 8\n\nT106 is ground\nT107 is ground\nX251 is free; \nX247 is free; \nX248 is free; \nX249 is free; \nX250 is free; \nconvert(T106, T107, X22) !=? convert([], X56, X57)\nhead(T106, 0) !=? head(.(X88, X89), X88)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(p(T113, X248), ','(tail(.(T113, T114), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5))))\n\nT107 is ground\nT113 is ground\nT114 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; \nhead(.(T113, T114), 0) !=? head(.(X88, X89), X88)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(p(T113, X248), ','(tail(.(T113, T114), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 11 | ','(p(T113, X248), ','(tail(.(T113, T114), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT107 is ground\nT113 is ground\nT114 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; \nhead(.(T113, T114), 0) !=? head(.(X88, X89), X88)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(tail(.(s(T118), T114), X249), ','(convert(.(T118, X249), T107, X250), ','(p(X251, X250), !_5))) | ','(p(s(T118), X248), ','(tail(.(s(T118), T114), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT107 is ground\nT114 is ground\nT118 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(p(T113, X248), ','(tail(.(T113, T114), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT107 is ground\nT113 is ground\nT114 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; \nhead(.(T113, T114), 0) !=? head(.(X88, X89), X88)\np(T113, X248) !=? p(s(X284), X284)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(tail(.(s(T118), T114), X249), ','(convert(.(T118, X249), T107, X250), ','(p(X251, X250), !_5))), SCOPE: 18, CLAUSE: 9 | ','(tail(.(s(T118), T114), X249), ','(convert(.(T118, X249), T107, X250), ','(p(X251, X250), !_5))), SCOPE: 18, CLAUSE: 10 | ?_18 | ','(p(s(T118), X248), ','(tail(.(s(T118), T114), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT107 is ground\nT114 is ground\nT118 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(tail(.(s(T118), T114), X249), ','(convert(.(T118, X249), T107, X250), ','(p(X251, X250), !_5))), SCOPE: 18, CLAUSE: 10 | ?_18 | ','(p(s(T118), X248), ','(tail(.(s(T118), T114), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT107 is ground\nT114 is ground\nT118 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(convert(.(T128, T129), T107, X250), ','(p(X251, X250), !_5)) | ?_18 | ','(p(s(T128), X248), ','(tail(.(s(T128), T129), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT107 is ground\nT128 is ground\nT129 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(convert(.(T128, T129), T107, X250), ','(p(X251, X250), !_5))\n\nT107 is ground\nT128 is ground\nT129 is ground\nX251 is free; \nX250 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ?_18 | ','(p(s(T128), X248), ','(tail(.(s(T128), T129), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT107 is ground\nT128 is ground\nT129 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: convert(.(T128, T129), T107, X250)\n\nT107 is ground\nT128 is ground\nT129 is ground\nX250 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(p(X251, T136), !_5)\n\nT136 is ground\nX251 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(p(X251, T136), !_5), SCOPE: 19, CLAUSE: 11 | ','(p(X251, T136), !_5), SCOPE: 19, CLAUSE: 12\n\nT136 is ground\nX251 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: !_5 | ','(p(X251, T142), !_5), SCOPE: 19, CLAUSE: 12\n\nT142 is ground\nX251 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(p(s(T128), X248), ','(tail(.(s(T128), T129), X249), ','(convert(.(X248, X249), T107, X250), ','(p(X251, X250), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT107 is ground\nT128 is ground\nT129 is ground\nX251 is free; \nX248 is free; \nX249 is free; \nX250 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: times(T31, T16, T18), SCOPE: 20, CLAUSE: 3 | times(T31, T16, T18), SCOPE: 20, CLAUSE: 4\n\nT16 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(!_20, eq(T151, 0)) | times(0, T149, T18), SCOPE: 20, CLAUSE: 4\n\nT149 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: times(T31, T16, T18), SCOPE: 20, CLAUSE: 4\n\nT16 is ground\nT31 is ground\ntimes(T31, T16, T18) !=? times(0, X345, X346)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: eq(T151, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: eq(T151, 0), SCOPE: 21, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(p(T163, X367), ','(times(X367, T164, X368), plus(T164, X368, T166)))\n\nT163 is ground\nT164 is ground\nX367 is free; \nX368 is free; \ntimes(T163, T164, T18) !=? times(0, X345, X346)", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(p(T163, X367), ','(times(X367, T164, X368), plus(T164, X368, T166))), SCOPE: 22, CLAUSE: 11 | ','(p(T163, X367), ','(times(X367, T164, X368), plus(T164, X368, T166))), SCOPE: 22, CLAUSE: 12\n\nT163 is ground\nT164 is ground\nX367 is free; \nX368 is free; \ntimes(T163, T164, T18) !=? times(0, X345, X346)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(p(T163, X367), ','(times(X367, T164, X368), plus(T164, X368, T166))), SCOPE: 22, CLAUSE: 11\n\nT163 is ground\nT164 is ground\nX367 is free; \nX368 is free; \ntimes(T163, T164, T18) !=? times(0, X345, X346)", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(p(T163, X367), ','(times(X367, T164, X368), plus(T164, X368, T166))), SCOPE: 22, CLAUSE: 12\n\nT163 is ground\nT164 is ground\nX367 is free; \nX368 is free; \ntimes(T163, T164, T18) !=? times(0, X345, X346)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(times(T172, T164, X368), plus(T164, X368, T166))\n\nT164 is ground\nT172 is ground\nX368 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: times(T172, T164, X368)\n\nT164 is ground\nT172 is ground\nX368 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: plus(T164, T174, T166)\n\nT164 is ground\nT174 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: plus(T164, T174, T166), SCOPE: 23, CLAUSE: 5 | plus(T164, T174, T166), SCOPE: 23, CLAUSE: 6\n\nT164 is ground\nT174 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(!_23, eq(T182, T184)) | plus(0, T182, T166), SCOPE: 23, CLAUSE: 6\n\nT182 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: plus(T164, T174, T166), SCOPE: 23, CLAUSE: 6\n\nT164 is ground\nT174 is ground\nplus(T164, T174, T166) !=? plus(0, X390, X391)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: eq(T182, T184)\n\nT182 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: eq(T182, T184), SCOPE: 24, CLAUSE: 13\n\nT182 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(p(T196, X412), ','(plus(X412, T197, X413), ','(p(T199, X413), !_23)))\n\nT196 is ground\nT197 is ground\nX412 is free; \nX413 is free; \nplus(T196, T197, T166) !=? plus(0, X390, X391)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(p(T196, X412), ','(plus(X412, T197, X413), ','(p(T199, X413), !_23))), SCOPE: 25, CLAUSE: 11 | ','(p(T196, X412), ','(plus(X412, T197, X413), ','(p(T199, X413), !_23))), SCOPE: 25, CLAUSE: 12\n\nT196 is ground\nT197 is ground\nX412 is free; \nX413 is free; \nplus(T196, T197, T166) !=? plus(0, X390, X391)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(plus(T203, T197, X413), ','(p(T199, X413), !_23)) | ','(p(s(T203), X412), ','(plus(X412, T197, X413), ','(p(T199, X413), !_23))), SCOPE: 25, CLAUSE: 12\n\nT197 is ground\nT203 is ground\nX412 is free; \nX413 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(p(T196, X412), ','(plus(X412, T197, X413), ','(p(T199, X413), !_23))), SCOPE: 25, CLAUSE: 12\n\nT196 is ground\nT197 is ground\nX412 is free; \nX413 is free; \nplus(T196, T197, T166) !=? plus(0, X390, X391)\np(T196, X412) !=? p(s(X419), X419)", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(plus(T203, T197, X413), ','(p(T199, X413), !_23))\n\nT197 is ground\nT203 is ground\nX413 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(p(s(T203), X412), ','(plus(X412, T197, X413), ','(p(T199, X413), !_23))), SCOPE: 25, CLAUSE: 12\n\nT197 is ground\nT203 is ground\nX412 is free; \nX413 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: plus(T203, T197, X413)\n\nT197 is ground\nT203 is ground\nX413 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(p(T199, T206), !_23)\n\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(p(T199, T206), !_23), SCOPE: 26, CLAUSE: 11 | ','(p(T199, T206), !_23), SCOPE: 26, CLAUSE: 12\n\nT206 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: !_23 | ','(p(T199, T210), !_23), SCOPE: 26, CLAUSE: 12\n\nT210 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(p(T199, T206), !_23), SCOPE: 26, CLAUSE: 12\n\nT206 is ground\np(T199, T206) !=? p(s(X432), X432)", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: !_23\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nconvert(T15, T16, T3) !=? convert([], X7, X8)\nhead(T15, 0) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(head(T219, X457), ','(p(X457, X458), ','(tail(T219, X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))))\n\nT219 is ground\nT220 is ground\nX457 is free; \nX458 is free; \nX459 is free; \nX460 is free; \nconvert(T219, T220, T3) !=? convert([], X7, X8)\nhead(T219, 0) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(head(T219, X457), ','(p(X457, X458), ','(tail(T219, X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1))))), SCOPE: 27, CLAUSE: 7 | ','(head(T219, X457), ','(p(X457, X458), ','(tail(T219, X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1))))), SCOPE: 27, CLAUSE: 8\n\nT219 is ground\nT220 is ground\nX457 is free; \nX458 is free; \nX459 is free; \nX460 is free; \nconvert(T219, T220, T3) !=? convert([], X7, X8)\nhead(T219, 0) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(head(T219, X457), ','(p(X457, X458), ','(tail(T219, X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1))))), SCOPE: 27, CLAUSE: 8\n\nT219 is ground\nT220 is ground\nX457 is free; \nX458 is free; \nX459 is free; \nX460 is free; \nconvert(T219, T220, T3) !=? convert([], X7, X8)\nhead(T219, 0) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(p(T228, X458), ','(tail(.(T228, T229), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1))))\n\nT220 is ground\nT228 is ground\nT229 is ground\nX458 is free; \nX459 is free; \nX460 is free; \nhead(.(T228, T229), 0) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(p(T228, X458), ','(tail(.(T228, T229), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 11 | ','(p(T228, X458), ','(tail(.(T228, T229), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT220 is ground\nT228 is ground\nT229 is ground\nX458 is free; \nX459 is free; \nX460 is free; \nhead(.(T228, T229), 0) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(tail(.(s(T233), T229), X459), ','(convert(.(T233, X459), T220, X460), ','(p(T222, X460), !_1))) | ','(p(s(T233), X458), ','(tail(.(s(T233), T229), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT220 is ground\nT229 is ground\nT233 is ground\nX458 is free; \nX459 is free; \nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(p(T228, X458), ','(tail(.(T228, T229), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT220 is ground\nT228 is ground\nT229 is ground\nX458 is free; \nX459 is free; \nX460 is free; \nhead(.(T228, T229), 0) !=? head(.(X28, X29), X28)\np(T228, X458) !=? p(s(X493), X493)", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(tail(.(s(T233), T229), X459), ','(convert(.(T233, X459), T220, X460), ','(p(T222, X460), !_1))), SCOPE: 29, CLAUSE: 9 | ','(tail(.(s(T233), T229), X459), ','(convert(.(T233, X459), T220, X460), ','(p(T222, X460), !_1))), SCOPE: 29, CLAUSE: 10 | ?_29 | ','(p(s(T233), X458), ','(tail(.(s(T233), T229), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT220 is ground\nT229 is ground\nT233 is ground\nX458 is free; \nX459 is free; \nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(tail(.(s(T233), T229), X459), ','(convert(.(T233, X459), T220, X460), ','(p(T222, X460), !_1))), SCOPE: 29, CLAUSE: 10 | ?_29 | ','(p(s(T233), X458), ','(tail(.(s(T233), T229), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT220 is ground\nT229 is ground\nT233 is ground\nX458 is free; \nX459 is free; \nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(convert(.(T243, T244), T220, X460), ','(p(T222, X460), !_1)) | ?_29 | ','(p(s(T243), X458), ','(tail(.(s(T243), T244), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT220 is ground\nT243 is ground\nT244 is ground\nX458 is free; \nX459 is free; \nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(convert(.(T243, T244), T220, X460), ','(p(T222, X460), !_1))\n\nT220 is ground\nT243 is ground\nT244 is ground\nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ?_29 | ','(p(s(T243), X458), ','(tail(.(s(T243), T244), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT220 is ground\nT243 is ground\nT244 is ground\nX458 is free; \nX459 is free; \nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: convert(.(T243, T244), T220, X460)\n\nT220 is ground\nT243 is ground\nT244 is ground\nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ','(p(T222, T251), !_1)\n\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(p(T222, T251), !_1), SCOPE: 30, CLAUSE: 11 | ','(p(T222, T251), !_1), SCOPE: 30, CLAUSE: 12\n\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: !_1 | ','(p(T222, T257), !_1), SCOPE: 30, CLAUSE: 12\n\nT257 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(p(T222, T251), !_1), SCOPE: 30, CLAUSE: 12\n\nT251 is ground\np(T222, T251) !=? p(s(X544), X544)", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: !_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(p(s(T243), X458), ','(tail(.(s(T243), T244), X459), ','(convert(.(X458, X459), T220, X460), ','(p(T222, X460), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT220 is ground\nT243 is ground\nT244 is ground\nX458 is free; \nX459 is free; \nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 171 [arrowhead = none ];
171 -> 2;

172 [label="EVAL with clause\nconvert([], X7, X8) :- ','(!_1, eq(X8, 0)).\nand substitution\nT1 -> []\nT2 -> T6\nX7 -> T6\nT3 -> T8\nX8 -> T8\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 172 [arrowhead = none ];
172 -> 3;

173 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 173 [arrowhead = none ];
173 -> 4;

174 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 174 [arrowhead = none ];
174 -> 5;

175 [label="ONLY EVAL with clause\nconvert(X18, X19, X20) :- ','(head(X18, 0), ','(!_1, ','(tail(X18, X21), ','(convert(X21, X19, X22), times(X22, X19, X20))))).\nand substitution\nT1 -> T15\nX18 -> T15\nT2 -> T16\nX19 -> T16\nT3 -> T18\nX20 -> T18\nT17 -> T18", fontsize=14, style = filled, fillcolor = white];
4 -> 175 [arrowhead = none ];
175 -> 10;

176 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 176 [arrowhead = none ];
176 -> 6;

177 [label="EVAL with clause\neq(X13, X13).\nand substitution\nT8 -> 0\nX13 -> 0\nT11 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 177 [arrowhead = none ];
177 -> 7;

178 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 178 [arrowhead = none ];
178 -> 8;

179 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 179 [arrowhead = none ];
179 -> 9;

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

181 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (convert(T15, T16, T3), convert([], X7, X8))", fontsize=14, style = filled, fillcolor = white];
11 -> 181 [arrowhead = none ];
181 -> 12;

182 [label="EVAL with clause\nhead(.(X28, X29), X28).\nand substitution\nX28 -> 0\nX29 -> T24\nT15 -> .(0, T24)\nT23 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 182 [arrowhead = none ];
182 -> 13;

183 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 183 [arrowhead = none ];
183 -> 14;

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

185 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 185 [arrowhead = none ];
185 -> 143;

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

187 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
16 -> 187 [arrowhead = none ];
187 -> 17;

188 [label="ONLY EVAL with clause\ntail(.(X42, X43), X43).\nand substitution\nX42 -> 0\nT24 -> T29\nX43 -> T29\nX21 -> T29", fontsize=14, style = filled, fillcolor = white];
17 -> 188 [arrowhead = none ];
188 -> 18;

189 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
18 -> 189 [arrowhead = none ];
189 -> 19;

190 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nreplacements:\nX22 -> T31", fontsize=14, style = filled, fillcolor = violet];
18 -> 190 [arrowhead = none ];
190 -> 20;

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

192 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
20 -> 192 [arrowhead = none ];
192 -> 99;

193 [label="EVAL with clause\nconvert([], X56, X57) :- ','(!_5, eq(X57, 0)).\nand substitution\nT29 -> []\nT16 -> T35\nX56 -> T35\nX22 -> X58\nX57 -> X58", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 193 [arrowhead = none ];
193 -> 22;

194 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 194 [arrowhead = none ];
194 -> 23;

195 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 195 [arrowhead = none ];
195 -> 24;

196 [label="ONLY EVAL with clause\nconvert(X77, X78, X79) :- ','(head(X77, 0), ','(!_5, ','(tail(X77, X80), ','(convert(X80, X78, X81), times(X81, X78, X79))))).\nand substitution\nT29 -> T40\nX77 -> T40\nT16 -> T41\nX78 -> T41\nX22 -> X82\nX79 -> X82", fontsize=14, style = filled, fillcolor = white];
23 -> 196 [arrowhead = none ];
196 -> 28;

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

198 [label="ONLY EVAL with clause\neq(X65, X65).\nand substitution\nX58 -> 0\nX65 -> 0\nX66 -> 0", fontsize=14, style = filled, fillcolor = white];
25 -> 198 [arrowhead = none ];
198 -> 26;

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

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

201 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (convert(T40, T41, X22), convert([], X56, X57))", fontsize=14, style = filled, fillcolor = white];
29 -> 201 [arrowhead = none ];
201 -> 30;

202 [label="EVAL with clause\nhead(.(X88, X89), X88).\nand substitution\nX88 -> 0\nX89 -> T47\nT40 -> .(0, T47)\nT46 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 202 [arrowhead = none ];
202 -> 31;

203 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 203 [arrowhead = none ];
203 -> 32;

204 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 204 [arrowhead = none ];
204 -> 33;

205 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 205 [arrowhead = none ];
205 -> 76;

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

207 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
34 -> 207 [arrowhead = none ];
207 -> 35;

208 [label="ONLY EVAL with clause\ntail(.(X102, X103), X103).\nand substitution\nX102 -> 0\nT47 -> T52\nX103 -> T52\nX80 -> T52", fontsize=14, style = filled, fillcolor = white];
35 -> 208 [arrowhead = none ];
208 -> 36;

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

210 [label="SPLIT 2\nnew knowledge:\nT54 is ground\nreplacements:\nX81 -> T54", fontsize=14, style = filled, fillcolor = violet];
36 -> 210 [arrowhead = none ];
210 -> 38;

211 [label="INSTANCE with matching:\nT29 -> T52\nT16 -> T41\nX22 -> X81", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 211 [arrowhead = none , style=dashed];
211 -> 19[style=dashed];

212 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
38 -> 212 [arrowhead = none ];
212 -> 39;

213 [label="EVAL with clause\ntimes(0, X119, X120) :- ','(!_9, eq(X120, 0)).\nand substitution\nT54 -> 0\nT41 -> T59\nX119 -> T59\nX82 -> X121\nX120 -> X121", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 213 [arrowhead = none ];
213 -> 40;

214 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 214 [arrowhead = none ];
214 -> 41;

215 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 215 [arrowhead = none ];
215 -> 42;

216 [label="ONLY EVAL with clause\ntimes(X143, X144, X145) :- ','(p(X143, X146), ','(times(X146, X144, X147), plus(X144, X147, X145))).\nand substitution\nT54 -> T65\nX143 -> T65\nT41 -> T66\nX144 -> T66\nX82 -> X148\nX145 -> X148", fontsize=14, style = filled, fillcolor = white];
41 -> 216 [arrowhead = none ];
216 -> 46;

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

218 [label="ONLY EVAL with clause\neq(X128, X128).\nand substitution\nX121 -> 0\nX128 -> 0\nX129 -> 0", fontsize=14, style = filled, fillcolor = white];
43 -> 218 [arrowhead = none ];
218 -> 44;

219 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 219 [arrowhead = none ];
219 -> 45;

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

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

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

223 [label="EVAL with clause\np(s(X156), X156).\nand substitution\nX156 -> T72\nT65 -> s(T72)\nX146 -> T72", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 223 [arrowhead = none ];
223 -> 50;

224 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 224 [arrowhead = none ];
224 -> 51;

225 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (times(T65, T66, X82), times(0, X119, X120))", fontsize=14, style = filled, fillcolor = white];
49 -> 225 [arrowhead = none ];
225 -> 75;

226 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
50 -> 226 [arrowhead = none ];
226 -> 52;

227 [label="SPLIT 2\nnew knowledge:\nT74 is ground\nreplacements:\nX147 -> T74", fontsize=14, style = filled, fillcolor = violet];
50 -> 227 [arrowhead = none ];
227 -> 53;

228 [label="INSTANCE with matching:\nT54 -> T72\nT41 -> T66\nX82 -> X147", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 228 [arrowhead = none , style=dashed];
228 -> 38[style=dashed];

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

230 [label="EVAL with clause\nplus(0, X173, X174) :- ','(!_12, eq(X173, X174)).\nand substitution\nT66 -> 0\nT74 -> T79\nX173 -> T79\nX148 -> X175\nX174 -> X175", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 230 [arrowhead = none ];
230 -> 55;

231 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 231 [arrowhead = none ];
231 -> 56;

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

233 [label="ONLY EVAL with clause\nplus(X194, X195, X196) :- ','(p(X194, X197), ','(plus(X197, X195, X198), ','(p(X196, X198), !_12))).\nand substitution\nT66 -> T88\nX194 -> T88\nT74 -> T89\nX195 -> T89\nX148 -> X199\nX196 -> X199", fontsize=14, style = filled, fillcolor = white];
56 -> 233 [arrowhead = none ];
233 -> 61;

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

235 [label="ONLY EVAL with clause\neq(X180, X180).\nand substitution\nT79 -> T82\nX180 -> T82\nX175 -> T82", fontsize=14, style = filled, fillcolor = white];
58 -> 235 [arrowhead = none ];
235 -> 59;

236 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 236 [arrowhead = none ];
236 -> 60;

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

238 [label="EVAL with clause\np(s(X205), X205).\nand substitution\nX205 -> T93\nT88 -> s(T93)\nX197 -> T93", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 238 [arrowhead = none ];
238 -> 63;

239 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 239 [arrowhead = none ];
239 -> 64;

240 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
63 -> 240 [arrowhead = none ];
240 -> 65;

241 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
63 -> 241 [arrowhead = none ];
241 -> 66;

242 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (plus(T88, T89, X148), plus(0, X173, X174))", fontsize=14, style = filled, fillcolor = white];
64 -> 242 [arrowhead = none ];
242 -> 74;

243 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
65 -> 243 [arrowhead = none ];
243 -> 67;

244 [label="SPLIT 2\nnew knowledge:\nT96 is ground\nreplacements:\nX198 -> T96", fontsize=14, style = filled, fillcolor = violet];
65 -> 244 [arrowhead = none ];
244 -> 68;

245 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
66 -> 245 [arrowhead = none ];
245 -> 73;

246 [label="INSTANCE with matching:\nT66 -> T93\nT74 -> T89\nX148 -> X198", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 246 [arrowhead = none , style=dashed];
246 -> 53[style=dashed];

247 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 247 [arrowhead = none ];
247 -> 69;

248 [label="ONLY EVAL with clause\np(s(X220), X220).\nand substitution\nX220 -> T100\nX199 -> s(T100)\nT96 -> T100\nX221 -> T100", fontsize=14, style = filled, fillcolor = white];
69 -> 248 [arrowhead = none ];
248 -> 70;

249 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 249 [arrowhead = none ];
249 -> 71;

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

251 [label="ONLY EVAL with clause\nconvert(X244, X245, X246) :- ','(head(X244, X247), ','(p(X247, X248), ','(tail(X244, X249), ','(convert(.(X248, X249), X245, X250), ','(p(X246, X250), !_5))))).\nand substitution\nT40 -> T106\nX244 -> T106\nT41 -> T107\nX245 -> T107\nX22 -> X251\nX246 -> X251", fontsize=14, style = filled, fillcolor = white];
76 -> 251 [arrowhead = none ];
251 -> 77;

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

253 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (convert(T106, T107, X22), convert([], X56, X57))", fontsize=14, style = filled, fillcolor = white];
78 -> 253 [arrowhead = none ];
253 -> 79;

254 [label="EVAL with clause\nhead(.(X268, X269), X268).\nand substitution\nX268 -> T113\nX269 -> T114\nT106 -> .(T113, T114)\nX247 -> T113", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 254 [arrowhead = none ];
254 -> 80;

255 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 255 [arrowhead = none ];
255 -> 81;

256 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
80 -> 256 [arrowhead = none ];
256 -> 82;

257 [label="EVAL with clause\np(s(X284), X284).\nand substitution\nX284 -> T118\nT113 -> s(T118)\nX248 -> T118", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 257 [arrowhead = none ];
257 -> 83;

258 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 258 [arrowhead = none ];
258 -> 84;

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

260 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (head(.(T113, T114), 0), head(.(X88, X89), X88))", fontsize=14, style = filled, fillcolor = white];
84 -> 260 [arrowhead = none ];
260 -> 98;

261 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
85 -> 261 [arrowhead = none ];
261 -> 86;

262 [label="ONLY EVAL with clause\ntail(.(X307, X308), X308).\nand substitution\nT118 -> T128\nX307 -> s(T128)\nT114 -> T129\nX308 -> T129\nX249 -> T129", fontsize=14, style = filled, fillcolor = white];
86 -> 262 [arrowhead = none ];
262 -> 87;

263 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 263 [arrowhead = none ];
263 -> 88;

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 264 [arrowhead = none ];
264 -> 89;

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

266 [label="SPLIT 2\nnew knowledge:\nT136 is ground\nreplacements:\nX250 -> T136", fontsize=14, style = filled, fillcolor = violet];
88 -> 266 [arrowhead = none ];
266 -> 91;

267 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 267 [arrowhead = none ];
267 -> 96;

268 [label="INSTANCE with matching:\nT1 -> .(T128, T129)\nT2 -> T107\nT3 -> X250", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 268 [arrowhead = none , style=dashed];
268 -> 1[style=dashed];

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

270 [label="ONLY EVAL with clause\np(s(X337), X337).\nand substitution\nX337 -> T142\nX251 -> s(T142)\nT136 -> T142\nX338 -> T142", fontsize=14, style = filled, fillcolor = white];
92 -> 270 [arrowhead = none ];
270 -> 93;

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

272 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 272 [arrowhead = none ];
272 -> 95;

273 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
96 -> 273 [arrowhead = none ];
273 -> 97;

274 [label="EVAL with clause\ntimes(0, X345, X346) :- ','(!_20, eq(X346, 0)).\nand substitution\nT31 -> 0\nT16 -> T149\nX345 -> T149\nT18 -> T151\nX346 -> T151\nT150 -> T151", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 274 [arrowhead = none ];
274 -> 100;

275 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 275 [arrowhead = none ];
275 -> 101;

276 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 276 [arrowhead = none ];
276 -> 102;

277 [label="ONLY EVAL with clause\ntimes(X364, X365, X366) :- ','(p(X364, X367), ','(times(X367, X365, X368), plus(X365, X368, X366))).\nand substitution\nT31 -> T163\nX364 -> T163\nT16 -> T164\nX365 -> T164\nT18 -> T166\nX366 -> T166\nT165 -> T166", fontsize=14, style = filled, fillcolor = white];
101 -> 277 [arrowhead = none ];
277 -> 107;

278 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
102 -> 278 [arrowhead = none ];
278 -> 103;

279 [label="EVAL with clause\neq(X351, X351).\nand substitution\nT151 -> 0\nX351 -> 0\nT154 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 279 [arrowhead = none ];
279 -> 104;

280 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 280 [arrowhead = none ];
280 -> 105;

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

282 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
107 -> 282 [arrowhead = none ];
282 -> 108;

283 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
108 -> 283 [arrowhead = none ];
283 -> 109;

284 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
108 -> 284 [arrowhead = none ];
284 -> 110;

285 [label="EVAL with clause\np(s(X376), X376).\nand substitution\nX376 -> T172\nT163 -> s(T172)\nX367 -> T172", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 285 [arrowhead = none ];
285 -> 111;

286 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 286 [arrowhead = none ];
286 -> 112;

287 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (times(T163, T164, T18), times(0, X345, X346))", fontsize=14, style = filled, fillcolor = white];
110 -> 287 [arrowhead = none ];
287 -> 142;

288 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
111 -> 288 [arrowhead = none ];
288 -> 113;

289 [label="SPLIT 2\nnew knowledge:\nT174 is ground\nreplacements:\nX368 -> T174", fontsize=14, style = filled, fillcolor = violet];
111 -> 289 [arrowhead = none ];
289 -> 114;

290 [label="INSTANCE with matching:\nT54 -> T172\nT41 -> T164\nX82 -> X368", fontsize=14, style = filled, fillcolor = lightgrey];
113 -> 290 [arrowhead = none , style=dashed];
290 -> 38[style=dashed];

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

292 [label="EVAL with clause\nplus(0, X390, X391) :- ','(!_23, eq(X390, X391)).\nand substitution\nT164 -> 0\nT174 -> T182\nX390 -> T182\nT166 -> T184\nX391 -> T184\nT183 -> T184", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 292 [arrowhead = none ];
292 -> 116;

293 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 293 [arrowhead = none ];
293 -> 117;

294 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 294 [arrowhead = none ];
294 -> 118;

295 [label="ONLY EVAL with clause\nplus(X409, X410, X411) :- ','(p(X409, X412), ','(plus(X412, X410, X413), ','(p(X411, X413), !_23))).\nand substitution\nT164 -> T196\nX409 -> T196\nT174 -> T197\nX410 -> T197\nT166 -> T199\nX411 -> T199\nT198 -> T199", fontsize=14, style = filled, fillcolor = white];
117 -> 295 [arrowhead = none ];
295 -> 123;

296 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
118 -> 296 [arrowhead = none ];
296 -> 119;

297 [label="EVAL with clause\neq(X396, X396).\nand substitution\nT182 -> T187\nX396 -> T187\nT184 -> T187", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 297 [arrowhead = none ];
297 -> 120;

298 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 298 [arrowhead = none ];
298 -> 121;

299 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 299 [arrowhead = none ];
299 -> 122;

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

301 [label="EVAL with clause\np(s(X419), X419).\nand substitution\nX419 -> T203\nT196 -> s(T203)\nX412 -> T203", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 301 [arrowhead = none ];
301 -> 125;

302 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 302 [arrowhead = none ];
302 -> 126;

303 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 303 [arrowhead = none ];
303 -> 127;

304 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 304 [arrowhead = none ];
304 -> 128;

305 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (plus(T196, T197, T166), plus(0, X390, X391))", fontsize=14, style = filled, fillcolor = white];
126 -> 305 [arrowhead = none ];
305 -> 141;

306 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
127 -> 306 [arrowhead = none ];
306 -> 129;

307 [label="SPLIT 2\nnew knowledge:\nT206 is ground\nreplacements:\nX413 -> T206", fontsize=14, style = filled, fillcolor = violet];
127 -> 307 [arrowhead = none ];
307 -> 130;

308 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
128 -> 308 [arrowhead = none ];
308 -> 140;

309 [label="INSTANCE with matching:\nT66 -> T203\nT74 -> T197\nX148 -> X413", fontsize=14, style = filled, fillcolor = lightgrey];
129 -> 309 [arrowhead = none , style=dashed];
309 -> 53[style=dashed];

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

311 [label="EVAL with clause\np(s(X432), X432).\nand substitution\nX432 -> T210\nT199 -> s(T210)\nT206 -> T210", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 311 [arrowhead = none ];
311 -> 132;

312 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 312 [arrowhead = none ];
312 -> 133;

313 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 313 [arrowhead = none ];
313 -> 134;

314 [label="EVAL with clause\np(0, 0).\nand substitution\nT199 -> 0\nT206 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 314 [arrowhead = none ];
314 -> 136;

315 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 315 [arrowhead = none ];
315 -> 137;

316 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 316 [arrowhead = none ];
316 -> 135;

317 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 317 [arrowhead = none ];
317 -> 138;

318 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 318 [arrowhead = none ];
318 -> 139;

319 [label="ONLY EVAL with clause\nconvert(X454, X455, X456) :- ','(head(X454, X457), ','(p(X457, X458), ','(tail(X454, X459), ','(convert(.(X458, X459), X455, X460), ','(p(X456, X460), !_1))))).\nand substitution\nT15 -> T219\nX454 -> T219\nT16 -> T220\nX455 -> T220\nT3 -> T222\nX456 -> T222\nT221 -> T222", fontsize=14, style = filled, fillcolor = white];
143 -> 319 [arrowhead = none ];
319 -> 144;

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

321 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (convert(T219, T220, T3), convert([], X7, X8))", fontsize=14, style = filled, fillcolor = white];
145 -> 321 [arrowhead = none ];
321 -> 146;

322 [label="EVAL with clause\nhead(.(X477, X478), X477).\nand substitution\nX477 -> T228\nX478 -> T229\nT219 -> .(T228, T229)\nX457 -> T228", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 322 [arrowhead = none ];
322 -> 147;

323 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 323 [arrowhead = none ];
323 -> 148;

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

325 [label="EVAL with clause\np(s(X493), X493).\nand substitution\nX493 -> T233\nT228 -> s(T233)\nX458 -> T233", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 325 [arrowhead = none ];
325 -> 150;

326 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 326 [arrowhead = none ];
326 -> 151;

327 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
150 -> 327 [arrowhead = none ];
327 -> 152;

328 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (head(.(T228, T229), 0), head(.(X28, X29), X28))", fontsize=14, style = filled, fillcolor = white];
151 -> 328 [arrowhead = none ];
328 -> 170;

329 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
152 -> 329 [arrowhead = none ];
329 -> 153;

330 [label="ONLY EVAL with clause\ntail(.(X516, X517), X517).\nand substitution\nT233 -> T243\nX516 -> s(T243)\nT229 -> T244\nX517 -> T244\nX459 -> T244", fontsize=14, style = filled, fillcolor = white];
153 -> 330 [arrowhead = none ];
330 -> 154;

331 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
154 -> 331 [arrowhead = none ];
331 -> 155;

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

333 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
155 -> 333 [arrowhead = none ];
333 -> 157;

334 [label="SPLIT 2\nnew knowledge:\nT251 is ground\nreplacements:\nX460 -> T251", fontsize=14, style = filled, fillcolor = violet];
155 -> 334 [arrowhead = none ];
334 -> 158;

335 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
156 -> 335 [arrowhead = none ];
335 -> 168;

336 [label="INSTANCE with matching:\nT1 -> .(T243, T244)\nT2 -> T220\nT3 -> X460", fontsize=14, style = filled, fillcolor = lightgrey];
157 -> 336 [arrowhead = none , style=dashed];
336 -> 1[style=dashed];

337 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
158 -> 337 [arrowhead = none ];
337 -> 159;

338 [label="EVAL with clause\np(s(X544), X544).\nand substitution\nX544 -> T257\nT222 -> s(T257)\nT251 -> T257", fontsize=14, style = filled, fillcolor = lightblue];
159 -> 338 [arrowhead = none ];
338 -> 160;

339 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
159 -> 339 [arrowhead = none ];
339 -> 161;

340 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 340 [arrowhead = none ];
340 -> 162;

341 [label="EVAL with clause\np(0, 0).\nand substitution\nT222 -> 0\nT251 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 341 [arrowhead = none ];
341 -> 164;

342 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 342 [arrowhead = none ];
342 -> 165;

343 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
162 -> 343 [arrowhead = none ];
343 -> 163;

344 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
164 -> 344 [arrowhead = none ];
344 -> 166;

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

346 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
168 -> 346 [arrowhead = none ];
346 -> 169;

}

(2) Obligation:

Triples:

convert19(.(0, T52), T41, X82) :- convert19(T52, T41, X81).
convert19(.(0, T52), T41, X82) :- ','(convertc19(T52, T41, T54), times38(T54, T41, X82)).
convert19(.(s(T128), T129), T107, X251) :- convert1(.(T128, T129), T107, X250).
times38(s(T72), T66, X148) :- times38(T72, T66, X147).
times38(s(T72), T66, X148) :- ','(timesc38(T72, T66, T74), plus53(T66, T74, X148)).
plus53(s(T93), T89, X199) :- plus53(T93, T89, X198).
convert1(.(0, T29), T16, T18) :- convert19(T29, T16, X22).
convert1(.(0, T29), T164, T166) :- ','(convertc19(T29, T164, s(T172)), times38(T172, T164, X368)).
convert1(.(0, T29), s(T203), T199) :- ','(convertc19(T29, s(T203), s(T172)), ','(timesc38(T172, s(T203), T197), plus53(T203, T197, X413))).
convert1(.(s(T243), T244), T220, T222) :- convert1(.(T243, T244), T220, X460).

Clauses:

convertc19([], T35, 0).
convertc19(.(0, T52), T41, X82) :- ','(convertc19(T52, T41, T54), timesc38(T54, T41, X82)).
convertc19(.(s(T128), T129), T107, s(T142)) :- convertc1(.(T128, T129), T107, T142).
timesc38(0, T59, 0).
timesc38(s(T72), T66, X148) :- ','(timesc38(T72, T66, T74), plusc53(T66, T74, X148)).
plusc53(0, T82, T82).
plusc53(s(T93), T89, s(T100)) :- plusc53(T93, T89, T100).
convertc1([], T6, 0).
convertc1(.(0, T29), T149, 0) :- convertc19(T29, T149, 0).
convertc1(.(0, T29), 0, T187) :- ','(convertc19(T29, 0, s(T172)), timesc38(T172, 0, T187)).
convertc1(.(0, T29), s(T203), s(T210)) :- ','(convertc19(T29, s(T203), s(T172)), ','(timesc38(T172, s(T203), T197), plusc53(T203, T197, T210))).
convertc1(.(0, T29), s(T203), 0) :- ','(convertc19(T29, s(T203), s(T172)), ','(timesc38(T172, s(T203), T197), plusc53(T203, T197, 0))).
convertc1(.(s(T243), T244), T220, s(T257)) :- convertc1(.(T243, T244), T220, T257).
convertc1(.(s(T243), T244), T220, 0) :- convertc1(.(T243, T244), T220, 0).

Afs:

convert1(x1, x2, x3)  =  convert1(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
convert1_in: (b,b,f)
convert19_in: (b,b,f)
convertc19_in: (b,b,f) (b,b,b)
convertc1_in: (b,b,f) (b,b,b)
timesc38_in: (b,b,b) (b,b,f)
plusc53_in: (b,b,f) (b,b,b)
times38_in: (b,b,f)
plus53_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

CONVERT1_IN_GGA(.(0, T29), T16, T18) → U9_GGA(T29, T16, T18, convert19_in_gga(T29, T16, X22))
CONVERT1_IN_GGA(.(0, T29), T16, T18) → CONVERT19_IN_GGA(T29, T16, X22)
CONVERT19_IN_GGA(.(0, T52), T41, X82) → U1_GGA(T52, T41, X82, convert19_in_gga(T52, T41, X81))
CONVERT19_IN_GGA(.(0, T52), T41, X82) → CONVERT19_IN_GGA(T52, T41, X81)
CONVERT19_IN_GGA(.(0, T52), T41, X82) → U2_GGA(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
U2_GGA(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U3_GGA(T52, T41, X82, times38_in_gga(T54, T41, X82))
U2_GGA(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → TIMES38_IN_GGA(T54, T41, X82)
TIMES38_IN_GGA(s(T72), T66, X148) → U5_GGA(T72, T66, X148, times38_in_gga(T72, T66, X147))
TIMES38_IN_GGA(s(T72), T66, X148) → TIMES38_IN_GGA(T72, T66, X147)
TIMES38_IN_GGA(s(T72), T66, X148) → U6_GGA(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
U6_GGA(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U7_GGA(T72, T66, X148, plus53_in_gga(T66, T74, X148))
U6_GGA(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → PLUS53_IN_GGA(T66, T74, X148)
PLUS53_IN_GGA(s(T93), T89, X199) → U8_GGA(T93, T89, X199, plus53_in_gga(T93, T89, X198))
PLUS53_IN_GGA(s(T93), T89, X199) → PLUS53_IN_GGA(T93, T89, X198)
CONVERT19_IN_GGA(.(s(T128), T129), T107, X251) → U4_GGA(T128, T129, T107, X251, convert1_in_gga(.(T128, T129), T107, X250))
CONVERT19_IN_GGA(.(s(T128), T129), T107, X251) → CONVERT1_IN_GGA(.(T128, T129), T107, X250)
CONVERT1_IN_GGA(.(0, T29), T164, T166) → U10_GGA(T29, T164, T166, convertc19_in_gga(T29, T164, s(T172)))
U10_GGA(T29, T164, T166, convertc19_out_gga(T29, T164, s(T172))) → U11_GGA(T29, T164, T166, times38_in_gga(T172, T164, X368))
U10_GGA(T29, T164, T166, convertc19_out_gga(T29, T164, s(T172))) → TIMES38_IN_GGA(T172, T164, X368)
CONVERT1_IN_GGA(.(0, T29), s(T203), T199) → U12_GGA(T29, T203, T199, convertc19_in_gga(T29, s(T203), s(T172)))
U12_GGA(T29, T203, T199, convertc19_out_gga(T29, s(T203), s(T172))) → U13_GGA(T29, T203, T199, timesc38_in_gga(T172, s(T203), T197))
U13_GGA(T29, T203, T199, timesc38_out_gga(T172, s(T203), T197)) → U14_GGA(T29, T203, T199, plus53_in_gga(T203, T197, X413))
U13_GGA(T29, T203, T199, timesc38_out_gga(T172, s(T203), T197)) → PLUS53_IN_GGA(T203, T197, X413)
CONVERT1_IN_GGA(.(s(T243), T244), T220, T222) → U15_GGA(T243, T244, T220, T222, convert1_in_gga(.(T243, T244), T220, X460))
CONVERT1_IN_GGA(.(s(T243), T244), T220, T222) → CONVERT1_IN_GGA(.(T243, T244), T220, X460)

The TRS R consists of the following rules:

convertc19_in_gga([], T35, 0) → convertc19_out_gga([], T35, 0)
convertc19_in_gga(.(0, T52), T41, X82) → U17_gga(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
convertc19_in_gga(.(s(T128), T129), T107, s(T142)) → U19_gga(T128, T129, T107, T142, convertc1_in_gga(.(T128, T129), T107, T142))
convertc1_in_gga([], T6, 0) → convertc1_out_gga([], T6, 0)
convertc1_in_gga(.(0, T29), T149, 0) → U23_gga(T29, T149, convertc19_in_ggg(T29, T149, 0))
convertc19_in_ggg([], T35, 0) → convertc19_out_ggg([], T35, 0)
convertc19_in_ggg(.(0, T52), T41, X82) → U17_ggg(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
U17_ggg(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_ggg(T52, T41, X82, timesc38_in_ggg(T54, T41, X82))
timesc38_in_ggg(0, T59, 0) → timesc38_out_ggg(0, T59, 0)
timesc38_in_ggg(s(T72), T66, X148) → U20_ggg(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
timesc38_in_gga(0, T59, 0) → timesc38_out_gga(0, T59, 0)
timesc38_in_gga(s(T72), T66, X148) → U20_gga(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
U20_gga(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_gga(T72, T66, X148, plusc53_in_gga(T66, T74, X148))
plusc53_in_gga(0, T82, T82) → plusc53_out_gga(0, T82, T82)
plusc53_in_gga(s(T93), T89, s(T100)) → U22_gga(T93, T89, T100, plusc53_in_gga(T93, T89, T100))
U22_gga(T93, T89, T100, plusc53_out_gga(T93, T89, T100)) → plusc53_out_gga(s(T93), T89, s(T100))
U21_gga(T72, T66, X148, plusc53_out_gga(T66, T74, X148)) → timesc38_out_gga(s(T72), T66, X148)
U20_ggg(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_ggg(T72, T66, X148, plusc53_in_ggg(T66, T74, X148))
plusc53_in_ggg(0, T82, T82) → plusc53_out_ggg(0, T82, T82)
plusc53_in_ggg(s(T93), T89, s(T100)) → U22_ggg(T93, T89, T100, plusc53_in_ggg(T93, T89, T100))
U22_ggg(T93, T89, T100, plusc53_out_ggg(T93, T89, T100)) → plusc53_out_ggg(s(T93), T89, s(T100))
U21_ggg(T72, T66, X148, plusc53_out_ggg(T66, T74, X148)) → timesc38_out_ggg(s(T72), T66, X148)
U18_ggg(T52, T41, X82, timesc38_out_ggg(T54, T41, X82)) → convertc19_out_ggg(.(0, T52), T41, X82)
convertc19_in_ggg(.(s(T128), T129), T107, s(T142)) → U19_ggg(T128, T129, T107, T142, convertc1_in_ggg(.(T128, T129), T107, T142))
convertc1_in_ggg([], T6, 0) → convertc1_out_ggg([], T6, 0)
convertc1_in_ggg(.(0, T29), T149, 0) → U23_ggg(T29, T149, convertc19_in_ggg(T29, T149, 0))
U23_ggg(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_ggg(.(0, T29), T149, 0)
convertc1_in_ggg(.(0, T29), 0, T187) → U24_ggg(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_ggg(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_ggg(T29, T187, timesc38_in_ggg(T172, 0, T187))
U25_ggg(T29, T187, timesc38_out_ggg(T172, 0, T187)) → convertc1_out_ggg(.(0, T29), 0, T187)
convertc1_in_ggg(.(0, T29), s(T203), s(T210)) → U26_ggg(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_ggg(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_ggg(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_ggg(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_ggg(T29, T203, T210, plusc53_in_ggg(T203, T197, T210))
U28_ggg(T29, T203, T210, plusc53_out_ggg(T203, T197, T210)) → convertc1_out_ggg(.(0, T29), s(T203), s(T210))
convertc1_in_ggg(.(0, T29), s(T203), 0) → U29_ggg(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_ggg(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_ggg(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_ggg(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_ggg(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_ggg(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_ggg(.(0, T29), s(T203), 0)
convertc1_in_ggg(.(s(T243), T244), T220, s(T257)) → U32_ggg(T243, T244, T220, T257, convertc1_in_ggg(.(T243, T244), T220, T257))
convertc1_in_ggg(.(s(T243), T244), T220, 0) → U33_ggg(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_ggg(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_ggg(.(s(T243), T244), T220, 0)
U32_ggg(T243, T244, T220, T257, convertc1_out_ggg(.(T243, T244), T220, T257)) → convertc1_out_ggg(.(s(T243), T244), T220, s(T257))
U19_ggg(T128, T129, T107, T142, convertc1_out_ggg(.(T128, T129), T107, T142)) → convertc19_out_ggg(.(s(T128), T129), T107, s(T142))
U23_gga(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_gga(.(0, T29), T149, 0)
convertc1_in_gga(.(0, T29), 0, T187) → U24_gga(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_gga(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_gga(T29, T187, timesc38_in_gga(T172, 0, T187))
U25_gga(T29, T187, timesc38_out_gga(T172, 0, T187)) → convertc1_out_gga(.(0, T29), 0, T187)
convertc1_in_gga(.(0, T29), s(T203), s(T210)) → U26_gga(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_gga(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_gga(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_gga(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_gga(T29, T203, T210, plusc53_in_gga(T203, T197, T210))
U28_gga(T29, T203, T210, plusc53_out_gga(T203, T197, T210)) → convertc1_out_gga(.(0, T29), s(T203), s(T210))
convertc1_in_gga(.(0, T29), s(T203), 0) → U29_gga(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_gga(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_gga(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_gga(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_gga(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_gga(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_gga(.(0, T29), s(T203), 0)
convertc1_in_gga(.(s(T243), T244), T220, s(T257)) → U32_gga(T243, T244, T220, T257, convertc1_in_gga(.(T243, T244), T220, T257))
convertc1_in_gga(.(s(T243), T244), T220, 0) → U33_gga(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_gga(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_gga(.(s(T243), T244), T220, 0)
U32_gga(T243, T244, T220, T257, convertc1_out_gga(.(T243, T244), T220, T257)) → convertc1_out_gga(.(s(T243), T244), T220, s(T257))
U19_gga(T128, T129, T107, T142, convertc1_out_gga(.(T128, T129), T107, T142)) → convertc19_out_gga(.(s(T128), T129), T107, s(T142))
U17_gga(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_gga(T52, T41, X82, timesc38_in_gga(T54, T41, X82))
U18_gga(T52, T41, X82, timesc38_out_gga(T54, T41, X82)) → convertc19_out_gga(.(0, T52), T41, X82)

The argument filtering Pi contains the following mapping:
convert1_in_gga(x1, x2, x3)  =  convert1_in_gga(x1, x2)
.(x1, x2)  =  .(x1, x2)
0  =  0
convert19_in_gga(x1, x2, x3)  =  convert19_in_gga(x1, x2)
convertc19_in_gga(x1, x2, x3)  =  convertc19_in_gga(x1, x2)
[]  =  []
convertc19_out_gga(x1, x2, x3)  =  convertc19_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
s(x1)  =  s(x1)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x2, x3, x5)
convertc1_in_gga(x1, x2, x3)  =  convertc1_in_gga(x1, x2)
convertc1_out_gga(x1, x2, x3)  =  convertc1_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x2, x3)
convertc19_in_ggg(x1, x2, x3)  =  convertc19_in_ggg(x1, x2, x3)
convertc19_out_ggg(x1, x2, x3)  =  convertc19_out_ggg(x1, x2, x3)
U17_ggg(x1, x2, x3, x4)  =  U17_ggg(x1, x2, x3, x4)
U18_ggg(x1, x2, x3, x4)  =  U18_ggg(x1, x2, x3, x4)
timesc38_in_ggg(x1, x2, x3)  =  timesc38_in_ggg(x1, x2, x3)
timesc38_out_ggg(x1, x2, x3)  =  timesc38_out_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
timesc38_in_gga(x1, x2, x3)  =  timesc38_in_gga(x1, x2)
timesc38_out_gga(x1, x2, x3)  =  timesc38_out_gga(x1, x2, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x1, x2, x4)
plusc53_in_gga(x1, x2, x3)  =  plusc53_in_gga(x1, x2)
plusc53_out_gga(x1, x2, x3)  =  plusc53_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
plusc53_in_ggg(x1, x2, x3)  =  plusc53_in_ggg(x1, x2, x3)
plusc53_out_ggg(x1, x2, x3)  =  plusc53_out_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U19_ggg(x1, x2, x3, x4, x5)  =  U19_ggg(x1, x2, x3, x4, x5)
convertc1_in_ggg(x1, x2, x3)  =  convertc1_in_ggg(x1, x2, x3)
convertc1_out_ggg(x1, x2, x3)  =  convertc1_out_ggg(x1, x2, x3)
U23_ggg(x1, x2, x3)  =  U23_ggg(x1, x2, x3)
U24_ggg(x1, x2, x3)  =  U24_ggg(x1, x2, x3)
U25_ggg(x1, x2, x3)  =  U25_ggg(x1, x2, x3)
U26_ggg(x1, x2, x3, x4)  =  U26_ggg(x1, x2, x3, x4)
U27_ggg(x1, x2, x3, x4)  =  U27_ggg(x1, x2, x3, x4)
U28_ggg(x1, x2, x3, x4)  =  U28_ggg(x1, x2, x3, x4)
U29_ggg(x1, x2, x3)  =  U29_ggg(x1, x2, x3)
U30_ggg(x1, x2, x3)  =  U30_ggg(x1, x2, x3)
U31_ggg(x1, x2, x3)  =  U31_ggg(x1, x2, x3)
U32_ggg(x1, x2, x3, x4, x5)  =  U32_ggg(x1, x2, x3, x4, x5)
U33_ggg(x1, x2, x3, x4)  =  U33_ggg(x1, x2, x3, x4)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x1, x2, x4)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x2, x3)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x3, x5)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x3, x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
times38_in_gga(x1, x2, x3)  =  times38_in_gga(x1, x2)
plus53_in_gga(x1, x2, x3)  =  plus53_in_gga(x1, x2)
CONVERT1_IN_GGA(x1, x2, x3)  =  CONVERT1_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
CONVERT19_IN_GGA(x1, x2, x3)  =  CONVERT19_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
TIMES38_IN_GGA(x1, x2, x3)  =  TIMES38_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
PLUS53_IN_GGA(x1, x2, x3)  =  PLUS53_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4, x5)  =  U15_GGA(x1, x2, x3, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

CONVERT1_IN_GGA(.(0, T29), T16, T18) → U9_GGA(T29, T16, T18, convert19_in_gga(T29, T16, X22))
CONVERT1_IN_GGA(.(0, T29), T16, T18) → CONVERT19_IN_GGA(T29, T16, X22)
CONVERT19_IN_GGA(.(0, T52), T41, X82) → U1_GGA(T52, T41, X82, convert19_in_gga(T52, T41, X81))
CONVERT19_IN_GGA(.(0, T52), T41, X82) → CONVERT19_IN_GGA(T52, T41, X81)
CONVERT19_IN_GGA(.(0, T52), T41, X82) → U2_GGA(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
U2_GGA(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U3_GGA(T52, T41, X82, times38_in_gga(T54, T41, X82))
U2_GGA(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → TIMES38_IN_GGA(T54, T41, X82)
TIMES38_IN_GGA(s(T72), T66, X148) → U5_GGA(T72, T66, X148, times38_in_gga(T72, T66, X147))
TIMES38_IN_GGA(s(T72), T66, X148) → TIMES38_IN_GGA(T72, T66, X147)
TIMES38_IN_GGA(s(T72), T66, X148) → U6_GGA(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
U6_GGA(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U7_GGA(T72, T66, X148, plus53_in_gga(T66, T74, X148))
U6_GGA(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → PLUS53_IN_GGA(T66, T74, X148)
PLUS53_IN_GGA(s(T93), T89, X199) → U8_GGA(T93, T89, X199, plus53_in_gga(T93, T89, X198))
PLUS53_IN_GGA(s(T93), T89, X199) → PLUS53_IN_GGA(T93, T89, X198)
CONVERT19_IN_GGA(.(s(T128), T129), T107, X251) → U4_GGA(T128, T129, T107, X251, convert1_in_gga(.(T128, T129), T107, X250))
CONVERT19_IN_GGA(.(s(T128), T129), T107, X251) → CONVERT1_IN_GGA(.(T128, T129), T107, X250)
CONVERT1_IN_GGA(.(0, T29), T164, T166) → U10_GGA(T29, T164, T166, convertc19_in_gga(T29, T164, s(T172)))
U10_GGA(T29, T164, T166, convertc19_out_gga(T29, T164, s(T172))) → U11_GGA(T29, T164, T166, times38_in_gga(T172, T164, X368))
U10_GGA(T29, T164, T166, convertc19_out_gga(T29, T164, s(T172))) → TIMES38_IN_GGA(T172, T164, X368)
CONVERT1_IN_GGA(.(0, T29), s(T203), T199) → U12_GGA(T29, T203, T199, convertc19_in_gga(T29, s(T203), s(T172)))
U12_GGA(T29, T203, T199, convertc19_out_gga(T29, s(T203), s(T172))) → U13_GGA(T29, T203, T199, timesc38_in_gga(T172, s(T203), T197))
U13_GGA(T29, T203, T199, timesc38_out_gga(T172, s(T203), T197)) → U14_GGA(T29, T203, T199, plus53_in_gga(T203, T197, X413))
U13_GGA(T29, T203, T199, timesc38_out_gga(T172, s(T203), T197)) → PLUS53_IN_GGA(T203, T197, X413)
CONVERT1_IN_GGA(.(s(T243), T244), T220, T222) → U15_GGA(T243, T244, T220, T222, convert1_in_gga(.(T243, T244), T220, X460))
CONVERT1_IN_GGA(.(s(T243), T244), T220, T222) → CONVERT1_IN_GGA(.(T243, T244), T220, X460)

The TRS R consists of the following rules:

convertc19_in_gga([], T35, 0) → convertc19_out_gga([], T35, 0)
convertc19_in_gga(.(0, T52), T41, X82) → U17_gga(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
convertc19_in_gga(.(s(T128), T129), T107, s(T142)) → U19_gga(T128, T129, T107, T142, convertc1_in_gga(.(T128, T129), T107, T142))
convertc1_in_gga([], T6, 0) → convertc1_out_gga([], T6, 0)
convertc1_in_gga(.(0, T29), T149, 0) → U23_gga(T29, T149, convertc19_in_ggg(T29, T149, 0))
convertc19_in_ggg([], T35, 0) → convertc19_out_ggg([], T35, 0)
convertc19_in_ggg(.(0, T52), T41, X82) → U17_ggg(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
U17_ggg(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_ggg(T52, T41, X82, timesc38_in_ggg(T54, T41, X82))
timesc38_in_ggg(0, T59, 0) → timesc38_out_ggg(0, T59, 0)
timesc38_in_ggg(s(T72), T66, X148) → U20_ggg(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
timesc38_in_gga(0, T59, 0) → timesc38_out_gga(0, T59, 0)
timesc38_in_gga(s(T72), T66, X148) → U20_gga(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
U20_gga(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_gga(T72, T66, X148, plusc53_in_gga(T66, T74, X148))
plusc53_in_gga(0, T82, T82) → plusc53_out_gga(0, T82, T82)
plusc53_in_gga(s(T93), T89, s(T100)) → U22_gga(T93, T89, T100, plusc53_in_gga(T93, T89, T100))
U22_gga(T93, T89, T100, plusc53_out_gga(T93, T89, T100)) → plusc53_out_gga(s(T93), T89, s(T100))
U21_gga(T72, T66, X148, plusc53_out_gga(T66, T74, X148)) → timesc38_out_gga(s(T72), T66, X148)
U20_ggg(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_ggg(T72, T66, X148, plusc53_in_ggg(T66, T74, X148))
plusc53_in_ggg(0, T82, T82) → plusc53_out_ggg(0, T82, T82)
plusc53_in_ggg(s(T93), T89, s(T100)) → U22_ggg(T93, T89, T100, plusc53_in_ggg(T93, T89, T100))
U22_ggg(T93, T89, T100, plusc53_out_ggg(T93, T89, T100)) → plusc53_out_ggg(s(T93), T89, s(T100))
U21_ggg(T72, T66, X148, plusc53_out_ggg(T66, T74, X148)) → timesc38_out_ggg(s(T72), T66, X148)
U18_ggg(T52, T41, X82, timesc38_out_ggg(T54, T41, X82)) → convertc19_out_ggg(.(0, T52), T41, X82)
convertc19_in_ggg(.(s(T128), T129), T107, s(T142)) → U19_ggg(T128, T129, T107, T142, convertc1_in_ggg(.(T128, T129), T107, T142))
convertc1_in_ggg([], T6, 0) → convertc1_out_ggg([], T6, 0)
convertc1_in_ggg(.(0, T29), T149, 0) → U23_ggg(T29, T149, convertc19_in_ggg(T29, T149, 0))
U23_ggg(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_ggg(.(0, T29), T149, 0)
convertc1_in_ggg(.(0, T29), 0, T187) → U24_ggg(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_ggg(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_ggg(T29, T187, timesc38_in_ggg(T172, 0, T187))
U25_ggg(T29, T187, timesc38_out_ggg(T172, 0, T187)) → convertc1_out_ggg(.(0, T29), 0, T187)
convertc1_in_ggg(.(0, T29), s(T203), s(T210)) → U26_ggg(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_ggg(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_ggg(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_ggg(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_ggg(T29, T203, T210, plusc53_in_ggg(T203, T197, T210))
U28_ggg(T29, T203, T210, plusc53_out_ggg(T203, T197, T210)) → convertc1_out_ggg(.(0, T29), s(T203), s(T210))
convertc1_in_ggg(.(0, T29), s(T203), 0) → U29_ggg(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_ggg(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_ggg(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_ggg(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_ggg(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_ggg(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_ggg(.(0, T29), s(T203), 0)
convertc1_in_ggg(.(s(T243), T244), T220, s(T257)) → U32_ggg(T243, T244, T220, T257, convertc1_in_ggg(.(T243, T244), T220, T257))
convertc1_in_ggg(.(s(T243), T244), T220, 0) → U33_ggg(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_ggg(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_ggg(.(s(T243), T244), T220, 0)
U32_ggg(T243, T244, T220, T257, convertc1_out_ggg(.(T243, T244), T220, T257)) → convertc1_out_ggg(.(s(T243), T244), T220, s(T257))
U19_ggg(T128, T129, T107, T142, convertc1_out_ggg(.(T128, T129), T107, T142)) → convertc19_out_ggg(.(s(T128), T129), T107, s(T142))
U23_gga(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_gga(.(0, T29), T149, 0)
convertc1_in_gga(.(0, T29), 0, T187) → U24_gga(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_gga(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_gga(T29, T187, timesc38_in_gga(T172, 0, T187))
U25_gga(T29, T187, timesc38_out_gga(T172, 0, T187)) → convertc1_out_gga(.(0, T29), 0, T187)
convertc1_in_gga(.(0, T29), s(T203), s(T210)) → U26_gga(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_gga(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_gga(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_gga(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_gga(T29, T203, T210, plusc53_in_gga(T203, T197, T210))
U28_gga(T29, T203, T210, plusc53_out_gga(T203, T197, T210)) → convertc1_out_gga(.(0, T29), s(T203), s(T210))
convertc1_in_gga(.(0, T29), s(T203), 0) → U29_gga(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_gga(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_gga(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_gga(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_gga(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_gga(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_gga(.(0, T29), s(T203), 0)
convertc1_in_gga(.(s(T243), T244), T220, s(T257)) → U32_gga(T243, T244, T220, T257, convertc1_in_gga(.(T243, T244), T220, T257))
convertc1_in_gga(.(s(T243), T244), T220, 0) → U33_gga(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_gga(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_gga(.(s(T243), T244), T220, 0)
U32_gga(T243, T244, T220, T257, convertc1_out_gga(.(T243, T244), T220, T257)) → convertc1_out_gga(.(s(T243), T244), T220, s(T257))
U19_gga(T128, T129, T107, T142, convertc1_out_gga(.(T128, T129), T107, T142)) → convertc19_out_gga(.(s(T128), T129), T107, s(T142))
U17_gga(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_gga(T52, T41, X82, timesc38_in_gga(T54, T41, X82))
U18_gga(T52, T41, X82, timesc38_out_gga(T54, T41, X82)) → convertc19_out_gga(.(0, T52), T41, X82)

The argument filtering Pi contains the following mapping:
convert1_in_gga(x1, x2, x3)  =  convert1_in_gga(x1, x2)
.(x1, x2)  =  .(x1, x2)
0  =  0
convert19_in_gga(x1, x2, x3)  =  convert19_in_gga(x1, x2)
convertc19_in_gga(x1, x2, x3)  =  convertc19_in_gga(x1, x2)
[]  =  []
convertc19_out_gga(x1, x2, x3)  =  convertc19_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
s(x1)  =  s(x1)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x2, x3, x5)
convertc1_in_gga(x1, x2, x3)  =  convertc1_in_gga(x1, x2)
convertc1_out_gga(x1, x2, x3)  =  convertc1_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x2, x3)
convertc19_in_ggg(x1, x2, x3)  =  convertc19_in_ggg(x1, x2, x3)
convertc19_out_ggg(x1, x2, x3)  =  convertc19_out_ggg(x1, x2, x3)
U17_ggg(x1, x2, x3, x4)  =  U17_ggg(x1, x2, x3, x4)
U18_ggg(x1, x2, x3, x4)  =  U18_ggg(x1, x2, x3, x4)
timesc38_in_ggg(x1, x2, x3)  =  timesc38_in_ggg(x1, x2, x3)
timesc38_out_ggg(x1, x2, x3)  =  timesc38_out_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
timesc38_in_gga(x1, x2, x3)  =  timesc38_in_gga(x1, x2)
timesc38_out_gga(x1, x2, x3)  =  timesc38_out_gga(x1, x2, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x1, x2, x4)
plusc53_in_gga(x1, x2, x3)  =  plusc53_in_gga(x1, x2)
plusc53_out_gga(x1, x2, x3)  =  plusc53_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
plusc53_in_ggg(x1, x2, x3)  =  plusc53_in_ggg(x1, x2, x3)
plusc53_out_ggg(x1, x2, x3)  =  plusc53_out_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U19_ggg(x1, x2, x3, x4, x5)  =  U19_ggg(x1, x2, x3, x4, x5)
convertc1_in_ggg(x1, x2, x3)  =  convertc1_in_ggg(x1, x2, x3)
convertc1_out_ggg(x1, x2, x3)  =  convertc1_out_ggg(x1, x2, x3)
U23_ggg(x1, x2, x3)  =  U23_ggg(x1, x2, x3)
U24_ggg(x1, x2, x3)  =  U24_ggg(x1, x2, x3)
U25_ggg(x1, x2, x3)  =  U25_ggg(x1, x2, x3)
U26_ggg(x1, x2, x3, x4)  =  U26_ggg(x1, x2, x3, x4)
U27_ggg(x1, x2, x3, x4)  =  U27_ggg(x1, x2, x3, x4)
U28_ggg(x1, x2, x3, x4)  =  U28_ggg(x1, x2, x3, x4)
U29_ggg(x1, x2, x3)  =  U29_ggg(x1, x2, x3)
U30_ggg(x1, x2, x3)  =  U30_ggg(x1, x2, x3)
U31_ggg(x1, x2, x3)  =  U31_ggg(x1, x2, x3)
U32_ggg(x1, x2, x3, x4, x5)  =  U32_ggg(x1, x2, x3, x4, x5)
U33_ggg(x1, x2, x3, x4)  =  U33_ggg(x1, x2, x3, x4)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x1, x2, x4)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x2, x3)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x3, x5)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x3, x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
times38_in_gga(x1, x2, x3)  =  times38_in_gga(x1, x2)
plus53_in_gga(x1, x2, x3)  =  plus53_in_gga(x1, x2)
CONVERT1_IN_GGA(x1, x2, x3)  =  CONVERT1_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
CONVERT19_IN_GGA(x1, x2, x3)  =  CONVERT19_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
TIMES38_IN_GGA(x1, x2, x3)  =  TIMES38_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
PLUS53_IN_GGA(x1, x2, x3)  =  PLUS53_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
U13_GGA(x1, x2, x3, x4)  =  U13_GGA(x1, x2, x4)
U14_GGA(x1, x2, x3, x4)  =  U14_GGA(x1, x2, x4)
U15_GGA(x1, x2, x3, x4, x5)  =  U15_GGA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 19 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

PLUS53_IN_GGA(s(T93), T89, X199) → PLUS53_IN_GGA(T93, T89, X198)

The TRS R consists of the following rules:

convertc19_in_gga([], T35, 0) → convertc19_out_gga([], T35, 0)
convertc19_in_gga(.(0, T52), T41, X82) → U17_gga(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
convertc19_in_gga(.(s(T128), T129), T107, s(T142)) → U19_gga(T128, T129, T107, T142, convertc1_in_gga(.(T128, T129), T107, T142))
convertc1_in_gga([], T6, 0) → convertc1_out_gga([], T6, 0)
convertc1_in_gga(.(0, T29), T149, 0) → U23_gga(T29, T149, convertc19_in_ggg(T29, T149, 0))
convertc19_in_ggg([], T35, 0) → convertc19_out_ggg([], T35, 0)
convertc19_in_ggg(.(0, T52), T41, X82) → U17_ggg(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
U17_ggg(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_ggg(T52, T41, X82, timesc38_in_ggg(T54, T41, X82))
timesc38_in_ggg(0, T59, 0) → timesc38_out_ggg(0, T59, 0)
timesc38_in_ggg(s(T72), T66, X148) → U20_ggg(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
timesc38_in_gga(0, T59, 0) → timesc38_out_gga(0, T59, 0)
timesc38_in_gga(s(T72), T66, X148) → U20_gga(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
U20_gga(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_gga(T72, T66, X148, plusc53_in_gga(T66, T74, X148))
plusc53_in_gga(0, T82, T82) → plusc53_out_gga(0, T82, T82)
plusc53_in_gga(s(T93), T89, s(T100)) → U22_gga(T93, T89, T100, plusc53_in_gga(T93, T89, T100))
U22_gga(T93, T89, T100, plusc53_out_gga(T93, T89, T100)) → plusc53_out_gga(s(T93), T89, s(T100))
U21_gga(T72, T66, X148, plusc53_out_gga(T66, T74, X148)) → timesc38_out_gga(s(T72), T66, X148)
U20_ggg(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_ggg(T72, T66, X148, plusc53_in_ggg(T66, T74, X148))
plusc53_in_ggg(0, T82, T82) → plusc53_out_ggg(0, T82, T82)
plusc53_in_ggg(s(T93), T89, s(T100)) → U22_ggg(T93, T89, T100, plusc53_in_ggg(T93, T89, T100))
U22_ggg(T93, T89, T100, plusc53_out_ggg(T93, T89, T100)) → plusc53_out_ggg(s(T93), T89, s(T100))
U21_ggg(T72, T66, X148, plusc53_out_ggg(T66, T74, X148)) → timesc38_out_ggg(s(T72), T66, X148)
U18_ggg(T52, T41, X82, timesc38_out_ggg(T54, T41, X82)) → convertc19_out_ggg(.(0, T52), T41, X82)
convertc19_in_ggg(.(s(T128), T129), T107, s(T142)) → U19_ggg(T128, T129, T107, T142, convertc1_in_ggg(.(T128, T129), T107, T142))
convertc1_in_ggg([], T6, 0) → convertc1_out_ggg([], T6, 0)
convertc1_in_ggg(.(0, T29), T149, 0) → U23_ggg(T29, T149, convertc19_in_ggg(T29, T149, 0))
U23_ggg(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_ggg(.(0, T29), T149, 0)
convertc1_in_ggg(.(0, T29), 0, T187) → U24_ggg(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_ggg(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_ggg(T29, T187, timesc38_in_ggg(T172, 0, T187))
U25_ggg(T29, T187, timesc38_out_ggg(T172, 0, T187)) → convertc1_out_ggg(.(0, T29), 0, T187)
convertc1_in_ggg(.(0, T29), s(T203), s(T210)) → U26_ggg(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_ggg(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_ggg(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_ggg(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_ggg(T29, T203, T210, plusc53_in_ggg(T203, T197, T210))
U28_ggg(T29, T203, T210, plusc53_out_ggg(T203, T197, T210)) → convertc1_out_ggg(.(0, T29), s(T203), s(T210))
convertc1_in_ggg(.(0, T29), s(T203), 0) → U29_ggg(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_ggg(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_ggg(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_ggg(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_ggg(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_ggg(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_ggg(.(0, T29), s(T203), 0)
convertc1_in_ggg(.(s(T243), T244), T220, s(T257)) → U32_ggg(T243, T244, T220, T257, convertc1_in_ggg(.(T243, T244), T220, T257))
convertc1_in_ggg(.(s(T243), T244), T220, 0) → U33_ggg(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_ggg(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_ggg(.(s(T243), T244), T220, 0)
U32_ggg(T243, T244, T220, T257, convertc1_out_ggg(.(T243, T244), T220, T257)) → convertc1_out_ggg(.(s(T243), T244), T220, s(T257))
U19_ggg(T128, T129, T107, T142, convertc1_out_ggg(.(T128, T129), T107, T142)) → convertc19_out_ggg(.(s(T128), T129), T107, s(T142))
U23_gga(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_gga(.(0, T29), T149, 0)
convertc1_in_gga(.(0, T29), 0, T187) → U24_gga(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_gga(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_gga(T29, T187, timesc38_in_gga(T172, 0, T187))
U25_gga(T29, T187, timesc38_out_gga(T172, 0, T187)) → convertc1_out_gga(.(0, T29), 0, T187)
convertc1_in_gga(.(0, T29), s(T203), s(T210)) → U26_gga(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_gga(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_gga(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_gga(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_gga(T29, T203, T210, plusc53_in_gga(T203, T197, T210))
U28_gga(T29, T203, T210, plusc53_out_gga(T203, T197, T210)) → convertc1_out_gga(.(0, T29), s(T203), s(T210))
convertc1_in_gga(.(0, T29), s(T203), 0) → U29_gga(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_gga(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_gga(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_gga(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_gga(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_gga(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_gga(.(0, T29), s(T203), 0)
convertc1_in_gga(.(s(T243), T244), T220, s(T257)) → U32_gga(T243, T244, T220, T257, convertc1_in_gga(.(T243, T244), T220, T257))
convertc1_in_gga(.(s(T243), T244), T220, 0) → U33_gga(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_gga(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_gga(.(s(T243), T244), T220, 0)
U32_gga(T243, T244, T220, T257, convertc1_out_gga(.(T243, T244), T220, T257)) → convertc1_out_gga(.(s(T243), T244), T220, s(T257))
U19_gga(T128, T129, T107, T142, convertc1_out_gga(.(T128, T129), T107, T142)) → convertc19_out_gga(.(s(T128), T129), T107, s(T142))
U17_gga(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_gga(T52, T41, X82, timesc38_in_gga(T54, T41, X82))
U18_gga(T52, T41, X82, timesc38_out_gga(T54, T41, X82)) → convertc19_out_gga(.(0, T52), T41, X82)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
0  =  0
convertc19_in_gga(x1, x2, x3)  =  convertc19_in_gga(x1, x2)
[]  =  []
convertc19_out_gga(x1, x2, x3)  =  convertc19_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
s(x1)  =  s(x1)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x2, x3, x5)
convertc1_in_gga(x1, x2, x3)  =  convertc1_in_gga(x1, x2)
convertc1_out_gga(x1, x2, x3)  =  convertc1_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x2, x3)
convertc19_in_ggg(x1, x2, x3)  =  convertc19_in_ggg(x1, x2, x3)
convertc19_out_ggg(x1, x2, x3)  =  convertc19_out_ggg(x1, x2, x3)
U17_ggg(x1, x2, x3, x4)  =  U17_ggg(x1, x2, x3, x4)
U18_ggg(x1, x2, x3, x4)  =  U18_ggg(x1, x2, x3, x4)
timesc38_in_ggg(x1, x2, x3)  =  timesc38_in_ggg(x1, x2, x3)
timesc38_out_ggg(x1, x2, x3)  =  timesc38_out_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
timesc38_in_gga(x1, x2, x3)  =  timesc38_in_gga(x1, x2)
timesc38_out_gga(x1, x2, x3)  =  timesc38_out_gga(x1, x2, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x1, x2, x4)
plusc53_in_gga(x1, x2, x3)  =  plusc53_in_gga(x1, x2)
plusc53_out_gga(x1, x2, x3)  =  plusc53_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
plusc53_in_ggg(x1, x2, x3)  =  plusc53_in_ggg(x1, x2, x3)
plusc53_out_ggg(x1, x2, x3)  =  plusc53_out_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U19_ggg(x1, x2, x3, x4, x5)  =  U19_ggg(x1, x2, x3, x4, x5)
convertc1_in_ggg(x1, x2, x3)  =  convertc1_in_ggg(x1, x2, x3)
convertc1_out_ggg(x1, x2, x3)  =  convertc1_out_ggg(x1, x2, x3)
U23_ggg(x1, x2, x3)  =  U23_ggg(x1, x2, x3)
U24_ggg(x1, x2, x3)  =  U24_ggg(x1, x2, x3)
U25_ggg(x1, x2, x3)  =  U25_ggg(x1, x2, x3)
U26_ggg(x1, x2, x3, x4)  =  U26_ggg(x1, x2, x3, x4)
U27_ggg(x1, x2, x3, x4)  =  U27_ggg(x1, x2, x3, x4)
U28_ggg(x1, x2, x3, x4)  =  U28_ggg(x1, x2, x3, x4)
U29_ggg(x1, x2, x3)  =  U29_ggg(x1, x2, x3)
U30_ggg(x1, x2, x3)  =  U30_ggg(x1, x2, x3)
U31_ggg(x1, x2, x3)  =  U31_ggg(x1, x2, x3)
U32_ggg(x1, x2, x3, x4, x5)  =  U32_ggg(x1, x2, x3, x4, x5)
U33_ggg(x1, x2, x3, x4)  =  U33_ggg(x1, x2, x3, x4)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x1, x2, x4)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x2, x3)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x3, x5)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x3, x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
PLUS53_IN_GGA(x1, x2, x3)  =  PLUS53_IN_GGA(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:

PLUS53_IN_GGA(s(T93), T89, X199) → PLUS53_IN_GGA(T93, T89, X198)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUS53_IN_GGA(x1, x2, x3)  =  PLUS53_IN_GGA(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:

PLUS53_IN_GGA(s(T93), T89) → PLUS53_IN_GGA(T93, T89)

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:

• PLUS53_IN_GGA(s(T93), T89) → PLUS53_IN_GGA(T93, T89)
  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:

TIMES38_IN_GGA(s(T72), T66, X148) → TIMES38_IN_GGA(T72, T66, X147)

The TRS R consists of the following rules:

convertc19_in_gga([], T35, 0) → convertc19_out_gga([], T35, 0)
convertc19_in_gga(.(0, T52), T41, X82) → U17_gga(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
convertc19_in_gga(.(s(T128), T129), T107, s(T142)) → U19_gga(T128, T129, T107, T142, convertc1_in_gga(.(T128, T129), T107, T142))
convertc1_in_gga([], T6, 0) → convertc1_out_gga([], T6, 0)
convertc1_in_gga(.(0, T29), T149, 0) → U23_gga(T29, T149, convertc19_in_ggg(T29, T149, 0))
convertc19_in_ggg([], T35, 0) → convertc19_out_ggg([], T35, 0)
convertc19_in_ggg(.(0, T52), T41, X82) → U17_ggg(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
U17_ggg(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_ggg(T52, T41, X82, timesc38_in_ggg(T54, T41, X82))
timesc38_in_ggg(0, T59, 0) → timesc38_out_ggg(0, T59, 0)
timesc38_in_ggg(s(T72), T66, X148) → U20_ggg(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
timesc38_in_gga(0, T59, 0) → timesc38_out_gga(0, T59, 0)
timesc38_in_gga(s(T72), T66, X148) → U20_gga(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
U20_gga(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_gga(T72, T66, X148, plusc53_in_gga(T66, T74, X148))
plusc53_in_gga(0, T82, T82) → plusc53_out_gga(0, T82, T82)
plusc53_in_gga(s(T93), T89, s(T100)) → U22_gga(T93, T89, T100, plusc53_in_gga(T93, T89, T100))
U22_gga(T93, T89, T100, plusc53_out_gga(T93, T89, T100)) → plusc53_out_gga(s(T93), T89, s(T100))
U21_gga(T72, T66, X148, plusc53_out_gga(T66, T74, X148)) → timesc38_out_gga(s(T72), T66, X148)
U20_ggg(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_ggg(T72, T66, X148, plusc53_in_ggg(T66, T74, X148))
plusc53_in_ggg(0, T82, T82) → plusc53_out_ggg(0, T82, T82)
plusc53_in_ggg(s(T93), T89, s(T100)) → U22_ggg(T93, T89, T100, plusc53_in_ggg(T93, T89, T100))
U22_ggg(T93, T89, T100, plusc53_out_ggg(T93, T89, T100)) → plusc53_out_ggg(s(T93), T89, s(T100))
U21_ggg(T72, T66, X148, plusc53_out_ggg(T66, T74, X148)) → timesc38_out_ggg(s(T72), T66, X148)
U18_ggg(T52, T41, X82, timesc38_out_ggg(T54, T41, X82)) → convertc19_out_ggg(.(0, T52), T41, X82)
convertc19_in_ggg(.(s(T128), T129), T107, s(T142)) → U19_ggg(T128, T129, T107, T142, convertc1_in_ggg(.(T128, T129), T107, T142))
convertc1_in_ggg([], T6, 0) → convertc1_out_ggg([], T6, 0)
convertc1_in_ggg(.(0, T29), T149, 0) → U23_ggg(T29, T149, convertc19_in_ggg(T29, T149, 0))
U23_ggg(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_ggg(.(0, T29), T149, 0)
convertc1_in_ggg(.(0, T29), 0, T187) → U24_ggg(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_ggg(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_ggg(T29, T187, timesc38_in_ggg(T172, 0, T187))
U25_ggg(T29, T187, timesc38_out_ggg(T172, 0, T187)) → convertc1_out_ggg(.(0, T29), 0, T187)
convertc1_in_ggg(.(0, T29), s(T203), s(T210)) → U26_ggg(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_ggg(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_ggg(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_ggg(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_ggg(T29, T203, T210, plusc53_in_ggg(T203, T197, T210))
U28_ggg(T29, T203, T210, plusc53_out_ggg(T203, T197, T210)) → convertc1_out_ggg(.(0, T29), s(T203), s(T210))
convertc1_in_ggg(.(0, T29), s(T203), 0) → U29_ggg(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_ggg(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_ggg(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_ggg(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_ggg(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_ggg(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_ggg(.(0, T29), s(T203), 0)
convertc1_in_ggg(.(s(T243), T244), T220, s(T257)) → U32_ggg(T243, T244, T220, T257, convertc1_in_ggg(.(T243, T244), T220, T257))
convertc1_in_ggg(.(s(T243), T244), T220, 0) → U33_ggg(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_ggg(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_ggg(.(s(T243), T244), T220, 0)
U32_ggg(T243, T244, T220, T257, convertc1_out_ggg(.(T243, T244), T220, T257)) → convertc1_out_ggg(.(s(T243), T244), T220, s(T257))
U19_ggg(T128, T129, T107, T142, convertc1_out_ggg(.(T128, T129), T107, T142)) → convertc19_out_ggg(.(s(T128), T129), T107, s(T142))
U23_gga(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_gga(.(0, T29), T149, 0)
convertc1_in_gga(.(0, T29), 0, T187) → U24_gga(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_gga(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_gga(T29, T187, timesc38_in_gga(T172, 0, T187))
U25_gga(T29, T187, timesc38_out_gga(T172, 0, T187)) → convertc1_out_gga(.(0, T29), 0, T187)
convertc1_in_gga(.(0, T29), s(T203), s(T210)) → U26_gga(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_gga(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_gga(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_gga(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_gga(T29, T203, T210, plusc53_in_gga(T203, T197, T210))
U28_gga(T29, T203, T210, plusc53_out_gga(T203, T197, T210)) → convertc1_out_gga(.(0, T29), s(T203), s(T210))
convertc1_in_gga(.(0, T29), s(T203), 0) → U29_gga(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_gga(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_gga(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_gga(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_gga(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_gga(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_gga(.(0, T29), s(T203), 0)
convertc1_in_gga(.(s(T243), T244), T220, s(T257)) → U32_gga(T243, T244, T220, T257, convertc1_in_gga(.(T243, T244), T220, T257))
convertc1_in_gga(.(s(T243), T244), T220, 0) → U33_gga(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_gga(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_gga(.(s(T243), T244), T220, 0)
U32_gga(T243, T244, T220, T257, convertc1_out_gga(.(T243, T244), T220, T257)) → convertc1_out_gga(.(s(T243), T244), T220, s(T257))
U19_gga(T128, T129, T107, T142, convertc1_out_gga(.(T128, T129), T107, T142)) → convertc19_out_gga(.(s(T128), T129), T107, s(T142))
U17_gga(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_gga(T52, T41, X82, timesc38_in_gga(T54, T41, X82))
U18_gga(T52, T41, X82, timesc38_out_gga(T54, T41, X82)) → convertc19_out_gga(.(0, T52), T41, X82)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
0  =  0
convertc19_in_gga(x1, x2, x3)  =  convertc19_in_gga(x1, x2)
[]  =  []
convertc19_out_gga(x1, x2, x3)  =  convertc19_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
s(x1)  =  s(x1)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x2, x3, x5)
convertc1_in_gga(x1, x2, x3)  =  convertc1_in_gga(x1, x2)
convertc1_out_gga(x1, x2, x3)  =  convertc1_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x2, x3)
convertc19_in_ggg(x1, x2, x3)  =  convertc19_in_ggg(x1, x2, x3)
convertc19_out_ggg(x1, x2, x3)  =  convertc19_out_ggg(x1, x2, x3)
U17_ggg(x1, x2, x3, x4)  =  U17_ggg(x1, x2, x3, x4)
U18_ggg(x1, x2, x3, x4)  =  U18_ggg(x1, x2, x3, x4)
timesc38_in_ggg(x1, x2, x3)  =  timesc38_in_ggg(x1, x2, x3)
timesc38_out_ggg(x1, x2, x3)  =  timesc38_out_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
timesc38_in_gga(x1, x2, x3)  =  timesc38_in_gga(x1, x2)
timesc38_out_gga(x1, x2, x3)  =  timesc38_out_gga(x1, x2, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x1, x2, x4)
plusc53_in_gga(x1, x2, x3)  =  plusc53_in_gga(x1, x2)
plusc53_out_gga(x1, x2, x3)  =  plusc53_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
plusc53_in_ggg(x1, x2, x3)  =  plusc53_in_ggg(x1, x2, x3)
plusc53_out_ggg(x1, x2, x3)  =  plusc53_out_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U19_ggg(x1, x2, x3, x4, x5)  =  U19_ggg(x1, x2, x3, x4, x5)
convertc1_in_ggg(x1, x2, x3)  =  convertc1_in_ggg(x1, x2, x3)
convertc1_out_ggg(x1, x2, x3)  =  convertc1_out_ggg(x1, x2, x3)
U23_ggg(x1, x2, x3)  =  U23_ggg(x1, x2, x3)
U24_ggg(x1, x2, x3)  =  U24_ggg(x1, x2, x3)
U25_ggg(x1, x2, x3)  =  U25_ggg(x1, x2, x3)
U26_ggg(x1, x2, x3, x4)  =  U26_ggg(x1, x2, x3, x4)
U27_ggg(x1, x2, x3, x4)  =  U27_ggg(x1, x2, x3, x4)
U28_ggg(x1, x2, x3, x4)  =  U28_ggg(x1, x2, x3, x4)
U29_ggg(x1, x2, x3)  =  U29_ggg(x1, x2, x3)
U30_ggg(x1, x2, x3)  =  U30_ggg(x1, x2, x3)
U31_ggg(x1, x2, x3)  =  U31_ggg(x1, x2, x3)
U32_ggg(x1, x2, x3, x4, x5)  =  U32_ggg(x1, x2, x3, x4, x5)
U33_ggg(x1, x2, x3, x4)  =  U33_ggg(x1, x2, x3, x4)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x1, x2, x4)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x2, x3)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x3, x5)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x3, x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
TIMES38_IN_GGA(x1, x2, x3)  =  TIMES38_IN_GGA(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:

TIMES38_IN_GGA(s(T72), T66, X148) → TIMES38_IN_GGA(T72, T66, X147)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
TIMES38_IN_GGA(x1, x2, x3)  =  TIMES38_IN_GGA(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:

TIMES38_IN_GGA(s(T72), T66) → TIMES38_IN_GGA(T72, T66)

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:

• TIMES38_IN_GGA(s(T72), T66) → TIMES38_IN_GGA(T72, T66)
  The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

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

CONVERT1_IN_GGA(.(0, T29), T16, T18) → CONVERT19_IN_GGA(T29, T16, X22)
CONVERT19_IN_GGA(.(0, T52), T41, X82) → CONVERT19_IN_GGA(T52, T41, X81)
CONVERT19_IN_GGA(.(s(T128), T129), T107, X251) → CONVERT1_IN_GGA(.(T128, T129), T107, X250)
CONVERT1_IN_GGA(.(s(T243), T244), T220, T222) → CONVERT1_IN_GGA(.(T243, T244), T220, X460)

The TRS R consists of the following rules:

convertc19_in_gga([], T35, 0) → convertc19_out_gga([], T35, 0)
convertc19_in_gga(.(0, T52), T41, X82) → U17_gga(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
convertc19_in_gga(.(s(T128), T129), T107, s(T142)) → U19_gga(T128, T129, T107, T142, convertc1_in_gga(.(T128, T129), T107, T142))
convertc1_in_gga([], T6, 0) → convertc1_out_gga([], T6, 0)
convertc1_in_gga(.(0, T29), T149, 0) → U23_gga(T29, T149, convertc19_in_ggg(T29, T149, 0))
convertc19_in_ggg([], T35, 0) → convertc19_out_ggg([], T35, 0)
convertc19_in_ggg(.(0, T52), T41, X82) → U17_ggg(T52, T41, X82, convertc19_in_gga(T52, T41, T54))
U17_ggg(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_ggg(T52, T41, X82, timesc38_in_ggg(T54, T41, X82))
timesc38_in_ggg(0, T59, 0) → timesc38_out_ggg(0, T59, 0)
timesc38_in_ggg(s(T72), T66, X148) → U20_ggg(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
timesc38_in_gga(0, T59, 0) → timesc38_out_gga(0, T59, 0)
timesc38_in_gga(s(T72), T66, X148) → U20_gga(T72, T66, X148, timesc38_in_gga(T72, T66, T74))
U20_gga(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_gga(T72, T66, X148, plusc53_in_gga(T66, T74, X148))
plusc53_in_gga(0, T82, T82) → plusc53_out_gga(0, T82, T82)
plusc53_in_gga(s(T93), T89, s(T100)) → U22_gga(T93, T89, T100, plusc53_in_gga(T93, T89, T100))
U22_gga(T93, T89, T100, plusc53_out_gga(T93, T89, T100)) → plusc53_out_gga(s(T93), T89, s(T100))
U21_gga(T72, T66, X148, plusc53_out_gga(T66, T74, X148)) → timesc38_out_gga(s(T72), T66, X148)
U20_ggg(T72, T66, X148, timesc38_out_gga(T72, T66, T74)) → U21_ggg(T72, T66, X148, plusc53_in_ggg(T66, T74, X148))
plusc53_in_ggg(0, T82, T82) → plusc53_out_ggg(0, T82, T82)
plusc53_in_ggg(s(T93), T89, s(T100)) → U22_ggg(T93, T89, T100, plusc53_in_ggg(T93, T89, T100))
U22_ggg(T93, T89, T100, plusc53_out_ggg(T93, T89, T100)) → plusc53_out_ggg(s(T93), T89, s(T100))
U21_ggg(T72, T66, X148, plusc53_out_ggg(T66, T74, X148)) → timesc38_out_ggg(s(T72), T66, X148)
U18_ggg(T52, T41, X82, timesc38_out_ggg(T54, T41, X82)) → convertc19_out_ggg(.(0, T52), T41, X82)
convertc19_in_ggg(.(s(T128), T129), T107, s(T142)) → U19_ggg(T128, T129, T107, T142, convertc1_in_ggg(.(T128, T129), T107, T142))
convertc1_in_ggg([], T6, 0) → convertc1_out_ggg([], T6, 0)
convertc1_in_ggg(.(0, T29), T149, 0) → U23_ggg(T29, T149, convertc19_in_ggg(T29, T149, 0))
U23_ggg(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_ggg(.(0, T29), T149, 0)
convertc1_in_ggg(.(0, T29), 0, T187) → U24_ggg(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_ggg(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_ggg(T29, T187, timesc38_in_ggg(T172, 0, T187))
U25_ggg(T29, T187, timesc38_out_ggg(T172, 0, T187)) → convertc1_out_ggg(.(0, T29), 0, T187)
convertc1_in_ggg(.(0, T29), s(T203), s(T210)) → U26_ggg(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_ggg(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_ggg(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_ggg(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_ggg(T29, T203, T210, plusc53_in_ggg(T203, T197, T210))
U28_ggg(T29, T203, T210, plusc53_out_ggg(T203, T197, T210)) → convertc1_out_ggg(.(0, T29), s(T203), s(T210))
convertc1_in_ggg(.(0, T29), s(T203), 0) → U29_ggg(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_ggg(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_ggg(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_ggg(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_ggg(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_ggg(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_ggg(.(0, T29), s(T203), 0)
convertc1_in_ggg(.(s(T243), T244), T220, s(T257)) → U32_ggg(T243, T244, T220, T257, convertc1_in_ggg(.(T243, T244), T220, T257))
convertc1_in_ggg(.(s(T243), T244), T220, 0) → U33_ggg(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_ggg(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_ggg(.(s(T243), T244), T220, 0)
U32_ggg(T243, T244, T220, T257, convertc1_out_ggg(.(T243, T244), T220, T257)) → convertc1_out_ggg(.(s(T243), T244), T220, s(T257))
U19_ggg(T128, T129, T107, T142, convertc1_out_ggg(.(T128, T129), T107, T142)) → convertc19_out_ggg(.(s(T128), T129), T107, s(T142))
U23_gga(T29, T149, convertc19_out_ggg(T29, T149, 0)) → convertc1_out_gga(.(0, T29), T149, 0)
convertc1_in_gga(.(0, T29), 0, T187) → U24_gga(T29, T187, convertc19_in_gga(T29, 0, s(T172)))
U24_gga(T29, T187, convertc19_out_gga(T29, 0, s(T172))) → U25_gga(T29, T187, timesc38_in_gga(T172, 0, T187))
U25_gga(T29, T187, timesc38_out_gga(T172, 0, T187)) → convertc1_out_gga(.(0, T29), 0, T187)
convertc1_in_gga(.(0, T29), s(T203), s(T210)) → U26_gga(T29, T203, T210, convertc19_in_gga(T29, s(T203), s(T172)))
U26_gga(T29, T203, T210, convertc19_out_gga(T29, s(T203), s(T172))) → U27_gga(T29, T203, T210, timesc38_in_gga(T172, s(T203), T197))
U27_gga(T29, T203, T210, timesc38_out_gga(T172, s(T203), T197)) → U28_gga(T29, T203, T210, plusc53_in_gga(T203, T197, T210))
U28_gga(T29, T203, T210, plusc53_out_gga(T203, T197, T210)) → convertc1_out_gga(.(0, T29), s(T203), s(T210))
convertc1_in_gga(.(0, T29), s(T203), 0) → U29_gga(T29, T203, convertc19_in_gga(T29, s(T203), s(T172)))
U29_gga(T29, T203, convertc19_out_gga(T29, s(T203), s(T172))) → U30_gga(T29, T203, timesc38_in_gga(T172, s(T203), T197))
U30_gga(T29, T203, timesc38_out_gga(T172, s(T203), T197)) → U31_gga(T29, T203, plusc53_in_ggg(T203, T197, 0))
U31_gga(T29, T203, plusc53_out_ggg(T203, T197, 0)) → convertc1_out_gga(.(0, T29), s(T203), 0)
convertc1_in_gga(.(s(T243), T244), T220, s(T257)) → U32_gga(T243, T244, T220, T257, convertc1_in_gga(.(T243, T244), T220, T257))
convertc1_in_gga(.(s(T243), T244), T220, 0) → U33_gga(T243, T244, T220, convertc1_in_ggg(.(T243, T244), T220, 0))
U33_gga(T243, T244, T220, convertc1_out_ggg(.(T243, T244), T220, 0)) → convertc1_out_gga(.(s(T243), T244), T220, 0)
U32_gga(T243, T244, T220, T257, convertc1_out_gga(.(T243, T244), T220, T257)) → convertc1_out_gga(.(s(T243), T244), T220, s(T257))
U19_gga(T128, T129, T107, T142, convertc1_out_gga(.(T128, T129), T107, T142)) → convertc19_out_gga(.(s(T128), T129), T107, s(T142))
U17_gga(T52, T41, X82, convertc19_out_gga(T52, T41, T54)) → U18_gga(T52, T41, X82, timesc38_in_gga(T54, T41, X82))
U18_gga(T52, T41, X82, timesc38_out_gga(T54, T41, X82)) → convertc19_out_gga(.(0, T52), T41, X82)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
0  =  0
convertc19_in_gga(x1, x2, x3)  =  convertc19_in_gga(x1, x2)
[]  =  []
convertc19_out_gga(x1, x2, x3)  =  convertc19_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
s(x1)  =  s(x1)
U19_gga(x1, x2, x3, x4, x5)  =  U19_gga(x1, x2, x3, x5)
convertc1_in_gga(x1, x2, x3)  =  convertc1_in_gga(x1, x2)
convertc1_out_gga(x1, x2, x3)  =  convertc1_out_gga(x1, x2, x3)
U23_gga(x1, x2, x3)  =  U23_gga(x1, x2, x3)
convertc19_in_ggg(x1, x2, x3)  =  convertc19_in_ggg(x1, x2, x3)
convertc19_out_ggg(x1, x2, x3)  =  convertc19_out_ggg(x1, x2, x3)
U17_ggg(x1, x2, x3, x4)  =  U17_ggg(x1, x2, x3, x4)
U18_ggg(x1, x2, x3, x4)  =  U18_ggg(x1, x2, x3, x4)
timesc38_in_ggg(x1, x2, x3)  =  timesc38_in_ggg(x1, x2, x3)
timesc38_out_ggg(x1, x2, x3)  =  timesc38_out_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
timesc38_in_gga(x1, x2, x3)  =  timesc38_in_gga(x1, x2)
timesc38_out_gga(x1, x2, x3)  =  timesc38_out_gga(x1, x2, x3)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x1, x2, x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x1, x2, x4)
plusc53_in_gga(x1, x2, x3)  =  plusc53_in_gga(x1, x2)
plusc53_out_gga(x1, x2, x3)  =  plusc53_out_gga(x1, x2, x3)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
plusc53_in_ggg(x1, x2, x3)  =  plusc53_in_ggg(x1, x2, x3)
plusc53_out_ggg(x1, x2, x3)  =  plusc53_out_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U19_ggg(x1, x2, x3, x4, x5)  =  U19_ggg(x1, x2, x3, x4, x5)
convertc1_in_ggg(x1, x2, x3)  =  convertc1_in_ggg(x1, x2, x3)
convertc1_out_ggg(x1, x2, x3)  =  convertc1_out_ggg(x1, x2, x3)
U23_ggg(x1, x2, x3)  =  U23_ggg(x1, x2, x3)
U24_ggg(x1, x2, x3)  =  U24_ggg(x1, x2, x3)
U25_ggg(x1, x2, x3)  =  U25_ggg(x1, x2, x3)
U26_ggg(x1, x2, x3, x4)  =  U26_ggg(x1, x2, x3, x4)
U27_ggg(x1, x2, x3, x4)  =  U27_ggg(x1, x2, x3, x4)
U28_ggg(x1, x2, x3, x4)  =  U28_ggg(x1, x2, x3, x4)
U29_ggg(x1, x2, x3)  =  U29_ggg(x1, x2, x3)
U30_ggg(x1, x2, x3)  =  U30_ggg(x1, x2, x3)
U31_ggg(x1, x2, x3)  =  U31_ggg(x1, x2, x3)
U32_ggg(x1, x2, x3, x4, x5)  =  U32_ggg(x1, x2, x3, x4, x5)
U33_ggg(x1, x2, x3, x4)  =  U33_ggg(x1, x2, x3, x4)
U24_gga(x1, x2, x3)  =  U24_gga(x1, x3)
U25_gga(x1, x2, x3)  =  U25_gga(x1, x3)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x1, x2, x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x1, x2, x4)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x2, x3)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x3, x5)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x3, x4)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x1, x2, x4)
CONVERT1_IN_GGA(x1, x2, x3)  =  CONVERT1_IN_GGA(x1, x2)
CONVERT19_IN_GGA(x1, x2, x3)  =  CONVERT19_IN_GGA(x1, x2)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

CONVERT1_IN_GGA(.(0, T29), T16, T18) → CONVERT19_IN_GGA(T29, T16, X22)
CONVERT19_IN_GGA(.(0, T52), T41, X82) → CONVERT19_IN_GGA(T52, T41, X81)
CONVERT19_IN_GGA(.(s(T128), T129), T107, X251) → CONVERT1_IN_GGA(.(T128, T129), T107, X250)
CONVERT1_IN_GGA(.(s(T243), T244), T220, T222) → CONVERT1_IN_GGA(.(T243, T244), T220, X460)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

CONVERT1_IN_GGA(.(0, T29), T16) → CONVERT19_IN_GGA(T29, T16)
CONVERT19_IN_GGA(.(0, T52), T41) → CONVERT19_IN_GGA(T52, T41)
CONVERT19_IN_GGA(.(s(T128), T129), T107) → CONVERT1_IN_GGA(.(T128, T129), T107)
CONVERT1_IN_GGA(.(s(T243), T244), T220) → CONVERT1_IN_GGA(.(T243, T244), T220)

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

(26) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

CONVERT1_IN_GGA(.(0, T29), T16) → CONVERT19_IN_GGA(T29, T16)
CONVERT19_IN_GGA(.(0, T52), T41) → CONVERT19_IN_GGA(T52, T41)
CONVERT19_IN_GGA(.(s(T128), T129), T107) → CONVERT1_IN_GGA(.(T128, T129), T107)
CONVERT1_IN_GGA(.(s(T243), T244), T220) → CONVERT1_IN_GGA(.(T243, T244), T220)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₁ + 2·x₂   
POL(0) = 0   
POL(CONVERT19_IN_GGA(x₁, x₂)) = 2 + 2·x₁ + x₂   
POL(CONVERT1_IN_GGA(x₁, x₂)) = 2 + x₁ + x₂   
POL(s(x₁)) = 2 + 2·x₁   

(27) Obligation:

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

(28) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(29) YES