Left Termination proof of /tmp/tmpHekA93/inorder-oi.pl

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

0 Prolog

↳1 PrologToTRSTransformerProof (⇒, 596 ms)

↳2 QTRS

↳3 DependencyPairsProof (⇔, 57 ms)

↳4 QDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 QDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔, 0 ms)

        ↳11 YES

    ↳12 QDP

        ↳13 UsableRulesProof (⇔, 0 ms)

        ↳14 QDP

        ↳15 QDPSizeChangeProof (⇔, 0 ms)

        ↳16 YES

    ↳17 QDP

        ↳18 QDPOrderProof (⇔, 5162 ms)

        ↳19 QDP

        ↳20 DependencyGraphProof (⇔, 0 ms)

        ↳21 QDP

        ↳22 QDPOrderProof (⇔, 1381 ms)

        ↳23 QDP

        ↳24 DependencyGraphProof (⇔, 0 ms)

        ↳25 TRUE

(0) Obligation:

Clauses:

in_order(void, L) :- ','(!, eq(L, [])).
in_order(T, Xs) :- ','(value(T, X), ','(app(Ls, .(X, Rs), Xs), ','(left(T, L), ','(in_order(L, Ls), ','(right(T, R), in_order(R, Rs)))))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
left(void, void).
left(node(L, X1, X2), L).
right(void, void).
right(node(X3, X4, R), R).
value(void, X5).
value(node(X6, X, X7), X).
eq(X, X).

Query: in_order(a,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: in_order(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: in_order(T1, T2), SCOPE: 1, CLAUSE: 0 | in_order(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(!_1, eq(T5, [])) | in_order(T1, T5), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: in_order(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX10 is free\nin_order(T1, T2) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: eq(T5, [])\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: eq(T5, []), SCOPE: 2, CLAUSE: 10\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(value(T20, X31), ','(app(X32, .(X31, X33), T19), ','(left(T20, X34), ','(in_order(X34, X32), ','(right(T20, X35), in_order(X35, X33))))))\n\nT19 is ground\nX10 is free\nX31 is free\nX32 is free\nX33 is free\nX34 is free\nX35 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(value(T20, X31), ','(app(X32, .(X31, X33), T19), ','(left(T20, X34), ','(in_order(X34, X32), ','(right(T20, X35), in_order(X35, X33)))))), SCOPE: 3, CLAUSE: 8 | ','(value(T20, X31), ','(app(X32, .(X31, X33), T19), ','(left(T20, X34), ','(in_order(X34, X32), ','(right(T20, X35), in_order(X35, X33)))))), SCOPE: 3, CLAUSE: 9\n\nT19 is ground\nX10 is free\nX31 is free\nX32 is free\nX33 is free\nX34 is free\nX35 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(value(T20, X31), ','(app(X32, .(X31, X33), T19), ','(left(T20, X34), ','(in_order(X34, X32), ','(right(T20, X35), in_order(X35, X33)))))), SCOPE: 3, CLAUSE: 8\n\nT19 is ground\nX10 is free\nX31 is free\nX32 is free\nX33 is free\nX34 is free\nX35 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(value(T20, X31), ','(app(X32, .(X31, X33), T19), ','(left(T20, X34), ','(in_order(X34, X32), ','(right(T20, X35), in_order(X35, X33)))))), SCOPE: 3, CLAUSE: 9\n\nT19 is ground\nX10 is free\nX31 is free\nX32 is free\nX33 is free\nX34 is free\nX35 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(app(X32, .(X51, X33), T19), ','(left(void, X34), ','(in_order(X34, X32), ','(right(void, X35), in_order(X35, X33)))))\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nX34 is free\nX35 is free\nX51 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: app(X32, .(X51, X33), T19)\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nX51 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(left(void, X34), ','(in_order(X34, T29), ','(right(void, X35), in_order(X35, T31))))\n\nT29 is ground\nT31 is ground\nX34 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: app(X32, .(X51, X33), T19), SCOPE: 4, CLAUSE: 2 | app(X32, .(X51, X33), T19), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nX51 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: app(X32, .(X51, X33), T19), SCOPE: 4, CLAUSE: 2\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nX51 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: app(X32, .(X51, X33), T19), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nX51 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: app(X100, .(X101, X102), T51)\n\nT50 is ground\nT51 is ground\nX10 is free\nX100 is free\nX101 is free\nX102 is free\nin_order(T1, .(T50, T51)) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: app(X100, .(X101, X102), T51), SCOPE: 5, CLAUSE: 2 | app(X100, .(X101, X102), T51), SCOPE: 5, CLAUSE: 3\n\nT50 is ground\nT51 is ground\nX10 is free\nX100 is free\nX101 is free\nX102 is free\nin_order(T1, .(T50, T51)) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: app(X100, .(X101, X102), T51), SCOPE: 5, CLAUSE: 2\n\nT50 is ground\nT51 is ground\nX10 is free\nX100 is free\nX101 is free\nX102 is free\nin_order(T1, .(T50, T51)) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: app(X100, .(X101, X102), T51), SCOPE: 5, CLAUSE: 3\n\nT50 is ground\nT51 is ground\nX10 is free\nX100 is free\nX101 is free\nX102 is free\nin_order(T1, .(T50, T51)) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: app(X145, .(X146, X147), T71)\n\nT50 is ground\nT70 is ground\nT71 is ground\nX10 is free\nX145 is free\nX146 is free\nX147 is free\nin_order(T1, .(T50, .(T70, T71))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: app(X145, .(X146, X147), T71), SCOPE: 6, CLAUSE: 2 | app(X145, .(X146, X147), T71), SCOPE: 6, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT71 is ground\nX10 is free\nX145 is free\nX146 is free\nX147 is free\nin_order(T1, .(T50, .(T70, T71))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: app(X145, .(X146, X147), T71), SCOPE: 6, CLAUSE: 2\n\nT50 is ground\nT70 is ground\nT71 is ground\nX10 is free\nX145 is free\nX146 is free\nX147 is free\nin_order(T1, .(T50, .(T70, T71))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: app(X145, .(X146, X147), T71), SCOPE: 6, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT71 is ground\nX10 is free\nX145 is free\nX146 is free\nX147 is free\nin_order(T1, .(T50, .(T70, T71))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: app(X190, .(X191, X192), T91)\n\nT50 is ground\nT70 is ground\nT90 is ground\nT91 is ground\nX10 is free\nX190 is free\nX191 is free\nX192 is free\nin_order(T1, .(T50, .(T70, .(T90, T91)))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: app(X190, .(X191, X192), T91), SCOPE: 7, CLAUSE: 2 | app(X190, .(X191, X192), T91), SCOPE: 7, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT91 is ground\nX10 is free\nX190 is free\nX191 is free\nX192 is free\nin_order(T1, .(T50, .(T70, .(T90, T91)))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: app(X190, .(X191, X192), T91), SCOPE: 7, CLAUSE: 2\n\nT50 is ground\nT70 is ground\nT90 is ground\nT91 is ground\nX10 is free\nX190 is free\nX191 is free\nX192 is free\nin_order(T1, .(T50, .(T70, .(T90, T91)))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: app(X190, .(X191, X192), T91), SCOPE: 7, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT91 is ground\nX10 is free\nX190 is free\nX191 is free\nX192 is free\nin_order(T1, .(T50, .(T70, .(T90, T91)))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: app(X235, .(X236, X237), T111)\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT111 is ground\nX10 is free\nX235 is free\nX236 is free\nX237 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, T111))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: app(X235, .(X236, X237), T111), SCOPE: 8, CLAUSE: 2 | app(X235, .(X236, X237), T111), SCOPE: 8, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT111 is ground\nX10 is free\nX235 is free\nX236 is free\nX237 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, T111))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: app(X235, .(X236, X237), T111), SCOPE: 8, CLAUSE: 2\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT111 is ground\nX10 is free\nX235 is free\nX236 is free\nX237 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, T111))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: app(X235, .(X236, X237), T111), SCOPE: 8, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT111 is ground\nX10 is free\nX235 is free\nX236 is free\nX237 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, T111))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: app(X280, .(X281, X282), T131)\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT131 is ground\nX10 is free\nX280 is free\nX281 is free\nX282 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, T131)))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: app(X280, .(X281, X282), T131), SCOPE: 9, CLAUSE: 2 | app(X280, .(X281, X282), T131), SCOPE: 9, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT131 is ground\nX10 is free\nX280 is free\nX281 is free\nX282 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, T131)))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: app(X280, .(X281, X282), T131), SCOPE: 9, CLAUSE: 2\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT131 is ground\nX10 is free\nX280 is free\nX281 is free\nX282 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, T131)))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: app(X280, .(X281, X282), T131), SCOPE: 9, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT131 is ground\nX10 is free\nX280 is free\nX281 is free\nX282 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, T131)))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: app(X325, .(X326, X327), T151)\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT151 is ground\nX10 is free\nX325 is free\nX326 is free\nX327 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, T151))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: app(X325, .(X326, X327), T151), SCOPE: 10, CLAUSE: 2 | app(X325, .(X326, X327), T151), SCOPE: 10, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT151 is ground\nX10 is free\nX325 is free\nX326 is free\nX327 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, T151))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: app(X325, .(X326, X327), T151), SCOPE: 10, CLAUSE: 2\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT151 is ground\nX10 is free\nX325 is free\nX326 is free\nX327 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, T151))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: app(X325, .(X326, X327), T151), SCOPE: 10, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT151 is ground\nX10 is free\nX325 is free\nX326 is free\nX327 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, T151))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: app(X370, .(X371, X372), T171)\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT170 is ground\nT171 is ground\nX10 is free\nX370 is free\nX371 is free\nX372 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, T171)))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: app(X370, .(X371, X372), T171), SCOPE: 11, CLAUSE: 2 | app(X370, .(X371, X372), T171), SCOPE: 11, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT170 is ground\nT171 is ground\nX10 is free\nX370 is free\nX371 is free\nX372 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, T171)))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: app(X370, .(X371, X372), T171), SCOPE: 11, CLAUSE: 2\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT170 is ground\nT171 is ground\nX10 is free\nX370 is free\nX371 is free\nX372 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, T171)))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: app(X370, .(X371, X372), T171), SCOPE: 11, CLAUSE: 3\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT170 is ground\nT171 is ground\nX10 is free\nX370 is free\nX371 is free\nX372 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, T171)))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: app(X415, .(X416, X417), T191)\n\nT50 is ground\nT70 is ground\nT90 is ground\nT110 is ground\nT130 is ground\nT150 is ground\nT170 is ground\nT190 is ground\nT191 is ground\nX10 is free\nX415 is free\nX416 is free\nX417 is free\nin_order(T1, .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: app(X415, .(X416, X417), T191)\n\nT191 is ground\nX415 is free\nX416 is free\nX417 is free", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: app(X415, .(X416, X417), T191), SCOPE: 12, CLAUSE: 2 | app(X415, .(X416, X417), T191), SCOPE: 12, CLAUSE: 3\n\nT191 is ground\nX415 is free\nX416 is free\nX417 is free", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: app(X415, .(X416, X417), T191), SCOPE: 12, CLAUSE: 2\n\nT191 is ground\nX415 is free\nX416 is free\nX417 is free", fontsize=16, style=filled, fillcolor=lightyellow];
346 [label="346: app(X415, .(X416, X417), T191), SCOPE: 12, CLAUSE: 3\n\nT191 is ground\nX415 is free\nX416 is free\nX417 is free", fontsize=16, style=filled, fillcolor=lightyellow];
351 [label="351: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
352 [label="352: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
354 [label="354: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
359 [label="359: app(X466, .(X467, X468), T216)\n\nT216 is ground\nX466 is free\nX467 is free\nX468 is free", fontsize=16, style=filled, fillcolor=lightyellow];
360 [label="360: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
367 [label="367: ','(left(void, X34), ','(in_order(X34, T29), ','(right(void, X35), in_order(X35, T31)))), SCOPE: 13, CLAUSE: 4 | ','(left(void, X34), ','(in_order(X34, T29), ','(right(void, X35), in_order(X35, T31)))), SCOPE: 13, CLAUSE: 5\n\nT29 is ground\nT31 is ground\nX34 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: ','(left(void, X34), ','(in_order(X34, T29), ','(right(void, X35), in_order(X35, T31)))), SCOPE: 13, CLAUSE: 4\n\nT29 is ground\nT31 is ground\nX34 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: ','(left(void, X34), ','(in_order(X34, T29), ','(right(void, X35), in_order(X35, T31)))), SCOPE: 13, CLAUSE: 5\n\nT29 is ground\nT31 is ground\nX34 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: ','(in_order(void, T29), ','(right(void, X35), in_order(X35, T31)))\n\nT29 is ground\nT31 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
385 [label="385: in_order(void, T29)\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: ','(right(void, X35), in_order(X35, T31))\n\nT31 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
390 [label="390: in_order(void, T29), SCOPE: 14, CLAUSE: 0 | in_order(void, T29), SCOPE: 14, CLAUSE: 1\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
391 [label="391: ','(!_14, eq(T228, [])) | in_order(void, T228), SCOPE: 14, CLAUSE: 1\n\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
392 [label="392: eq(T228, [])\n\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
393 [label="393: eq(T228, []), SCOPE: 15, CLAUSE: 10\n\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
395 [label="395: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
396 [label="396: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
399 [label="399: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
401 [label="401: ','(right(void, X35), in_order(X35, T31)), SCOPE: 16, CLAUSE: 6 | ','(right(void, X35), in_order(X35, T31)), SCOPE: 16, CLAUSE: 7\n\nT31 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
410 [label="410: ','(right(void, X35), in_order(X35, T31)), SCOPE: 16, CLAUSE: 6\n\nT31 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
411 [label="411: ','(right(void, X35), in_order(X35, T31)), SCOPE: 16, CLAUSE: 7\n\nT31 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
412 [label="412: in_order(void, T31)\n\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
417 [label="417: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
418 [label="418: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
422 [label="422: ','(app(X32, .(T245, X33), T19), ','(left(node(T246, T245, T247), X34), ','(in_order(X34, X32), ','(right(node(T246, T245, T247), X35), in_order(X35, X33)))))\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nX34 is free\nX35 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
423 [label="423: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
438 [label="438: app(X32, .(T245, X33), T19)\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
439 [label="439: ','(left(node(T254, T255, T256), X34), ','(in_order(X34, T252), ','(right(node(T254, T255, T256), X35), in_order(X35, T253))))\n\nT252 is ground\nT255 is ground\nT253 is ground\nX34 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
442 [label="442: app(X32, .(T245, X33), T19), SCOPE: 17, CLAUSE: 2 | app(X32, .(T245, X33), T19), SCOPE: 17, CLAUSE: 3\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
443 [label="443: app(X32, .(T245, X33), T19), SCOPE: 17, CLAUSE: 2\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
444 [label="444: app(X32, .(T245, X33), T19), SCOPE: 17, CLAUSE: 3\n\nT19 is ground\nX10 is free\nX32 is free\nX33 is free\nin_order(T1, T19) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
447 [label="447: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
448 [label="448: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
449 [label="449: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
463 [label="463: app(X542, .(T281, X543), T280)\n\nT279 is ground\nT280 is ground\nX10 is free\nX542 is free\nX543 is free\nin_order(T1, .(T279, T280)) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
464 [label="464: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
467 [label="467: app(X542, .(T281, X543), T280), SCOPE: 18, CLAUSE: 2 | app(X542, .(T281, X543), T280), SCOPE: 18, CLAUSE: 3\n\nT279 is ground\nT280 is ground\nX10 is free\nX542 is free\nX543 is free\nin_order(T1, .(T279, T280)) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
478 [label="478: app(X542, .(T281, X543), T280), SCOPE: 18, CLAUSE: 2\n\nT279 is ground\nT280 is ground\nX10 is free\nX542 is free\nX543 is free\nin_order(T1, .(T279, T280)) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
479 [label="479: app(X542, .(T281, X543), T280), SCOPE: 18, CLAUSE: 3\n\nT279 is ground\nT280 is ground\nX10 is free\nX542 is free\nX543 is free\nin_order(T1, .(T279, T280)) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
483 [label="483: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
484 [label="484: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
485 [label="485: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
488 [label="488: app(X577, .(T305, X578), T304)\n\nT279 is ground\nT303 is ground\nT304 is ground\nX10 is free\nX577 is free\nX578 is free\nin_order(T1, .(T279, .(T303, T304))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
489 [label="489: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
501 [label="501: app(X577, .(T305, X578), T304), SCOPE: 19, CLAUSE: 2 | app(X577, .(T305, X578), T304), SCOPE: 19, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT304 is ground\nX10 is free\nX577 is free\nX578 is free\nin_order(T1, .(T279, .(T303, T304))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
502 [label="502: app(X577, .(T305, X578), T304), SCOPE: 19, CLAUSE: 2\n\nT279 is ground\nT303 is ground\nT304 is ground\nX10 is free\nX577 is free\nX578 is free\nin_order(T1, .(T279, .(T303, T304))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
503 [label="503: app(X577, .(T305, X578), T304), SCOPE: 19, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT304 is ground\nX10 is free\nX577 is free\nX578 is free\nin_order(T1, .(T279, .(T303, T304))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
504 [label="504: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
505 [label="505: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
506 [label="506: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
508 [label="508: app(X612, .(T329, X613), T328)\n\nT279 is ground\nT303 is ground\nT327 is ground\nT328 is ground\nX10 is free\nX612 is free\nX613 is free\nin_order(T1, .(T279, .(T303, .(T327, T328)))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
509 [label="509: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
513 [label="513: app(X612, .(T329, X613), T328), SCOPE: 20, CLAUSE: 2 | app(X612, .(T329, X613), T328), SCOPE: 20, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT328 is ground\nX10 is free\nX612 is free\nX613 is free\nin_order(T1, .(T279, .(T303, .(T327, T328)))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
514 [label="514: app(X612, .(T329, X613), T328), SCOPE: 20, CLAUSE: 2\n\nT279 is ground\nT303 is ground\nT327 is ground\nT328 is ground\nX10 is free\nX612 is free\nX613 is free\nin_order(T1, .(T279, .(T303, .(T327, T328)))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
515 [label="515: app(X612, .(T329, X613), T328), SCOPE: 20, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT328 is ground\nX10 is free\nX612 is free\nX613 is free\nin_order(T1, .(T279, .(T303, .(T327, T328)))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
519 [label="519: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
520 [label="520: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
521 [label="521: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
522 [label="522: app(X647, .(T353, X648), T352)\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT352 is ground\nX10 is free\nX647 is free\nX648 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, T352))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
523 [label="523: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
526 [label="526: app(X647, .(T353, X648), T352), SCOPE: 21, CLAUSE: 2 | app(X647, .(T353, X648), T352), SCOPE: 21, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT352 is ground\nX10 is free\nX647 is free\nX648 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, T352))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
527 [label="527: app(X647, .(T353, X648), T352), SCOPE: 21, CLAUSE: 2\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT352 is ground\nX10 is free\nX647 is free\nX648 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, T352))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
528 [label="528: app(X647, .(T353, X648), T352), SCOPE: 21, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT352 is ground\nX10 is free\nX647 is free\nX648 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, T352))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
531 [label="531: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
532 [label="532: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
533 [label="533: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
535 [label="535: app(X682, .(T377, X683), T376)\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT376 is ground\nX10 is free\nX682 is free\nX683 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, T376)))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
536 [label="536: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
541 [label="541: app(X682, .(T377, X683), T376), SCOPE: 22, CLAUSE: 2 | app(X682, .(T377, X683), T376), SCOPE: 22, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT376 is ground\nX10 is free\nX682 is free\nX683 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, T376)))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
542 [label="542: app(X682, .(T377, X683), T376), SCOPE: 22, CLAUSE: 2\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT376 is ground\nX10 is free\nX682 is free\nX683 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, T376)))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
543 [label="543: app(X682, .(T377, X683), T376), SCOPE: 22, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT376 is ground\nX10 is free\nX682 is free\nX683 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, T376)))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
545 [label="545: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
546 [label="546: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
547 [label="547: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
548 [label="548: app(X717, .(T401, X718), T400)\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT400 is ground\nX10 is free\nX717 is free\nX718 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, T400))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
549 [label="549: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
550 [label="550: app(X717, .(T401, X718), T400), SCOPE: 23, CLAUSE: 2 | app(X717, .(T401, X718), T400), SCOPE: 23, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT400 is ground\nX10 is free\nX717 is free\nX718 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, T400))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
551 [label="551: app(X717, .(T401, X718), T400), SCOPE: 23, CLAUSE: 2\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT400 is ground\nX10 is free\nX717 is free\nX718 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, T400))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
552 [label="552: app(X717, .(T401, X718), T400), SCOPE: 23, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT400 is ground\nX10 is free\nX717 is free\nX718 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, T400))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
553 [label="553: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
554 [label="554: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
555 [label="555: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
611 [label="611: app(X752, .(T425, X753), T424)\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT423 is ground\nT424 is ground\nX10 is free\nX752 is free\nX753 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, T424)))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
612 [label="612: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
801 [label="801: app(X752, .(T425, X753), T424), SCOPE: 24, CLAUSE: 2 | app(X752, .(T425, X753), T424), SCOPE: 24, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT423 is ground\nT424 is ground\nX10 is free\nX752 is free\nX753 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, T424)))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
918 [label="918: app(X752, .(T425, X753), T424), SCOPE: 24, CLAUSE: 2\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT423 is ground\nT424 is ground\nX10 is free\nX752 is free\nX753 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, T424)))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
925 [label="925: app(X752, .(T425, X753), T424), SCOPE: 24, CLAUSE: 3\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT423 is ground\nT424 is ground\nX10 is free\nX752 is free\nX753 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, T424)))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
1225 [label="1225: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
1226 [label="1226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
1227 [label="1227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
1228 [label="1228: app(X787, .(T449, X788), T448)\n\nT279 is ground\nT303 is ground\nT327 is ground\nT351 is ground\nT375 is ground\nT399 is ground\nT423 is ground\nT447 is ground\nT448 is ground\nX10 is free\nX787 is free\nX788 is free\nin_order(T1, .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) !=? in_order(void, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
1229 [label="1229: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
1230 [label="1230: app(X787, .(T449, X788), T448)\n\nT448 is ground\nX787 is free\nX788 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1231 [label="1231: app(X787, .(T449, X788), T448), SCOPE: 25, CLAUSE: 2 | app(X787, .(T449, X788), T448), SCOPE: 25, CLAUSE: 3\n\nT448 is ground\nX787 is free\nX788 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1232 [label="1232: app(X787, .(T449, X788), T448), SCOPE: 25, CLAUSE: 2\n\nT448 is ground\nX787 is free\nX788 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1233 [label="1233: app(X787, .(T449, X788), T448), SCOPE: 25, CLAUSE: 3\n\nT448 is ground\nX787 is free\nX788 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1234 [label="1234: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
1235 [label="1235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
1236 [label="1236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
1237 [label="1237: app(X826, .(T478, X827), T477)\n\nT477 is ground\nX826 is free\nX827 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1238 [label="1238: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
1239 [label="1239: ','(left(node(T254, T255, T256), X34), ','(in_order(X34, T252), ','(right(node(T254, T255, T256), X35), in_order(X35, T253)))), SCOPE: 26, CLAUSE: 4 | ','(left(node(T254, T255, T256), X34), ','(in_order(X34, T252), ','(right(node(T254, T255, T256), X35), in_order(X35, T253)))), SCOPE: 26, CLAUSE: 5\n\nT252 is ground\nT255 is ground\nT253 is ground\nX34 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1240 [label="1240: ','(left(node(T254, T255, T256), X34), ','(in_order(X34, T252), ','(right(node(T254, T255, T256), X35), in_order(X35, T253)))), SCOPE: 26, CLAUSE: 5\n\nT252 is ground\nT255 is ground\nT253 is ground\nX34 is free\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1241 [label="1241: ','(in_order(T496, T252), ','(right(node(T496, T494, T497), X35), in_order(X35, T253)))\n\nT252 is ground\nT253 is ground\nT494 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1242 [label="1242: in_order(T496, T252)\n\nT252 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
1243 [label="1243: ','(right(node(T499, T494, T500), X35), in_order(X35, T253))\n\nT253 is ground\nT494 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1244 [label="1244: ','(right(node(T499, T494, T500), X35), in_order(X35, T253)), SCOPE: 27, CLAUSE: 6 | ','(right(node(T499, T494, T500), X35), in_order(X35, T253)), SCOPE: 27, CLAUSE: 7\n\nT253 is ground\nT494 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1245 [label="1245: ','(right(node(T499, T494, T500), X35), in_order(X35, T253)), SCOPE: 27, CLAUSE: 7\n\nT253 is ground\nT494 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
1246 [label="1246: in_order(T514, T253)\n\nT253 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
1247 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 1247 [arrowhead = none ];
1247 -> 6;

1248 [label="EVAL with clause\nin_order(void, X10) :- ','(!_1, eq(X10, [])).\nand substitutionT1 -> void,\nT2 -> T5,\nX10 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 1248 [arrowhead = none ];
1248 -> 9;

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

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

1251 [label="ONLY EVAL with clause\nin_order(X29, X30) :- ','(value(X29, X31), ','(app(X32, .(X31, X33), X30), ','(left(X29, X34), ','(in_order(X34, X32), ','(right(X29, X35), in_order(X35, X33)))))).\nand substitutionT1 -> T20,\nX29 -> T20,\nT2 -> T19,\nX30 -> T19,\nT18 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 1251 [arrowhead = none ];
1251 -> 40;

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

1253 [label="EVAL with clause\neq(X13, X13).\nand substitutionT5 -> [],\nX13 -> [],\nT8 -> []", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 1253 [arrowhead = none ];
1253 -> 21;

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

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

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

1257 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
41 -> 1257 [arrowhead = none ];
1257 -> 42;

1258 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
41 -> 1258 [arrowhead = none ];
1258 -> 43;

1259 [label="EVAL with clause\nvalue(void, X50).\nand substitutionT20 -> void,\nX31 -> X51,\nX50 -> X51", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 1259 [arrowhead = none ];
1259 -> 48;

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

1261 [label="EVAL with clause\nvalue(node(X502, X503, X504), X503).\nand substitutionX502 -> T246,\nX503 -> T245,\nX504 -> T247,\nT20 -> node(T246, T245, T247),\nX31 -> T245,\nT243 -> T245,\nT242 -> T246,\nT244 -> T247", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 1261 [arrowhead = none ];
1261 -> 422;

1262 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 1262 [arrowhead = none ];
1262 -> 423;

1263 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
48 -> 1263 [arrowhead = none ];
1263 -> 56;

1264 [label="SPLIT 2\nnew knowledge:\nT29 is ground\nT30 is ground\nT31 is ground\nT19 is ground\nreplacements:X32 -> T29,\nX51 -> T30,\nX33 -> T31", fontsize=14, style = filled, fillcolor = violet];
48 -> 1264 [arrowhead = none ];
1264 -> 57;

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

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

1267 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
61 -> 1267 [arrowhead = none ];
1267 -> 72;

1268 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
61 -> 1268 [arrowhead = none ];
1268 -> 73;

1269 [label="EVAL with clause\napp([], X76, X76).\nand substitutionX32 -> [],\nX51 -> T44,\nX33 -> T45,\nX76 -> .(T44, T45),\nX77 -> T44,\nX78 -> T45,\nT19 -> .(T44, T45)", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 1269 [arrowhead = none ];
1269 -> 77;

1270 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 1270 [arrowhead = none ];
1270 -> 78;

1271 [label="EVAL with clause\napp(.(X95, X96), X97, .(X95, X98)) :- app(X96, X97, X98).\nand substitutionX95 -> T50,\nX96 -> X100,\nX32 -> .(T50, X100),\nX51 -> X101,\nX33 -> X102,\nX97 -> .(X101, X102),\nX99 -> T50,\nX98 -> T51,\nT19 -> .(T50, T51)", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 1271 [arrowhead = none ];
1271 -> 91;

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

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

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

1275 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
96 -> 1275 [arrowhead = none ];
1275 -> 104;

1276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
96 -> 1276 [arrowhead = none ];
1276 -> 106;

1277 [label="EVAL with clause\napp([], X121, X121).\nand substitutionX100 -> [],\nX101 -> T64,\nX102 -> T65,\nX121 -> .(T64, T65),\nX122 -> T64,\nX123 -> T65,\nT51 -> .(T64, T65)", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 1277 [arrowhead = none ];
1277 -> 107;

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

1279 [label="EVAL with clause\napp(.(X140, X141), X142, .(X140, X143)) :- app(X141, X142, X143).\nand substitutionX140 -> T70,\nX141 -> X145,\nX100 -> .(T70, X145),\nX101 -> X146,\nX102 -> X147,\nX142 -> .(X146, X147),\nX144 -> T70,\nX143 -> T71,\nT51 -> .(T70, T71)", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 1279 [arrowhead = none ];
1279 -> 117;

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

1281 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 1281 [arrowhead = none ];
1281 -> 110;

1282 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
117 -> 1282 [arrowhead = none ];
1282 -> 126;

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

1284 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 1284 [arrowhead = none ];
1284 -> 130;

1285 [label="EVAL with clause\napp([], X166, X166).\nand substitutionX145 -> [],\nX146 -> T84,\nX147 -> T85,\nX166 -> .(T84, T85),\nX167 -> T84,\nX168 -> T85,\nT71 -> .(T84, T85)", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 1285 [arrowhead = none ];
1285 -> 131;

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

1287 [label="EVAL with clause\napp(.(X185, X186), X187, .(X185, X188)) :- app(X186, X187, X188).\nand substitutionX185 -> T90,\nX186 -> X190,\nX145 -> .(T90, X190),\nX146 -> X191,\nX147 -> X192,\nX187 -> .(X191, X192),\nX189 -> T90,\nX188 -> T91,\nT71 -> .(T90, T91)", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 1287 [arrowhead = none ];
1287 -> 147;

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

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

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

1291 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
158 -> 1291 [arrowhead = none ];
1291 -> 162;

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

1293 [label="EVAL with clause\napp([], X211, X211).\nand substitutionX190 -> [],\nX191 -> T104,\nX192 -> T105,\nX211 -> .(T104, T105),\nX212 -> T104,\nX213 -> T105,\nT91 -> .(T104, T105)", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 1293 [arrowhead = none ];
1293 -> 164;

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

1295 [label="EVAL with clause\napp(.(X230, X231), X232, .(X230, X233)) :- app(X231, X232, X233).\nand substitutionX230 -> T110,\nX231 -> X235,\nX190 -> .(T110, X235),\nX191 -> X236,\nX192 -> X237,\nX232 -> .(X236, X237),\nX234 -> T110,\nX233 -> T111,\nT91 -> .(T110, T111)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 1295 [arrowhead = none ];
1295 -> 179;

1296 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
163 -> 1296 [arrowhead = none ];
1296 -> 180;

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

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

1299 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
184 -> 1299 [arrowhead = none ];
1299 -> 189;

1300 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
184 -> 1300 [arrowhead = none ];
1300 -> 190;

1301 [label="EVAL with clause\napp([], X256, X256).\nand substitutionX235 -> [],\nX236 -> T124,\nX237 -> T125,\nX256 -> .(T124, T125),\nX257 -> T124,\nX258 -> T125,\nT111 -> .(T124, T125)", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 1301 [arrowhead = none ];
1301 -> 192;

1302 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
189 -> 1302 [arrowhead = none ];
1302 -> 193;

1303 [label="EVAL with clause\napp(.(X275, X276), X277, .(X275, X278)) :- app(X276, X277, X278).\nand substitutionX275 -> T130,\nX276 -> X280,\nX235 -> .(T130, X280),\nX236 -> X281,\nX237 -> X282,\nX277 -> .(X281, X282),\nX279 -> T130,\nX278 -> T131,\nT111 -> .(T130, T131)", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 1303 [arrowhead = none ];
1303 -> 196;

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

1305 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
192 -> 1305 [arrowhead = none ];
1305 -> 194;

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

1307 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
200 -> 1307 [arrowhead = none ];
1307 -> 204;

1308 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
200 -> 1308 [arrowhead = none ];
1308 -> 205;

1309 [label="EVAL with clause\napp([], X301, X301).\nand substitutionX280 -> [],\nX281 -> T144,\nX282 -> T145,\nX301 -> .(T144, T145),\nX302 -> T144,\nX303 -> T145,\nT131 -> .(T144, T145)", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 1309 [arrowhead = none ];
1309 -> 224;

1310 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
204 -> 1310 [arrowhead = none ];
1310 -> 225;

1311 [label="EVAL with clause\napp(.(X320, X321), X322, .(X320, X323)) :- app(X321, X322, X323).\nand substitutionX320 -> T150,\nX321 -> X325,\nX280 -> .(T150, X325),\nX281 -> X326,\nX282 -> X327,\nX322 -> .(X326, X327),\nX324 -> T150,\nX323 -> T151,\nT131 -> .(T150, T151)", fontsize=14, style = filled, fillcolor = lightblue];
205 -> 1311 [arrowhead = none ];
1311 -> 237;

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

1313 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
224 -> 1313 [arrowhead = none ];
1313 -> 227;

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

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

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

1317 [label="EVAL with clause\napp([], X346, X346).\nand substitutionX325 -> [],\nX326 -> T164,\nX327 -> T165,\nX346 -> .(T164, T165),\nX347 -> T164,\nX348 -> T165,\nT151 -> .(T164, T165)", fontsize=14, style = filled, fillcolor = lightblue];
250 -> 1317 [arrowhead = none ];
1317 -> 253;

1318 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
250 -> 1318 [arrowhead = none ];
1318 -> 254;

1319 [label="EVAL with clause\napp(.(X365, X366), X367, .(X365, X368)) :- app(X366, X367, X368).\nand substitutionX365 -> T170,\nX366 -> X370,\nX325 -> .(T170, X370),\nX326 -> X371,\nX327 -> X372,\nX367 -> .(X371, X372),\nX369 -> T170,\nX368 -> T171,\nT151 -> .(T170, T171)", fontsize=14, style = filled, fillcolor = lightblue];
252 -> 1319 [arrowhead = none ];
1319 -> 264;

1320 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
252 -> 1320 [arrowhead = none ];
1320 -> 265;

1321 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
253 -> 1321 [arrowhead = none ];
1321 -> 255;

1322 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
264 -> 1322 [arrowhead = none ];
1322 -> 277;

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

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

1325 [label="EVAL with clause\napp([], X391, X391).\nand substitutionX370 -> [],\nX371 -> T184,\nX372 -> T185,\nX391 -> .(T184, T185),\nX392 -> T184,\nX393 -> T185,\nT171 -> .(T184, T185)", fontsize=14, style = filled, fillcolor = lightblue];
283 -> 1325 [arrowhead = none ];
1325 -> 285;

1326 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
283 -> 1326 [arrowhead = none ];
1326 -> 286;

1327 [label="EVAL with clause\napp(.(X410, X411), X412, .(X410, X413)) :- app(X411, X412, X413).\nand substitutionX410 -> T190,\nX411 -> X415,\nX370 -> .(T190, X415),\nX371 -> X416,\nX372 -> X417,\nX412 -> .(X416, X417),\nX414 -> T190,\nX413 -> T191,\nT171 -> .(T190, T191)", fontsize=14, style = filled, fillcolor = lightblue];
284 -> 1327 [arrowhead = none ];
1327 -> 305;

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

1329 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
285 -> 1329 [arrowhead = none ];
1329 -> 288;

1330 [label="GENERALIZATION\nT196 <-- .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))\n\nNew Knowledge:\nT196 is ground", fontsize=14, style = filled, fillcolor = violet];
305 -> 1330 [arrowhead = none ];
1330 -> 328;

1331 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
328 -> 1331 [arrowhead = none ];
1331 -> 335;

1332 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
335 -> 1332 [arrowhead = none ];
1332 -> 336;

1333 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
335 -> 1333 [arrowhead = none ];
1333 -> 346;

1334 [label="EVAL with clause\napp([], X442, X442).\nand substitutionX415 -> [],\nX416 -> T209,\nX417 -> T210,\nX442 -> .(T209, T210),\nX443 -> T209,\nX444 -> T210,\nT191 -> .(T209, T210)", fontsize=14, style = filled, fillcolor = lightblue];
336 -> 1334 [arrowhead = none ];
1334 -> 351;

1335 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
336 -> 1335 [arrowhead = none ];
1335 -> 352;

1336 [label="EVAL with clause\napp(.(X461, X462), X463, .(X461, X464)) :- app(X462, X463, X464).\nand substitutionX461 -> T215,\nX462 -> X466,\nX415 -> .(T215, X466),\nX416 -> X467,\nX417 -> X468,\nX463 -> .(X467, X468),\nX465 -> T215,\nX464 -> T216,\nT191 -> .(T215, T216)", fontsize=14, style = filled, fillcolor = lightblue];
346 -> 1336 [arrowhead = none ];
1336 -> 359;

1337 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
346 -> 1337 [arrowhead = none ];
1337 -> 360;

1338 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
351 -> 1338 [arrowhead = none ];
1338 -> 354;

1339 [label="INSTANCE with matching:\nX415 -> X466\nX416 -> X467\nX417 -> X468\nT191 -> T216", fontsize=14, style = filled, fillcolor = lightgrey];
359 -> 1339 [arrowhead = none , style=dashed];
1339 -> 328[style=dashed];

1340 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
367 -> 1340 [arrowhead = none ];
1340 -> 370;

1341 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
367 -> 1341 [arrowhead = none ];
1341 -> 371;

1342 [label="ONLY EVAL with clause\nleft(void, void).\nand substitutionX34 -> void", fontsize=14, style = filled, fillcolor = lightblue];
370 -> 1342 [arrowhead = none ];
1342 -> 382;

1343 [label="BACKTRACK\nfor clause: left(node(L, X1, X2), L)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
371 -> 1343 [arrowhead = none ];
1343 -> 418;

1344 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
382 -> 1344 [arrowhead = none ];
1344 -> 385;

1345 [label="SPLIT 2\nnew knowledge:\nT29 is ground", fontsize=14, style = filled, fillcolor = violet];
382 -> 1345 [arrowhead = none ];
1345 -> 387;

1346 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
385 -> 1346 [arrowhead = none ];
1346 -> 390;

1347 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
387 -> 1347 [arrowhead = none ];
1347 -> 401;

1348 [label="ONLY EVAL with clause\nin_order(void, X482) :- ','(!_14, eq(X482, [])).\nand substitutionT29 -> T228,\nX482 -> T228", fontsize=14, style = filled, fillcolor = lightblue];
390 -> 1348 [arrowhead = none ];
1348 -> 391;

1349 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
391 -> 1349 [arrowhead = none ];
1349 -> 392;

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

1351 [label="EVAL with clause\neq(X485, X485).\nand substitutionT228 -> [],\nX485 -> [],\nT231 -> []", fontsize=14, style = filled, fillcolor = lightblue];
393 -> 1351 [arrowhead = none ];
1351 -> 395;

1352 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
393 -> 1352 [arrowhead = none ];
1352 -> 396;

1353 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
395 -> 1353 [arrowhead = none ];
1353 -> 399;

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

1355 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
401 -> 1355 [arrowhead = none ];
1355 -> 411;

1356 [label="ONLY EVAL with clause\nright(void, void).\nand substitutionX35 -> void", fontsize=14, style = filled, fillcolor = lightblue];
410 -> 1356 [arrowhead = none ];
1356 -> 412;

1357 [label="BACKTRACK\nfor clause: right(node(X3, X4, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
411 -> 1357 [arrowhead = none ];
1357 -> 417;

1358 [label="INSTANCE with matching:\nT29 -> T31", fontsize=14, style = filled, fillcolor = lightgrey];
412 -> 1358 [arrowhead = none , style=dashed];
1358 -> 385[style=dashed];

1359 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
422 -> 1359 [arrowhead = none ];
1359 -> 438;

1360 [label="SPLIT 2\nnew knowledge:\nT252 is ground\nT255 is ground\nT253 is ground\nT19 is ground\nreplacements:X32 -> T252,\nX33 -> T253,\nT246 -> T254,\nT245 -> T255,\nT247 -> T256,\nT1 -> T257", fontsize=14, style = filled, fillcolor = violet];
422 -> 1360 [arrowhead = none ];
1360 -> 439;

1361 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
438 -> 1361 [arrowhead = none ];
1361 -> 442;

1362 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
439 -> 1362 [arrowhead = none ];
1362 -> 1239;

1363 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
442 -> 1363 [arrowhead = none ];
1363 -> 443;

1364 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
442 -> 1364 [arrowhead = none ];
1364 -> 444;

1365 [label="EVAL with clause\napp([], X521, X521).\nand substitutionX32 -> [],\nT245 -> T270,\nX33 -> T271,\nX521 -> .(T270, T271),\nX522 -> T271,\nT19 -> .(T270, T271)", fontsize=14, style = filled, fillcolor = lightblue];
443 -> 1365 [arrowhead = none ];
1365 -> 447;

1366 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
443 -> 1366 [arrowhead = none ];
1366 -> 448;

1367 [label="EVAL with clause\napp(.(X537, X538), X539, .(X537, X540)) :- app(X538, X539, X540).\nand substitutionX537 -> T279,\nX538 -> X542,\nX32 -> .(T279, X542),\nT245 -> T281,\nX33 -> X543,\nX539 -> .(T281, X543),\nX541 -> T279,\nX540 -> T280,\nT19 -> .(T279, T280),\nT278 -> T281", fontsize=14, style = filled, fillcolor = lightblue];
444 -> 1367 [arrowhead = none ];
1367 -> 463;

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

1369 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
447 -> 1369 [arrowhead = none ];
1369 -> 449;

1370 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
463 -> 1370 [arrowhead = none ];
1370 -> 467;

1371 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
467 -> 1371 [arrowhead = none ];
1371 -> 478;

1372 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
467 -> 1372 [arrowhead = none ];
1372 -> 479;

1373 [label="EVAL with clause\napp([], X556, X556).\nand substitutionX542 -> [],\nT281 -> T294,\nX543 -> T295,\nX556 -> .(T294, T295),\nX557 -> T295,\nT280 -> .(T294, T295)", fontsize=14, style = filled, fillcolor = lightblue];
478 -> 1373 [arrowhead = none ];
1373 -> 483;

1374 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
478 -> 1374 [arrowhead = none ];
1374 -> 484;

1375 [label="EVAL with clause\napp(.(X572, X573), X574, .(X572, X575)) :- app(X573, X574, X575).\nand substitutionX572 -> T303,\nX573 -> X577,\nX542 -> .(T303, X577),\nT281 -> T305,\nX543 -> X578,\nX574 -> .(T305, X578),\nX576 -> T303,\nX575 -> T304,\nT280 -> .(T303, T304),\nT302 -> T305", fontsize=14, style = filled, fillcolor = lightblue];
479 -> 1375 [arrowhead = none ];
1375 -> 488;

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

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

1378 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
488 -> 1378 [arrowhead = none ];
1378 -> 501;

1379 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
501 -> 1379 [arrowhead = none ];
1379 -> 502;

1380 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
501 -> 1380 [arrowhead = none ];
1380 -> 503;

1381 [label="EVAL with clause\napp([], X591, X591).\nand substitutionX577 -> [],\nT305 -> T318,\nX578 -> T319,\nX591 -> .(T318, T319),\nX592 -> T319,\nT304 -> .(T318, T319)", fontsize=14, style = filled, fillcolor = lightblue];
502 -> 1381 [arrowhead = none ];
1381 -> 504;

1382 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
502 -> 1382 [arrowhead = none ];
1382 -> 505;

1383 [label="EVAL with clause\napp(.(X607, X608), X609, .(X607, X610)) :- app(X608, X609, X610).\nand substitutionX607 -> T327,\nX608 -> X612,\nX577 -> .(T327, X612),\nT305 -> T329,\nX578 -> X613,\nX609 -> .(T329, X613),\nX611 -> T327,\nX610 -> T328,\nT304 -> .(T327, T328),\nT326 -> T329", fontsize=14, style = filled, fillcolor = lightblue];
503 -> 1383 [arrowhead = none ];
1383 -> 508;

1384 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
503 -> 1384 [arrowhead = none ];
1384 -> 509;

1385 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
504 -> 1385 [arrowhead = none ];
1385 -> 506;

1386 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
508 -> 1386 [arrowhead = none ];
1386 -> 513;

1387 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
513 -> 1387 [arrowhead = none ];
1387 -> 514;

1388 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
513 -> 1388 [arrowhead = none ];
1388 -> 515;

1389 [label="EVAL with clause\napp([], X626, X626).\nand substitutionX612 -> [],\nT329 -> T342,\nX613 -> T343,\nX626 -> .(T342, T343),\nX627 -> T343,\nT328 -> .(T342, T343)", fontsize=14, style = filled, fillcolor = lightblue];
514 -> 1389 [arrowhead = none ];
1389 -> 519;

1390 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
514 -> 1390 [arrowhead = none ];
1390 -> 520;

1391 [label="EVAL with clause\napp(.(X642, X643), X644, .(X642, X645)) :- app(X643, X644, X645).\nand substitutionX642 -> T351,\nX643 -> X647,\nX612 -> .(T351, X647),\nT329 -> T353,\nX613 -> X648,\nX644 -> .(T353, X648),\nX646 -> T351,\nX645 -> T352,\nT328 -> .(T351, T352),\nT350 -> T353", fontsize=14, style = filled, fillcolor = lightblue];
515 -> 1391 [arrowhead = none ];
1391 -> 522;

1392 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
515 -> 1392 [arrowhead = none ];
1392 -> 523;

1393 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
519 -> 1393 [arrowhead = none ];
1393 -> 521;

1394 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
522 -> 1394 [arrowhead = none ];
1394 -> 526;

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

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

1397 [label="EVAL with clause\napp([], X661, X661).\nand substitutionX647 -> [],\nT353 -> T366,\nX648 -> T367,\nX661 -> .(T366, T367),\nX662 -> T367,\nT352 -> .(T366, T367)", fontsize=14, style = filled, fillcolor = lightblue];
527 -> 1397 [arrowhead = none ];
1397 -> 531;

1398 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
527 -> 1398 [arrowhead = none ];
1398 -> 532;

1399 [label="EVAL with clause\napp(.(X677, X678), X679, .(X677, X680)) :- app(X678, X679, X680).\nand substitutionX677 -> T375,\nX678 -> X682,\nX647 -> .(T375, X682),\nT353 -> T377,\nX648 -> X683,\nX679 -> .(T377, X683),\nX681 -> T375,\nX680 -> T376,\nT352 -> .(T375, T376),\nT374 -> T377", fontsize=14, style = filled, fillcolor = lightblue];
528 -> 1399 [arrowhead = none ];
1399 -> 535;

1400 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
528 -> 1400 [arrowhead = none ];
1400 -> 536;

1401 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
531 -> 1401 [arrowhead = none ];
1401 -> 533;

1402 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
535 -> 1402 [arrowhead = none ];
1402 -> 541;

1403 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
541 -> 1403 [arrowhead = none ];
1403 -> 542;

1404 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
541 -> 1404 [arrowhead = none ];
1404 -> 543;

1405 [label="EVAL with clause\napp([], X696, X696).\nand substitutionX682 -> [],\nT377 -> T390,\nX683 -> T391,\nX696 -> .(T390, T391),\nX697 -> T391,\nT376 -> .(T390, T391)", fontsize=14, style = filled, fillcolor = lightblue];
542 -> 1405 [arrowhead = none ];
1405 -> 545;

1406 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
542 -> 1406 [arrowhead = none ];
1406 -> 546;

1407 [label="EVAL with clause\napp(.(X712, X713), X714, .(X712, X715)) :- app(X713, X714, X715).\nand substitutionX712 -> T399,\nX713 -> X717,\nX682 -> .(T399, X717),\nT377 -> T401,\nX683 -> X718,\nX714 -> .(T401, X718),\nX716 -> T399,\nX715 -> T400,\nT376 -> .(T399, T400),\nT398 -> T401", fontsize=14, style = filled, fillcolor = lightblue];
543 -> 1407 [arrowhead = none ];
1407 -> 548;

1408 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
543 -> 1408 [arrowhead = none ];
1408 -> 549;

1409 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
545 -> 1409 [arrowhead = none ];
1409 -> 547;

1410 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
548 -> 1410 [arrowhead = none ];
1410 -> 550;

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

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

1413 [label="EVAL with clause\napp([], X731, X731).\nand substitutionX717 -> [],\nT401 -> T414,\nX718 -> T415,\nX731 -> .(T414, T415),\nX732 -> T415,\nT400 -> .(T414, T415)", fontsize=14, style = filled, fillcolor = lightblue];
551 -> 1413 [arrowhead = none ];
1413 -> 553;

1414 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
551 -> 1414 [arrowhead = none ];
1414 -> 554;

1415 [label="EVAL with clause\napp(.(X747, X748), X749, .(X747, X750)) :- app(X748, X749, X750).\nand substitutionX747 -> T423,\nX748 -> X752,\nX717 -> .(T423, X752),\nT401 -> T425,\nX718 -> X753,\nX749 -> .(T425, X753),\nX751 -> T423,\nX750 -> T424,\nT400 -> .(T423, T424),\nT422 -> T425", fontsize=14, style = filled, fillcolor = lightblue];
552 -> 1415 [arrowhead = none ];
1415 -> 611;

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

1417 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
553 -> 1417 [arrowhead = none ];
1417 -> 555;

1418 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
611 -> 1418 [arrowhead = none ];
1418 -> 801;

1419 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
801 -> 1419 [arrowhead = none ];
1419 -> 918;

1420 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
801 -> 1420 [arrowhead = none ];
1420 -> 925;

1421 [label="EVAL with clause\napp([], X766, X766).\nand substitutionX752 -> [],\nT425 -> T438,\nX753 -> T439,\nX766 -> .(T438, T439),\nX767 -> T439,\nT424 -> .(T438, T439)", fontsize=14, style = filled, fillcolor = lightblue];
918 -> 1421 [arrowhead = none ];
1421 -> 1225;

1422 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
918 -> 1422 [arrowhead = none ];
1422 -> 1226;

1423 [label="EVAL with clause\napp(.(X782, X783), X784, .(X782, X785)) :- app(X783, X784, X785).\nand substitutionX782 -> T447,\nX783 -> X787,\nX752 -> .(T447, X787),\nT425 -> T449,\nX753 -> X788,\nX784 -> .(T449, X788),\nX786 -> T447,\nX785 -> T448,\nT424 -> .(T447, T448),\nT446 -> T449", fontsize=14, style = filled, fillcolor = lightblue];
925 -> 1423 [arrowhead = none ];
1423 -> 1228;

1424 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
925 -> 1424 [arrowhead = none ];
1424 -> 1229;

1425 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
1225 -> 1425 [arrowhead = none ];
1425 -> 1227;

1426 [label="GENERALIZATION\nT454 <-- .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))\n\nNew Knowledge:\nT454 is ground", fontsize=14, style = filled, fillcolor = violet];
1228 -> 1426 [arrowhead = none ];
1426 -> 1230;

1427 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1230 -> 1427 [arrowhead = none ];
1427 -> 1231;

1428 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
1231 -> 1428 [arrowhead = none ];
1428 -> 1232;

1429 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
1231 -> 1429 [arrowhead = none ];
1429 -> 1233;

1430 [label="EVAL with clause\napp([], X805, X805).\nand substitutionX787 -> [],\nT449 -> T467,\nX788 -> T468,\nX805 -> .(T467, T468),\nX806 -> T468,\nT448 -> .(T467, T468)", fontsize=14, style = filled, fillcolor = lightblue];
1232 -> 1430 [arrowhead = none ];
1430 -> 1234;

1431 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
1232 -> 1431 [arrowhead = none ];
1431 -> 1235;

1432 [label="EVAL with clause\napp(.(X821, X822), X823, .(X821, X824)) :- app(X822, X823, X824).\nand substitutionX821 -> T476,\nX822 -> X826,\nX787 -> .(T476, X826),\nT449 -> T478,\nX788 -> X827,\nX823 -> .(T478, X827),\nX825 -> T476,\nX824 -> T477,\nT448 -> .(T476, T477),\nT475 -> T478", fontsize=14, style = filled, fillcolor = lightblue];
1233 -> 1432 [arrowhead = none ];
1432 -> 1237;

1433 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
1233 -> 1433 [arrowhead = none ];
1433 -> 1238;

1434 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
1234 -> 1434 [arrowhead = none ];
1434 -> 1236;

1435 [label="INSTANCE with matching:\nX787 -> X826\nT449 -> T478\nX788 -> X827\nT448 -> T477", fontsize=14, style = filled, fillcolor = lightgrey];
1237 -> 1435 [arrowhead = none , style=dashed];
1435 -> 1230[style=dashed];

1436 [label="BACKTRACK\nfor clause: left(void, void)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
1239 -> 1436 [arrowhead = none ];
1436 -> 1240;

1437 [label="ONLY EVAL with clause\nleft(node(X840, X841, X842), X840).\nand substitutionT254 -> T496,\nX840 -> T496,\nT255 -> T494,\nX841 -> T494,\nT256 -> T497,\nX842 -> T497,\nX34 -> T496,\nT493 -> T496,\nT495 -> T497", fontsize=14, style = filled, fillcolor = lightblue];
1240 -> 1437 [arrowhead = none ];
1437 -> 1241;

1438 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
1241 -> 1438 [arrowhead = none ];
1438 -> 1242;

1439 [label="SPLIT 2\nnew knowledge:\nT252 is ground\nreplacements:T496 -> T499,\nT497 -> T500", fontsize=14, style = filled, fillcolor = violet];
1241 -> 1439 [arrowhead = none ];
1439 -> 1243;

1440 [label="INSTANCE with matching:\nT1 -> T496\nT2 -> T252", fontsize=14, style = filled, fillcolor = lightgrey];
1242 -> 1440 [arrowhead = none , style=dashed];
1440 -> 3[style=dashed];

1441 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1243 -> 1441 [arrowhead = none ];
1441 -> 1244;

1442 [label="BACKTRACK\nfor clause: right(void, void)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
1244 -> 1442 [arrowhead = none ];
1442 -> 1245;

1443 [label="ONLY EVAL with clause\nright(node(X853, X854, X855), X855).\nand substitutionT499 -> T511,\nX853 -> T511,\nT494 -> T512,\nX854 -> T512,\nT500 -> T514,\nX855 -> T514,\nX35 -> T514,\nT513 -> T514", fontsize=14, style = filled, fillcolor = lightblue];
1245 -> 1443 [arrowhead = none ];
1443 -> 1246;

1444 [label="INSTANCE with matching:\nT1 -> T514\nT2 -> T253", fontsize=14, style = filled, fillcolor = lightgrey];
1246 -> 1444 [arrowhead = none , style=dashed];
1444 -> 3[style=dashed];

}

(2) Obligation:

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

f3_in([]) → f3_out1
f3_in(T19) → U1(f48_in(T19), T19)
U1(f48_out1(X32, X51, X33, X34, X35), T19) → f3_out1
f3_in(T19) → U2(f422_in(T19), T19)
U2(f422_out1(X32, T245, X33), T19) → f3_out1
f328_in(.(T209, T210)) → f328_out1([], T209, T210)
f328_in(.(T215, T216)) → U3(f328_in(T216), .(T215, T216))
U3(f328_out1(X466, X467, X468), .(T215, T216)) → f328_out1(.(T215, X466), X467, X468)
f385_in([]) → f385_out1
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)
f56_in(.(T44, T45)) → f56_out1([], T44, T45)
f56_in(.(T50, .(T64, T65))) → f56_out1(.(T50, []), T64, T65)
f56_in(.(T50, .(T70, .(T84, T85)))) → f56_out1(.(T50, .(T70, [])), T84, T85)
f56_in(.(T50, .(T70, .(T90, .(T104, T105))))) → f56_out1(.(T50, .(T70, .(T90, []))), T104, T105)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T124, T125)))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, [])))), T124, T125)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T144, T145))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, []))))), T144, T145)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T164, T165)))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, [])))))), T164, T165)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T184, T185))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, []))))))), T184, T185)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
U5(f328_out1(X415, X416, X417), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, X415)))))))), X416, X417)
f57_in(T29, T31) → U6(f382_in(T29, T31), T29, T31)
U6(f382_out1(X35), T29, T31) → f57_out1(void, X35)
f387_in(T31) → U7(f385_in(T31), T31)
U7(f385_out1, T31) → f387_out1(void)
f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
f439_in(T494, T252, T253) → U9(f1241_in(T252, T494, T253), T494, T252, T253)
U9(f1241_out1, T494, T252, T253) → f439_out1
f1243_in(T512, T253) → U10(f3_in(T253), T512, T253)
U10(f3_out1, T512, T253) → f1243_out1
f48_in(T19) → U11(f56_in(T19), T19)
U11(f56_out1(T29, T30, T31), T19) → U12(f57_in(T29, T31), T19, T29, T30, T31)
U12(f57_out1(X34, X35), T19, T29, T30, T31) → f48_out1(T29, T30, T31, X34, X35)
f382_in(T29, T31) → U13(f385_in(T29), T29, T31)
U13(f385_out1, T29, T31) → U14(f387_in(T31), T29, T31)
U14(f387_out1(X35), T29, T31) → f382_out1(X35)
f422_in(T19) → U15(f438_in(T19), T19)
U15(f438_out1(T252, T255, T253), T19) → U16(f439_in(T255, T252, T253), T19, T252, T255, T253)
U16(f439_out1, T19, T252, T255, T253) → f422_out1(T252, T255, T253)
f1241_in(T252, T494, T253) → U17(f3_in(T252), T252, T494, T253)
U17(f3_out1, T252, T494, T253) → U18(f1243_in(T494, T253), T252, T494, T253)
U18(f1243_out1, T252, T494, T253) → f1241_out1

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

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

F3_IN(T19) → U1¹(f48_in(T19), T19)
F3_IN(T19) → F48_IN(T19)
F3_IN(T19) → U2¹(f422_in(T19), T19)
F3_IN(T19) → F422_IN(T19)
F328_IN(.(T215, T216)) → U3¹(f328_in(T216), .(T215, T216))
F328_IN(.(T215, T216)) → F328_IN(T216)
F1230_IN(.(T476, T477)) → U4¹(f1230_in(T477), .(T476, T477))
F1230_IN(.(T476, T477)) → F1230_IN(T477)
F56_IN(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5¹(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
F56_IN(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → F328_IN(T191)
F57_IN(T29, T31) → U6¹(f382_in(T29, T31), T29, T31)
F57_IN(T29, T31) → F382_IN(T29, T31)
F387_IN(T31) → U7¹(f385_in(T31), T31)
F387_IN(T31) → F385_IN(T31)
F438_IN(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8¹(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
F438_IN(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → F1230_IN(T448)
F439_IN(T494, T252, T253) → U9¹(f1241_in(T252, T494, T253), T494, T252, T253)
F439_IN(T494, T252, T253) → F1241_IN(T252, T494, T253)
F1243_IN(T512, T253) → U10¹(f3_in(T253), T512, T253)
F1243_IN(T512, T253) → F3_IN(T253)
F48_IN(T19) → U11¹(f56_in(T19), T19)
F48_IN(T19) → F56_IN(T19)
U11¹(f56_out1(T29, T30, T31), T19) → U12¹(f57_in(T29, T31), T19, T29, T30, T31)
U11¹(f56_out1(T29, T30, T31), T19) → F57_IN(T29, T31)
F382_IN(T29, T31) → U13¹(f385_in(T29), T29, T31)
F382_IN(T29, T31) → F385_IN(T29)
U13¹(f385_out1, T29, T31) → U14¹(f387_in(T31), T29, T31)
U13¹(f385_out1, T29, T31) → F387_IN(T31)
F422_IN(T19) → U15¹(f438_in(T19), T19)
F422_IN(T19) → F438_IN(T19)
U15¹(f438_out1(T252, T255, T253), T19) → U16¹(f439_in(T255, T252, T253), T19, T252, T255, T253)
U15¹(f438_out1(T252, T255, T253), T19) → F439_IN(T255, T252, T253)
F1241_IN(T252, T494, T253) → U17¹(f3_in(T252), T252, T494, T253)
F1241_IN(T252, T494, T253) → F3_IN(T252)
U17¹(f3_out1, T252, T494, T253) → U18¹(f1243_in(T494, T253), T252, T494, T253)
U17¹(f3_out1, T252, T494, T253) → F1243_IN(T494, T253)

The TRS R consists of the following rules:

f3_in([]) → f3_out1
f3_in(T19) → U1(f48_in(T19), T19)
U1(f48_out1(X32, X51, X33, X34, X35), T19) → f3_out1
f3_in(T19) → U2(f422_in(T19), T19)
U2(f422_out1(X32, T245, X33), T19) → f3_out1
f328_in(.(T209, T210)) → f328_out1([], T209, T210)
f328_in(.(T215, T216)) → U3(f328_in(T216), .(T215, T216))
U3(f328_out1(X466, X467, X468), .(T215, T216)) → f328_out1(.(T215, X466), X467, X468)
f385_in([]) → f385_out1
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)
f56_in(.(T44, T45)) → f56_out1([], T44, T45)
f56_in(.(T50, .(T64, T65))) → f56_out1(.(T50, []), T64, T65)
f56_in(.(T50, .(T70, .(T84, T85)))) → f56_out1(.(T50, .(T70, [])), T84, T85)
f56_in(.(T50, .(T70, .(T90, .(T104, T105))))) → f56_out1(.(T50, .(T70, .(T90, []))), T104, T105)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T124, T125)))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, [])))), T124, T125)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T144, T145))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, []))))), T144, T145)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T164, T165)))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, [])))))), T164, T165)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T184, T185))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, []))))))), T184, T185)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
U5(f328_out1(X415, X416, X417), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, X415)))))))), X416, X417)
f57_in(T29, T31) → U6(f382_in(T29, T31), T29, T31)
U6(f382_out1(X35), T29, T31) → f57_out1(void, X35)
f387_in(T31) → U7(f385_in(T31), T31)
U7(f385_out1, T31) → f387_out1(void)
f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
f439_in(T494, T252, T253) → U9(f1241_in(T252, T494, T253), T494, T252, T253)
U9(f1241_out1, T494, T252, T253) → f439_out1
f1243_in(T512, T253) → U10(f3_in(T253), T512, T253)
U10(f3_out1, T512, T253) → f1243_out1
f48_in(T19) → U11(f56_in(T19), T19)
U11(f56_out1(T29, T30, T31), T19) → U12(f57_in(T29, T31), T19, T29, T30, T31)
U12(f57_out1(X34, X35), T19, T29, T30, T31) → f48_out1(T29, T30, T31, X34, X35)
f382_in(T29, T31) → U13(f385_in(T29), T29, T31)
U13(f385_out1, T29, T31) → U14(f387_in(T31), T29, T31)
U14(f387_out1(X35), T29, T31) → f382_out1(X35)
f422_in(T19) → U15(f438_in(T19), T19)
U15(f438_out1(T252, T255, T253), T19) → U16(f439_in(T255, T252, T253), T19, T252, T255, T253)
U16(f439_out1, T19, T252, T255, T253) → f422_out1(T252, T255, T253)
f1241_in(T252, T494, T253) → U17(f3_in(T252), T252, T494, T253)
U17(f3_out1, T252, T494, T253) → U18(f1243_in(T494, T253), T252, T494, T253)
U18(f1243_out1, T252, T494, T253) → f1241_out1

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 26 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

F1230_IN(.(T476, T477)) → F1230_IN(T477)

The TRS R consists of the following rules:

f3_in([]) → f3_out1
f3_in(T19) → U1(f48_in(T19), T19)
U1(f48_out1(X32, X51, X33, X34, X35), T19) → f3_out1
f3_in(T19) → U2(f422_in(T19), T19)
U2(f422_out1(X32, T245, X33), T19) → f3_out1
f328_in(.(T209, T210)) → f328_out1([], T209, T210)
f328_in(.(T215, T216)) → U3(f328_in(T216), .(T215, T216))
U3(f328_out1(X466, X467, X468), .(T215, T216)) → f328_out1(.(T215, X466), X467, X468)
f385_in([]) → f385_out1
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)
f56_in(.(T44, T45)) → f56_out1([], T44, T45)
f56_in(.(T50, .(T64, T65))) → f56_out1(.(T50, []), T64, T65)
f56_in(.(T50, .(T70, .(T84, T85)))) → f56_out1(.(T50, .(T70, [])), T84, T85)
f56_in(.(T50, .(T70, .(T90, .(T104, T105))))) → f56_out1(.(T50, .(T70, .(T90, []))), T104, T105)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T124, T125)))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, [])))), T124, T125)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T144, T145))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, []))))), T144, T145)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T164, T165)))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, [])))))), T164, T165)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T184, T185))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, []))))))), T184, T185)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
U5(f328_out1(X415, X416, X417), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, X415)))))))), X416, X417)
f57_in(T29, T31) → U6(f382_in(T29, T31), T29, T31)
U6(f382_out1(X35), T29, T31) → f57_out1(void, X35)
f387_in(T31) → U7(f385_in(T31), T31)
U7(f385_out1, T31) → f387_out1(void)
f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
f439_in(T494, T252, T253) → U9(f1241_in(T252, T494, T253), T494, T252, T253)
U9(f1241_out1, T494, T252, T253) → f439_out1
f1243_in(T512, T253) → U10(f3_in(T253), T512, T253)
U10(f3_out1, T512, T253) → f1243_out1
f48_in(T19) → U11(f56_in(T19), T19)
U11(f56_out1(T29, T30, T31), T19) → U12(f57_in(T29, T31), T19, T29, T30, T31)
U12(f57_out1(X34, X35), T19, T29, T30, T31) → f48_out1(T29, T30, T31, X34, X35)
f382_in(T29, T31) → U13(f385_in(T29), T29, T31)
U13(f385_out1, T29, T31) → U14(f387_in(T31), T29, T31)
U14(f387_out1(X35), T29, T31) → f382_out1(X35)
f422_in(T19) → U15(f438_in(T19), T19)
U15(f438_out1(T252, T255, T253), T19) → U16(f439_in(T255, T252, T253), T19, T252, T255, T253)
U16(f439_out1, T19, T252, T255, T253) → f422_out1(T252, T255, T253)
f1241_in(T252, T494, T253) → U17(f3_in(T252), T252, T494, T253)
U17(f3_out1, T252, T494, T253) → U18(f1243_in(T494, T253), T252, T494, T253)
U18(f1243_out1, T252, T494, T253) → f1241_out1

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

