Left Termination of the query pattern
convert(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).

Query: convert(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: convert(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: 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];
7 [label="7: ','(!_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];
10 [label="10: convert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | convert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX7 is free\nX8 is free\nconvert(T1, T2, T3) !=? convert([], X7, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: eq(T8, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: eq(T8, 0), SCOPE: 2, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(head(T15, 0), ','(!_1, ','(tail(T15, X18), ','(convert(X18, T16, X19), times(X19, T16, T18))))) | convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX7 is free\nX8 is free\nX18 is free\nX19 is free\nconvert(T15, T16, T3) !=? convert([], X7, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(head(T15, 0), ','(!_1, ','(tail(T15, X18), ','(convert(X18, T16, X19), times(X19, T16, T18))))), SCOPE: 3, CLAUSE: 7 | ','(head(T15, 0), ','(!_1, ','(tail(T15, X18), ','(convert(X18, T16, X19), times(X19, T16, T18))))), SCOPE: 3, CLAUSE: 8 | ?_3 | convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX7 is free\nX8 is free\nX18 is free\nX19 is free\nconvert(T15, T16, T3) !=? convert([], X7, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(head(T15, 0), ','(!_1, ','(tail(T15, X18), ','(convert(X18, T16, X19), times(X19, T16, T18))))), SCOPE: 3, CLAUSE: 8 | ?_3 | convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX7 is free\nX8 is free\nX18 is free\nX19 is free\nconvert(T15, T16, T3) !=? convert([], X7, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(!_1, ','(tail(.(0, T24), X18), ','(convert(X18, T16, X19), times(X19, T16, T18)))) | ?_3 | convert(.(0, T24), T16, T3), SCOPE: 1, CLAUSE: 2\n\nT16 is ground\nT24 is ground\nX18 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ?_3 | convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX7 is free\nX8 is free\nX25 is free\nX26 is free\nconvert(T15, T16, T3) !=? convert([], X7, X8)\nhead(T15, 0) !=? head(.(X25, X26), X25)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(tail(.(0, T24), X18), ','(convert(X18, T16, X19), times(X19, T16, T18)))\n\nT16 is ground\nT24 is ground\nX18 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(tail(.(0, T24), X18), ','(convert(X18, T16, X19), times(X19, T16, T18))), SCOPE: 4, CLAUSE: 9 | ','(tail(.(0, T24), X18), ','(convert(X18, T16, X19), times(X19, T16, T18))), SCOPE: 4, CLAUSE: 10\n\nT16 is ground\nT24 is ground\nX18 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(tail(.(0, T24), X18), ','(convert(X18, T16, X19), times(X19, T16, T18))), SCOPE: 4, CLAUSE: 10\n\nT16 is ground\nT24 is ground\nX18 is free\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="B: ','(convert(T29, T16, X19), times(X19, T16, T18))\n\nT16 is ground\nT29 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="D: convert(T29, T16, X19)\n\nT16 is ground\nT29 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="K: times(T31, T16, T18)\n\nT16 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: convert(T29, T16, X19), SCOPE: 5, CLAUSE: 0 | convert(T29, T16, X19), SCOPE: 5, CLAUSE: 1 | convert(T29, T16, X19), SCOPE: 5, CLAUSE: 2\n\nT16 is ground\nT29 is ground\nX19 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(!_5, eq(X53, 0)) | convert([], T35, X19), SCOPE: 5, CLAUSE: 1 | convert([], T35, X19), SCOPE: 5, CLAUSE: 2\n\nT35 is ground\nX19 is free\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: convert(T29, T16, X19), SCOPE: 5, CLAUSE: 1 | convert(T29, T16, X19), SCOPE: 5, CLAUSE: 2\n\nT16 is ground\nT29 is ground\nX19 is free\nX51 is free\nX52 is free\nconvert(T29, T16, X19) !=? convert([], X51, X52)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: eq(X53, 0)\n\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: eq(X53, 0), SCOPE: 6, CLAUSE: 13\n\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(head(T40, 0), ','(!_5, ','(tail(T40, X73), ','(convert(X73, T41, X74), times(X74, T41, X75))))) | convert(T40, T41, X19), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX19 is free\nX51 is free\nX52 is free\nX75 is free\nX73 is free\nX74 is free\nconvert(T40, T41, X19) !=? convert([], X51, X52)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(head(T40, 0), ','(!_5, ','(tail(T40, X73), ','(convert(X73, T41, X74), times(X74, T41, X75))))), SCOPE: 7, CLAUSE: 7 | ','(head(T40, 0), ','(!_5, ','(tail(T40, X73), ','(convert(X73, T41, X74), times(X74, T41, X75))))), SCOPE: 7, CLAUSE: 8 | ?_7 | convert(T40, T41, X19), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX19 is free\nX51 is free\nX52 is free\nX75 is free\nX73 is free\nX74 is free\nconvert(T40, T41, X19) !=? convert([], X51, X52)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(head(T40, 0), ','(!_5, ','(tail(T40, X73), ','(convert(X73, T41, X74), times(X74, T41, X75))))), SCOPE: 7, CLAUSE: 8 | ?_7 | convert(T40, T41, X19), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX19 is free\nX51 is free\nX52 is free\nX75 is free\nX73 is free\nX74 is free\nconvert(T40, T41, X19) !=? convert([], X51, X52)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(!_5, ','(tail(.(0, T47), X73), ','(convert(X73, T41, X74), times(X74, T41, X75)))) | ?_7 | convert(.(0, T47), T41, X19), SCOPE: 5, CLAUSE: 2\n\nT41 is ground\nT47 is ground\nX19 is free\nX75 is free\nX73 is free\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ?_7 | convert(T40, T41, X19), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX19 is free\nX51 is free\nX52 is free\nX81 is free\nX82 is free\nconvert(T40, T41, X19) !=? convert([], X51, X52)\nhead(T40, 0) !=? head(.(X81, X82), X81)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(tail(.(0, T47), X73), ','(convert(X73, T41, X74), times(X74, T41, X75)))\n\nT41 is ground\nT47 is ground\nX75 is free\nX73 is free\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(tail(.(0, T47), X73), ','(convert(X73, T41, X74), times(X74, T41, X75))), SCOPE: 8, CLAUSE: 9 | ','(tail(.(0, T47), X73), ','(convert(X73, T41, X74), times(X74, T41, X75))), SCOPE: 8, CLAUSE: 10\n\nT41 is ground\nT47 is ground\nX75 is free\nX73 is free\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(tail(.(0, T47), X73), ','(convert(X73, T41, X74), times(X74, T41, X75))), SCOPE: 8, CLAUSE: 10\n\nT41 is ground\nT47 is ground\nX75 is free\nX73 is free\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="E: ','(convert(T52, T41, X74), times(X74, T41, X75))\n\nT41 is ground\nT52 is ground\nX75 is free\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: convert(T52, T41, X74)\n\nT41 is ground\nT52 is ground\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="G: times(T54, T41, X75)\n\nT41 is ground\nT54 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: times(T54, T41, X75), SCOPE: 9, CLAUSE: 3 | times(T54, T41, X75), SCOPE: 9, CLAUSE: 4\n\nT41 is ground\nT54 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(!_9, eq(X112, 0)) | times(0, T59, X75), SCOPE: 9, CLAUSE: 4\n\nT59 is ground\nX75 is free\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: times(T54, T41, X75), SCOPE: 9, CLAUSE: 4\n\nT41 is ground\nT54 is ground\nX75 is free\nX110 is free\nX111 is free\ntimes(T54, T41, X75) !=? times(0, X110, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: eq(X112, 0)\n\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: eq(X112, 0), SCOPE: 10, CLAUSE: 13\n\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(p(T65, X135), ','(times(X135, T66, X136), plus(T66, X136, X137)))\n\nT65 is ground\nT66 is ground\nX75 is free\nX110 is free\nX111 is free\nX137 is free\nX135 is free\nX136 is free\ntimes(T65, T66, X75) !=? times(0, X110, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(p(T65, X135), ','(times(X135, T66, X136), plus(T66, X136, X137))), SCOPE: 11, CLAUSE: 11 | ','(p(T65, X135), ','(times(X135, T66, X136), plus(T66, X136, X137))), SCOPE: 11, CLAUSE: 12\n\nT65 is ground\nT66 is ground\nX75 is free\nX110 is free\nX111 is free\nX137 is free\nX135 is free\nX136 is free\ntimes(T65, T66, X75) !=? times(0, X110, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(p(T65, X135), ','(times(X135, T66, X136), plus(T66, X136, X137))), SCOPE: 11, CLAUSE: 11\n\nT65 is ground\nT66 is ground\nX75 is free\nX110 is free\nX111 is free\nX137 is free\nX135 is free\nX136 is free\ntimes(T65, T66, X75) !=? times(0, X110, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(p(T65, X135), ','(times(X135, T66, X136), plus(T66, X136, X137))), SCOPE: 11, CLAUSE: 12\n\nT65 is ground\nT66 is ground\nX75 is free\nX110 is free\nX111 is free\nX137 is free\nX135 is free\nX136 is free\ntimes(T65, T66, X75) !=? times(0, X110, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="H: ','(times(T72, T66, X136), plus(T66, X136, X137))\n\nT66 is ground\nT72 is ground\nX137 is free\nX136 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: times(T72, T66, X136)\n\nT66 is ground\nT72 is ground\nX136 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="I: plus(T66, T74, X137)\n\nT66 is ground\nT74 is ground\nX137 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: plus(T66, T74, X137), SCOPE: 12, CLAUSE: 5 | plus(T66, T74, X137), SCOPE: 12, CLAUSE: 6\n\nT66 is ground\nT74 is ground\nX137 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(!_12, eq(T79, X163)) | plus(0, T79, X137), SCOPE: 12, CLAUSE: 6\n\nT79 is ground\nX137 is free\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: plus(T66, T74, X137), SCOPE: 12, CLAUSE: 6\n\nT66 is ground\nT74 is ground\nX137 is free\nX161 is free\nX162 is free\nplus(T66, T74, X137) !=? plus(0, X161, X162)", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: eq(T79, X163)\n\nT79 is ground\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: eq(T79, X163), SCOPE: 13, CLAUSE: 13\n\nT79 is ground\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(p(T88, X183), ','(plus(X183, T89, X184), ','(p(X185, X184), !_12)))\n\nT88 is ground\nT89 is ground\nX137 is free\nX161 is free\nX162 is free\nX185 is free\nX183 is free\nX184 is free\nplus(T88, T89, X137) !=? plus(0, X161, X162)", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(p(T88, X183), ','(plus(X183, T89, X184), ','(p(X185, X184), !_12))), SCOPE: 14, CLAUSE: 11 | ','(p(T88, X183), ','(plus(X183, T89, X184), ','(p(X185, X184), !_12))), SCOPE: 14, CLAUSE: 12\n\nT88 is ground\nT89 is ground\nX137 is free\nX161 is free\nX162 is free\nX185 is free\nX183 is free\nX184 is free\nplus(T88, T89, X137) !=? plus(0, X161, X162)", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(plus(T93, T89, X184), ','(p(X185, X184), !_12)) | ','(p(s(T93), X183), ','(plus(X183, T89, X184), ','(p(X185, X184), !_12))), SCOPE: 14, CLAUSE: 12\n\nT89 is ground\nT93 is ground\nX185 is free\nX183 is free\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: ','(p(T88, X183), ','(plus(X183, T89, X184), ','(p(X185, X184), !_12))), SCOPE: 14, CLAUSE: 12\n\nT88 is ground\nT89 is ground\nX137 is free\nX161 is free\nX162 is free\nX185 is free\nX183 is free\nX184 is free\nX191 is free\nplus(T88, T89, X137) !=? plus(0, X161, X162)\np(T88, X183) !=? p(s(X191), X191)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="J: ','(plus(T93, T89, X184), ','(p(X185, X184), !_12))\n\nT89 is ground\nT93 is ground\nX185 is free\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(p(s(T93), X183), ','(plus(X183, T89, X184), ','(p(X185, X184), !_12))), SCOPE: 14, CLAUSE: 12\n\nT89 is ground\nT93 is ground\nX185 is free\nX183 is free\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: plus(T93, T89, X184)\n\nT89 is ground\nT93 is ground\nX184 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="M: ','(p(X185, T96), !_12)\n\nT96 is ground\nX185 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(p(X185, T96), !_12), SCOPE: 15, CLAUSE: 11 | ','(p(X185, T96), !_12), SCOPE: 15, CLAUSE: 12\n\nT96 is ground\nX185 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: !_12 | ','(p(X185, T100), !_12), SCOPE: 15, CLAUSE: 12\n\nT100 is ground\nX185 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: convert(T40, T41, X19), SCOPE: 5, CLAUSE: 2\n\nT40 is ground\nT41 is ground\nX19 is free\nX51 is free\nX52 is free\nX81 is free\nX82 is free\nconvert(T40, T41, X19) !=? convert([], X51, X52)\nhead(T40, 0) !=? head(.(X81, X82), X81)", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(head(T105, X224), ','(p(X224, X225), ','(tail(T105, X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))))\n\nT105 is ground\nT106 is ground\nX19 is free\nX51 is free\nX52 is free\nX81 is free\nX82 is free\nX228 is free\nX224 is free\nX225 is free\nX226 is free\nX227 is free\nconvert(T105, T106, X19) !=? convert([], X51, X52)\nhead(T105, 0) !=? head(.(X81, X82), X81)", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(head(T105, X224), ','(p(X224, X225), ','(tail(T105, X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5))))), SCOPE: 16, CLAUSE: 7 | ','(head(T105, X224), ','(p(X224, X225), ','(tail(T105, X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5))))), SCOPE: 16, CLAUSE: 8\n\nT105 is ground\nT106 is ground\nX19 is free\nX51 is free\nX52 is free\nX81 is free\nX82 is free\nX228 is free\nX224 is free\nX225 is free\nX226 is free\nX227 is free\nconvert(T105, T106, X19) !=? convert([], X51, X52)\nhead(T105, 0) !=? head(.(X81, X82), X81)", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(head(T105, X224), ','(p(X224, X225), ','(tail(T105, X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5))))), SCOPE: 16, CLAUSE: 8\n\nT105 is ground\nT106 is ground\nX19 is free\nX51 is free\nX52 is free\nX81 is free\nX82 is free\nX228 is free\nX224 is free\nX225 is free\nX226 is free\nX227 is free\nconvert(T105, T106, X19) !=? convert([], X51, X52)\nhead(T105, 0) !=? head(.(X81, X82), X81)", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(p(T111, X225), ','(tail(.(T111, T112), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5))))\n\nT106 is ground\nT111 is ground\nT112 is ground\nX81 is free\nX82 is free\nX228 is free\nX225 is free\nX226 is free\nX227 is free\nhead(.(T111, T112), 0) !=? head(.(X81, X82), X81)", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(p(T111, X225), ','(tail(.(T111, T112), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 11 | ','(p(T111, X225), ','(tail(.(T111, T112), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT106 is ground\nT111 is ground\nT112 is ground\nX81 is free\nX82 is free\nX228 is free\nX225 is free\nX226 is free\nX227 is free\nhead(.(T111, T112), 0) !=? head(.(X81, X82), X81)", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(tail(.(s(T115), T112), X226), ','(convert(.(T115, X226), T106, X227), ','(p(X228, X227), !_5))) | ','(p(s(T115), X225), ','(tail(.(s(T115), T112), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT106 is ground\nT112 is ground\nT115 is ground\nX228 is free\nX225 is free\nX226 is free\nX227 is free", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(p(T111, X225), ','(tail(.(T111, T112), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT106 is ground\nT111 is ground\nT112 is ground\nX81 is free\nX82 is free\nX228 is free\nX225 is free\nX226 is free\nX227 is free\nX243 is free\nhead(.(T111, T112), 0) !=? head(.(X81, X82), X81)\np(T111, X225) !=? p(s(X243), X243)", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(tail(.(s(T115), T112), X226), ','(convert(.(T115, X226), T106, X227), ','(p(X228, X227), !_5))), SCOPE: 18, CLAUSE: 9 | ','(tail(.(s(T115), T112), X226), ','(convert(.(T115, X226), T106, X227), ','(p(X228, X227), !_5))), SCOPE: 18, CLAUSE: 10 | ?_18 | ','(p(s(T115), X225), ','(tail(.(s(T115), T112), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT106 is ground\nT112 is ground\nT115 is ground\nX228 is free\nX225 is free\nX226 is free\nX227 is free", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ','(tail(.(s(T115), T112), X226), ','(convert(.(T115, X226), T106, X227), ','(p(X228, X227), !_5))), SCOPE: 18, CLAUSE: 10 | ?_18 | ','(p(s(T115), X225), ','(tail(.(s(T115), T112), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT106 is ground\nT112 is ground\nT115 is ground\nX228 is free\nX225 is free\nX226 is free\nX227 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(convert(.(T120, T121), T106, X227), ','(p(X228, X227), !_5)) | ?_18 | ','(p(s(T120), X225), ','(tail(.(s(T120), T121), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT106 is ground\nT120 is ground\nT121 is ground\nX228 is free\nX225 is free\nX226 is free\nX227 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="F: ','(convert(.(T120, T121), T106, X227), ','(p(X228, X227), !_5))\n\nT106 is ground\nT120 is ground\nT121 is ground\nX228 is free\nX227 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ?_18 | ','(p(s(T120), X225), ','(tail(.(s(T120), T121), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT106 is ground\nT120 is ground\nT121 is ground\nX228 is free\nX225 is free\nX226 is free\nX227 is free", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: convert(.(T120, T121), T106, X227)\n\nT106 is ground\nT120 is ground\nT121 is ground\nX227 is free", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="N: ','(p(X228, T122), !_5)\n\nT122 is ground\nX228 is free", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(p(X228, T122), !_5), SCOPE: 19, CLAUSE: 11 | ','(p(X228, T122), !_5), SCOPE: 19, CLAUSE: 12\n\nT122 is ground\nX228 is free", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: !_5 | ','(p(X228, T125), !_5), SCOPE: 19, CLAUSE: 12\n\nT125 is ground\nX228 is free", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(p(s(T120), X225), ','(tail(.(s(T120), T121), X226), ','(convert(.(X225, X226), T106, X227), ','(p(X228, X227), !_5)))), SCOPE: 17, CLAUSE: 12\n\nT106 is ground\nT120 is ground\nT121 is ground\nX228 is free\nX225 is free\nX226 is free\nX227 is free", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: 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];
239 [label="239: ','(!_20, eq(T134, 0)) | times(0, T132, T18), SCOPE: 20, CLAUSE: 4\n\nT132 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: times(T31, T16, T18), SCOPE: 20, CLAUSE: 4\n\nT16 is ground\nT31 is ground\nX272 is free\nX273 is free\ntimes(T31, T16, T18) !=? times(0, X272, X273)", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: eq(T134, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: eq(T134, 0), SCOPE: 21, CLAUSE: 13\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: ','(p(T146, X291), ','(times(X291, T147, X292), plus(T147, X292, T149)))\n\nT146 is ground\nT147 is ground\nX272 is free\nX273 is free\nX291 is free\nX292 is free\ntimes(T146, T147, T18) !=? times(0, X272, X273)", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: ','(p(T146, X291), ','(times(X291, T147, X292), plus(T147, X292, T149))), SCOPE: 22, CLAUSE: 11 | ','(p(T146, X291), ','(times(X291, T147, X292), plus(T147, X292, T149))), SCOPE: 22, CLAUSE: 12\n\nT146 is ground\nT147 is ground\nX272 is free\nX273 is free\nX291 is free\nX292 is free\ntimes(T146, T147, T18) !=? times(0, X272, X273)", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: ','(p(T146, X291), ','(times(X291, T147, X292), plus(T147, X292, T149))), SCOPE: 22, CLAUSE: 11\n\nT146 is ground\nT147 is ground\nX272 is free\nX273 is free\nX291 is free\nX292 is free\ntimes(T146, T147, T18) !=? times(0, X272, X273)", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: ','(p(T146, X291), ','(times(X291, T147, X292), plus(T147, X292, T149))), SCOPE: 22, CLAUSE: 12\n\nT146 is ground\nT147 is ground\nX272 is free\nX273 is free\nX291 is free\nX292 is free\ntimes(T146, T147, T18) !=? times(0, X272, X273)", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="L: ','(times(T155, T147, X292), plus(T147, X292, T149))\n\nT147 is ground\nT155 is ground\nX292 is free", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: times(T155, T147, X292)\n\nT147 is ground\nT155 is ground\nX292 is free", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="O: plus(T147, T157, T149)\n\nT147 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: plus(T147, T157, T149), SCOPE: 23, CLAUSE: 5 | plus(T147, T157, T149), SCOPE: 23, CLAUSE: 6\n\nT147 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: ','(!_23, eq(T165, T167)) | plus(0, T165, T149), SCOPE: 23, CLAUSE: 6\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: plus(T147, T157, T149), SCOPE: 23, CLAUSE: 6\n\nT147 is ground\nT157 is ground\nX313 is free\nX314 is free\nplus(T147, T157, T149) !=? plus(0, X313, X314)", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: eq(T165, T167)\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: eq(T165, T167), SCOPE: 24, CLAUSE: 13\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
309 [label="309: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: ','(p(T179, X332), ','(plus(X332, T180, X333), ','(p(T182, X333), !_23)))\n\nT179 is ground\nT180 is ground\nX313 is free\nX314 is free\nX332 is free\nX333 is free\nplus(T179, T180, T149) !=? plus(0, X313, X314)", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: ','(p(T179, X332), ','(plus(X332, T180, X333), ','(p(T182, X333), !_23))), SCOPE: 25, CLAUSE: 11 | ','(p(T179, X332), ','(plus(X332, T180, X333), ','(p(T182, X333), !_23))), SCOPE: 25, CLAUSE: 12\n\nT179 is ground\nT180 is ground\nX313 is free\nX314 is free\nX332 is free\nX333 is free\nplus(T179, T180, T149) !=? plus(0, X313, X314)", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: ','(plus(T186, T180, X333), ','(p(T182, X333), !_23)) | ','(p(s(T186), X332), ','(plus(X332, T180, X333), ','(p(T182, X333), !_23))), SCOPE: 25, CLAUSE: 12\n\nT180 is ground\nT186 is ground\nX332 is free\nX333 is free", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: ','(p(T179, X332), ','(plus(X332, T180, X333), ','(p(T182, X333), !_23))), SCOPE: 25, CLAUSE: 12\n\nT179 is ground\nT180 is ground\nX313 is free\nX314 is free\nX332 is free\nX333 is free\nX339 is free\nplus(T179, T180, T149) !=? plus(0, X313, X314)\np(T179, X332) !=? p(s(X339), X339)", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="P: ','(plus(T186, T180, X333), ','(p(T182, X333), !_23))\n\nT180 is ground\nT186 is ground\nX333 is free", fontsize=16, style=filled, fillcolor=lightyellow];
332 [label="332: ','(p(s(T186), X332), ','(plus(X332, T180, X333), ','(p(T182, X333), !_23))), SCOPE: 25, CLAUSE: 12\n\nT180 is ground\nT186 is ground\nX332 is free\nX333 is free", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: plus(T186, T180, X333)\n\nT180 is ground\nT186 is ground\nX333 is free", fontsize=16, style=filled, fillcolor=lightyellow];
350 [label="Q: ','(p(T182, T189), !_23)\n\nT189 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
351 [label="351: ','(p(T182, T189), !_23), SCOPE: 26, CLAUSE: 11 | ','(p(T182, T189), !_23), SCOPE: 26, CLAUSE: 12\n\nT189 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
355 [label="355: !_23 | ','(p(T182, T193), !_23), SCOPE: 26, CLAUSE: 12\n\nT193 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: ','(p(T182, T189), !_23), SCOPE: 26, CLAUSE: 12\n\nT189 is ground\nX351 is free\np(T182, T189) !=? p(s(X351), X351)", fontsize=16, style=filled, fillcolor=lightyellow];
357 [label="357: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
358 [label="358: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
359 [label="359: !_23\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
361 [label="361: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
363 [label="363: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
368 [label="368: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="373: convert(T15, T16, T3), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nT16 is ground\nX7 is free\nX8 is free\nX25 is free\nX26 is free\nconvert(T15, T16, T3) !=? convert([], X7, X8)\nhead(T15, 0) !=? head(.(X25, X26), X25)", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: ','(head(T201, X367), ','(p(X367, X368), ','(tail(T201, X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))))\n\nT201 is ground\nT202 is ground\nX7 is free\nX8 is free\nX25 is free\nX26 is free\nX367 is free\nX368 is free\nX369 is free\nX370 is free\nconvert(T201, T202, T3) !=? convert([], X7, X8)\nhead(T201, 0) !=? head(.(X25, X26), X25)", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: ','(head(T201, X367), ','(p(X367, X368), ','(tail(T201, X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1))))), SCOPE: 27, CLAUSE: 7 | ','(head(T201, X367), ','(p(X367, X368), ','(tail(T201, X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1))))), SCOPE: 27, CLAUSE: 8\n\nT201 is ground\nT202 is ground\nX7 is free\nX8 is free\nX25 is free\nX26 is free\nX367 is free\nX368 is free\nX369 is free\nX370 is free\nconvert(T201, T202, T3) !=? convert([], X7, X8)\nhead(T201, 0) !=? head(.(X25, X26), X25)", fontsize=16, style=filled, fillcolor=lightyellow];
384 [label="384: ','(head(T201, X367), ','(p(X367, X368), ','(tail(T201, X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1))))), SCOPE: 27, CLAUSE: 8\n\nT201 is ground\nT202 is ground\nX7 is free\nX8 is free\nX25 is free\nX26 is free\nX367 is free\nX368 is free\nX369 is free\nX370 is free\nconvert(T201, T202, T3) !=? convert([], X7, X8)\nhead(T201, 0) !=? head(.(X25, X26), X25)", fontsize=16, style=filled, fillcolor=lightyellow];
388 [label="388: ','(p(T209, X368), ','(tail(.(T209, T210), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1))))\n\nT202 is ground\nT209 is ground\nT210 is ground\nX25 is free\nX26 is free\nX368 is free\nX369 is free\nX370 is free\nhead(.(T209, T210), 0) !=? head(.(X25, X26), X25)", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
392 [label="392: ','(p(T209, X368), ','(tail(.(T209, T210), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 11 | ','(p(T209, X368), ','(tail(.(T209, T210), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT202 is ground\nT209 is ground\nT210 is ground\nX25 is free\nX26 is free\nX368 is free\nX369 is free\nX370 is free\nhead(.(T209, T210), 0) !=? head(.(X25, X26), X25)", fontsize=16, style=filled, fillcolor=lightyellow];
397 [label="397: ','(tail(.(s(T213), T210), X369), ','(convert(.(T213, X369), T202, X370), ','(p(T204, X370), !_1))) | ','(p(s(T213), X368), ','(tail(.(s(T213), T210), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT202 is ground\nT210 is ground\nT213 is ground\nX368 is free\nX369 is free\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
401 [label="401: ','(p(T209, X368), ','(tail(.(T209, T210), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT202 is ground\nT209 is ground\nT210 is ground\nX25 is free\nX26 is free\nX368 is free\nX369 is free\nX370 is free\nX385 is free\nhead(.(T209, T210), 0) !=? head(.(X25, X26), X25)\np(T209, X368) !=? p(s(X385), X385)", fontsize=16, style=filled, fillcolor=lightyellow];
402 [label="402: ','(tail(.(s(T213), T210), X369), ','(convert(.(T213, X369), T202, X370), ','(p(T204, X370), !_1))), SCOPE: 29, CLAUSE: 9 | ','(tail(.(s(T213), T210), X369), ','(convert(.(T213, X369), T202, X370), ','(p(T204, X370), !_1))), SCOPE: 29, CLAUSE: 10 | ?_29 | ','(p(s(T213), X368), ','(tail(.(s(T213), T210), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT202 is ground\nT210 is ground\nT213 is ground\nX368 is free\nX369 is free\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
403 [label="403: ','(tail(.(s(T213), T210), X369), ','(convert(.(T213, X369), T202, X370), ','(p(T204, X370), !_1))), SCOPE: 29, CLAUSE: 10 | ?_29 | ','(p(s(T213), X368), ','(tail(.(s(T213), T210), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT202 is ground\nT210 is ground\nT213 is ground\nX368 is free\nX369 is free\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
407 [label="407: ','(convert(.(T218, T219), T202, X370), ','(p(T204, X370), !_1)) | ?_29 | ','(p(s(T218), X368), ','(tail(.(s(T218), T219), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT202 is ground\nT218 is ground\nT219 is ground\nX368 is free\nX369 is free\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
409 [label="C: ','(convert(.(T218, T219), T202, X370), ','(p(T204, X370), !_1))\n\nT202 is ground\nT218 is ground\nT219 is ground\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
410 [label="410: ?_29 | ','(p(s(T218), X368), ','(tail(.(s(T218), T219), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT202 is ground\nT218 is ground\nT219 is ground\nX368 is free\nX369 is free\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
431 [label="431: convert(.(T218, T219), T202, X370)\n\nT202 is ground\nT218 is ground\nT219 is ground\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
432 [label="R: ','(p(T204, T220), !_1)\n\nT220 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
435 [label="435: ','(p(T204, T220), !_1), SCOPE: 30, CLAUSE: 11 | ','(p(T204, T220), !_1), SCOPE: 30, CLAUSE: 12\n\nT220 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
439 [label="439: !_1 | ','(p(T204, T223), !_1), SCOPE: 30, CLAUSE: 12\n\nT223 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
440 [label="440: ','(p(T204, T220), !_1), SCOPE: 30, CLAUSE: 12\n\nT220 is ground\nX404 is free\np(T204, T220) !=? p(s(X404), X404)", fontsize=16, style=filled, fillcolor=lightyellow];
442 [label="442: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
443 [label="443: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
448 [label="448: !_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
449 [label="449: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
450 [label="450: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
453 [label="453: ','(p(s(T218), X368), ','(tail(.(s(T218), T219), X369), ','(convert(.(X368, X369), T202, X370), ','(p(T204, X370), !_1)))), SCOPE: 28, CLAUSE: 12\n\nT202 is ground\nT218 is ground\nT219 is ground\nX368 is free\nX369 is free\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
454 [label="454: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
456 [label="456: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
457 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 457 [arrowhead = none ];
457 -> 5;

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

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

460 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 460 [arrowhead = none ];
460 -> 14;

461 [label="ONLY EVAL with clause\nconvert(X15, X16, X17) :- ','(head(X15, 0), ','(!_1, ','(tail(X15, X18), ','(convert(X18, X16, X19), times(X19, X16, X17))))).\nand substitutionT1 -> T15,\nX15 -> T15,\nT2 -> T16,\nX16 -> T16,\nT3 -> T18,\nX17 -> T18,\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 461 [arrowhead = none ];
461 -> 28;

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

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

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

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

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

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

468 [label="EVAL with clause\nhead(.(X25, X26), X25).\nand substitutionX25 -> 0,\nX26 -> T24,\nT15 -> .(0, T24),\nT23 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 468 [arrowhead = none ];
468 -> 37;

469 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 469 [arrowhead = none ];
469 -> 39;

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

471 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 471 [arrowhead = none ];
471 -> 373;

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

473 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 473 [arrowhead = none ];
473 -> 45;

474 [label="ONLY EVAL with clause\ntail(.(X37, X38), X38).\nand substitutionX37 -> 0,\nT24 -> T29,\nX38 -> T29,\nX18 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 474 [arrowhead = none ];
474 -> 50;

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

476 [label="SPLIT 2\nnew knowledge:\nT29 is ground\nT16 is ground\nT31 is ground\nreplacements:X19 -> T31", fontsize=14, style = filled, fillcolor = violet];
50 -> 476 [arrowhead = none ];
476 -> 56;

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

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

479 [label="EVAL with clause\nconvert([], X51, X52) :- ','(!_5, eq(X52, 0)).\nand substitutionT29 -> [],\nT16 -> T35,\nX51 -> T35,\nX19 -> X53,\nX52 -> X53", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 479 [arrowhead = none ];
479 -> 63;

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

481 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 481 [arrowhead = none ];
481 -> 66;

482 [label="ONLY EVAL with clause\nconvert(X70, X71, X72) :- ','(head(X70, 0), ','(!_5, ','(tail(X70, X73), ','(convert(X73, X71, X74), times(X74, X71, X72))))).\nand substitutionT29 -> T40,\nX70 -> T40,\nT16 -> T41,\nX71 -> T41,\nX19 -> X75,\nX72 -> X75", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 482 [arrowhead = none ];
482 -> 78;

483 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
66 -> 483 [arrowhead = none ];
483 -> 67;

484 [label="ONLY EVAL with clause\neq(X58, X58).\nand substitutionX53 -> 0,\nX58 -> 0,\nX59 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 484 [arrowhead = none ];
484 -> 70;

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

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

487 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (convert(T40, T41, X19), convert([], X51, X52))", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 487 [arrowhead = none ];
487 -> 80;

488 [label="EVAL with clause\nhead(.(X81, X82), X81).\nand substitutionX81 -> 0,\nX82 -> T47,\nT40 -> .(0, T47),\nT46 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 488 [arrowhead = none ];
488 -> 84;

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

490 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 490 [arrowhead = none ];
490 -> 90;

491 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 491 [arrowhead = none ];
491 -> 181;

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

493 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 493 [arrowhead = none ];
493 -> 92;

494 [label="ONLY EVAL with clause\ntail(.(X93, X94), X94).\nand substitutionX93 -> 0,\nT47 -> T52,\nX94 -> T52,\nX73 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 494 [arrowhead = none ];
494 -> 99;

495 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
99 -> 495 [arrowhead = none ];
495 -> 103;

496 [label="SPLIT 2\nnew knowledge:\nT52 is ground\nT41 is ground\nT54 is ground\nreplacements:X74 -> T54", fontsize=14, style = filled, fillcolor = violet];
99 -> 496 [arrowhead = none ];
496 -> 104;

497 [label="INSTANCE with matching:\nT29 -> T52\nT16 -> T41\nX19 -> X74", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 497 [arrowhead = none , style=dashed];
497 -> 55[style=dashed];

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

499 [label="EVAL with clause\ntimes(0, X110, X111) :- ','(!_9, eq(X111, 0)).\nand substitutionT54 -> 0,\nT41 -> T59,\nX110 -> T59,\nX75 -> X112,\nX111 -> X112", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 499 [arrowhead = none ];
499 -> 112;

500 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 500 [arrowhead = none ];
500 -> 113;

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

502 [label="ONLY EVAL with clause\ntimes(X132, X133, X134) :- ','(p(X132, X135), ','(times(X135, X133, X136), plus(X133, X136, X134))).\nand substitutionT54 -> T65,\nX132 -> T65,\nT41 -> T66,\nX133 -> T66,\nX75 -> X137,\nX134 -> X137", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 502 [arrowhead = none ];
502 -> 127;

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

504 [label="ONLY EVAL with clause\neq(X117, X117).\nand substitutionX112 -> 0,\nX117 -> 0,\nX118 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 504 [arrowhead = none ];
504 -> 122;

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

506 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
127 -> 506 [arrowhead = none ];
506 -> 129;

507 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
129 -> 507 [arrowhead = none ];
507 -> 131;

508 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
129 -> 508 [arrowhead = none ];
508 -> 132;

509 [label="EVAL with clause\np(s(X145), X145).\nand substitutionX145 -> T72,\nT65 -> s(T72),\nX135 -> T72", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 509 [arrowhead = none ];
509 -> 136;

510 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
131 -> 510 [arrowhead = none ];
510 -> 138;

511 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (times(T65, T66, X75), times(0, X110, X111))", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 511 [arrowhead = none ];
511 -> 180;

512 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
136 -> 512 [arrowhead = none ];
512 -> 140;

513 [label="SPLIT 2\nnew knowledge:\nT72 is ground\nT66 is ground\nT74 is ground\nreplacements:X136 -> T74", fontsize=14, style = filled, fillcolor = violet];
136 -> 513 [arrowhead = none ];
513 -> 141;

514 [label="INSTANCE with matching:\nT54 -> T72\nT41 -> T66\nX75 -> X136", fontsize=14, style = filled, fillcolor = lightgrey];
140 -> 514 [arrowhead = none , style=dashed];
514 -> 104[style=dashed];

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

516 [label="EVAL with clause\nplus(0, X161, X162) :- ','(!_12, eq(X161, X162)).\nand substitutionT66 -> 0,\nT74 -> T79,\nX161 -> T79,\nX137 -> X163,\nX162 -> X163", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 516 [arrowhead = none ];
516 -> 147;

517 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
145 -> 517 [arrowhead = none ];
517 -> 148;

518 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 518 [arrowhead = none ];
518 -> 149;

519 [label="ONLY EVAL with clause\nplus(X180, X181, X182) :- ','(p(X180, X183), ','(plus(X183, X181, X184), ','(p(X182, X184), !_12))).\nand substitutionT66 -> T88,\nX180 -> T88,\nT74 -> T89,\nX181 -> T89,\nX137 -> X185,\nX182 -> X185", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 519 [arrowhead = none ];
519 -> 159;

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

521 [label="ONLY EVAL with clause\neq(X166, X166).\nand substitutionT79 -> T82,\nX166 -> T82,\nX163 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 521 [arrowhead = none ];
521 -> 152;

522 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 522 [arrowhead = none ];
522 -> 153;

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

524 [label="EVAL with clause\np(s(X191), X191).\nand substitutionX191 -> T93,\nT88 -> s(T93),\nX183 -> T93", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 524 [arrowhead = none ];
524 -> 161;

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

526 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 526 [arrowhead = none ];
526 -> 163;

527 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 527 [arrowhead = none ];
527 -> 164;

528 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (plus(T88, T89, X137), plus(0, X161, X162))", fontsize=14, style = filled, fillcolor = lightgreen];
162 -> 528 [arrowhead = none ];
528 -> 179;

529 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
163 -> 529 [arrowhead = none ];
529 -> 166;

530 [label="SPLIT 2\nnew knowledge:\nT93 is ground\nT89 is ground\nT96 is ground\nreplacements:X184 -> T96", fontsize=14, style = filled, fillcolor = violet];
163 -> 530 [arrowhead = none ];
530 -> 167;

531 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
164 -> 531 [arrowhead = none ];
531 -> 178;

532 [label="INSTANCE with matching:\nT66 -> T93\nT74 -> T89\nX137 -> X184", fontsize=14, style = filled, fillcolor = lightgrey];
166 -> 532 [arrowhead = none , style=dashed];
532 -> 141[style=dashed];

533 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
167 -> 533 [arrowhead = none ];
533 -> 172;

534 [label="ONLY EVAL with clause\np(s(X205), X205).\nand substitutionX205 -> T100,\nX185 -> s(T100),\nT96 -> T100,\nX206 -> T100", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 534 [arrowhead = none ];
534 -> 175;

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

536 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 536 [arrowhead = none ];
536 -> 177;

537 [label="ONLY EVAL with clause\nconvert(X221, X222, X223) :- ','(head(X221, X224), ','(p(X224, X225), ','(tail(X221, X226), ','(convert(.(X225, X226), X222, X227), ','(p(X223, X227), !_5))))).\nand substitutionT40 -> T105,\nX221 -> T105,\nT41 -> T106,\nX222 -> T106,\nX19 -> X228,\nX223 -> X228", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 537 [arrowhead = none ];
537 -> 188;

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

539 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (convert(T105, T106, X19), convert([], X51, X52))", fontsize=14, style = filled, fillcolor = lightgreen];
189 -> 539 [arrowhead = none ];
539 -> 190;

540 [label="EVAL with clause\nhead(.(X237, X238), X237).\nand substitutionX237 -> T111,\nX238 -> T112,\nT105 -> .(T111, T112),\nX224 -> T111", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 540 [arrowhead = none ];
540 -> 192;

541 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
190 -> 541 [arrowhead = none ];
541 -> 194;

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

543 [label="EVAL with clause\np(s(X243), X243).\nand substitutionX243 -> T115,\nT111 -> s(T115),\nX225 -> T115", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 543 [arrowhead = none ];
543 -> 198;

544 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
195 -> 544 [arrowhead = none ];
544 -> 201;

545 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
198 -> 545 [arrowhead = none ];
545 -> 202;

546 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (head(.(T111, T112), 0), head(.(X81, X82), X81))", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 546 [arrowhead = none ];
546 -> 236;

547 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
202 -> 547 [arrowhead = none ];
547 -> 203;

548 [label="ONLY EVAL with clause\ntail(.(X252, X253), X253).\nand substitutionT115 -> T120,\nX252 -> s(T120),\nT112 -> T121,\nX253 -> T121,\nX226 -> T121", fontsize=14, style = filled, fillcolor = lightblue];
203 -> 548 [arrowhead = none ];
548 -> 206;

549 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
206 -> 549 [arrowhead = none ];
549 -> 207;

550 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
206 -> 550 [arrowhead = none ];
550 -> 209;

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

552 [label="SPLIT 2\nnew knowledge:\nT120 is ground\nT121 is ground\nT106 is ground\nT122 is ground\nreplacements:X227 -> T122", fontsize=14, style = filled, fillcolor = violet];
207 -> 552 [arrowhead = none ];
552 -> 219;

553 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 553 [arrowhead = none ];
553 -> 234;

554 [label="INSTANCE with matching:\nT1 -> .(T120, T121)\nT2 -> T106\nT3 -> X227", fontsize=14, style = filled, fillcolor = lightgrey];
218 -> 554 [arrowhead = none , style=dashed];
554 -> 3[style=dashed];

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

556 [label="ONLY EVAL with clause\np(s(X264), X264).\nand substitutionX264 -> T125,\nX228 -> s(T125),\nT122 -> T125,\nX265 -> T125", fontsize=14, style = filled, fillcolor = lightblue];
221 -> 556 [arrowhead = none ];
556 -> 231;

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

558 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
232 -> 558 [arrowhead = none ];
558 -> 233;

559 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
234 -> 559 [arrowhead = none ];
559 -> 235;

560 [label="EVAL with clause\ntimes(0, X272, X273) :- ','(!_20, eq(X273, 0)).\nand substitutionT31 -> 0,\nT16 -> T132,\nX272 -> T132,\nT18 -> T134,\nX273 -> T134,\nT133 -> T134", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 560 [arrowhead = none ];
560 -> 239;

561 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
237 -> 561 [arrowhead = none ];
561 -> 240;

562 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
239 -> 562 [arrowhead = none ];
562 -> 241;

563 [label="ONLY EVAL with clause\ntimes(X288, X289, X290) :- ','(p(X288, X291), ','(times(X291, X289, X292), plus(X289, X292, X290))).\nand substitutionT31 -> T146,\nX288 -> T146,\nT16 -> T147,\nX289 -> T147,\nT18 -> T149,\nX290 -> T149,\nT148 -> T149", fontsize=14, style = filled, fillcolor = lightblue];
240 -> 563 [arrowhead = none ];
563 -> 259;

564 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
241 -> 564 [arrowhead = none ];
564 -> 242;

565 [label="EVAL with clause\neq(X276, X276).\nand substitutionT134 -> 0,\nX276 -> 0,\nT137 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
242 -> 565 [arrowhead = none ];
565 -> 245;

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

567 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
245 -> 567 [arrowhead = none ];
567 -> 248;

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

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

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

571 [label="EVAL with clause\np(s(X300), X300).\nand substitutionX300 -> T155,\nT146 -> s(T155),\nX291 -> T155", fontsize=14, style = filled, fillcolor = lightblue];
267 -> 571 [arrowhead = none ];
571 -> 274;

572 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
267 -> 572 [arrowhead = none ];
572 -> 276;

573 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (times(T146, T147, T18), times(0, X272, X273))", fontsize=14, style = filled, fillcolor = lightgreen];
269 -> 573 [arrowhead = none ];
573 -> 370;

574 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
274 -> 574 [arrowhead = none ];
574 -> 281;

575 [label="SPLIT 2\nnew knowledge:\nT155 is ground\nT147 is ground\nT157 is ground\nreplacements:X292 -> T157", fontsize=14, style = filled, fillcolor = violet];
274 -> 575 [arrowhead = none ];
575 -> 282;

576 [label="INSTANCE with matching:\nT54 -> T155\nT41 -> T147\nX75 -> X292", fontsize=14, style = filled, fillcolor = lightgrey];
281 -> 576 [arrowhead = none , style=dashed];
576 -> 104[style=dashed];

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

578 [label="EVAL with clause\nplus(0, X313, X314) :- ','(!_23, eq(X313, X314)).\nand substitutionT147 -> 0,\nT157 -> T165,\nX313 -> T165,\nT149 -> T167,\nX314 -> T167,\nT166 -> T167", fontsize=14, style = filled, fillcolor = lightblue];
295 -> 578 [arrowhead = none ];
578 -> 301;

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

580 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
301 -> 580 [arrowhead = none ];
580 -> 303;

581 [label="ONLY EVAL with clause\nplus(X329, X330, X331) :- ','(p(X329, X332), ','(plus(X332, X330, X333), ','(p(X331, X333), !_23))).\nand substitutionT147 -> T179,\nX329 -> T179,\nT157 -> T180,\nX330 -> T180,\nT149 -> T182,\nX331 -> T182,\nT181 -> T182", fontsize=14, style = filled, fillcolor = lightblue];
302 -> 581 [arrowhead = none ];
581 -> 318;

582 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
303 -> 582 [arrowhead = none ];
582 -> 304;

583 [label="EVAL with clause\neq(X317, X317).\nand substitutionT165 -> T170,\nX317 -> T170,\nT167 -> T170", fontsize=14, style = filled, fillcolor = lightblue];
304 -> 583 [arrowhead = none ];
583 -> 306;

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

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

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

587 [label="EVAL with clause\np(s(X339), X339).\nand substitutionX339 -> T186,\nT179 -> s(T186),\nX332 -> T186", fontsize=14, style = filled, fillcolor = lightblue];
320 -> 587 [arrowhead = none ];
587 -> 322;

588 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
320 -> 588 [arrowhead = none ];
588 -> 326;

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

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

591 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (plus(T179, T180, T149), plus(0, X313, X314))", fontsize=14, style = filled, fillcolor = lightgreen];
326 -> 591 [arrowhead = none ];
591 -> 368;

592 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
331 -> 592 [arrowhead = none ];
592 -> 349;

593 [label="SPLIT 2\nnew knowledge:\nT186 is ground\nT180 is ground\nT189 is ground\nreplacements:X333 -> T189", fontsize=14, style = filled, fillcolor = violet];
331 -> 593 [arrowhead = none ];
593 -> 350;

594 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
332 -> 594 [arrowhead = none ];
594 -> 366;

595 [label="INSTANCE with matching:\nT66 -> T186\nT74 -> T180\nX137 -> X333", fontsize=14, style = filled, fillcolor = lightgrey];
349 -> 595 [arrowhead = none , style=dashed];
595 -> 141[style=dashed];

596 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
350 -> 596 [arrowhead = none ];
596 -> 351;

597 [label="EVAL with clause\np(s(X351), X351).\nand substitutionX351 -> T193,\nT182 -> s(T193),\nT189 -> T193", fontsize=14, style = filled, fillcolor = lightblue];
351 -> 597 [arrowhead = none ];
597 -> 355;

598 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
351 -> 598 [arrowhead = none ];
598 -> 356;

599 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
355 -> 599 [arrowhead = none ];
599 -> 357;

600 [label="EVAL with clause\np(0, 0).\nand substitutionT182 -> 0,\nT189 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
356 -> 600 [arrowhead = none ];
600 -> 359;

601 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
356 -> 601 [arrowhead = none ];
601 -> 361;

602 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
357 -> 602 [arrowhead = none ];
602 -> 358;

603 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
359 -> 603 [arrowhead = none ];
603 -> 363;

604 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
363 -> 604 [arrowhead = none ];
604 -> 365;

605 [label="ONLY EVAL with clause\nconvert(X364, X365, X366) :- ','(head(X364, X367), ','(p(X367, X368), ','(tail(X364, X369), ','(convert(.(X368, X369), X365, X370), ','(p(X366, X370), !_1))))).\nand substitutionT15 -> T201,\nX364 -> T201,\nT16 -> T202,\nX365 -> T202,\nT3 -> T204,\nX366 -> T204,\nT203 -> T204", fontsize=14, style = filled, fillcolor = lightblue];
373 -> 605 [arrowhead = none ];
605 -> 379;

606 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
379 -> 606 [arrowhead = none ];
606 -> 382;

607 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (convert(T201, T202, T3), convert([], X7, X8))", fontsize=14, style = filled, fillcolor = lightgreen];
382 -> 607 [arrowhead = none ];
607 -> 384;

608 [label="EVAL with clause\nhead(.(X379, X380), X379).\nand substitutionX379 -> T209,\nX380 -> T210,\nT201 -> .(T209, T210),\nX367 -> T209", fontsize=14, style = filled, fillcolor = lightblue];
384 -> 608 [arrowhead = none ];
608 -> 388;

609 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
384 -> 609 [arrowhead = none ];
609 -> 389;

610 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
388 -> 610 [arrowhead = none ];
610 -> 392;

611 [label="EVAL with clause\np(s(X385), X385).\nand substitutionX385 -> T213,\nT209 -> s(T213),\nX368 -> T213", fontsize=14, style = filled, fillcolor = lightblue];
392 -> 611 [arrowhead = none ];
611 -> 397;

612 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
392 -> 612 [arrowhead = none ];
612 -> 401;

613 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
397 -> 613 [arrowhead = none ];
613 -> 402;

614 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (head(.(T209, T210), 0), head(.(X25, X26), X25))", fontsize=14, style = filled, fillcolor = lightgreen];
401 -> 614 [arrowhead = none ];
614 -> 456;

615 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
402 -> 615 [arrowhead = none ];
615 -> 403;

616 [label="ONLY EVAL with clause\ntail(.(X394, X395), X395).\nand substitutionT213 -> T218,\nX394 -> s(T218),\nT210 -> T219,\nX395 -> T219,\nX369 -> T219", fontsize=14, style = filled, fillcolor = lightblue];
403 -> 616 [arrowhead = none ];
616 -> 407;

617 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
407 -> 617 [arrowhead = none ];
617 -> 409;

618 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
407 -> 618 [arrowhead = none ];
618 -> 410;

619 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
409 -> 619 [arrowhead = none ];
619 -> 431;

620 [label="SPLIT 2\nnew knowledge:\nT218 is ground\nT219 is ground\nT202 is ground\nT220 is ground\nreplacements:X370 -> T220", fontsize=14, style = filled, fillcolor = violet];
409 -> 620 [arrowhead = none ];
620 -> 432;

621 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
410 -> 621 [arrowhead = none ];
621 -> 453;

622 [label="INSTANCE with matching:\nT1 -> .(T218, T219)\nT2 -> T202\nT3 -> X370", fontsize=14, style = filled, fillcolor = lightgrey];
431 -> 622 [arrowhead = none , style=dashed];
622 -> 3[style=dashed];

623 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
432 -> 623 [arrowhead = none ];
623 -> 435;

624 [label="EVAL with clause\np(s(X404), X404).\nand substitutionX404 -> T223,\nT204 -> s(T223),\nT220 -> T223", fontsize=14, style = filled, fillcolor = lightblue];
435 -> 624 [arrowhead = none ];
624 -> 439;

625 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
435 -> 625 [arrowhead = none ];
625 -> 440;

626 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
439 -> 626 [arrowhead = none ];
626 -> 442;

627 [label="EVAL with clause\np(0, 0).\nand substitutionT204 -> 0,\nT220 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
440 -> 627 [arrowhead = none ];
627 -> 448;

628 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
440 -> 628 [arrowhead = none ];
628 -> 449;

629 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
442 -> 629 [arrowhead = none ];
629 -> 443;

630 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
448 -> 630 [arrowhead = none ];
630 -> 450;

631 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
450 -> 631 [arrowhead = none ];
631 -> 451;

632 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
453 -> 632 [arrowhead = none ];
632 -> 454;

}

(2) Obligation:

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

convertA_in_gga([], T6, 0) → convertA_out_gga([], T6, 0)
convertA_in_gga(.(0, T29), T16, T18) → U1_gga(T29, T16, T18, pB_in_ggaa(T29, T16, X19, T18))
pB_in_ggaa(T29, T16, T31, T18) → U9_ggaa(T29, T16, T31, T18, convertD_in_gga(T29, T16, T31))
convertD_in_gga([], T35, 0) → convertD_out_gga([], T35, 0)
convertD_in_gga(.(0, T52), T41, X75) → U3_gga(T52, T41, X75, pE_in_ggaa(T52, T41, X74, X75))
pE_in_ggaa(T52, T41, T54, X75) → U11_ggaa(T52, T41, T54, X75, convertD_in_gga(T52, T41, T54))
convertD_in_gga(.(s(T120), T121), T106, X228) → U4_gga(T120, T121, T106, X228, pF_in_gggaa(T120, T121, T106, X227, X228))
pF_in_gggaa(T120, T121, T106, T122, X228) → U17_gggaa(T120, T121, T106, T122, X228, convertA_in_gga(.(T120, T121), T106, T122))
convertA_in_gga(.(s(T218), T219), T202, T204) → U2_gga(T218, T219, T202, T204, pC_in_gggaa(T218, T219, T202, X370, T204))
pC_in_gggaa(T218, T219, T202, T220, T204) → U23_gggaa(T218, T219, T202, T220, T204, convertA_in_gga(.(T218, T219), T202, T220))
U23_gggaa(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → U24_gggaa(T218, T219, T202, T220, T204, pR_in_ag(T204, T220))
pR_in_ag(s(T223), T223) → pR_out_ag(s(T223), T223)
pR_in_ag(0, 0) → pR_out_ag(0, 0)
U24_gggaa(T218, T219, T202, T220, T204, pR_out_ag(T204, T220)) → pC_out_gggaa(T218, T219, T202, T220, T204)
U2_gga(T218, T219, T202, T204, pC_out_gggaa(T218, T219, T202, X370, T204)) → convertA_out_gga(.(s(T218), T219), T202, T204)
U17_gggaa(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → U18_gggaa(T120, T121, T106, T122, X228, pN_in_ag(X228, T122))
pN_in_ag(s(T125), T125) → pN_out_ag(s(T125), T125)
U18_gggaa(T120, T121, T106, T122, X228, pN_out_ag(X228, T122)) → pF_out_gggaa(T120, T121, T106, T122, X228)
U4_gga(T120, T121, T106, X228, pF_out_gggaa(T120, T121, T106, X227, X228)) → convertD_out_gga(.(s(T120), T121), T106, X228)
U11_ggaa(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → U12_ggaa(T52, T41, T54, X75, timesG_in_gga(T54, T41, X75))
timesG_in_gga(0, T59, 0) → timesG_out_gga(0, T59, 0)
timesG_in_gga(s(T72), T66, X137) → U5_gga(T72, T66, X137, pH_in_ggaa(T72, T66, X136, X137))
pH_in_ggaa(T72, T66, T74, X137) → U13_ggaa(T72, T66, T74, X137, timesG_in_gga(T72, T66, T74))
U13_ggaa(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → U14_ggaa(T72, T66, T74, X137, plusI_in_gga(T66, T74, X137))
plusI_in_gga(0, T82, T82) → plusI_out_gga(0, T82, T82)
plusI_in_gga(s(T93), T89, X185) → U6_gga(T93, T89, X185, pJ_in_ggaa(T93, T89, X184, X185))
pJ_in_ggaa(T93, T89, T96, X185) → U15_ggaa(T93, T89, T96, X185, plusI_in_gga(T93, T89, T96))
U15_ggaa(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → U16_ggaa(T93, T89, T96, X185, pM_in_ag(X185, T96))
pM_in_ag(s(T100), T100) → pM_out_ag(s(T100), T100)
U16_ggaa(T93, T89, T96, X185, pM_out_ag(X185, T96)) → pJ_out_ggaa(T93, T89, T96, X185)
U6_gga(T93, T89, X185, pJ_out_ggaa(T93, T89, X184, X185)) → plusI_out_gga(s(T93), T89, X185)
U14_ggaa(T72, T66, T74, X137, plusI_out_gga(T66, T74, X137)) → pH_out_ggaa(T72, T66, T74, X137)
U5_gga(T72, T66, X137, pH_out_ggaa(T72, T66, X136, X137)) → timesG_out_gga(s(T72), T66, X137)
U12_ggaa(T52, T41, T54, X75, timesG_out_gga(T54, T41, X75)) → pE_out_ggaa(T52, T41, T54, X75)
U3_gga(T52, T41, X75, pE_out_ggaa(T52, T41, X74, X75)) → convertD_out_gga(.(0, T52), T41, X75)
U9_ggaa(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → U10_ggaa(T29, T16, T31, T18, timesK_in_gga(T31, T16, T18))
timesK_in_gga(0, T132, 0) → timesK_out_gga(0, T132, 0)
timesK_in_gga(s(T155), T147, T149) → U7_gga(T155, T147, T149, pL_in_ggaa(T155, T147, X292, T149))
pL_in_ggaa(T155, T147, T157, T149) → U19_ggaa(T155, T147, T157, T149, timesG_in_gga(T155, T147, T157))
U19_ggaa(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → U20_ggaa(T155, T147, T157, T149, plusO_in_gga(T147, T157, T149))
plusO_in_gga(0, T170, T170) → plusO_out_gga(0, T170, T170)
plusO_in_gga(s(T186), T180, T182) → U8_gga(T186, T180, T182, pP_in_ggaa(T186, T180, X333, T182))
pP_in_ggaa(T186, T180, T189, T182) → U21_ggaa(T186, T180, T189, T182, plusI_in_gga(T186, T180, T189))
U21_ggaa(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → U22_ggaa(T186, T180, T189, T182, pQ_in_ag(T182, T189))
pQ_in_ag(s(T193), T193) → pQ_out_ag(s(T193), T193)
pQ_in_ag(0, 0) → pQ_out_ag(0, 0)
U22_ggaa(T186, T180, T189, T182, pQ_out_ag(T182, T189)) → pP_out_ggaa(T186, T180, T189, T182)
U8_gga(T186, T180, T182, pP_out_ggaa(T186, T180, X333, T182)) → plusO_out_gga(s(T186), T180, T182)
U20_ggaa(T155, T147, T157, T149, plusO_out_gga(T147, T157, T149)) → pL_out_ggaa(T155, T147, T157, T149)
U7_gga(T155, T147, T149, pL_out_ggaa(T155, T147, X292, T149)) → timesK_out_gga(s(T155), T147, T149)
U10_ggaa(T29, T16, T31, T18, timesK_out_gga(T31, T16, T18)) → pB_out_ggaa(T29, T16, T31, T18)
U1_gga(T29, T16, T18, pB_out_ggaa(T29, T16, X19, T18)) → convertA_out_gga(.(0, T29), T16, T18)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
convertD_in_gga(x1, x2, x3)  =  convertD_in_gga(x1, x2)
convertD_out_gga(x1, x2, x3)  =  convertD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pF_in_gggaa(x1, x2, x3, x4, x5)  =  pF_in_gggaa(x1, x2, x3)
U17_gggaa(x1, x2, x3, x4, x5, x6)  =  U17_gggaa(x1, x2, x3, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U23_gggaa(x1, x2, x3, x4, x5, x6)  =  U23_gggaa(x1, x2, x3, x6)
U24_gggaa(x1, x2, x3, x4, x5, x6)  =  U24_gggaa(x1, x2, x3, x4, x6)
pR_in_ag(x1, x2)  =  pR_in_ag(x2)
pR_out_ag(x1, x2)  =  pR_out_ag(x1, x2)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U18_gggaa(x1, x2, x3, x4, x5, x6)  =  U18_gggaa(x1, x2, x3, x4, x6)
pN_in_ag(x1, x2)  =  pN_in_ag(x2)
pN_out_ag(x1, x2)  =  pN_out_ag(x1, x2)
pF_out_gggaa(x1, x2, x3, x4, x5)  =  pF_out_gggaa(x1, x2, x3, x4, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pM_in_ag(x1, x2)  =  pM_in_ag(x2)
pM_out_ag(x1, x2)  =  pM_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusO_in_gga(x1, x2, x3)  =  plusO_in_gga(x1, x2)
plusO_out_gga(x1, x2, x3)  =  plusO_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pP_in_ggaa(x1, x2, x3, x4)  =  pP_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
pQ_in_ag(x1, x2)  =  pQ_in_ag(x2)
pQ_out_ag(x1, x2)  =  pQ_out_ag(x1, x2)
pP_out_ggaa(x1, x2, x3, x4)  =  pP_out_ggaa(x1, x2, x3, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

CONVERTA_IN_GGA(.(0, T29), T16, T18) → U1_GGA(T29, T16, T18, pB_in_ggaa(T29, T16, X19, T18))
CONVERTA_IN_GGA(.(0, T29), T16, T18) → PB_IN_GGAA(T29, T16, X19, T18)
PB_IN_GGAA(T29, T16, T31, T18) → U9_GGAA(T29, T16, T31, T18, convertD_in_gga(T29, T16, T31))
PB_IN_GGAA(T29, T16, T31, T18) → CONVERTD_IN_GGA(T29, T16, T31)
CONVERTD_IN_GGA(.(0, T52), T41, X75) → U3_GGA(T52, T41, X75, pE_in_ggaa(T52, T41, X74, X75))
CONVERTD_IN_GGA(.(0, T52), T41, X75) → PE_IN_GGAA(T52, T41, X74, X75)
PE_IN_GGAA(T52, T41, T54, X75) → U11_GGAA(T52, T41, T54, X75, convertD_in_gga(T52, T41, T54))
PE_IN_GGAA(T52, T41, T54, X75) → CONVERTD_IN_GGA(T52, T41, T54)
CONVERTD_IN_GGA(.(s(T120), T121), T106, X228) → U4_GGA(T120, T121, T106, X228, pF_in_gggaa(T120, T121, T106, X227, X228))
CONVERTD_IN_GGA(.(s(T120), T121), T106, X228) → PF_IN_GGGAA(T120, T121, T106, X227, X228)
PF_IN_GGGAA(T120, T121, T106, T122, X228) → U17_GGGAA(T120, T121, T106, T122, X228, convertA_in_gga(.(T120, T121), T106, T122))
PF_IN_GGGAA(T120, T121, T106, T122, X228) → CONVERTA_IN_GGA(.(T120, T121), T106, T122)
CONVERTA_IN_GGA(.(s(T218), T219), T202, T204) → U2_GGA(T218, T219, T202, T204, pC_in_gggaa(T218, T219, T202, X370, T204))
CONVERTA_IN_GGA(.(s(T218), T219), T202, T204) → PC_IN_GGGAA(T218, T219, T202, X370, T204)
PC_IN_GGGAA(T218, T219, T202, T220, T204) → U23_GGGAA(T218, T219, T202, T220, T204, convertA_in_gga(.(T218, T219), T202, T220))
PC_IN_GGGAA(T218, T219, T202, T220, T204) → CONVERTA_IN_GGA(.(T218, T219), T202, T220)
U23_GGGAA(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → U24_GGGAA(T218, T219, T202, T220, T204, pR_in_ag(T204, T220))
U23_GGGAA(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → PR_IN_AG(T204, T220)
U17_GGGAA(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → U18_GGGAA(T120, T121, T106, T122, X228, pN_in_ag(X228, T122))
U17_GGGAA(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → PN_IN_AG(X228, T122)
U11_GGAA(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → U12_GGAA(T52, T41, T54, X75, timesG_in_gga(T54, T41, X75))
U11_GGAA(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → TIMESG_IN_GGA(T54, T41, X75)
TIMESG_IN_GGA(s(T72), T66, X137) → U5_GGA(T72, T66, X137, pH_in_ggaa(T72, T66, X136, X137))
TIMESG_IN_GGA(s(T72), T66, X137) → PH_IN_GGAA(T72, T66, X136, X137)
PH_IN_GGAA(T72, T66, T74, X137) → U13_GGAA(T72, T66, T74, X137, timesG_in_gga(T72, T66, T74))
PH_IN_GGAA(T72, T66, T74, X137) → TIMESG_IN_GGA(T72, T66, T74)
U13_GGAA(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → U14_GGAA(T72, T66, T74, X137, plusI_in_gga(T66, T74, X137))
U13_GGAA(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → PLUSI_IN_GGA(T66, T74, X137)
PLUSI_IN_GGA(s(T93), T89, X185) → U6_GGA(T93, T89, X185, pJ_in_ggaa(T93, T89, X184, X185))
PLUSI_IN_GGA(s(T93), T89, X185) → PJ_IN_GGAA(T93, T89, X184, X185)
PJ_IN_GGAA(T93, T89, T96, X185) → U15_GGAA(T93, T89, T96, X185, plusI_in_gga(T93, T89, T96))
PJ_IN_GGAA(T93, T89, T96, X185) → PLUSI_IN_GGA(T93, T89, T96)
U15_GGAA(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → U16_GGAA(T93, T89, T96, X185, pM_in_ag(X185, T96))
U15_GGAA(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → PM_IN_AG(X185, T96)
U9_GGAA(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → U10_GGAA(T29, T16, T31, T18, timesK_in_gga(T31, T16, T18))
U9_GGAA(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → TIMESK_IN_GGA(T31, T16, T18)
TIMESK_IN_GGA(s(T155), T147, T149) → U7_GGA(T155, T147, T149, pL_in_ggaa(T155, T147, X292, T149))
TIMESK_IN_GGA(s(T155), T147, T149) → PL_IN_GGAA(T155, T147, X292, T149)
PL_IN_GGAA(T155, T147, T157, T149) → U19_GGAA(T155, T147, T157, T149, timesG_in_gga(T155, T147, T157))
PL_IN_GGAA(T155, T147, T157, T149) → TIMESG_IN_GGA(T155, T147, T157)
U19_GGAA(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → U20_GGAA(T155, T147, T157, T149, plusO_in_gga(T147, T157, T149))
U19_GGAA(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → PLUSO_IN_GGA(T147, T157, T149)
PLUSO_IN_GGA(s(T186), T180, T182) → U8_GGA(T186, T180, T182, pP_in_ggaa(T186, T180, X333, T182))
PLUSO_IN_GGA(s(T186), T180, T182) → PP_IN_GGAA(T186, T180, X333, T182)
PP_IN_GGAA(T186, T180, T189, T182) → U21_GGAA(T186, T180, T189, T182, plusI_in_gga(T186, T180, T189))
PP_IN_GGAA(T186, T180, T189, T182) → PLUSI_IN_GGA(T186, T180, T189)
U21_GGAA(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → U22_GGAA(T186, T180, T189, T182, pQ_in_ag(T182, T189))
U21_GGAA(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → PQ_IN_AG(T182, T189)

The TRS R consists of the following rules:

convertA_in_gga([], T6, 0) → convertA_out_gga([], T6, 0)
convertA_in_gga(.(0, T29), T16, T18) → U1_gga(T29, T16, T18, pB_in_ggaa(T29, T16, X19, T18))
pB_in_ggaa(T29, T16, T31, T18) → U9_ggaa(T29, T16, T31, T18, convertD_in_gga(T29, T16, T31))
convertD_in_gga([], T35, 0) → convertD_out_gga([], T35, 0)
convertD_in_gga(.(0, T52), T41, X75) → U3_gga(T52, T41, X75, pE_in_ggaa(T52, T41, X74, X75))
pE_in_ggaa(T52, T41, T54, X75) → U11_ggaa(T52, T41, T54, X75, convertD_in_gga(T52, T41, T54))
convertD_in_gga(.(s(T120), T121), T106, X228) → U4_gga(T120, T121, T106, X228, pF_in_gggaa(T120, T121, T106, X227, X228))
pF_in_gggaa(T120, T121, T106, T122, X228) → U17_gggaa(T120, T121, T106, T122, X228, convertA_in_gga(.(T120, T121), T106, T122))
convertA_in_gga(.(s(T218), T219), T202, T204) → U2_gga(T218, T219, T202, T204, pC_in_gggaa(T218, T219, T202, X370, T204))
pC_in_gggaa(T218, T219, T202, T220, T204) → U23_gggaa(T218, T219, T202, T220, T204, convertA_in_gga(.(T218, T219), T202, T220))
U23_gggaa(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → U24_gggaa(T218, T219, T202, T220, T204, pR_in_ag(T204, T220))
pR_in_ag(s(T223), T223) → pR_out_ag(s(T223), T223)
pR_in_ag(0, 0) → pR_out_ag(0, 0)
U24_gggaa(T218, T219, T202, T220, T204, pR_out_ag(T204, T220)) → pC_out_gggaa(T218, T219, T202, T220, T204)
U2_gga(T218, T219, T202, T204, pC_out_gggaa(T218, T219, T202, X370, T204)) → convertA_out_gga(.(s(T218), T219), T202, T204)
U17_gggaa(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → U18_gggaa(T120, T121, T106, T122, X228, pN_in_ag(X228, T122))
pN_in_ag(s(T125), T125) → pN_out_ag(s(T125), T125)
U18_gggaa(T120, T121, T106, T122, X228, pN_out_ag(X228, T122)) → pF_out_gggaa(T120, T121, T106, T122, X228)
U4_gga(T120, T121, T106, X228, pF_out_gggaa(T120, T121, T106, X227, X228)) → convertD_out_gga(.(s(T120), T121), T106, X228)
U11_ggaa(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → U12_ggaa(T52, T41, T54, X75, timesG_in_gga(T54, T41, X75))
timesG_in_gga(0, T59, 0) → timesG_out_gga(0, T59, 0)
timesG_in_gga(s(T72), T66, X137) → U5_gga(T72, T66, X137, pH_in_ggaa(T72, T66, X136, X137))
pH_in_ggaa(T72, T66, T74, X137) → U13_ggaa(T72, T66, T74, X137, timesG_in_gga(T72, T66, T74))
U13_ggaa(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → U14_ggaa(T72, T66, T74, X137, plusI_in_gga(T66, T74, X137))
plusI_in_gga(0, T82, T82) → plusI_out_gga(0, T82, T82)
plusI_in_gga(s(T93), T89, X185) → U6_gga(T93, T89, X185, pJ_in_ggaa(T93, T89, X184, X185))
pJ_in_ggaa(T93, T89, T96, X185) → U15_ggaa(T93, T89, T96, X185, plusI_in_gga(T93, T89, T96))
U15_ggaa(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → U16_ggaa(T93, T89, T96, X185, pM_in_ag(X185, T96))
pM_in_ag(s(T100), T100) → pM_out_ag(s(T100), T100)
U16_ggaa(T93, T89, T96, X185, pM_out_ag(X185, T96)) → pJ_out_ggaa(T93, T89, T96, X185)
U6_gga(T93, T89, X185, pJ_out_ggaa(T93, T89, X184, X185)) → plusI_out_gga(s(T93), T89, X185)
U14_ggaa(T72, T66, T74, X137, plusI_out_gga(T66, T74, X137)) → pH_out_ggaa(T72, T66, T74, X137)
U5_gga(T72, T66, X137, pH_out_ggaa(T72, T66, X136, X137)) → timesG_out_gga(s(T72), T66, X137)
U12_ggaa(T52, T41, T54, X75, timesG_out_gga(T54, T41, X75)) → pE_out_ggaa(T52, T41, T54, X75)
U3_gga(T52, T41, X75, pE_out_ggaa(T52, T41, X74, X75)) → convertD_out_gga(.(0, T52), T41, X75)
U9_ggaa(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → U10_ggaa(T29, T16, T31, T18, timesK_in_gga(T31, T16, T18))
timesK_in_gga(0, T132, 0) → timesK_out_gga(0, T132, 0)
timesK_in_gga(s(T155), T147, T149) → U7_gga(T155, T147, T149, pL_in_ggaa(T155, T147, X292, T149))
pL_in_ggaa(T155, T147, T157, T149) → U19_ggaa(T155, T147, T157, T149, timesG_in_gga(T155, T147, T157))
U19_ggaa(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → U20_ggaa(T155, T147, T157, T149, plusO_in_gga(T147, T157, T149))
plusO_in_gga(0, T170, T170) → plusO_out_gga(0, T170, T170)
plusO_in_gga(s(T186), T180, T182) → U8_gga(T186, T180, T182, pP_in_ggaa(T186, T180, X333, T182))
pP_in_ggaa(T186, T180, T189, T182) → U21_ggaa(T186, T180, T189, T182, plusI_in_gga(T186, T180, T189))
U21_ggaa(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → U22_ggaa(T186, T180, T189, T182, pQ_in_ag(T182, T189))
pQ_in_ag(s(T193), T193) → pQ_out_ag(s(T193), T193)
pQ_in_ag(0, 0) → pQ_out_ag(0, 0)
U22_ggaa(T186, T180, T189, T182, pQ_out_ag(T182, T189)) → pP_out_ggaa(T186, T180, T189, T182)
U8_gga(T186, T180, T182, pP_out_ggaa(T186, T180, X333, T182)) → plusO_out_gga(s(T186), T180, T182)
U20_ggaa(T155, T147, T157, T149, plusO_out_gga(T147, T157, T149)) → pL_out_ggaa(T155, T147, T157, T149)
U7_gga(T155, T147, T149, pL_out_ggaa(T155, T147, X292, T149)) → timesK_out_gga(s(T155), T147, T149)
U10_ggaa(T29, T16, T31, T18, timesK_out_gga(T31, T16, T18)) → pB_out_ggaa(T29, T16, T31, T18)
U1_gga(T29, T16, T18, pB_out_ggaa(T29, T16, X19, T18)) → convertA_out_gga(.(0, T29), T16, T18)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
convertD_in_gga(x1, x2, x3)  =  convertD_in_gga(x1, x2)
convertD_out_gga(x1, x2, x3)  =  convertD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pF_in_gggaa(x1, x2, x3, x4, x5)  =  pF_in_gggaa(x1, x2, x3)
U17_gggaa(x1, x2, x3, x4, x5, x6)  =  U17_gggaa(x1, x2, x3, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U23_gggaa(x1, x2, x3, x4, x5, x6)  =  U23_gggaa(x1, x2, x3, x6)
U24_gggaa(x1, x2, x3, x4, x5, x6)  =  U24_gggaa(x1, x2, x3, x4, x6)
pR_in_ag(x1, x2)  =  pR_in_ag(x2)
pR_out_ag(x1, x2)  =  pR_out_ag(x1, x2)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U18_gggaa(x1, x2, x3, x4, x5, x6)  =  U18_gggaa(x1, x2, x3, x4, x6)
pN_in_ag(x1, x2)  =  pN_in_ag(x2)
pN_out_ag(x1, x2)  =  pN_out_ag(x1, x2)
pF_out_gggaa(x1, x2, x3, x4, x5)  =  pF_out_gggaa(x1, x2, x3, x4, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pM_in_ag(x1, x2)  =  pM_in_ag(x2)
pM_out_ag(x1, x2)  =  pM_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusO_in_gga(x1, x2, x3)  =  plusO_in_gga(x1, x2)
plusO_out_gga(x1, x2, x3)  =  plusO_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pP_in_ggaa(x1, x2, x3, x4)  =  pP_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
pQ_in_ag(x1, x2)  =  pQ_in_ag(x2)
pQ_out_ag(x1, x2)  =  pQ_out_ag(x1, x2)
pP_out_ggaa(x1, x2, x3, x4)  =  pP_out_ggaa(x1, x2, x3, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
CONVERTA_IN_GGA(x1, x2, x3)  =  CONVERTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4, x5)  =  U9_GGAA(x1, x2, x5)
CONVERTD_IN_GGA(x1, x2, x3)  =  CONVERTD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PE_IN_GGAA(x1, x2, x3, x4)  =  PE_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)
PF_IN_GGGAA(x1, x2, x3, x4, x5)  =  PF_IN_GGGAA(x1, x2, x3)
U17_GGGAA(x1, x2, x3, x4, x5, x6)  =  U17_GGGAA(x1, x2, x3, x6)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
PC_IN_GGGAA(x1, x2, x3, x4, x5)  =  PC_IN_GGGAA(x1, x2, x3)
U23_GGGAA(x1, x2, x3, x4, x5, x6)  =  U23_GGGAA(x1, x2, x3, x6)
U24_GGGAA(x1, x2, x3, x4, x5, x6)  =  U24_GGGAA(x1, x2, x3, x4, x6)
PR_IN_AG(x1, x2)  =  PR_IN_AG(x2)
U18_GGGAA(x1, x2, x3, x4, x5, x6)  =  U18_GGGAA(x1, x2, x3, x4, x6)
PN_IN_AG(x1, x2)  =  PN_IN_AG(x2)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
U13_GGAA(x1, x2, x3, x4, x5)  =  U13_GGAA(x1, x2, x5)
U14_GGAA(x1, x2, x3, x4, x5)  =  U14_GGAA(x1, x2, x3, x5)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
PJ_IN_GGAA(x1, x2, x3, x4)  =  PJ_IN_GGAA(x1, x2)
U15_GGAA(x1, x2, x3, x4, x5)  =  U15_GGAA(x1, x2, x5)
U16_GGAA(x1, x2, x3, x4, x5)  =  U16_GGAA(x1, x2, x3, x5)
PM_IN_AG(x1, x2)  =  PM_IN_AG(x2)
U10_GGAA(x1, x2, x3, x4, x5)  =  U10_GGAA(x1, x2, x3, x5)
TIMESK_IN_GGA(x1, x2, x3)  =  TIMESK_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
PL_IN_GGAA(x1, x2, x3, x4)  =  PL_IN_GGAA(x1, x2)
U19_GGAA(x1, x2, x3, x4, x5)  =  U19_GGAA(x1, x2, x5)
U20_GGAA(x1, x2, x3, x4, x5)  =  U20_GGAA(x1, x2, x3, x5)
PLUSO_IN_GGA(x1, x2, x3)  =  PLUSO_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
PP_IN_GGAA(x1, x2, x3, x4)  =  PP_IN_GGAA(x1, x2)
U21_GGAA(x1, x2, x3, x4, x5)  =  U21_GGAA(x1, x2, x5)
U22_GGAA(x1, x2, x3, x4, x5)  =  U22_GGAA(x1, x2, x3, x5)
PQ_IN_AG(x1, x2)  =  PQ_IN_AG(x2)

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

(4) Obligation:

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

CONVERTA_IN_GGA(.(0, T29), T16, T18) → U1_GGA(T29, T16, T18, pB_in_ggaa(T29, T16, X19, T18))
CONVERTA_IN_GGA(.(0, T29), T16, T18) → PB_IN_GGAA(T29, T16, X19, T18)
PB_IN_GGAA(T29, T16, T31, T18) → U9_GGAA(T29, T16, T31, T18, convertD_in_gga(T29, T16, T31))
PB_IN_GGAA(T29, T16, T31, T18) → CONVERTD_IN_GGA(T29, T16, T31)
CONVERTD_IN_GGA(.(0, T52), T41, X75) → U3_GGA(T52, T41, X75, pE_in_ggaa(T52, T41, X74, X75))
CONVERTD_IN_GGA(.(0, T52), T41, X75) → PE_IN_GGAA(T52, T41, X74, X75)
PE_IN_GGAA(T52, T41, T54, X75) → U11_GGAA(T52, T41, T54, X75, convertD_in_gga(T52, T41, T54))
PE_IN_GGAA(T52, T41, T54, X75) → CONVERTD_IN_GGA(T52, T41, T54)
CONVERTD_IN_GGA(.(s(T120), T121), T106, X228) → U4_GGA(T120, T121, T106, X228, pF_in_gggaa(T120, T121, T106, X227, X228))
CONVERTD_IN_GGA(.(s(T120), T121), T106, X228) → PF_IN_GGGAA(T120, T121, T106, X227, X228)
PF_IN_GGGAA(T120, T121, T106, T122, X228) → U17_GGGAA(T120, T121, T106, T122, X228, convertA_in_gga(.(T120, T121), T106, T122))
PF_IN_GGGAA(T120, T121, T106, T122, X228) → CONVERTA_IN_GGA(.(T120, T121), T106, T122)
CONVERTA_IN_GGA(.(s(T218), T219), T202, T204) → U2_GGA(T218, T219, T202, T204, pC_in_gggaa(T218, T219, T202, X370, T204))
CONVERTA_IN_GGA(.(s(T218), T219), T202, T204) → PC_IN_GGGAA(T218, T219, T202, X370, T204)
PC_IN_GGGAA(T218, T219, T202, T220, T204) → U23_GGGAA(T218, T219, T202, T220, T204, convertA_in_gga(.(T218, T219), T202, T220))
PC_IN_GGGAA(T218, T219, T202, T220, T204) → CONVERTA_IN_GGA(.(T218, T219), T202, T220)
U23_GGGAA(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → U24_GGGAA(T218, T219, T202, T220, T204, pR_in_ag(T204, T220))
U23_GGGAA(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → PR_IN_AG(T204, T220)
U17_GGGAA(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → U18_GGGAA(T120, T121, T106, T122, X228, pN_in_ag(X228, T122))
U17_GGGAA(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → PN_IN_AG(X228, T122)
U11_GGAA(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → U12_GGAA(T52, T41, T54, X75, timesG_in_gga(T54, T41, X75))
U11_GGAA(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → TIMESG_IN_GGA(T54, T41, X75)
TIMESG_IN_GGA(s(T72), T66, X137) → U5_GGA(T72, T66, X137, pH_in_ggaa(T72, T66, X136, X137))
TIMESG_IN_GGA(s(T72), T66, X137) → PH_IN_GGAA(T72, T66, X136, X137)
PH_IN_GGAA(T72, T66, T74, X137) → U13_GGAA(T72, T66, T74, X137, timesG_in_gga(T72, T66, T74))
PH_IN_GGAA(T72, T66, T74, X137) → TIMESG_IN_GGA(T72, T66, T74)
U13_GGAA(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → U14_GGAA(T72, T66, T74, X137, plusI_in_gga(T66, T74, X137))
U13_GGAA(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → PLUSI_IN_GGA(T66, T74, X137)
PLUSI_IN_GGA(s(T93), T89, X185) → U6_GGA(T93, T89, X185, pJ_in_ggaa(T93, T89, X184, X185))
PLUSI_IN_GGA(s(T93), T89, X185) → PJ_IN_GGAA(T93, T89, X184, X185)
PJ_IN_GGAA(T93, T89, T96, X185) → U15_GGAA(T93, T89, T96, X185, plusI_in_gga(T93, T89, T96))
PJ_IN_GGAA(T93, T89, T96, X185) → PLUSI_IN_GGA(T93, T89, T96)
U15_GGAA(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → U16_GGAA(T93, T89, T96, X185, pM_in_ag(X185, T96))
U15_GGAA(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → PM_IN_AG(X185, T96)
U9_GGAA(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → U10_GGAA(T29, T16, T31, T18, timesK_in_gga(T31, T16, T18))
U9_GGAA(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → TIMESK_IN_GGA(T31, T16, T18)
TIMESK_IN_GGA(s(T155), T147, T149) → U7_GGA(T155, T147, T149, pL_in_ggaa(T155, T147, X292, T149))
TIMESK_IN_GGA(s(T155), T147, T149) → PL_IN_GGAA(T155, T147, X292, T149)
PL_IN_GGAA(T155, T147, T157, T149) → U19_GGAA(T155, T147, T157, T149, timesG_in_gga(T155, T147, T157))
PL_IN_GGAA(T155, T147, T157, T149) → TIMESG_IN_GGA(T155, T147, T157)
U19_GGAA(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → U20_GGAA(T155, T147, T157, T149, plusO_in_gga(T147, T157, T149))
U19_GGAA(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → PLUSO_IN_GGA(T147, T157, T149)
PLUSO_IN_GGA(s(T186), T180, T182) → U8_GGA(T186, T180, T182, pP_in_ggaa(T186, T180, X333, T182))
PLUSO_IN_GGA(s(T186), T180, T182) → PP_IN_GGAA(T186, T180, X333, T182)
PP_IN_GGAA(T186, T180, T189, T182) → U21_GGAA(T186, T180, T189, T182, plusI_in_gga(T186, T180, T189))
PP_IN_GGAA(T186, T180, T189, T182) → PLUSI_IN_GGA(T186, T180, T189)
U21_GGAA(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → U22_GGAA(T186, T180, T189, T182, pQ_in_ag(T182, T189))
U21_GGAA(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → PQ_IN_AG(T182, T189)

The TRS R consists of the following rules:

convertA_in_gga([], T6, 0) → convertA_out_gga([], T6, 0)
convertA_in_gga(.(0, T29), T16, T18) → U1_gga(T29, T16, T18, pB_in_ggaa(T29, T16, X19, T18))
pB_in_ggaa(T29, T16, T31, T18) → U9_ggaa(T29, T16, T31, T18, convertD_in_gga(T29, T16, T31))
convertD_in_gga([], T35, 0) → convertD_out_gga([], T35, 0)
convertD_in_gga(.(0, T52), T41, X75) → U3_gga(T52, T41, X75, pE_in_ggaa(T52, T41, X74, X75))
pE_in_ggaa(T52, T41, T54, X75) → U11_ggaa(T52, T41, T54, X75, convertD_in_gga(T52, T41, T54))
convertD_in_gga(.(s(T120), T121), T106, X228) → U4_gga(T120, T121, T106, X228, pF_in_gggaa(T120, T121, T106, X227, X228))
pF_in_gggaa(T120, T121, T106, T122, X228) → U17_gggaa(T120, T121, T106, T122, X228, convertA_in_gga(.(T120, T121), T106, T122))
convertA_in_gga(.(s(T218), T219), T202, T204) → U2_gga(T218, T219, T202, T204, pC_in_gggaa(T218, T219, T202, X370, T204))
pC_in_gggaa(T218, T219, T202, T220, T204) → U23_gggaa(T218, T219, T202, T220, T204, convertA_in_gga(.(T218, T219), T202, T220))
U23_gggaa(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → U24_gggaa(T218, T219, T202, T220, T204, pR_in_ag(T204, T220))
pR_in_ag(s(T223), T223) → pR_out_ag(s(T223), T223)
pR_in_ag(0, 0) → pR_out_ag(0, 0)
U24_gggaa(T218, T219, T202, T220, T204, pR_out_ag(T204, T220)) → pC_out_gggaa(T218, T219, T202, T220, T204)
U2_gga(T218, T219, T202, T204, pC_out_gggaa(T218, T219, T202, X370, T204)) → convertA_out_gga(.(s(T218), T219), T202, T204)
U17_gggaa(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → U18_gggaa(T120, T121, T106, T122, X228, pN_in_ag(X228, T122))
pN_in_ag(s(T125), T125) → pN_out_ag(s(T125), T125)
U18_gggaa(T120, T121, T106, T122, X228, pN_out_ag(X228, T122)) → pF_out_gggaa(T120, T121, T106, T122, X228)
U4_gga(T120, T121, T106, X228, pF_out_gggaa(T120, T121, T106, X227, X228)) → convertD_out_gga(.(s(T120), T121), T106, X228)
U11_ggaa(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → U12_ggaa(T52, T41, T54, X75, timesG_in_gga(T54, T41, X75))
timesG_in_gga(0, T59, 0) → timesG_out_gga(0, T59, 0)
timesG_in_gga(s(T72), T66, X137) → U5_gga(T72, T66, X137, pH_in_ggaa(T72, T66, X136, X137))
pH_in_ggaa(T72, T66, T74, X137) → U13_ggaa(T72, T66, T74, X137, timesG_in_gga(T72, T66, T74))
U13_ggaa(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → U14_ggaa(T72, T66, T74, X137, plusI_in_gga(T66, T74, X137))
plusI_in_gga(0, T82, T82) → plusI_out_gga(0, T82, T82)
plusI_in_gga(s(T93), T89, X185) → U6_gga(T93, T89, X185, pJ_in_ggaa(T93, T89, X184, X185))
pJ_in_ggaa(T93, T89, T96, X185) → U15_ggaa(T93, T89, T96, X185, plusI_in_gga(T93, T89, T96))
U15_ggaa(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → U16_ggaa(T93, T89, T96, X185, pM_in_ag(X185, T96))
pM_in_ag(s(T100), T100) → pM_out_ag(s(T100), T100)
U16_ggaa(T93, T89, T96, X185, pM_out_ag(X185, T96)) → pJ_out_ggaa(T93, T89, T96, X185)
U6_gga(T93, T89, X185, pJ_out_ggaa(T93, T89, X184, X185)) → plusI_out_gga(s(T93), T89, X185)
U14_ggaa(T72, T66, T74, X137, plusI_out_gga(T66, T74, X137)) → pH_out_ggaa(T72, T66, T74, X137)
U5_gga(T72, T66, X137, pH_out_ggaa(T72, T66, X136, X137)) → timesG_out_gga(s(T72), T66, X137)
U12_ggaa(T52, T41, T54, X75, timesG_out_gga(T54, T41, X75)) → pE_out_ggaa(T52, T41, T54, X75)
U3_gga(T52, T41, X75, pE_out_ggaa(T52, T41, X74, X75)) → convertD_out_gga(.(0, T52), T41, X75)
U9_ggaa(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → U10_ggaa(T29, T16, T31, T18, timesK_in_gga(T31, T16, T18))
timesK_in_gga(0, T132, 0) → timesK_out_gga(0, T132, 0)
timesK_in_gga(s(T155), T147, T149) → U7_gga(T155, T147, T149, pL_in_ggaa(T155, T147, X292, T149))
pL_in_ggaa(T155, T147, T157, T149) → U19_ggaa(T155, T147, T157, T149, timesG_in_gga(T155, T147, T157))
U19_ggaa(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → U20_ggaa(T155, T147, T157, T149, plusO_in_gga(T147, T157, T149))
plusO_in_gga(0, T170, T170) → plusO_out_gga(0, T170, T170)
plusO_in_gga(s(T186), T180, T182) → U8_gga(T186, T180, T182, pP_in_ggaa(T186, T180, X333, T182))
pP_in_ggaa(T186, T180, T189, T182) → U21_ggaa(T186, T180, T189, T182, plusI_in_gga(T186, T180, T189))
U21_ggaa(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → U22_ggaa(T186, T180, T189, T182, pQ_in_ag(T182, T189))
pQ_in_ag(s(T193), T193) → pQ_out_ag(s(T193), T193)
pQ_in_ag(0, 0) → pQ_out_ag(0, 0)
U22_ggaa(T186, T180, T189, T182, pQ_out_ag(T182, T189)) → pP_out_ggaa(T186, T180, T189, T182)
U8_gga(T186, T180, T182, pP_out_ggaa(T186, T180, X333, T182)) → plusO_out_gga(s(T186), T180, T182)
U20_ggaa(T155, T147, T157, T149, plusO_out_gga(T147, T157, T149)) → pL_out_ggaa(T155, T147, T157, T149)
U7_gga(T155, T147, T149, pL_out_ggaa(T155, T147, X292, T149)) → timesK_out_gga(s(T155), T147, T149)
U10_ggaa(T29, T16, T31, T18, timesK_out_gga(T31, T16, T18)) → pB_out_ggaa(T29, T16, T31, T18)
U1_gga(T29, T16, T18, pB_out_ggaa(T29, T16, X19, T18)) → convertA_out_gga(.(0, T29), T16, T18)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
convertD_in_gga(x1, x2, x3)  =  convertD_in_gga(x1, x2)
convertD_out_gga(x1, x2, x3)  =  convertD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pF_in_gggaa(x1, x2, x3, x4, x5)  =  pF_in_gggaa(x1, x2, x3)
U17_gggaa(x1, x2, x3, x4, x5, x6)  =  U17_gggaa(x1, x2, x3, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U23_gggaa(x1, x2, x3, x4, x5, x6)  =  U23_gggaa(x1, x2, x3, x6)
U24_gggaa(x1, x2, x3, x4, x5, x6)  =  U24_gggaa(x1, x2, x3, x4, x6)
pR_in_ag(x1, x2)  =  pR_in_ag(x2)
pR_out_ag(x1, x2)  =  pR_out_ag(x1, x2)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U18_gggaa(x1, x2, x3, x4, x5, x6)  =  U18_gggaa(x1, x2, x3, x4, x6)
pN_in_ag(x1, x2)  =  pN_in_ag(x2)
pN_out_ag(x1, x2)  =  pN_out_ag(x1, x2)
pF_out_gggaa(x1, x2, x3, x4, x5)  =  pF_out_gggaa(x1, x2, x3, x4, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pM_in_ag(x1, x2)  =  pM_in_ag(x2)
pM_out_ag(x1, x2)  =  pM_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusO_in_gga(x1, x2, x3)  =  plusO_in_gga(x1, x2)
plusO_out_gga(x1, x2, x3)  =  plusO_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pP_in_ggaa(x1, x2, x3, x4)  =  pP_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
pQ_in_ag(x1, x2)  =  pQ_in_ag(x2)
pQ_out_ag(x1, x2)  =  pQ_out_ag(x1, x2)
pP_out_ggaa(x1, x2, x3, x4)  =  pP_out_ggaa(x1, x2, x3, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
CONVERTA_IN_GGA(x1, x2, x3)  =  CONVERTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4)  =  U1_GGA(x1, x2, x4)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4, x5)  =  U9_GGAA(x1, x2, x5)
CONVERTD_IN_GGA(x1, x2, x3)  =  CONVERTD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
PE_IN_GGAA(x1, x2, x3, x4)  =  PE_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x1, x2, x3, x5)
PF_IN_GGGAA(x1, x2, x3, x4, x5)  =  PF_IN_GGGAA(x1, x2, x3)
U17_GGGAA(x1, x2, x3, x4, x5, x6)  =  U17_GGGAA(x1, x2, x3, x6)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
PC_IN_GGGAA(x1, x2, x3, x4, x5)  =  PC_IN_GGGAA(x1, x2, x3)
U23_GGGAA(x1, x2, x3, x4, x5, x6)  =  U23_GGGAA(x1, x2, x3, x6)
U24_GGGAA(x1, x2, x3, x4, x5, x6)  =  U24_GGGAA(x1, x2, x3, x4, x6)
PR_IN_AG(x1, x2)  =  PR_IN_AG(x2)
U18_GGGAA(x1, x2, x3, x4, x5, x6)  =  U18_GGGAA(x1, x2, x3, x4, x6)
PN_IN_AG(x1, x2)  =  PN_IN_AG(x2)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
U13_GGAA(x1, x2, x3, x4, x5)  =  U13_GGAA(x1, x2, x5)
U14_GGAA(x1, x2, x3, x4, x5)  =  U14_GGAA(x1, x2, x3, x5)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
PJ_IN_GGAA(x1, x2, x3, x4)  =  PJ_IN_GGAA(x1, x2)
U15_GGAA(x1, x2, x3, x4, x5)  =  U15_GGAA(x1, x2, x5)
U16_GGAA(x1, x2, x3, x4, x5)  =  U16_GGAA(x1, x2, x3, x5)
PM_IN_AG(x1, x2)  =  PM_IN_AG(x2)
U10_GGAA(x1, x2, x3, x4, x5)  =  U10_GGAA(x1, x2, x3, x5)
TIMESK_IN_GGA(x1, x2, x3)  =  TIMESK_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
PL_IN_GGAA(x1, x2, x3, x4)  =  PL_IN_GGAA(x1, x2)
U19_GGAA(x1, x2, x3, x4, x5)  =  U19_GGAA(x1, x2, x5)
U20_GGAA(x1, x2, x3, x4, x5)  =  U20_GGAA(x1, x2, x3, x5)
PLUSO_IN_GGA(x1, x2, x3)  =  PLUSO_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
PP_IN_GGAA(x1, x2, x3, x4)  =  PP_IN_GGAA(x1, x2)
U21_GGAA(x1, x2, x3, x4, x5)  =  U21_GGAA(x1, x2, x5)
U22_GGAA(x1, x2, x3, x4, x5)  =  U22_GGAA(x1, x2, x3, x5)
PQ_IN_AG(x1, x2)  =  PQ_IN_AG(x2)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

PLUSI_IN_GGA(s(T93), T89, X185) → PJ_IN_GGAA(T93, T89, X184, X185)
PJ_IN_GGAA(T93, T89, T96, X185) → PLUSI_IN_GGA(T93, T89, T96)

The TRS R consists of the following rules:

convertA_in_gga([], T6, 0) → convertA_out_gga([], T6, 0)
convertA_in_gga(.(0, T29), T16, T18) → U1_gga(T29, T16, T18, pB_in_ggaa(T29, T16, X19, T18))
pB_in_ggaa(T29, T16, T31, T18) → U9_ggaa(T29, T16, T31, T18, convertD_in_gga(T29, T16, T31))
convertD_in_gga([], T35, 0) → convertD_out_gga([], T35, 0)
convertD_in_gga(.(0, T52), T41, X75) → U3_gga(T52, T41, X75, pE_in_ggaa(T52, T41, X74, X75))
pE_in_ggaa(T52, T41, T54, X75) → U11_ggaa(T52, T41, T54, X75, convertD_in_gga(T52, T41, T54))
convertD_in_gga(.(s(T120), T121), T106, X228) → U4_gga(T120, T121, T106, X228, pF_in_gggaa(T120, T121, T106, X227, X228))
pF_in_gggaa(T120, T121, T106, T122, X228) → U17_gggaa(T120, T121, T106, T122, X228, convertA_in_gga(.(T120, T121), T106, T122))
convertA_in_gga(.(s(T218), T219), T202, T204) → U2_gga(T218, T219, T202, T204, pC_in_gggaa(T218, T219, T202, X370, T204))
pC_in_gggaa(T218, T219, T202, T220, T204) → U23_gggaa(T218, T219, T202, T220, T204, convertA_in_gga(.(T218, T219), T202, T220))
U23_gggaa(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → U24_gggaa(T218, T219, T202, T220, T204, pR_in_ag(T204, T220))
pR_in_ag(s(T223), T223) → pR_out_ag(s(T223), T223)
pR_in_ag(0, 0) → pR_out_ag(0, 0)
U24_gggaa(T218, T219, T202, T220, T204, pR_out_ag(T204, T220)) → pC_out_gggaa(T218, T219, T202, T220, T204)
U2_gga(T218, T219, T202, T204, pC_out_gggaa(T218, T219, T202, X370, T204)) → convertA_out_gga(.(s(T218), T219), T202, T204)
U17_gggaa(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → U18_gggaa(T120, T121, T106, T122, X228, pN_in_ag(X228, T122))
pN_in_ag(s(T125), T125) → pN_out_ag(s(T125), T125)
U18_gggaa(T120, T121, T106, T122, X228, pN_out_ag(X228, T122)) → pF_out_gggaa(T120, T121, T106, T122, X228)
U4_gga(T120, T121, T106, X228, pF_out_gggaa(T120, T121, T106, X227, X228)) → convertD_out_gga(.(s(T120), T121), T106, X228)
U11_ggaa(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → U12_ggaa(T52, T41, T54, X75, timesG_in_gga(T54, T41, X75))
timesG_in_gga(0, T59, 0) → timesG_out_gga(0, T59, 0)
timesG_in_gga(s(T72), T66, X137) → U5_gga(T72, T66, X137, pH_in_ggaa(T72, T66, X136, X137))
pH_in_ggaa(T72, T66, T74, X137) → U13_ggaa(T72, T66, T74, X137, timesG_in_gga(T72, T66, T74))
U13_ggaa(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → U14_ggaa(T72, T66, T74, X137, plusI_in_gga(T66, T74, X137))
plusI_in_gga(0, T82, T82) → plusI_out_gga(0, T82, T82)
plusI_in_gga(s(T93), T89, X185) → U6_gga(T93, T89, X185, pJ_in_ggaa(T93, T89, X184, X185))
pJ_in_ggaa(T93, T89, T96, X185) → U15_ggaa(T93, T89, T96, X185, plusI_in_gga(T93, T89, T96))
U15_ggaa(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → U16_ggaa(T93, T89, T96, X185, pM_in_ag(X185, T96))
pM_in_ag(s(T100), T100) → pM_out_ag(s(T100), T100)
U16_ggaa(T93, T89, T96, X185, pM_out_ag(X185, T96)) → pJ_out_ggaa(T93, T89, T96, X185)
U6_gga(T93, T89, X185, pJ_out_ggaa(T93, T89, X184, X185)) → plusI_out_gga(s(T93), T89, X185)
U14_ggaa(T72, T66, T74, X137, plusI_out_gga(T66, T74, X137)) → pH_out_ggaa(T72, T66, T74, X137)
U5_gga(T72, T66, X137, pH_out_ggaa(T72, T66, X136, X137)) → timesG_out_gga(s(T72), T66, X137)
U12_ggaa(T52, T41, T54, X75, timesG_out_gga(T54, T41, X75)) → pE_out_ggaa(T52, T41, T54, X75)
U3_gga(T52, T41, X75, pE_out_ggaa(T52, T41, X74, X75)) → convertD_out_gga(.(0, T52), T41, X75)
U9_ggaa(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → U10_ggaa(T29, T16, T31, T18, timesK_in_gga(T31, T16, T18))
timesK_in_gga(0, T132, 0) → timesK_out_gga(0, T132, 0)
timesK_in_gga(s(T155), T147, T149) → U7_gga(T155, T147, T149, pL_in_ggaa(T155, T147, X292, T149))
pL_in_ggaa(T155, T147, T157, T149) → U19_ggaa(T155, T147, T157, T149, timesG_in_gga(T155, T147, T157))
U19_ggaa(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → U20_ggaa(T155, T147, T157, T149, plusO_in_gga(T147, T157, T149))
plusO_in_gga(0, T170, T170) → plusO_out_gga(0, T170, T170)
plusO_in_gga(s(T186), T180, T182) → U8_gga(T186, T180, T182, pP_in_ggaa(T186, T180, X333, T182))
pP_in_ggaa(T186, T180, T189, T182) → U21_ggaa(T186, T180, T189, T182, plusI_in_gga(T186, T180, T189))
U21_ggaa(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → U22_ggaa(T186, T180, T189, T182, pQ_in_ag(T182, T189))
pQ_in_ag(s(T193), T193) → pQ_out_ag(s(T193), T193)
pQ_in_ag(0, 0) → pQ_out_ag(0, 0)
U22_ggaa(T186, T180, T189, T182, pQ_out_ag(T182, T189)) → pP_out_ggaa(T186, T180, T189, T182)
U8_gga(T186, T180, T182, pP_out_ggaa(T186, T180, X333, T182)) → plusO_out_gga(s(T186), T180, T182)
U20_ggaa(T155, T147, T157, T149, plusO_out_gga(T147, T157, T149)) → pL_out_ggaa(T155, T147, T157, T149)
U7_gga(T155, T147, T149, pL_out_ggaa(T155, T147, X292, T149)) → timesK_out_gga(s(T155), T147, T149)
U10_ggaa(T29, T16, T31, T18, timesK_out_gga(T31, T16, T18)) → pB_out_ggaa(T29, T16, T31, T18)
U1_gga(T29, T16, T18, pB_out_ggaa(T29, T16, X19, T18)) → convertA_out_gga(.(0, T29), T16, T18)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
convertD_in_gga(x1, x2, x3)  =  convertD_in_gga(x1, x2)
convertD_out_gga(x1, x2, x3)  =  convertD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pF_in_gggaa(x1, x2, x3, x4, x5)  =  pF_in_gggaa(x1, x2, x3)
U17_gggaa(x1, x2, x3, x4, x5, x6)  =  U17_gggaa(x1, x2, x3, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U23_gggaa(x1, x2, x3, x4, x5, x6)  =  U23_gggaa(x1, x2, x3, x6)
U24_gggaa(x1, x2, x3, x4, x5, x6)  =  U24_gggaa(x1, x2, x3, x4, x6)
pR_in_ag(x1, x2)  =  pR_in_ag(x2)
pR_out_ag(x1, x2)  =  pR_out_ag(x1, x2)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U18_gggaa(x1, x2, x3, x4, x5, x6)  =  U18_gggaa(x1, x2, x3, x4, x6)
pN_in_ag(x1, x2)  =  pN_in_ag(x2)
pN_out_ag(x1, x2)  =  pN_out_ag(x1, x2)
pF_out_gggaa(x1, x2, x3, x4, x5)  =  pF_out_gggaa(x1, x2, x3, x4, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pM_in_ag(x1, x2)  =  pM_in_ag(x2)
pM_out_ag(x1, x2)  =  pM_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusO_in_gga(x1, x2, x3)  =  plusO_in_gga(x1, x2)
plusO_out_gga(x1, x2, x3)  =  plusO_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pP_in_ggaa(x1, x2, x3, x4)  =  pP_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
pQ_in_ag(x1, x2)  =  pQ_in_ag(x2)
pQ_out_ag(x1, x2)  =  pQ_out_ag(x1, x2)
pP_out_ggaa(x1, x2, x3, x4)  =  pP_out_ggaa(x1, x2, x3, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
PLUSI_IN_GGA(x1, x2, x3)  =  PLUSI_IN_GGA(x1, x2)
PJ_IN_GGAA(x1, x2, x3, x4)  =  PJ_IN_GGAA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

PLUSI_IN_GGA(s(T93), T89, X185) → PJ_IN_GGAA(T93, T89, X184, X185)
PJ_IN_GGAA(T93, T89, T96, X185) → PLUSI_IN_GGA(T93, T89, T96)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

PLUSI_IN_GGA(s(T93), T89) → PJ_IN_GGAA(T93, T89)
PJ_IN_GGAA(T93, T89) → PLUSI_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:

• PJ_IN_GGAA(T93, T89) → PLUSI_IN_GGA(T93, T89)
  The graph contains the following edges 1 >= 1, 2 >= 2

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

TIMESG_IN_GGA(s(T72), T66, X137) → PH_IN_GGAA(T72, T66, X136, X137)
PH_IN_GGAA(T72, T66, T74, X137) → TIMESG_IN_GGA(T72, T66, T74)

The TRS R consists of the following rules:

convertA_in_gga([], T6, 0) → convertA_out_gga([], T6, 0)
convertA_in_gga(.(0, T29), T16, T18) → U1_gga(T29, T16, T18, pB_in_ggaa(T29, T16, X19, T18))
pB_in_ggaa(T29, T16, T31, T18) → U9_ggaa(T29, T16, T31, T18, convertD_in_gga(T29, T16, T31))
convertD_in_gga([], T35, 0) → convertD_out_gga([], T35, 0)
convertD_in_gga(.(0, T52), T41, X75) → U3_gga(T52, T41, X75, pE_in_ggaa(T52, T41, X74, X75))
pE_in_ggaa(T52, T41, T54, X75) → U11_ggaa(T52, T41, T54, X75, convertD_in_gga(T52, T41, T54))
convertD_in_gga(.(s(T120), T121), T106, X228) → U4_gga(T120, T121, T106, X228, pF_in_gggaa(T120, T121, T106, X227, X228))
pF_in_gggaa(T120, T121, T106, T122, X228) → U17_gggaa(T120, T121, T106, T122, X228, convertA_in_gga(.(T120, T121), T106, T122))
convertA_in_gga(.(s(T218), T219), T202, T204) → U2_gga(T218, T219, T202, T204, pC_in_gggaa(T218, T219, T202, X370, T204))
pC_in_gggaa(T218, T219, T202, T220, T204) → U23_gggaa(T218, T219, T202, T220, T204, convertA_in_gga(.(T218, T219), T202, T220))
U23_gggaa(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → U24_gggaa(T218, T219, T202, T220, T204, pR_in_ag(T204, T220))
pR_in_ag(s(T223), T223) → pR_out_ag(s(T223), T223)
pR_in_ag(0, 0) → pR_out_ag(0, 0)
U24_gggaa(T218, T219, T202, T220, T204, pR_out_ag(T204, T220)) → pC_out_gggaa(T218, T219, T202, T220, T204)
U2_gga(T218, T219, T202, T204, pC_out_gggaa(T218, T219, T202, X370, T204)) → convertA_out_gga(.(s(T218), T219), T202, T204)
U17_gggaa(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → U18_gggaa(T120, T121, T106, T122, X228, pN_in_ag(X228, T122))
pN_in_ag(s(T125), T125) → pN_out_ag(s(T125), T125)
U18_gggaa(T120, T121, T106, T122, X228, pN_out_ag(X228, T122)) → pF_out_gggaa(T120, T121, T106, T122, X228)
U4_gga(T120, T121, T106, X228, pF_out_gggaa(T120, T121, T106, X227, X228)) → convertD_out_gga(.(s(T120), T121), T106, X228)
U11_ggaa(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → U12_ggaa(T52, T41, T54, X75, timesG_in_gga(T54, T41, X75))
timesG_in_gga(0, T59, 0) → timesG_out_gga(0, T59, 0)
timesG_in_gga(s(T72), T66, X137) → U5_gga(T72, T66, X137, pH_in_ggaa(T72, T66, X136, X137))
pH_in_ggaa(T72, T66, T74, X137) → U13_ggaa(T72, T66, T74, X137, timesG_in_gga(T72, T66, T74))
U13_ggaa(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → U14_ggaa(T72, T66, T74, X137, plusI_in_gga(T66, T74, X137))
plusI_in_gga(0, T82, T82) → plusI_out_gga(0, T82, T82)
plusI_in_gga(s(T93), T89, X185) → U6_gga(T93, T89, X185, pJ_in_ggaa(T93, T89, X184, X185))
pJ_in_ggaa(T93, T89, T96, X185) → U15_ggaa(T93, T89, T96, X185, plusI_in_gga(T93, T89, T96))
U15_ggaa(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → U16_ggaa(T93, T89, T96, X185, pM_in_ag(X185, T96))
pM_in_ag(s(T100), T100) → pM_out_ag(s(T100), T100)
U16_ggaa(T93, T89, T96, X185, pM_out_ag(X185, T96)) → pJ_out_ggaa(T93, T89, T96, X185)
U6_gga(T93, T89, X185, pJ_out_ggaa(T93, T89, X184, X185)) → plusI_out_gga(s(T93), T89, X185)
U14_ggaa(T72, T66, T74, X137, plusI_out_gga(T66, T74, X137)) → pH_out_ggaa(T72, T66, T74, X137)
U5_gga(T72, T66, X137, pH_out_ggaa(T72, T66, X136, X137)) → timesG_out_gga(s(T72), T66, X137)
U12_ggaa(T52, T41, T54, X75, timesG_out_gga(T54, T41, X75)) → pE_out_ggaa(T52, T41, T54, X75)
U3_gga(T52, T41, X75, pE_out_ggaa(T52, T41, X74, X75)) → convertD_out_gga(.(0, T52), T41, X75)
U9_ggaa(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → U10_ggaa(T29, T16, T31, T18, timesK_in_gga(T31, T16, T18))
timesK_in_gga(0, T132, 0) → timesK_out_gga(0, T132, 0)
timesK_in_gga(s(T155), T147, T149) → U7_gga(T155, T147, T149, pL_in_ggaa(T155, T147, X292, T149))
pL_in_ggaa(T155, T147, T157, T149) → U19_ggaa(T155, T147, T157, T149, timesG_in_gga(T155, T147, T157))
U19_ggaa(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → U20_ggaa(T155, T147, T157, T149, plusO_in_gga(T147, T157, T149))
plusO_in_gga(0, T170, T170) → plusO_out_gga(0, T170, T170)
plusO_in_gga(s(T186), T180, T182) → U8_gga(T186, T180, T182, pP_in_ggaa(T186, T180, X333, T182))
pP_in_ggaa(T186, T180, T189, T182) → U21_ggaa(T186, T180, T189, T182, plusI_in_gga(T186, T180, T189))
U21_ggaa(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → U22_ggaa(T186, T180, T189, T182, pQ_in_ag(T182, T189))
pQ_in_ag(s(T193), T193) → pQ_out_ag(s(T193), T193)
pQ_in_ag(0, 0) → pQ_out_ag(0, 0)
U22_ggaa(T186, T180, T189, T182, pQ_out_ag(T182, T189)) → pP_out_ggaa(T186, T180, T189, T182)
U8_gga(T186, T180, T182, pP_out_ggaa(T186, T180, X333, T182)) → plusO_out_gga(s(T186), T180, T182)
U20_ggaa(T155, T147, T157, T149, plusO_out_gga(T147, T157, T149)) → pL_out_ggaa(T155, T147, T157, T149)
U7_gga(T155, T147, T149, pL_out_ggaa(T155, T147, X292, T149)) → timesK_out_gga(s(T155), T147, T149)
U10_ggaa(T29, T16, T31, T18, timesK_out_gga(T31, T16, T18)) → pB_out_ggaa(T29, T16, T31, T18)
U1_gga(T29, T16, T18, pB_out_ggaa(T29, T16, X19, T18)) → convertA_out_gga(.(0, T29), T16, T18)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
convertD_in_gga(x1, x2, x3)  =  convertD_in_gga(x1, x2)
convertD_out_gga(x1, x2, x3)  =  convertD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pF_in_gggaa(x1, x2, x3, x4, x5)  =  pF_in_gggaa(x1, x2, x3)
U17_gggaa(x1, x2, x3, x4, x5, x6)  =  U17_gggaa(x1, x2, x3, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U23_gggaa(x1, x2, x3, x4, x5, x6)  =  U23_gggaa(x1, x2, x3, x6)
U24_gggaa(x1, x2, x3, x4, x5, x6)  =  U24_gggaa(x1, x2, x3, x4, x6)
pR_in_ag(x1, x2)  =  pR_in_ag(x2)
pR_out_ag(x1, x2)  =  pR_out_ag(x1, x2)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U18_gggaa(x1, x2, x3, x4, x5, x6)  =  U18_gggaa(x1, x2, x3, x4, x6)
pN_in_ag(x1, x2)  =  pN_in_ag(x2)
pN_out_ag(x1, x2)  =  pN_out_ag(x1, x2)
pF_out_gggaa(x1, x2, x3, x4, x5)  =  pF_out_gggaa(x1, x2, x3, x4, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pM_in_ag(x1, x2)  =  pM_in_ag(x2)
pM_out_ag(x1, x2)  =  pM_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusO_in_gga(x1, x2, x3)  =  plusO_in_gga(x1, x2)
plusO_out_gga(x1, x2, x3)  =  plusO_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pP_in_ggaa(x1, x2, x3, x4)  =  pP_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
pQ_in_ag(x1, x2)  =  pQ_in_ag(x2)
pQ_out_ag(x1, x2)  =  pQ_out_ag(x1, x2)
pP_out_ggaa(x1, x2, x3, x4)  =  pP_out_ggaa(x1, x2, x3, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
TIMESG_IN_GGA(x1, x2, x3)  =  TIMESG_IN_GGA(x1, x2)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

TIMESG_IN_GGA(s(T72), T66, X137) → PH_IN_GGAA(T72, T66, X136, X137)
PH_IN_GGAA(T72, T66, T74, X137) → TIMESG_IN_GGA(T72, T66, T74)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

TIMESG_IN_GGA(s(T72), T66) → PH_IN_GGAA(T72, T66)
PH_IN_GGAA(T72, T66) → TIMESG_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:

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

• TIMESG_IN_GGA(s(T72), T66) → PH_IN_GGAA(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:

CONVERTA_IN_GGA(.(0, T29), T16, T18) → PB_IN_GGAA(T29, T16, X19, T18)
PB_IN_GGAA(T29, T16, T31, T18) → CONVERTD_IN_GGA(T29, T16, T31)
CONVERTD_IN_GGA(.(0, T52), T41, X75) → PE_IN_GGAA(T52, T41, X74, X75)
PE_IN_GGAA(T52, T41, T54, X75) → CONVERTD_IN_GGA(T52, T41, T54)
CONVERTD_IN_GGA(.(s(T120), T121), T106, X228) → PF_IN_GGGAA(T120, T121, T106, X227, X228)
PF_IN_GGGAA(T120, T121, T106, T122, X228) → CONVERTA_IN_GGA(.(T120, T121), T106, T122)
CONVERTA_IN_GGA(.(s(T218), T219), T202, T204) → PC_IN_GGGAA(T218, T219, T202, X370, T204)
PC_IN_GGGAA(T218, T219, T202, T220, T204) → CONVERTA_IN_GGA(.(T218, T219), T202, T220)

The TRS R consists of the following rules:

convertA_in_gga([], T6, 0) → convertA_out_gga([], T6, 0)
convertA_in_gga(.(0, T29), T16, T18) → U1_gga(T29, T16, T18, pB_in_ggaa(T29, T16, X19, T18))
pB_in_ggaa(T29, T16, T31, T18) → U9_ggaa(T29, T16, T31, T18, convertD_in_gga(T29, T16, T31))
convertD_in_gga([], T35, 0) → convertD_out_gga([], T35, 0)
convertD_in_gga(.(0, T52), T41, X75) → U3_gga(T52, T41, X75, pE_in_ggaa(T52, T41, X74, X75))
pE_in_ggaa(T52, T41, T54, X75) → U11_ggaa(T52, T41, T54, X75, convertD_in_gga(T52, T41, T54))
convertD_in_gga(.(s(T120), T121), T106, X228) → U4_gga(T120, T121, T106, X228, pF_in_gggaa(T120, T121, T106, X227, X228))
pF_in_gggaa(T120, T121, T106, T122, X228) → U17_gggaa(T120, T121, T106, T122, X228, convertA_in_gga(.(T120, T121), T106, T122))
convertA_in_gga(.(s(T218), T219), T202, T204) → U2_gga(T218, T219, T202, T204, pC_in_gggaa(T218, T219, T202, X370, T204))
pC_in_gggaa(T218, T219, T202, T220, T204) → U23_gggaa(T218, T219, T202, T220, T204, convertA_in_gga(.(T218, T219), T202, T220))
U23_gggaa(T218, T219, T202, T220, T204, convertA_out_gga(.(T218, T219), T202, T220)) → U24_gggaa(T218, T219, T202, T220, T204, pR_in_ag(T204, T220))
pR_in_ag(s(T223), T223) → pR_out_ag(s(T223), T223)
pR_in_ag(0, 0) → pR_out_ag(0, 0)
U24_gggaa(T218, T219, T202, T220, T204, pR_out_ag(T204, T220)) → pC_out_gggaa(T218, T219, T202, T220, T204)
U2_gga(T218, T219, T202, T204, pC_out_gggaa(T218, T219, T202, X370, T204)) → convertA_out_gga(.(s(T218), T219), T202, T204)
U17_gggaa(T120, T121, T106, T122, X228, convertA_out_gga(.(T120, T121), T106, T122)) → U18_gggaa(T120, T121, T106, T122, X228, pN_in_ag(X228, T122))
pN_in_ag(s(T125), T125) → pN_out_ag(s(T125), T125)
U18_gggaa(T120, T121, T106, T122, X228, pN_out_ag(X228, T122)) → pF_out_gggaa(T120, T121, T106, T122, X228)
U4_gga(T120, T121, T106, X228, pF_out_gggaa(T120, T121, T106, X227, X228)) → convertD_out_gga(.(s(T120), T121), T106, X228)
U11_ggaa(T52, T41, T54, X75, convertD_out_gga(T52, T41, T54)) → U12_ggaa(T52, T41, T54, X75, timesG_in_gga(T54, T41, X75))
timesG_in_gga(0, T59, 0) → timesG_out_gga(0, T59, 0)
timesG_in_gga(s(T72), T66, X137) → U5_gga(T72, T66, X137, pH_in_ggaa(T72, T66, X136, X137))
pH_in_ggaa(T72, T66, T74, X137) → U13_ggaa(T72, T66, T74, X137, timesG_in_gga(T72, T66, T74))
U13_ggaa(T72, T66, T74, X137, timesG_out_gga(T72, T66, T74)) → U14_ggaa(T72, T66, T74, X137, plusI_in_gga(T66, T74, X137))
plusI_in_gga(0, T82, T82) → plusI_out_gga(0, T82, T82)
plusI_in_gga(s(T93), T89, X185) → U6_gga(T93, T89, X185, pJ_in_ggaa(T93, T89, X184, X185))
pJ_in_ggaa(T93, T89, T96, X185) → U15_ggaa(T93, T89, T96, X185, plusI_in_gga(T93, T89, T96))
U15_ggaa(T93, T89, T96, X185, plusI_out_gga(T93, T89, T96)) → U16_ggaa(T93, T89, T96, X185, pM_in_ag(X185, T96))
pM_in_ag(s(T100), T100) → pM_out_ag(s(T100), T100)
U16_ggaa(T93, T89, T96, X185, pM_out_ag(X185, T96)) → pJ_out_ggaa(T93, T89, T96, X185)
U6_gga(T93, T89, X185, pJ_out_ggaa(T93, T89, X184, X185)) → plusI_out_gga(s(T93), T89, X185)
U14_ggaa(T72, T66, T74, X137, plusI_out_gga(T66, T74, X137)) → pH_out_ggaa(T72, T66, T74, X137)
U5_gga(T72, T66, X137, pH_out_ggaa(T72, T66, X136, X137)) → timesG_out_gga(s(T72), T66, X137)
U12_ggaa(T52, T41, T54, X75, timesG_out_gga(T54, T41, X75)) → pE_out_ggaa(T52, T41, T54, X75)
U3_gga(T52, T41, X75, pE_out_ggaa(T52, T41, X74, X75)) → convertD_out_gga(.(0, T52), T41, X75)
U9_ggaa(T29, T16, T31, T18, convertD_out_gga(T29, T16, T31)) → U10_ggaa(T29, T16, T31, T18, timesK_in_gga(T31, T16, T18))
timesK_in_gga(0, T132, 0) → timesK_out_gga(0, T132, 0)
timesK_in_gga(s(T155), T147, T149) → U7_gga(T155, T147, T149, pL_in_ggaa(T155, T147, X292, T149))
pL_in_ggaa(T155, T147, T157, T149) → U19_ggaa(T155, T147, T157, T149, timesG_in_gga(T155, T147, T157))
U19_ggaa(T155, T147, T157, T149, timesG_out_gga(T155, T147, T157)) → U20_ggaa(T155, T147, T157, T149, plusO_in_gga(T147, T157, T149))
plusO_in_gga(0, T170, T170) → plusO_out_gga(0, T170, T170)
plusO_in_gga(s(T186), T180, T182) → U8_gga(T186, T180, T182, pP_in_ggaa(T186, T180, X333, T182))
pP_in_ggaa(T186, T180, T189, T182) → U21_ggaa(T186, T180, T189, T182, plusI_in_gga(T186, T180, T189))
U21_ggaa(T186, T180, T189, T182, plusI_out_gga(T186, T180, T189)) → U22_ggaa(T186, T180, T189, T182, pQ_in_ag(T182, T189))
pQ_in_ag(s(T193), T193) → pQ_out_ag(s(T193), T193)
pQ_in_ag(0, 0) → pQ_out_ag(0, 0)
U22_ggaa(T186, T180, T189, T182, pQ_out_ag(T182, T189)) → pP_out_ggaa(T186, T180, T189, T182)
U8_gga(T186, T180, T182, pP_out_ggaa(T186, T180, X333, T182)) → plusO_out_gga(s(T186), T180, T182)
U20_ggaa(T155, T147, T157, T149, plusO_out_gga(T147, T157, T149)) → pL_out_ggaa(T155, T147, T157, T149)
U7_gga(T155, T147, T149, pL_out_ggaa(T155, T147, X292, T149)) → timesK_out_gga(s(T155), T147, T149)
U10_ggaa(T29, T16, T31, T18, timesK_out_gga(T31, T16, T18)) → pB_out_ggaa(T29, T16, T31, T18)
U1_gga(T29, T16, T18, pB_out_ggaa(T29, T16, X19, T18)) → convertA_out_gga(.(0, T29), T16, T18)

The argument filtering Pi contains the following mapping:
convertA_in_gga(x1, x2, x3)  =  convertA_in_gga(x1, x2)
[]  =  []
convertA_out_gga(x1, x2, x3)  =  convertA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
0  =  0
U1_gga(x1, x2, x3, x4)  =  U1_gga(x1, x2, x4)
pB_in_ggaa(x1, x2, x3, x4)  =  pB_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
convertD_in_gga(x1, x2, x3)  =  convertD_in_gga(x1, x2)
convertD_out_gga(x1, x2, x3)  =  convertD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
s(x1)  =  s(x1)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pF_in_gggaa(x1, x2, x3, x4, x5)  =  pF_in_gggaa(x1, x2, x3)
U17_gggaa(x1, x2, x3, x4, x5, x6)  =  U17_gggaa(x1, x2, x3, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5)  =  pC_in_gggaa(x1, x2, x3)
U23_gggaa(x1, x2, x3, x4, x5, x6)  =  U23_gggaa(x1, x2, x3, x6)
U24_gggaa(x1, x2, x3, x4, x5, x6)  =  U24_gggaa(x1, x2, x3, x4, x6)
pR_in_ag(x1, x2)  =  pR_in_ag(x2)
pR_out_ag(x1, x2)  =  pR_out_ag(x1, x2)
pC_out_gggaa(x1, x2, x3, x4, x5)  =  pC_out_gggaa(x1, x2, x3, x4, x5)
U18_gggaa(x1, x2, x3, x4, x5, x6)  =  U18_gggaa(x1, x2, x3, x4, x6)
pN_in_ag(x1, x2)  =  pN_in_ag(x2)
pN_out_ag(x1, x2)  =  pN_out_ag(x1, x2)
pF_out_gggaa(x1, x2, x3, x4, x5)  =  pF_out_gggaa(x1, x2, x3, x4, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
timesG_in_gga(x1, x2, x3)  =  timesG_in_gga(x1, x2)
timesG_out_gga(x1, x2, x3)  =  timesG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U13_ggaa(x1, x2, x3, x4, x5)  =  U13_ggaa(x1, x2, x5)
U14_ggaa(x1, x2, x3, x4, x5)  =  U14_ggaa(x1, x2, x3, x5)
plusI_in_gga(x1, x2, x3)  =  plusI_in_gga(x1, x2)
plusI_out_gga(x1, x2, x3)  =  plusI_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pJ_in_ggaa(x1, x2, x3, x4)  =  pJ_in_ggaa(x1, x2)
U15_ggaa(x1, x2, x3, x4, x5)  =  U15_ggaa(x1, x2, x5)
U16_ggaa(x1, x2, x3, x4, x5)  =  U16_ggaa(x1, x2, x3, x5)
pM_in_ag(x1, x2)  =  pM_in_ag(x2)
pM_out_ag(x1, x2)  =  pM_out_ag(x1, x2)
pJ_out_ggaa(x1, x2, x3, x4)  =  pJ_out_ggaa(x1, x2, x3, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pL_in_ggaa(x1, x2, x3, x4)  =  pL_in_ggaa(x1, x2)
U19_ggaa(x1, x2, x3, x4, x5)  =  U19_ggaa(x1, x2, x5)
U20_ggaa(x1, x2, x3, x4, x5)  =  U20_ggaa(x1, x2, x3, x5)
plusO_in_gga(x1, x2, x3)  =  plusO_in_gga(x1, x2)
plusO_out_gga(x1, x2, x3)  =  plusO_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
pP_in_ggaa(x1, x2, x3, x4)  =  pP_in_ggaa(x1, x2)
U21_ggaa(x1, x2, x3, x4, x5)  =  U21_ggaa(x1, x2, x5)
U22_ggaa(x1, x2, x3, x4, x5)  =  U22_ggaa(x1, x2, x3, x5)
pQ_in_ag(x1, x2)  =  pQ_in_ag(x2)
pQ_out_ag(x1, x2)  =  pQ_out_ag(x1, x2)
pP_out_ggaa(x1, x2, x3, x4)  =  pP_out_ggaa(x1, x2, x3, x4)
pL_out_ggaa(x1, x2, x3, x4)  =  pL_out_ggaa(x1, x2, x3, x4)
pB_out_ggaa(x1, x2, x3, x4)  =  pB_out_ggaa(x1, x2, x3, x4)
CONVERTA_IN_GGA(x1, x2, x3)  =  CONVERTA_IN_GGA(x1, x2)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
CONVERTD_IN_GGA(x1, x2, x3)  =  CONVERTD_IN_GGA(x1, x2)
PE_IN_GGAA(x1, x2, x3, x4)  =  PE_IN_GGAA(x1, x2)
PF_IN_GGGAA(x1, x2, x3, x4, x5)  =  PF_IN_GGGAA(x1, x2, x3)
PC_IN_GGGAA(x1, x2, x3, x4, x5)  =  PC_IN_GGGAA(x1, x2, x3)

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:

CONVERTA_IN_GGA(.(0, T29), T16, T18) → PB_IN_GGAA(T29, T16, X19, T18)
PB_IN_GGAA(T29, T16, T31, T18) → CONVERTD_IN_GGA(T29, T16, T31)
CONVERTD_IN_GGA(.(0, T52), T41, X75) → PE_IN_GGAA(T52, T41, X74, X75)
PE_IN_GGAA(T52, T41, T54, X75) → CONVERTD_IN_GGA(T52, T41, T54)
CONVERTD_IN_GGA(.(s(T120), T121), T106, X228) → PF_IN_GGGAA(T120, T121, T106, X227, X228)
PF_IN_GGGAA(T120, T121, T106, T122, X228) → CONVERTA_IN_GGA(.(T120, T121), T106, T122)
CONVERTA_IN_GGA(.(s(T218), T219), T202, T204) → PC_IN_GGGAA(T218, T219, T202, X370, T204)
PC_IN_GGGAA(T218, T219, T202, T220, T204) → CONVERTA_IN_GGA(.(T218, T219), T202, T220)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
0  =  0
s(x1)  =  s(x1)
CONVERTA_IN_GGA(x1, x2, x3)  =  CONVERTA_IN_GGA(x1, x2)
PB_IN_GGAA(x1, x2, x3, x4)  =  PB_IN_GGAA(x1, x2)
CONVERTD_IN_GGA(x1, x2, x3)  =  CONVERTD_IN_GGA(x1, x2)
PE_IN_GGAA(x1, x2, x3, x4)  =  PE_IN_GGAA(x1, x2)
PF_IN_GGGAA(x1, x2, x3, x4, x5)  =  PF_IN_GGGAA(x1, x2, x3)
PC_IN_GGGAA(x1, x2, x3, x4, x5)  =  PC_IN_GGGAA(x1, x2, x3)

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:

CONVERTA_IN_GGA(.(0, T29), T16) → PB_IN_GGAA(T29, T16)
PB_IN_GGAA(T29, T16) → CONVERTD_IN_GGA(T29, T16)
CONVERTD_IN_GGA(.(0, T52), T41) → PE_IN_GGAA(T52, T41)
PE_IN_GGAA(T52, T41) → CONVERTD_IN_GGA(T52, T41)
CONVERTD_IN_GGA(.(s(T120), T121), T106) → PF_IN_GGGAA(T120, T121, T106)
PF_IN_GGGAA(T120, T121, T106) → CONVERTA_IN_GGA(.(T120, T121), T106)
CONVERTA_IN_GGA(.(s(T218), T219), T202) → PC_IN_GGGAA(T218, T219, T202)
PC_IN_GGGAA(T218, T219, T202) → CONVERTA_IN_GGA(.(T218, T219), T202)

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:

CONVERTA_IN_GGA(.(0, T29), T16) → PB_IN_GGAA(T29, T16)
PB_IN_GGAA(T29, T16) → CONVERTD_IN_GGA(T29, T16)
CONVERTD_IN_GGA(.(0, T52), T41) → PE_IN_GGAA(T52, T41)
PE_IN_GGAA(T52, T41) → CONVERTD_IN_GGA(T52, T41)
CONVERTD_IN_GGA(.(s(T120), T121), T106) → PF_IN_GGGAA(T120, T121, T106)
PF_IN_GGGAA(T120, T121, T106) → CONVERTA_IN_GGA(.(T120, T121), T106)
CONVERTA_IN_GGA(.(s(T218), T219), T202) → PC_IN_GGGAA(T218, T219, T202)
PC_IN_GGGAA(T218, T219, T202) → CONVERTA_IN_GGA(.(T218, T219), T202)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = x₁ + x₂   
POL(0) = 1   
POL(CONVERTA_IN_GGA(x₁, x₂)) = 1 + 2·x₁ + x₂   
POL(CONVERTD_IN_GGA(x₁, x₂)) = 1 + 2·x₁ + x₂   
POL(PB_IN_GGAA(x₁, x₂)) = 2 + 2·x₁ + x₂   
POL(PC_IN_GGGAA(x₁, x₂, x₃)) = 2 + 2·x₁ + 2·x₂ + x₃   
POL(PE_IN_GGAA(x₁, x₂)) = 2 + 2·x₁ + x₂   
POL(PF_IN_GGGAA(x₁, x₂, x₃)) = 2 + 2·x₁ + 2·x₂ + x₃   
POL(s(x₁)) = 1 + 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