(8) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

F1230_IN(.(T476, T477)) → F1230_IN(T477)

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

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

F1230_IN(.(T476, T477)) → F1230_IN(T477)
The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

F328_IN(.(T215, T216)) → F328_IN(T216)

The TRS R consists of the following rules:

f3_in([]) → f3_out1
f3_in(T19) → U1(f48_in(T19), T19)
U1(f48_out1(X32, X51, X33, X34, X35), T19) → f3_out1
f3_in(T19) → U2(f422_in(T19), T19)
U2(f422_out1(X32, T245, X33), T19) → f3_out1
f328_in(.(T209, T210)) → f328_out1([], T209, T210)
f328_in(.(T215, T216)) → U3(f328_in(T216), .(T215, T216))
U3(f328_out1(X466, X467, X468), .(T215, T216)) → f328_out1(.(T215, X466), X467, X468)
f385_in([]) → f385_out1
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)
f56_in(.(T44, T45)) → f56_out1([], T44, T45)
f56_in(.(T50, .(T64, T65))) → f56_out1(.(T50, []), T64, T65)
f56_in(.(T50, .(T70, .(T84, T85)))) → f56_out1(.(T50, .(T70, [])), T84, T85)
f56_in(.(T50, .(T70, .(T90, .(T104, T105))))) → f56_out1(.(T50, .(T70, .(T90, []))), T104, T105)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T124, T125)))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, [])))), T124, T125)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T144, T145))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, []))))), T144, T145)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T164, T165)))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, [])))))), T164, T165)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T184, T185))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, []))))))), T184, T185)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
U5(f328_out1(X415, X416, X417), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, X415)))))))), X416, X417)
f57_in(T29, T31) → U6(f382_in(T29, T31), T29, T31)
U6(f382_out1(X35), T29, T31) → f57_out1(void, X35)
f387_in(T31) → U7(f385_in(T31), T31)
U7(f385_out1, T31) → f387_out1(void)
f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
f439_in(T494, T252, T253) → U9(f1241_in(T252, T494, T253), T494, T252, T253)
U9(f1241_out1, T494, T252, T253) → f439_out1
f1243_in(T512, T253) → U10(f3_in(T253), T512, T253)
U10(f3_out1, T512, T253) → f1243_out1
f48_in(T19) → U11(f56_in(T19), T19)
U11(f56_out1(T29, T30, T31), T19) → U12(f57_in(T29, T31), T19, T29, T30, T31)
U12(f57_out1(X34, X35), T19, T29, T30, T31) → f48_out1(T29, T30, T31, X34, X35)
f382_in(T29, T31) → U13(f385_in(T29), T29, T31)
U13(f385_out1, T29, T31) → U14(f387_in(T31), T29, T31)
U14(f387_out1(X35), T29, T31) → f382_out1(X35)
f422_in(T19) → U15(f438_in(T19), T19)
U15(f438_out1(T252, T255, T253), T19) → U16(f439_in(T255, T252, T253), T19, T252, T255, T253)
U16(f439_out1, T19, T252, T255, T253) → f422_out1(T252, T255, T253)
f1241_in(T252, T494, T253) → U17(f3_in(T252), T252, T494, T253)
U17(f3_out1, T252, T494, T253) → U18(f1243_in(T494, T253), T252, T494, T253)
U18(f1243_out1, T252, T494, T253) → f1241_out1

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

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

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

F328_IN(.(T215, T216)) → F328_IN(T216)

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

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

F328_IN(.(T215, T216)) → F328_IN(T216)
The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

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

F3_IN(T19) → F422_IN(T19)
F422_IN(T19) → U15¹(f438_in(T19), T19)
U15¹(f438_out1(T252, T255, T253), T19) → F439_IN(T255, T252, T253)
F439_IN(T494, T252, T253) → F1241_IN(T252, T494, T253)
F1241_IN(T252, T494, T253) → U17¹(f3_in(T252), T252, T494, T253)
U17¹(f3_out1, T252, T494, T253) → F1243_IN(T494, T253)
F1243_IN(T512, T253) → F3_IN(T253)
F1241_IN(T252, T494, T253) → F3_IN(T252)

The TRS R consists of the following rules:

f3_in([]) → f3_out1
f3_in(T19) → U1(f48_in(T19), T19)
U1(f48_out1(X32, X51, X33, X34, X35), T19) → f3_out1
f3_in(T19) → U2(f422_in(T19), T19)
U2(f422_out1(X32, T245, X33), T19) → f3_out1
f328_in(.(T209, T210)) → f328_out1([], T209, T210)
f328_in(.(T215, T216)) → U3(f328_in(T216), .(T215, T216))
U3(f328_out1(X466, X467, X468), .(T215, T216)) → f328_out1(.(T215, X466), X467, X468)
f385_in([]) → f385_out1
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)
f56_in(.(T44, T45)) → f56_out1([], T44, T45)
f56_in(.(T50, .(T64, T65))) → f56_out1(.(T50, []), T64, T65)
f56_in(.(T50, .(T70, .(T84, T85)))) → f56_out1(.(T50, .(T70, [])), T84, T85)
f56_in(.(T50, .(T70, .(T90, .(T104, T105))))) → f56_out1(.(T50, .(T70, .(T90, []))), T104, T105)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T124, T125)))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, [])))), T124, T125)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T144, T145))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, []))))), T144, T145)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T164, T165)))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, [])))))), T164, T165)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T184, T185))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, []))))))), T184, T185)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
U5(f328_out1(X415, X416, X417), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, X415)))))))), X416, X417)
f57_in(T29, T31) → U6(f382_in(T29, T31), T29, T31)
U6(f382_out1(X35), T29, T31) → f57_out1(void, X35)
f387_in(T31) → U7(f385_in(T31), T31)
U7(f385_out1, T31) → f387_out1(void)
f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
f439_in(T494, T252, T253) → U9(f1241_in(T252, T494, T253), T494, T252, T253)
U9(f1241_out1, T494, T252, T253) → f439_out1
f1243_in(T512, T253) → U10(f3_in(T253), T512, T253)
U10(f3_out1, T512, T253) → f1243_out1
f48_in(T19) → U11(f56_in(T19), T19)
U11(f56_out1(T29, T30, T31), T19) → U12(f57_in(T29, T31), T19, T29, T30, T31)
U12(f57_out1(X34, X35), T19, T29, T30, T31) → f48_out1(T29, T30, T31, X34, X35)
f382_in(T29, T31) → U13(f385_in(T29), T29, T31)
U13(f385_out1, T29, T31) → U14(f387_in(T31), T29, T31)
U14(f387_out1(X35), T29, T31) → f382_out1(X35)
f422_in(T19) → U15(f438_in(T19), T19)
U15(f438_out1(T252, T255, T253), T19) → U16(f439_in(T255, T252, T253), T19, T252, T255, T253)
U16(f439_out1, T19, T252, T255, T253) → f422_out1(T252, T255, T253)
f1241_in(T252, T494, T253) → U17(f3_in(T252), T252, T494, T253)
U17(f3_out1, T252, T494, T253) → U18(f1243_in(T494, T253), T252, T494, T253)
U18(f1243_out1, T252, T494, T253) → f1241_out1

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

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

F1243_IN(T512, T253) → F3_IN(T253)

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(F3_IN(x₁)) = 0A + 3A · x₁

POL(F422_IN(x₁)) = 0A + 3A · x₁

POL(U15¹(x₁, x₂)) = -I + 3A · x₁ + -I · x₂

POL(f438_in(x₁)) = -I + 0A · x₁

POL(f438_out1(x₁, x₂, x₃)) = 0A + 0A · x₁ + -I · x₂ + 1A · x₃

POL(F439_IN(x₁, x₂, x₃)) = 3A + -I · x₁ + 3A · x₂ + 4A · x₃

POL(F1241_IN(x₁, x₂, x₃)) = 3A + 3A · x₁ + -I · x₂ + 4A · x₃

POL(U17¹(x₁, x₂, x₃, x₄)) = 3A + -I · x₁ + 3A · x₂ + -I · x₃ + 4A · x₄

POL(f3_in(x₁)) = 0A + -I · x₁

POL(f3_out1) = 1A

POL(F1243_IN(x₁, x₂)) = 3A + -I · x₁ + 4A · x₂

POL(.(x₁, x₂)) = 0A + -I · x₁ + 1A · x₂

POL([]) = 0A

POL(U8(x₁, x₂)) = 0A + 3A · x₁ + 0A · x₂

POL(f1230_in(x₁)) = 0A + 5A · x₁

POL(U1(x₁, x₂)) = -I + -I · x₁ + 3A · x₂

POL(f48_in(x₁)) = 0A + -I · x₁

POL(U2(x₁, x₂)) = -I + 5A · x₁ + -I · x₂

POL(f422_in(x₁)) = 1A + 5A · x₁

POL(f422_out1(x₁, x₂, x₃)) = 0A + -I · x₁ + 5A · x₂ + 5A · x₃

POL(U15(x₁, x₂)) = 5A + -I · x₁ + -I · x₂

POL(U16(x₁, x₂, x₃, x₄, x₅)) = -I + 0A · x₁ + -I · x₂ + -I · x₃ + 2A · x₄ + -I · x₅

POL(f439_in(x₁, x₂, x₃)) = 0A + -I · x₁ + 0A · x₂ + -I · x₃

POL(f439_out1) = 5A

POL(U9(x₁, x₂, x₃, x₄)) = 1A + 0A · x₁ + 2A · x₂ + 0A · x₃ + -I · x₄

POL(f1241_in(x₁, x₂, x₃)) = 0A + -I · x₁ + 0A · x₂ + 3A · x₃

POL(f1241_out1) = 1A

POL(U17(x₁, x₂, x₃, x₄)) = 1A + 0A · x₁ + 0A · x₂ + -I · x₃ + 5A · x₄

POL(U18(x₁, x₂, x₃, x₄)) = -I + 0A · x₁ + 5A · x₂ + -I · x₃ + -I · x₄

POL(f1243_in(x₁, x₂)) = 4A + 2A · x₁ + -I · x₂

POL(f1243_out1) = 0A

POL(U10(x₁, x₂, x₃)) = 1A + -I · x₁ + 4A · x₂ + 0A · x₃

POL(U11(x₁, x₂)) = -I + -I · x₁ + 0A · x₂

POL(f56_in(x₁)) = 0A + 0A · x₁

POL(f48_out1(x₁, x₂, x₃, x₄, x₅)) = -I + 5A · x₁ + 4A · x₂ + 5A · x₃ + 5A · x₄ + -I · x₅

POL(f56_out1(x₁, x₂, x₃)) = -I + -I · x₁ + 4A · x₂ + 4A · x₃

POL(U5(x₁, x₂)) = 0A + -I · x₁ + -I · x₂

POL(f328_in(x₁)) = 0A + -I · x₁

POL(U12(x₁, x₂, x₃, x₄, x₅)) = -I + 0A · x₁ + 5A · x₂ + -I · x₃ + 5A · x₄ + -I · x₅

POL(f57_in(x₁, x₂)) = 0A + 0A · x₁ + 0A · x₂

POL(f328_out1(x₁, x₂, x₃)) = 2A + -I · x₁ + 5A · x₂ + -I · x₃

POL(U3(x₁, x₂)) = 0A + -I · x₁ + -I · x₂

POL(U6(x₁, x₂, x₃)) = -I + 2A · x₁ + -I · x₂ + -I · x₃

POL(f382_in(x₁, x₂)) = -I + 0A · x₁ + -I · x₂

POL(f57_out1(x₁, x₂)) = 0A + 1A · x₁ + 5A · x₂

POL(U13(x₁, x₂, x₃)) = 0A + 0A · x₁ + 0A · x₂ + -I · x₃

POL(f385_in(x₁)) = 5A + -I · x₁

POL(f382_out1(x₁)) = 1A + -I · x₁

POL(void) = 2A

POL(f385_out1) = 0A

POL(U14(x₁, x₂, x₃)) = 1A + 0A · x₁ + 2A · x₂ + -I · x₃

POL(f387_in(x₁)) = -I + 0A · x₁

POL(U7(x₁, x₂)) = 2A + -I · x₁ + 2A · x₂

POL(f387_out1(x₁)) = -I + 1A · x₁

POL(f1230_out1(x₁, x₂, x₃)) = 0A + 5A · x₁ + -I · x₂ + 0A · x₃

POL(U4(x₁, x₂)) = -I + 1A · x₁ + 5A · x₂

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)

(19) Obligation:

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

F3_IN(T19) → F422_IN(T19)
F422_IN(T19) → U15¹(f438_in(T19), T19)
U15¹(f438_out1(T252, T255, T253), T19) → F439_IN(T255, T252, T253)
F439_IN(T494, T252, T253) → F1241_IN(T252, T494, T253)
F1241_IN(T252, T494, T253) → U17¹(f3_in(T252), T252, T494, T253)
U17¹(f3_out1, T252, T494, T253) → F1243_IN(T494, T253)
F1241_IN(T252, T494, T253) → F3_IN(T252)

The TRS R consists of the following rules:

f3_in([]) → f3_out1
f3_in(T19) → U1(f48_in(T19), T19)
U1(f48_out1(X32, X51, X33, X34, X35), T19) → f3_out1
f3_in(T19) → U2(f422_in(T19), T19)
U2(f422_out1(X32, T245, X33), T19) → f3_out1
f328_in(.(T209, T210)) → f328_out1([], T209, T210)
f328_in(.(T215, T216)) → U3(f328_in(T216), .(T215, T216))
U3(f328_out1(X466, X467, X468), .(T215, T216)) → f328_out1(.(T215, X466), X467, X468)
f385_in([]) → f385_out1
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)
f56_in(.(T44, T45)) → f56_out1([], T44, T45)
f56_in(.(T50, .(T64, T65))) → f56_out1(.(T50, []), T64, T65)
f56_in(.(T50, .(T70, .(T84, T85)))) → f56_out1(.(T50, .(T70, [])), T84, T85)
f56_in(.(T50, .(T70, .(T90, .(T104, T105))))) → f56_out1(.(T50, .(T70, .(T90, []))), T104, T105)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T124, T125)))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, [])))), T124, T125)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T144, T145))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, []))))), T144, T145)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T164, T165)))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, [])))))), T164, T165)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T184, T185))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, []))))))), T184, T185)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
U5(f328_out1(X415, X416, X417), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, X415)))))))), X416, X417)
f57_in(T29, T31) → U6(f382_in(T29, T31), T29, T31)
U6(f382_out1(X35), T29, T31) → f57_out1(void, X35)
f387_in(T31) → U7(f385_in(T31), T31)
U7(f385_out1, T31) → f387_out1(void)
f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
f439_in(T494, T252, T253) → U9(f1241_in(T252, T494, T253), T494, T252, T253)
U9(f1241_out1, T494, T252, T253) → f439_out1
f1243_in(T512, T253) → U10(f3_in(T253), T512, T253)
U10(f3_out1, T512, T253) → f1243_out1
f48_in(T19) → U11(f56_in(T19), T19)
U11(f56_out1(T29, T30, T31), T19) → U12(f57_in(T29, T31), T19, T29, T30, T31)
U12(f57_out1(X34, X35), T19, T29, T30, T31) → f48_out1(T29, T30, T31, X34, X35)
f382_in(T29, T31) → U13(f385_in(T29), T29, T31)
U13(f385_out1, T29, T31) → U14(f387_in(T31), T29, T31)
U14(f387_out1(X35), T29, T31) → f382_out1(X35)
f422_in(T19) → U15(f438_in(T19), T19)
U15(f438_out1(T252, T255, T253), T19) → U16(f439_in(T255, T252, T253), T19, T252, T255, T253)
U16(f439_out1, T19, T252, T255, T253) → f422_out1(T252, T255, T253)
f1241_in(T252, T494, T253) → U17(f3_in(T252), T252, T494, T253)
U17(f3_out1, T252, T494, T253) → U18(f1243_in(T494, T253), T252, T494, T253)
U18(f1243_out1, T252, T494, T253) → f1241_out1

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

(20) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(21) Obligation:

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

F422_IN(T19) → U15¹(f438_in(T19), T19)
U15¹(f438_out1(T252, T255, T253), T19) → F439_IN(T255, T252, T253)
F439_IN(T494, T252, T253) → F1241_IN(T252, T494, T253)
F1241_IN(T252, T494, T253) → F3_IN(T252)
F3_IN(T19) → F422_IN(T19)

The TRS R consists of the following rules:

f3_in([]) → f3_out1
f3_in(T19) → U1(f48_in(T19), T19)
U1(f48_out1(X32, X51, X33, X34, X35), T19) → f3_out1
f3_in(T19) → U2(f422_in(T19), T19)
U2(f422_out1(X32, T245, X33), T19) → f3_out1
f328_in(.(T209, T210)) → f328_out1([], T209, T210)
f328_in(.(T215, T216)) → U3(f328_in(T216), .(T215, T216))
U3(f328_out1(X466, X467, X468), .(T215, T216)) → f328_out1(.(T215, X466), X467, X468)
f385_in([]) → f385_out1
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)
f56_in(.(T44, T45)) → f56_out1([], T44, T45)
f56_in(.(T50, .(T64, T65))) → f56_out1(.(T50, []), T64, T65)
f56_in(.(T50, .(T70, .(T84, T85)))) → f56_out1(.(T50, .(T70, [])), T84, T85)
f56_in(.(T50, .(T70, .(T90, .(T104, T105))))) → f56_out1(.(T50, .(T70, .(T90, []))), T104, T105)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T124, T125)))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, [])))), T124, T125)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T144, T145))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, []))))), T144, T145)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T164, T165)))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, [])))))), T164, T165)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T184, T185))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, []))))))), T184, T185)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
U5(f328_out1(X415, X416, X417), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, X415)))))))), X416, X417)
f57_in(T29, T31) → U6(f382_in(T29, T31), T29, T31)
U6(f382_out1(X35), T29, T31) → f57_out1(void, X35)
f387_in(T31) → U7(f385_in(T31), T31)
U7(f385_out1, T31) → f387_out1(void)
f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
f439_in(T494, T252, T253) → U9(f1241_in(T252, T494, T253), T494, T252, T253)
U9(f1241_out1, T494, T252, T253) → f439_out1
f1243_in(T512, T253) → U10(f3_in(T253), T512, T253)
U10(f3_out1, T512, T253) → f1243_out1
f48_in(T19) → U11(f56_in(T19), T19)
U11(f56_out1(T29, T30, T31), T19) → U12(f57_in(T29, T31), T19, T29, T30, T31)
U12(f57_out1(X34, X35), T19, T29, T30, T31) → f48_out1(T29, T30, T31, X34, X35)
f382_in(T29, T31) → U13(f385_in(T29), T29, T31)
U13(f385_out1, T29, T31) → U14(f387_in(T31), T29, T31)
U14(f387_out1(X35), T29, T31) → f382_out1(X35)
f422_in(T19) → U15(f438_in(T19), T19)
U15(f438_out1(T252, T255, T253), T19) → U16(f439_in(T255, T252, T253), T19, T252, T255, T253)
U16(f439_out1, T19, T252, T255, T253) → f422_out1(T252, T255, T253)
f1241_in(T252, T494, T253) → U17(f3_in(T252), T252, T494, T253)
U17(f3_out1, T252, T494, T253) → U18(f1243_in(T494, T253), T252, T494, T253)
U18(f1243_out1, T252, T494, T253) → f1241_out1

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

(22) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

F3_IN(T19) → F422_IN(T19)

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:

POL(F422_IN(x₁)) = 0A + 0A · x₁

POL(U15¹(x₁, x₂)) = 0A + 0A · x₁ + -I · x₂

POL(f438_in(x₁)) = -I + 0A · x₁

POL(f438_out1(x₁, x₂, x₃)) = 1A + 1A · x₁ + -I · x₂ + -I · x₃

POL(F439_IN(x₁, x₂, x₃)) = 1A + -I · x₁ + 1A · x₂ + -I · x₃

POL(F1241_IN(x₁, x₂, x₃)) = 1A + 1A · x₁ + -I · x₂ + -I · x₃

POL(F3_IN(x₁)) = 1A + 1A · x₁

POL(.(x₁, x₂)) = 1A + -I · x₁ + 1A · x₂

POL([]) = 0A

POL(U8(x₁, x₂)) = -I + 4A · x₁ + -I · x₂

POL(f1230_in(x₁)) = -I + 4A · x₁

POL(f1230_out1(x₁, x₂, x₃)) = 5A + 5A · x₁ + -I · x₂ + -I · x₃

POL(U4(x₁, x₂)) = -I + 1A · x₁ + -I · x₂

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)

(23) Obligation:

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

F422_IN(T19) → U15¹(f438_in(T19), T19)
U15¹(f438_out1(T252, T255, T253), T19) → F439_IN(T255, T252, T253)
F439_IN(T494, T252, T253) → F1241_IN(T252, T494, T253)
F1241_IN(T252, T494, T253) → F3_IN(T252)

The TRS R consists of the following rules:

f3_in([]) → f3_out1
f3_in(T19) → U1(f48_in(T19), T19)
U1(f48_out1(X32, X51, X33, X34, X35), T19) → f3_out1
f3_in(T19) → U2(f422_in(T19), T19)
U2(f422_out1(X32, T245, X33), T19) → f3_out1
f328_in(.(T209, T210)) → f328_out1([], T209, T210)
f328_in(.(T215, T216)) → U3(f328_in(T216), .(T215, T216))
U3(f328_out1(X466, X467, X468), .(T215, T216)) → f328_out1(.(T215, X466), X467, X468)
f385_in([]) → f385_out1
f1230_in(.(T467, T468)) → f1230_out1([], T467, T468)
f1230_in(.(T476, T477)) → U4(f1230_in(T477), .(T476, T477))
U4(f1230_out1(X826, T478, X827), .(T476, T477)) → f1230_out1(.(T476, X826), T478, X827)
f56_in(.(T44, T45)) → f56_out1([], T44, T45)
f56_in(.(T50, .(T64, T65))) → f56_out1(.(T50, []), T64, T65)
f56_in(.(T50, .(T70, .(T84, T85)))) → f56_out1(.(T50, .(T70, [])), T84, T85)
f56_in(.(T50, .(T70, .(T90, .(T104, T105))))) → f56_out1(.(T50, .(T70, .(T90, []))), T104, T105)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T124, T125)))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, [])))), T124, T125)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T144, T145))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, []))))), T144, T145)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T164, T165)))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, [])))))), T164, T165)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T184, T185))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, []))))))), T184, T185)
f56_in(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → U5(f328_in(T191), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191)))))))))
U5(f328_out1(X415, X416, X417), .(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, T191))))))))) → f56_out1(.(T50, .(T70, .(T90, .(T110, .(T130, .(T150, .(T170, .(T190, X415)))))))), X416, X417)
f57_in(T29, T31) → U6(f382_in(T29, T31), T29, T31)
U6(f382_out1(X35), T29, T31) → f57_out1(void, X35)
f387_in(T31) → U7(f385_in(T31), T31)
U7(f385_out1, T31) → f387_out1(void)
f438_in(.(T270, T271)) → f438_out1([], T270, T271)
f438_in(.(T279, .(T294, T295))) → f438_out1(.(T279, []), T294, T295)
f438_in(.(T279, .(T303, .(T318, T319)))) → f438_out1(.(T279, .(T303, [])), T318, T319)
f438_in(.(T279, .(T303, .(T327, .(T342, T343))))) → f438_out1(.(T279, .(T303, .(T327, []))), T342, T343)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T366, T367)))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, [])))), T366, T367)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T390, T391))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, []))))), T390, T391)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T414, T415)))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, [])))))), T414, T415)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T438, T439))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, []))))))), T438, T439)
f438_in(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → U8(f1230_in(T448), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448)))))))))
U8(f1230_out1(X787, T449, X788), .(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, T448))))))))) → f438_out1(.(T279, .(T303, .(T327, .(T351, .(T375, .(T399, .(T423, .(T447, X787)))))))), T449, X788)
f439_in(T494, T252, T253) → U9(f1241_in(T252, T494, T253), T494, T252, T253)
U9(f1241_out1, T494, T252, T253) → f439_out1
f1243_in(T512, T253) → U10(f3_in(T253), T512, T253)
U10(f3_out1, T512, T253) → f1243_out1
f48_in(T19) → U11(f56_in(T19), T19)
U11(f56_out1(T29, T30, T31), T19) → U12(f57_in(T29, T31), T19, T29, T30, T31)
U12(f57_out1(X34, X35), T19, T29, T30, T31) → f48_out1(T29, T30, T31, X34, X35)
f382_in(T29, T31) → U13(f385_in(T29), T29, T31)
U13(f385_out1, T29, T31) → U14(f387_in(T31), T29, T31)
U14(f387_out1(X35), T29, T31) → f382_out1(X35)
f422_in(T19) → U15(f438_in(T19), T19)
U15(f438_out1(T252, T255, T253), T19) → U16(f439_in(T255, T252, T253), T19, T252, T255, T253)
U16(f439_out1, T19, T252, T255, T253) → f422_out1(T252, T255, T253)
f1241_in(T252, T494, T253) → U17(f3_in(T252), T252, T494, T253)
U17(f3_out1, T252, T494, T253) → U18(f1243_in(T494, T253), T252, T494, T253)
U18(f1243_out1, T252, T494, T253) → f1241_out1

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

(24) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.

(0) Obligation:

(1) PrologToTRSTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) UsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

(15) QDPSizeChangeProof (EQUIVALENT transformation)

(16) YES

(17) Obligation:

(18) QDPOrderProof (EQUIVALENT transformation)

(19) Obligation:

(20) DependencyGraphProof (EQUIVALENT transformation)

(21) Obligation:

(22) QDPOrderProof (EQUIVALENT transformation)

(23) Obligation:

(24) DependencyGraphProof (EQUIVALENT transformation)

(25) TRUE