Left Termination proof of /tmp/tmpOQ49d9/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 PrologToPrologProblemTransformerProof (⇒, 489 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 12 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 307 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 11 ms)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇒, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇒, 0 ms)

        ↳20 QDP

        ↳21 QDPSizeChangeProof (⇔, 0 ms)

        ↳22 YES

    ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 25 ms)

        ↳25 QDP

        ↳26 MRRProof (⇔, 708 ms)

        ↳27 QDP

        ↳28 PisEmptyProof (⇔, 0 ms)

        ↳29 YES

(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) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: in_order(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: 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];
3 [label="3: ','(!_1, eq(T4, [])) | in_order(T1, T4), SCOPE: 1, CLAUSE: 1\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: in_order(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX9 is free\nin_order(T1, T2) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: eq(T4, [])\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: eq(T4, []), SCOPE: 2, CLAUSE: 10\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19))))))\n\nT11 is ground\nX9 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19)))))), SCOPE: 3, CLAUSE: 8 | ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19)))))), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX9 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19)))))), SCOPE: 3, CLAUSE: 8\n\nT11 is ground\nX9 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(value(T12, X17), ','(app(X18, .(X17, X19), T11), ','(left(T12, X20), ','(in_order(X20, X18), ','(right(T12, X21), in_order(X21, X19)))))), SCOPE: 3, CLAUSE: 9\n\nT11 is ground\nX9 is free\nX17 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(app(X18, .(X31, X19), T11), ','(left(void, X20), ','(in_order(X20, X18), ','(right(void, X21), in_order(X21, X19)))))\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: app(X18, .(X31, X19), T11)\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19))))\n\nT17 is ground\nT19 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: app(X18, .(X31, X19), T11), SCOPE: 4, CLAUSE: 2 | app(X18, .(X31, X19), T11), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: app(X18, .(X31, X19), T11), SCOPE: 4, CLAUSE: 2\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: app(X18, .(X31, X19), T11), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX31 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: app(X80, .(X81, X82), T39)\n\nT38 is ground\nT39 is ground\nX9 is free\nX80 is free\nX81 is free\nX82 is free\nin_order(T1, .(T38, T39)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: app(X80, .(X81, X82), T39), SCOPE: 5, CLAUSE: 2 | app(X80, .(X81, X82), T39), SCOPE: 5, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nX9 is free\nX80 is free\nX81 is free\nX82 is free\nin_order(T1, .(T38, T39)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: app(X80, .(X81, X82), T39), SCOPE: 5, CLAUSE: 2\n\nT38 is ground\nT39 is ground\nX9 is free\nX80 is free\nX81 is free\nX82 is free\nin_order(T1, .(T38, T39)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: app(X80, .(X81, X82), T39), SCOPE: 5, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nX9 is free\nX80 is free\nX81 is free\nX82 is free\nin_order(T1, .(T38, T39)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: app(X125, .(X126, X127), T59)\n\nT38 is ground\nT58 is ground\nT59 is ground\nX9 is free\nX125 is free\nX126 is free\nX127 is free\nin_order(T1, .(T38, .(T58, T59))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: app(X125, .(X126, X127), T59), SCOPE: 6, CLAUSE: 2 | app(X125, .(X126, X127), T59), SCOPE: 6, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT59 is ground\nX9 is free\nX125 is free\nX126 is free\nX127 is free\nin_order(T1, .(T38, .(T58, T59))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: app(X125, .(X126, X127), T59), SCOPE: 6, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT59 is ground\nX9 is free\nX125 is free\nX126 is free\nX127 is free\nin_order(T1, .(T38, .(T58, T59))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: app(X125, .(X126, X127), T59), SCOPE: 6, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT59 is ground\nX9 is free\nX125 is free\nX126 is free\nX127 is free\nin_order(T1, .(T38, .(T58, T59))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: app(X170, .(X171, X172), T79)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT79 is ground\nX9 is free\nX170 is free\nX171 is free\nX172 is free\nin_order(T1, .(T38, .(T58, .(T78, T79)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: app(X170, .(X171, X172), T79), SCOPE: 7, CLAUSE: 2 | app(X170, .(X171, X172), T79), SCOPE: 7, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT79 is ground\nX9 is free\nX170 is free\nX171 is free\nX172 is free\nin_order(T1, .(T38, .(T58, .(T78, T79)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: app(X170, .(X171, X172), T79), SCOPE: 7, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT79 is ground\nX9 is free\nX170 is free\nX171 is free\nX172 is free\nin_order(T1, .(T38, .(T58, .(T78, T79)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: app(X170, .(X171, X172), T79), SCOPE: 7, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT79 is ground\nX9 is free\nX170 is free\nX171 is free\nX172 is free\nin_order(T1, .(T38, .(T58, .(T78, T79)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: app(X215, .(X216, X217), T99)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT99 is ground\nX9 is free\nX215 is free\nX216 is free\nX217 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, T99))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: app(X215, .(X216, X217), T99), SCOPE: 8, CLAUSE: 2 | app(X215, .(X216, X217), T99), SCOPE: 8, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT99 is ground\nX9 is free\nX215 is free\nX216 is free\nX217 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, T99))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: app(X215, .(X216, X217), T99), SCOPE: 8, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT99 is ground\nX9 is free\nX215 is free\nX216 is free\nX217 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, T99))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: app(X215, .(X216, X217), T99), SCOPE: 8, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT99 is ground\nX9 is free\nX215 is free\nX216 is free\nX217 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, T99))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: app(X260, .(X261, X262), T119)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT119 is ground\nX9 is free\nX260 is free\nX261 is free\nX262 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, T119)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: app(X260, .(X261, X262), T119), SCOPE: 9, CLAUSE: 2 | app(X260, .(X261, X262), T119), SCOPE: 9, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT119 is ground\nX9 is free\nX260 is free\nX261 is free\nX262 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, T119)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: app(X260, .(X261, X262), T119), SCOPE: 9, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT119 is ground\nX9 is free\nX260 is free\nX261 is free\nX262 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, T119)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: app(X260, .(X261, X262), T119), SCOPE: 9, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT119 is ground\nX9 is free\nX260 is free\nX261 is free\nX262 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, T119)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: app(X305, .(X306, X307), T139)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT139 is ground\nX9 is free\nX305 is free\nX306 is free\nX307 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, T139))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: app(X305, .(X306, X307), T139), SCOPE: 10, CLAUSE: 2 | app(X305, .(X306, X307), T139), SCOPE: 10, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT139 is ground\nX9 is free\nX305 is free\nX306 is free\nX307 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, T139))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: app(X305, .(X306, X307), T139), SCOPE: 10, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT139 is ground\nX9 is free\nX305 is free\nX306 is free\nX307 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, T139))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: app(X305, .(X306, X307), T139), SCOPE: 10, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT139 is ground\nX9 is free\nX305 is free\nX306 is free\nX307 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, T139))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: app(X350, .(X351, X352), T159)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT159 is ground\nX9 is free\nX350 is free\nX351 is free\nX352 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, T159)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: app(X350, .(X351, X352), T159), SCOPE: 11, CLAUSE: 2 | app(X350, .(X351, X352), T159), SCOPE: 11, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT159 is ground\nX9 is free\nX350 is free\nX351 is free\nX352 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, T159)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: app(X350, .(X351, X352), T159), SCOPE: 11, CLAUSE: 2\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT159 is ground\nX9 is free\nX350 is free\nX351 is free\nX352 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, T159)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: app(X350, .(X351, X352), T159), SCOPE: 11, CLAUSE: 3\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT159 is ground\nX9 is free\nX350 is free\nX351 is free\nX352 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, T159)))))))) !=? in_order(void, X9)", 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];
80 [label="80: app(X395, .(X396, X397), T179)\n\nT38 is ground\nT58 is ground\nT78 is ground\nT98 is ground\nT118 is ground\nT138 is ground\nT158 is ground\nT178 is ground\nT179 is ground\nX9 is free\nX395 is free\nX396 is free\nX397 is free\nin_order(T1, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: app(X395, .(X396, X397), T179)\n\nT179 is ground\nX395 is free\nX396 is free\nX397 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: app(X395, .(X396, X397), T179), SCOPE: 12, CLAUSE: 2 | app(X395, .(X396, X397), T179), SCOPE: 12, CLAUSE: 3\n\nT179 is ground\nX395 is free\nX396 is free\nX397 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: app(X395, .(X396, X397), T179), SCOPE: 12, CLAUSE: 2\n\nT179 is ground\nX395 is free\nX396 is free\nX397 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: app(X395, .(X396, X397), T179), SCOPE: 12, CLAUSE: 3\n\nT179 is ground\nX395 is free\nX396 is free\nX397 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: app(X446, .(X447, X448), T204)\n\nT204 is ground\nX446 is free\nX447 is free\nX448 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19)))), SCOPE: 13, CLAUSE: 4 | ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19)))), SCOPE: 13, CLAUSE: 5\n\nT17 is ground\nT19 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19)))), SCOPE: 13, CLAUSE: 4\n\nT17 is ground\nT19 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(left(void, X20), ','(in_order(X20, T17), ','(right(void, X21), in_order(X21, T19)))), SCOPE: 13, CLAUSE: 5\n\nT17 is ground\nT19 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(in_order(void, T17), ','(right(void, X21), in_order(X21, T19)))\n\nT17 is ground\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: in_order(void, T17)\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(right(void, X21), in_order(X21, T19))\n\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: in_order(void, T17), SCOPE: 14, CLAUSE: 0 | in_order(void, T17), SCOPE: 14, CLAUSE: 1\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(!_14, eq(T216, [])) | in_order(void, T216), SCOPE: 14, CLAUSE: 1\n\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: eq(T216, [])\n\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: eq(T216, []), SCOPE: 15, CLAUSE: 10\n\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(right(void, X21), in_order(X21, T19)), SCOPE: 16, CLAUSE: 6 | ','(right(void, X21), in_order(X21, T19)), SCOPE: 16, CLAUSE: 7\n\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(right(void, X21), in_order(X21, T19)), SCOPE: 16, CLAUSE: 6\n\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(right(void, X21), in_order(X21, T19)), SCOPE: 16, CLAUSE: 7\n\nT19 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: in_order(void, T19)\n\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(app(X18, .(T233, X19), T11), ','(left(node(T234, T233, T235), X20), ','(in_order(X20, X18), ','(right(node(T234, T233, T235), X21), in_order(X21, X19)))))\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nX20 is free\nX21 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: app(X18, .(T233, X19), T11)\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(left(node(T242, T243, T244), X20), ','(in_order(X20, T240), ','(right(node(T242, T243, T244), X21), in_order(X21, T241))))\n\nT240 is ground\nT243 is ground\nT241 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: app(X18, .(T233, X19), T11), SCOPE: 17, CLAUSE: 2 | app(X18, .(T233, X19), T11), SCOPE: 17, CLAUSE: 3\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: app(X18, .(T233, X19), T11), SCOPE: 17, CLAUSE: 2\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: app(X18, .(T233, X19), T11), SCOPE: 17, CLAUSE: 3\n\nT11 is ground\nX9 is free\nX18 is free\nX19 is free\nin_order(T1, T11) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: app(X522, .(T269, X523), T268)\n\nT267 is ground\nT268 is ground\nX9 is free\nX522 is free\nX523 is free\nin_order(T1, .(T267, T268)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: app(X522, .(T269, X523), T268), SCOPE: 18, CLAUSE: 2 | app(X522, .(T269, X523), T268), SCOPE: 18, CLAUSE: 3\n\nT267 is ground\nT268 is ground\nX9 is free\nX522 is free\nX523 is free\nin_order(T1, .(T267, T268)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: app(X522, .(T269, X523), T268), SCOPE: 18, CLAUSE: 2\n\nT267 is ground\nT268 is ground\nX9 is free\nX522 is free\nX523 is free\nin_order(T1, .(T267, T268)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: app(X522, .(T269, X523), T268), SCOPE: 18, CLAUSE: 3\n\nT267 is ground\nT268 is ground\nX9 is free\nX522 is free\nX523 is free\nin_order(T1, .(T267, T268)) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: app(X557, .(T293, X558), T292)\n\nT267 is ground\nT291 is ground\nT292 is ground\nX9 is free\nX557 is free\nX558 is free\nin_order(T1, .(T267, .(T291, T292))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: app(X557, .(T293, X558), T292), SCOPE: 19, CLAUSE: 2 | app(X557, .(T293, X558), T292), SCOPE: 19, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT292 is ground\nX9 is free\nX557 is free\nX558 is free\nin_order(T1, .(T267, .(T291, T292))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: app(X557, .(T293, X558), T292), SCOPE: 19, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT292 is ground\nX9 is free\nX557 is free\nX558 is free\nin_order(T1, .(T267, .(T291, T292))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: app(X557, .(T293, X558), T292), SCOPE: 19, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT292 is ground\nX9 is free\nX557 is free\nX558 is free\nin_order(T1, .(T267, .(T291, T292))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: app(X592, .(T317, X593), T316)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT316 is ground\nX9 is free\nX592 is free\nX593 is free\nin_order(T1, .(T267, .(T291, .(T315, T316)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: app(X592, .(T317, X593), T316), SCOPE: 20, CLAUSE: 2 | app(X592, .(T317, X593), T316), SCOPE: 20, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT316 is ground\nX9 is free\nX592 is free\nX593 is free\nin_order(T1, .(T267, .(T291, .(T315, T316)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: app(X592, .(T317, X593), T316), SCOPE: 20, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT316 is ground\nX9 is free\nX592 is free\nX593 is free\nin_order(T1, .(T267, .(T291, .(T315, T316)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: app(X592, .(T317, X593), T316), SCOPE: 20, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT316 is ground\nX9 is free\nX592 is free\nX593 is free\nin_order(T1, .(T267, .(T291, .(T315, T316)))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: app(X627, .(T341, X628), T340)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT340 is ground\nX9 is free\nX627 is free\nX628 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, T340))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: app(X627, .(T341, X628), T340), SCOPE: 21, CLAUSE: 2 | app(X627, .(T341, X628), T340), SCOPE: 21, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT340 is ground\nX9 is free\nX627 is free\nX628 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, T340))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: app(X627, .(T341, X628), T340), SCOPE: 21, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT340 is ground\nX9 is free\nX627 is free\nX628 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, T340))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: app(X627, .(T341, X628), T340), SCOPE: 21, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT340 is ground\nX9 is free\nX627 is free\nX628 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, T340))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: app(X662, .(T365, X663), T364)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT364 is ground\nX9 is free\nX662 is free\nX663 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, T364)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: app(X662, .(T365, X663), T364), SCOPE: 22, CLAUSE: 2 | app(X662, .(T365, X663), T364), SCOPE: 22, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT364 is ground\nX9 is free\nX662 is free\nX663 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, T364)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: app(X662, .(T365, X663), T364), SCOPE: 22, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT364 is ground\nX9 is free\nX662 is free\nX663 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, T364)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: app(X662, .(T365, X663), T364), SCOPE: 22, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT364 is ground\nX9 is free\nX662 is free\nX663 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, T364)))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: app(X697, .(T389, X698), T388)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT388 is ground\nX9 is free\nX697 is free\nX698 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, T388))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: app(X697, .(T389, X698), T388), SCOPE: 23, CLAUSE: 2 | app(X697, .(T389, X698), T388), SCOPE: 23, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT388 is ground\nX9 is free\nX697 is free\nX698 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, T388))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: app(X697, .(T389, X698), T388), SCOPE: 23, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT388 is ground\nX9 is free\nX697 is free\nX698 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, T388))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: app(X697, .(T389, X698), T388), SCOPE: 23, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT388 is ground\nX9 is free\nX697 is free\nX698 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, T388))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: app(X732, .(T413, X733), T412)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT412 is ground\nX9 is free\nX732 is free\nX733 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, T412)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: app(X732, .(T413, X733), T412), SCOPE: 24, CLAUSE: 2 | app(X732, .(T413, X733), T412), SCOPE: 24, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT412 is ground\nX9 is free\nX732 is free\nX733 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, T412)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: app(X732, .(T413, X733), T412), SCOPE: 24, CLAUSE: 2\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT412 is ground\nX9 is free\nX732 is free\nX733 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, T412)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: app(X732, .(T413, X733), T412), SCOPE: 24, CLAUSE: 3\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT412 is ground\nX9 is free\nX732 is free\nX733 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, T412)))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: app(X767, .(T437, X768), T436)\n\nT267 is ground\nT291 is ground\nT315 is ground\nT339 is ground\nT363 is ground\nT387 is ground\nT411 is ground\nT435 is ground\nT436 is ground\nX9 is free\nX767 is free\nX768 is free\nin_order(T1, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) !=? in_order(void, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: app(X767, .(T437, X768), T436)\n\nT436 is ground\nX767 is free\nX768 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: app(X767, .(T437, X768), T436), SCOPE: 25, CLAUSE: 2 | app(X767, .(T437, X768), T436), SCOPE: 25, CLAUSE: 3\n\nT436 is ground\nX767 is free\nX768 is free", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: app(X767, .(T437, X768), T436), SCOPE: 25, CLAUSE: 2\n\nT436 is ground\nX767 is free\nX768 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: app(X767, .(T437, X768), T436), SCOPE: 25, CLAUSE: 3\n\nT436 is ground\nX767 is free\nX768 is free", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: app(X806, .(T466, X807), T465)\n\nT465 is ground\nX806 is free\nX807 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(left(node(T242, T243, T244), X20), ','(in_order(X20, T240), ','(right(node(T242, T243, T244), X21), in_order(X21, T241)))), SCOPE: 26, CLAUSE: 4 | ','(left(node(T242, T243, T244), X20), ','(in_order(X20, T240), ','(right(node(T242, T243, T244), X21), in_order(X21, T241)))), SCOPE: 26, CLAUSE: 5\n\nT240 is ground\nT243 is ground\nT241 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(left(node(T242, T243, T244), X20), ','(in_order(X20, T240), ','(right(node(T242, T243, T244), X21), in_order(X21, T241)))), SCOPE: 26, CLAUSE: 5\n\nT240 is ground\nT243 is ground\nT241 is ground\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(in_order(T484, T240), ','(right(node(T484, T482, T485), X21), in_order(X21, T241)))\n\nT240 is ground\nT241 is ground\nT482 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: in_order(T484, T240)\n\nT240 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(right(node(T487, T482, T488), X21), in_order(X21, T241))\n\nT241 is ground\nT482 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(right(node(T487, T482, T488), X21), in_order(X21, T241)), SCOPE: 27, CLAUSE: 6 | ','(right(node(T487, T482, T488), X21), in_order(X21, T241)), SCOPE: 27, CLAUSE: 7\n\nT241 is ground\nT482 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(right(node(T487, T482, T488), X21), in_order(X21, T241)), SCOPE: 27, CLAUSE: 7\n\nT241 is ground\nT482 is ground\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: in_order(T502, T241)\n\nT241 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 195 [arrowhead = none ];
195 -> 2;

196 [label="EVAL with clause\nin_order(void, X9) :- ','(!_1, eq(X9, [])).\nand substitutionT1 -> void,\nT2 -> T4,\nX9 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 196 [arrowhead = none ];
196 -> 3;

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

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

199 [label="ONLY EVAL with clause\nin_order(X15, X16) :- ','(value(X15, X17), ','(app(X18, .(X17, X19), X16), ','(left(X15, X20), ','(in_order(X20, X18), ','(right(X15, X21), in_order(X21, X19)))))).\nand substitutionT1 -> T12,\nX15 -> T12,\nT2 -> T11,\nX16 -> T11,\nT10 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 199 [arrowhead = none ];
199 -> 10;

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

201 [label="EVAL with clause\neq(X12, X12).\nand substitutionT4 -> [],\nX12 -> [],\nT7 -> []", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 201 [arrowhead = none ];
201 -> 7;

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

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

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

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

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

207 [label="EVAL with clause\nvalue(void, X30).\nand substitutionT12 -> void,\nX17 -> X31,\nX30 -> X31", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 207 [arrowhead = none ];
207 -> 14;

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

209 [label="EVAL with clause\nvalue(node(X482, X483, X484), X483).\nand substitutionX482 -> T234,\nX483 -> T233,\nX484 -> T235,\nT12 -> node(T234, T233, T235),\nX17 -> T233,\nT231 -> T233,\nT230 -> T234,\nT232 -> T235", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 209 [arrowhead = none ];
209 -> 110;

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

211 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
14 -> 211 [arrowhead = none ];
211 -> 16;

212 [label="SPLIT 2\nnew knowledge:\nT17 is ground\nT18 is ground\nT19 is ground\nT11 is ground\nreplacements:X18 -> T17,\nX31 -> T18,\nX19 -> T19", fontsize=14, style = filled, fillcolor = violet];
14 -> 212 [arrowhead = none ];
212 -> 17;

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

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

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

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

217 [label="EVAL with clause\napp([], X56, X56).\nand substitutionX18 -> [],\nX31 -> T32,\nX19 -> T33,\nX56 -> .(T32, T33),\nX57 -> T32,\nX58 -> T33,\nT11 -> .(T32, T33)", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 217 [arrowhead = none ];
217 -> 21;

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

219 [label="EVAL with clause\napp(.(X75, X76), X77, .(X75, X78)) :- app(X76, X77, X78).\nand substitutionX75 -> T38,\nX76 -> X80,\nX18 -> .(T38, X80),\nX31 -> X81,\nX19 -> X82,\nX77 -> .(X81, X82),\nX79 -> T38,\nX78 -> T39,\nT11 -> .(T38, T39)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 219 [arrowhead = none ];
219 -> 24;

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

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

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

223 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 223 [arrowhead = none ];
223 -> 27;

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 224 [arrowhead = none ];
224 -> 28;

225 [label="EVAL with clause\napp([], X101, X101).\nand substitutionX80 -> [],\nX81 -> T52,\nX82 -> T53,\nX101 -> .(T52, T53),\nX102 -> T52,\nX103 -> T53,\nT39 -> .(T52, T53)", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 225 [arrowhead = none ];
225 -> 29;

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

227 [label="EVAL with clause\napp(.(X120, X121), X122, .(X120, X123)) :- app(X121, X122, X123).\nand substitutionX120 -> T58,\nX121 -> X125,\nX80 -> .(T58, X125),\nX81 -> X126,\nX82 -> X127,\nX122 -> .(X126, X127),\nX124 -> T58,\nX123 -> T59,\nT39 -> .(T58, T59)", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 227 [arrowhead = none ];
227 -> 32;

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

229 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 229 [arrowhead = none ];
229 -> 31;

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

231 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 231 [arrowhead = none ];
231 -> 35;

232 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 232 [arrowhead = none ];
232 -> 36;

233 [label="EVAL with clause\napp([], X146, X146).\nand substitutionX125 -> [],\nX126 -> T72,\nX127 -> T73,\nX146 -> .(T72, T73),\nX147 -> T72,\nX148 -> T73,\nT59 -> .(T72, T73)", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 233 [arrowhead = none ];
233 -> 37;

234 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 234 [arrowhead = none ];
234 -> 38;

235 [label="EVAL with clause\napp(.(X165, X166), X167, .(X165, X168)) :- app(X166, X167, X168).\nand substitutionX165 -> T78,\nX166 -> X170,\nX125 -> .(T78, X170),\nX126 -> X171,\nX127 -> X172,\nX167 -> .(X171, X172),\nX169 -> T78,\nX168 -> T79,\nT59 -> .(T78, T79)", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 235 [arrowhead = none ];
235 -> 40;

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

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

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

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

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

241 [label="EVAL with clause\napp([], X191, X191).\nand substitutionX170 -> [],\nX171 -> T92,\nX172 -> T93,\nX191 -> .(T92, T93),\nX192 -> T92,\nX193 -> T93,\nT79 -> .(T92, T93)", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 241 [arrowhead = none ];
241 -> 45;

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

243 [label="EVAL with clause\napp(.(X210, X211), X212, .(X210, X213)) :- app(X211, X212, X213).\nand substitutionX210 -> T98,\nX211 -> X215,\nX170 -> .(T98, X215),\nX171 -> X216,\nX172 -> X217,\nX212 -> .(X216, X217),\nX214 -> T98,\nX213 -> T99,\nT79 -> .(T98, T99)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 243 [arrowhead = none ];
243 -> 48;

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

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

246 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
48 -> 246 [arrowhead = none ];
246 -> 50;

247 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 247 [arrowhead = none ];
247 -> 51;

248 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 248 [arrowhead = none ];
248 -> 52;

249 [label="EVAL with clause\napp([], X236, X236).\nand substitutionX215 -> [],\nX216 -> T112,\nX217 -> T113,\nX236 -> .(T112, T113),\nX237 -> T112,\nX238 -> T113,\nT99 -> .(T112, T113)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 249 [arrowhead = none ];
249 -> 53;

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

251 [label="EVAL with clause\napp(.(X255, X256), X257, .(X255, X258)) :- app(X256, X257, X258).\nand substitutionX255 -> T118,\nX256 -> X260,\nX215 -> .(T118, X260),\nX216 -> X261,\nX217 -> X262,\nX257 -> .(X261, X262),\nX259 -> T118,\nX258 -> T119,\nT99 -> .(T118, T119)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 251 [arrowhead = none ];
251 -> 56;

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

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

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

255 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 255 [arrowhead = none ];
255 -> 59;

256 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 256 [arrowhead = none ];
256 -> 60;

257 [label="EVAL with clause\napp([], X281, X281).\nand substitutionX260 -> [],\nX261 -> T132,\nX262 -> T133,\nX281 -> .(T132, T133),\nX282 -> T132,\nX283 -> T133,\nT119 -> .(T132, T133)", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 257 [arrowhead = none ];
257 -> 61;

258 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 258 [arrowhead = none ];
258 -> 62;

259 [label="EVAL with clause\napp(.(X300, X301), X302, .(X300, X303)) :- app(X301, X302, X303).\nand substitutionX300 -> T138,\nX301 -> X305,\nX260 -> .(T138, X305),\nX261 -> X306,\nX262 -> X307,\nX302 -> .(X306, X307),\nX304 -> T138,\nX303 -> T139,\nT119 -> .(T138, T139)", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 259 [arrowhead = none ];
259 -> 64;

260 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 260 [arrowhead = none ];
260 -> 65;

261 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 261 [arrowhead = none ];
261 -> 63;

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

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

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

265 [label="EVAL with clause\napp([], X326, X326).\nand substitutionX305 -> [],\nX306 -> T152,\nX307 -> T153,\nX326 -> .(T152, T153),\nX327 -> T152,\nX328 -> T153,\nT139 -> .(T152, T153)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 265 [arrowhead = none ];
265 -> 69;

266 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 266 [arrowhead = none ];
266 -> 70;

267 [label="EVAL with clause\napp(.(X345, X346), X347, .(X345, X348)) :- app(X346, X347, X348).\nand substitutionX345 -> T158,\nX346 -> X350,\nX305 -> .(T158, X350),\nX306 -> X351,\nX307 -> X352,\nX347 -> .(X351, X352),\nX349 -> T158,\nX348 -> T159,\nT139 -> .(T158, T159)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 267 [arrowhead = none ];
267 -> 72;

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

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

270 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 270 [arrowhead = none ];
270 -> 74;

271 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 271 [arrowhead = none ];
271 -> 75;

272 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 272 [arrowhead = none ];
272 -> 76;

273 [label="EVAL with clause\napp([], X371, X371).\nand substitutionX350 -> [],\nX351 -> T172,\nX352 -> T173,\nX371 -> .(T172, T173),\nX372 -> T172,\nX373 -> T173,\nT159 -> .(T172, T173)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 273 [arrowhead = none ];
273 -> 77;

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

275 [label="EVAL with clause\napp(.(X390, X391), X392, .(X390, X393)) :- app(X391, X392, X393).\nand substitutionX390 -> T178,\nX391 -> X395,\nX350 -> .(T178, X395),\nX351 -> X396,\nX352 -> X397,\nX392 -> .(X396, X397),\nX394 -> T178,\nX393 -> T179,\nT159 -> .(T178, T179)", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 275 [arrowhead = none ];
275 -> 80;

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

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

278 [label="GENERALIZATION\nT184 <-- .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))\n\nNew Knowledge:\nT184 is ground", fontsize=14, style = filled, fillcolor = violet];
80 -> 278 [arrowhead = none ];
278 -> 82;

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

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

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

282 [label="EVAL with clause\napp([], X422, X422).\nand substitutionX395 -> [],\nX396 -> T197,\nX397 -> T198,\nX422 -> .(T197, T198),\nX423 -> T197,\nX424 -> T198,\nT179 -> .(T197, T198)", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 282 [arrowhead = none ];
282 -> 86;

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

284 [label="EVAL with clause\napp(.(X441, X442), X443, .(X441, X444)) :- app(X442, X443, X444).\nand substitutionX441 -> T203,\nX442 -> X446,\nX395 -> .(T203, X446),\nX396 -> X447,\nX397 -> X448,\nX443 -> .(X447, X448),\nX445 -> T203,\nX444 -> T204,\nT179 -> .(T203, T204)", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 284 [arrowhead = none ];
284 -> 89;

285 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 285 [arrowhead = none ];
285 -> 90;

286 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 286 [arrowhead = none ];
286 -> 88;

287 [label="INSTANCE with matching:\nX395 -> X446\nX396 -> X447\nX397 -> X448\nT179 -> T204", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 287 [arrowhead = none , style=dashed];
287 -> 82[style=dashed];

288 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
91 -> 288 [arrowhead = none ];
288 -> 92;

289 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
91 -> 289 [arrowhead = none ];
289 -> 93;

290 [label="ONLY EVAL with clause\nleft(void, void).\nand substitutionX20 -> void", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 290 [arrowhead = none ];
290 -> 94;

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

292 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
94 -> 292 [arrowhead = none ];
292 -> 95;

293 [label="SPLIT 2\nnew knowledge:\nT17 is ground", fontsize=14, style = filled, fillcolor = violet];
94 -> 293 [arrowhead = none ];
293 -> 96;

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

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

296 [label="ONLY EVAL with clause\nin_order(void, X462) :- ','(!_14, eq(X462, [])).\nand substitutionT17 -> T216,\nX462 -> T216", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 296 [arrowhead = none ];
296 -> 98;

297 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 297 [arrowhead = none ];
297 -> 99;

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

299 [label="EVAL with clause\neq(X465, X465).\nand substitutionT216 -> [],\nX465 -> [],\nT219 -> []", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 299 [arrowhead = none ];
299 -> 101;

300 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 300 [arrowhead = none ];
300 -> 102;

301 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 301 [arrowhead = none ];
301 -> 103;

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

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

304 [label="ONLY EVAL with clause\nright(void, void).\nand substitutionX21 -> void", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 304 [arrowhead = none ];
304 -> 107;

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

306 [label="INSTANCE with matching:\nT17 -> T19", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 306 [arrowhead = none , style=dashed];
306 -> 95[style=dashed];

307 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
110 -> 307 [arrowhead = none ];
307 -> 112;

308 [label="SPLIT 2\nnew knowledge:\nT240 is ground\nT243 is ground\nT241 is ground\nT11 is ground\nreplacements:X18 -> T240,\nX19 -> T241,\nT234 -> T242,\nT233 -> T243,\nT235 -> T244,\nT1 -> T245", fontsize=14, style = filled, fillcolor = violet];
110 -> 308 [arrowhead = none ];
308 -> 113;

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

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

311 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
114 -> 311 [arrowhead = none ];
311 -> 115;

312 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
114 -> 312 [arrowhead = none ];
312 -> 116;

313 [label="EVAL with clause\napp([], X501, X501).\nand substitutionX18 -> [],\nT233 -> T258,\nX19 -> T259,\nX501 -> .(T258, T259),\nX502 -> T259,\nT11 -> .(T258, T259)", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 313 [arrowhead = none ];
313 -> 117;

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

315 [label="EVAL with clause\napp(.(X517, X518), X519, .(X517, X520)) :- app(X518, X519, X520).\nand substitutionX517 -> T267,\nX518 -> X522,\nX18 -> .(T267, X522),\nT233 -> T269,\nX19 -> X523,\nX519 -> .(T269, X523),\nX521 -> T267,\nX520 -> T268,\nT11 -> .(T267, T268),\nT266 -> T269", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 315 [arrowhead = none ];
315 -> 120;

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

317 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 317 [arrowhead = none ];
317 -> 119;

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

319 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
122 -> 319 [arrowhead = none ];
319 -> 123;

320 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
122 -> 320 [arrowhead = none ];
320 -> 124;

321 [label="EVAL with clause\napp([], X536, X536).\nand substitutionX522 -> [],\nT269 -> T282,\nX523 -> T283,\nX536 -> .(T282, T283),\nX537 -> T283,\nT268 -> .(T282, T283)", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 321 [arrowhead = none ];
321 -> 125;

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

323 [label="EVAL with clause\napp(.(X552, X553), X554, .(X552, X555)) :- app(X553, X554, X555).\nand substitutionX552 -> T291,\nX553 -> X557,\nX522 -> .(T291, X557),\nT269 -> T293,\nX523 -> X558,\nX554 -> .(T293, X558),\nX556 -> T291,\nX555 -> T292,\nT268 -> .(T291, T292),\nT290 -> T293", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 323 [arrowhead = none ];
323 -> 128;

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

325 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 325 [arrowhead = none ];
325 -> 127;

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

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

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

329 [label="EVAL with clause\napp([], X571, X571).\nand substitutionX557 -> [],\nT293 -> T306,\nX558 -> T307,\nX571 -> .(T306, T307),\nX572 -> T307,\nT292 -> .(T306, T307)", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 329 [arrowhead = none ];
329 -> 133;

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

331 [label="EVAL with clause\napp(.(X587, X588), X589, .(X587, X590)) :- app(X588, X589, X590).\nand substitutionX587 -> T315,\nX588 -> X592,\nX557 -> .(T315, X592),\nT293 -> T317,\nX558 -> X593,\nX589 -> .(T317, X593),\nX591 -> T315,\nX590 -> T316,\nT292 -> .(T315, T316),\nT314 -> T317", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 331 [arrowhead = none ];
331 -> 136;

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

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

334 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
136 -> 334 [arrowhead = none ];
334 -> 138;

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

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

337 [label="EVAL with clause\napp([], X606, X606).\nand substitutionX592 -> [],\nT317 -> T330,\nX593 -> T331,\nX606 -> .(T330, T331),\nX607 -> T331,\nT316 -> .(T330, T331)", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 337 [arrowhead = none ];
337 -> 141;

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

339 [label="EVAL with clause\napp(.(X622, X623), X624, .(X622, X625)) :- app(X623, X624, X625).\nand substitutionX622 -> T339,\nX623 -> X627,\nX592 -> .(T339, X627),\nT317 -> T341,\nX593 -> X628,\nX624 -> .(T341, X628),\nX626 -> T339,\nX625 -> T340,\nT316 -> .(T339, T340),\nT338 -> T341", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 339 [arrowhead = none ];
339 -> 144;

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

341 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 341 [arrowhead = none ];
341 -> 143;

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

343 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
146 -> 343 [arrowhead = none ];
343 -> 147;

344 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
146 -> 344 [arrowhead = none ];
344 -> 148;

345 [label="EVAL with clause\napp([], X641, X641).\nand substitutionX627 -> [],\nT341 -> T354,\nX628 -> T355,\nX641 -> .(T354, T355),\nX642 -> T355,\nT340 -> .(T354, T355)", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 345 [arrowhead = none ];
345 -> 149;

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

347 [label="EVAL with clause\napp(.(X657, X658), X659, .(X657, X660)) :- app(X658, X659, X660).\nand substitutionX657 -> T363,\nX658 -> X662,\nX627 -> .(T363, X662),\nT341 -> T365,\nX628 -> X663,\nX659 -> .(T365, X663),\nX661 -> T363,\nX660 -> T364,\nT340 -> .(T363, T364),\nT362 -> T365", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 347 [arrowhead = none ];
347 -> 152;

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

349 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 349 [arrowhead = none ];
349 -> 151;

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

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

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

353 [label="EVAL with clause\napp([], X676, X676).\nand substitutionX662 -> [],\nT365 -> T378,\nX663 -> T379,\nX676 -> .(T378, T379),\nX677 -> T379,\nT364 -> .(T378, T379)", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 353 [arrowhead = none ];
353 -> 157;

354 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 354 [arrowhead = none ];
354 -> 158;

355 [label="EVAL with clause\napp(.(X692, X693), X694, .(X692, X695)) :- app(X693, X694, X695).\nand substitutionX692 -> T387,\nX693 -> X697,\nX662 -> .(T387, X697),\nT365 -> T389,\nX663 -> X698,\nX694 -> .(T389, X698),\nX696 -> T387,\nX695 -> T388,\nT364 -> .(T387, T388),\nT386 -> T389", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 355 [arrowhead = none ];
355 -> 160;

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

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

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

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

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

361 [label="EVAL with clause\napp([], X711, X711).\nand substitutionX697 -> [],\nT389 -> T402,\nX698 -> T403,\nX711 -> .(T402, T403),\nX712 -> T403,\nT388 -> .(T402, T403)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 361 [arrowhead = none ];
361 -> 165;

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

363 [label="EVAL with clause\napp(.(X727, X728), X729, .(X727, X730)) :- app(X728, X729, X730).\nand substitutionX727 -> T411,\nX728 -> X732,\nX697 -> .(T411, X732),\nT389 -> T413,\nX698 -> X733,\nX729 -> .(T413, X733),\nX731 -> T411,\nX730 -> T412,\nT388 -> .(T411, T412),\nT410 -> T413", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 363 [arrowhead = none ];
363 -> 168;

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

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

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

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

368 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
170 -> 368 [arrowhead = none ];
368 -> 172;

369 [label="EVAL with clause\napp([], X746, X746).\nand substitutionX732 -> [],\nT413 -> T426,\nX733 -> T427,\nX746 -> .(T426, T427),\nX747 -> T427,\nT412 -> .(T426, T427)", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 369 [arrowhead = none ];
369 -> 173;

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

371 [label="EVAL with clause\napp(.(X762, X763), X764, .(X762, X765)) :- app(X763, X764, X765).\nand substitutionX762 -> T435,\nX763 -> X767,\nX732 -> .(T435, X767),\nT413 -> T437,\nX733 -> X768,\nX764 -> .(T437, X768),\nX766 -> T435,\nX765 -> T436,\nT412 -> .(T435, T436),\nT434 -> T437", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 371 [arrowhead = none ];
371 -> 176;

372 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 372 [arrowhead = none ];
372 -> 177;

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

374 [label="GENERALIZATION\nT442 <-- .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))\n\nNew Knowledge:\nT442 is ground", fontsize=14, style = filled, fillcolor = violet];
176 -> 374 [arrowhead = none ];
374 -> 178;

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

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

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

378 [label="EVAL with clause\napp([], X785, X785).\nand substitutionX767 -> [],\nT437 -> T455,\nX768 -> T456,\nX785 -> .(T455, T456),\nX786 -> T456,\nT436 -> .(T455, T456)", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 378 [arrowhead = none ];
378 -> 182;

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

380 [label="EVAL with clause\napp(.(X801, X802), X803, .(X801, X804)) :- app(X802, X803, X804).\nand substitutionX801 -> T464,\nX802 -> X806,\nX767 -> .(T464, X806),\nT437 -> T466,\nX768 -> X807,\nX803 -> .(T466, X807),\nX805 -> T464,\nX804 -> T465,\nT436 -> .(T464, T465),\nT463 -> T466", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 380 [arrowhead = none ];
380 -> 185;

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

382 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 382 [arrowhead = none ];
382 -> 184;

383 [label="INSTANCE with matching:\nX767 -> X806\nT437 -> T466\nX768 -> X807\nT436 -> T465", fontsize=14, style = filled, fillcolor = lightgrey];
185 -> 383 [arrowhead = none , style=dashed];
383 -> 178[style=dashed];

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

385 [label="ONLY EVAL with clause\nleft(node(X820, X821, X822), X820).\nand substitutionT242 -> T484,\nX820 -> T484,\nT243 -> T482,\nX821 -> T482,\nT244 -> T485,\nX822 -> T485,\nX20 -> T484,\nT481 -> T484,\nT483 -> T485", fontsize=14, style = filled, fillcolor = lightblue];
188 -> 385 [arrowhead = none ];
385 -> 189;

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

387 [label="SPLIT 2\nnew knowledge:\nT240 is ground\nreplacements:T484 -> T487,\nT485 -> T488", fontsize=14, style = filled, fillcolor = violet];
189 -> 387 [arrowhead = none ];
387 -> 191;

388 [label="INSTANCE with matching:\nT1 -> T484\nT2 -> T240", fontsize=14, style = filled, fillcolor = lightgrey];
190 -> 388 [arrowhead = none , style=dashed];
388 -> 1[style=dashed];

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

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

391 [label="ONLY EVAL with clause\nright(node(X833, X834, X835), X835).\nand substitutionT487 -> T499,\nX833 -> T499,\nT482 -> T500,\nX834 -> T500,\nT488 -> T502,\nX835 -> T502,\nX21 -> T502,\nT501 -> T502", fontsize=14, style = filled, fillcolor = lightblue];
193 -> 391 [arrowhead = none ];
391 -> 194;

392 [label="INSTANCE with matching:\nT1 -> T502\nT2 -> T241", fontsize=14, style = filled, fillcolor = lightgrey];
194 -> 392 [arrowhead = none , style=dashed];
392 -> 1[style=dashed];

}

(2) Obligation:

Clauses:

appA([], T197, T198, .(T197, T198)).
appA(.(T203, X446), X447, X448, .(T203, T204)) :- appA(X446, X447, X448, T204).
in_orderB([]).
appC([], T455, T456, .(T455, T456)).
appC(.(T464, X806), T466, X807, .(T464, T465)) :- appC(X806, T466, X807, T465).
appD([], T32, T33, .(T32, T33)).
appD(.(T38, []), T52, T53, .(T38, .(T52, T53))).
appD(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73)))).
appD(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93))))).
appD(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113)))))).
appD(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))).
appD(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))).
appD(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))).
appD(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) :- appA(X395, X396, X397, T179).
appE([], T258, T259, .(T258, T259)).
appE(.(T267, []), T282, T283, .(T267, .(T282, T283))).
appE(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307)))).
appE(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331))))).
appE(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355)))))).
appE(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))).
appE(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))).
appE(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))).
appE(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) :- appC(X767, T437, X768, T436).
in_orderF(void, []).
in_orderF(void, T11) :- appD(X18, X31, X19, T11).
in_orderF(void, T11) :- ','(appD(T17, T18, T19, T11), in_orderB(T17)).
in_orderF(void, T11) :- ','(appD(T17, T18, T19, T11), ','(in_orderB(T17), in_orderB(T19))).
in_orderF(node(T234, T233, T235), T11) :- appE(X18, T233, X19, T11).
in_orderF(node(T484, T482, T485), T11) :- ','(appE(T240, T482, T241, T11), in_orderF(T484, T240)).
in_orderF(node(T499, T500, T502), T11) :- ','(appE(T240, T500, T241, T11), ','(in_orderF(T499, T240), in_orderF(T502, T241))).

Query: in_orderF(a,g)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
in_orderF_in: (f,b)
appD_in: (f,f,f,b)
appA_in: (f,f,f,b)
appE_in: (f,f,f,b)
appC_in: (f,f,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

in_orderF_in_ag(void, []) → in_orderF_out_ag(void, [])
in_orderF_in_ag(void, T11) → U5_ag(T11, appD_in_aaag(X18, X31, X19, T11))
appD_in_aaag([], T32, T33, .(T32, T33)) → appD_out_aaag([], T32, T33, .(T32, T33))
appD_in_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53)))
appD_in_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73))))
appD_in_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93)))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133)))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173)))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
appA_in_aaag([], T197, T198, .(T197, T198)) → appA_out_aaag([], T197, T198, .(T197, T198))
appA_in_aaag(.(T203, X446), X447, X448, .(T203, T204)) → U1_aaag(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
U1_aaag(T203, X446, X447, X448, T204, appA_out_aaag(X446, X447, X448, T204)) → appA_out_aaag(.(T203, X446), X447, X448, .(T203, T204))
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_out_aaag(X395, X396, X397, T179)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))))
U5_ag(T11, appD_out_aaag(X18, X31, X19, T11)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(void, T11) → U6_ag(T11, appD_in_aaag(T17, T18, T19, T11))
U6_ag(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_ag(T11, T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g([])
U7_ag(T11, T19, in_orderB_out_g(T17)) → in_orderF_out_ag(void, T11)
U7_ag(T11, T19, in_orderB_out_g(T17)) → U8_ag(T11, in_orderB_in_g(T19))
U8_ag(T11, in_orderB_out_g(T19)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(node(T234, T233, T235), T11) → U9_ag(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
appE_in_aaag([], T258, T259, .(T258, T259)) → appE_out_aaag([], T258, T259, .(T258, T259))
appE_in_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283)))
appE_in_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307))))
appE_in_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331)))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379)))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427)))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
appC_in_aaag([], T455, T456, .(T455, T456)) → appC_out_aaag([], T455, T456, .(T455, T456))
appC_in_aaag(.(T464, X806), T466, X807, .(T464, T465)) → U2_aaag(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
U2_aaag(T464, X806, T466, X807, T465, appC_out_aaag(X806, T466, X807, T465)) → appC_out_aaag(.(T464, X806), T466, X807, .(T464, T465))
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_out_aaag(X767, T437, X768, T436)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))))
U9_ag(T234, T233, T235, T11, appE_out_aaag(X18, T233, X19, T11)) → in_orderF_out_ag(node(T234, T233, T235), T11)
in_orderF_in_ag(node(T484, T482, T485), T11) → U10_ag(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_ag(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_ag(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
in_orderF_in_ag(node(T499, T500, T502), T11) → U12_ag(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_ag(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_ag(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U13_ag(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_ag(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U14_ag(T499, T500, T502, T11, in_orderF_out_ag(T502, T241)) → in_orderF_out_ag(node(T499, T500, T502), T11)
U11_ag(T484, T482, T485, T11, in_orderF_out_ag(T484, T240)) → in_orderF_out_ag(node(T484, T482, T485), T11)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

in_orderF_in_ag(void, []) → in_orderF_out_ag(void, [])
in_orderF_in_ag(void, T11) → U5_ag(T11, appD_in_aaag(X18, X31, X19, T11))
appD_in_aaag([], T32, T33, .(T32, T33)) → appD_out_aaag([], T32, T33, .(T32, T33))
appD_in_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53)))
appD_in_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73))))
appD_in_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93)))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133)))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173)))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
appA_in_aaag([], T197, T198, .(T197, T198)) → appA_out_aaag([], T197, T198, .(T197, T198))
appA_in_aaag(.(T203, X446), X447, X448, .(T203, T204)) → U1_aaag(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
U1_aaag(T203, X446, X447, X448, T204, appA_out_aaag(X446, X447, X448, T204)) → appA_out_aaag(.(T203, X446), X447, X448, .(T203, T204))
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_out_aaag(X395, X396, X397, T179)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))))
U5_ag(T11, appD_out_aaag(X18, X31, X19, T11)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(void, T11) → U6_ag(T11, appD_in_aaag(T17, T18, T19, T11))
U6_ag(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_ag(T11, T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g([])
U7_ag(T11, T19, in_orderB_out_g(T17)) → in_orderF_out_ag(void, T11)
U7_ag(T11, T19, in_orderB_out_g(T17)) → U8_ag(T11, in_orderB_in_g(T19))
U8_ag(T11, in_orderB_out_g(T19)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(node(T234, T233, T235), T11) → U9_ag(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
appE_in_aaag([], T258, T259, .(T258, T259)) → appE_out_aaag([], T258, T259, .(T258, T259))
appE_in_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283)))
appE_in_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307))))
appE_in_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331)))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379)))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427)))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
appC_in_aaag([], T455, T456, .(T455, T456)) → appC_out_aaag([], T455, T456, .(T455, T456))
appC_in_aaag(.(T464, X806), T466, X807, .(T464, T465)) → U2_aaag(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
U2_aaag(T464, X806, T466, X807, T465, appC_out_aaag(X806, T466, X807, T465)) → appC_out_aaag(.(T464, X806), T466, X807, .(T464, T465))
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_out_aaag(X767, T437, X768, T436)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))))
U9_ag(T234, T233, T235, T11, appE_out_aaag(X18, T233, X19, T11)) → in_orderF_out_ag(node(T234, T233, T235), T11)
in_orderF_in_ag(node(T484, T482, T485), T11) → U10_ag(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_ag(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_ag(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
in_orderF_in_ag(node(T499, T500, T502), T11) → U12_ag(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_ag(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_ag(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U13_ag(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_ag(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U14_ag(T499, T500, T502, T11, in_orderF_out_ag(T502, T241)) → in_orderF_out_ag(node(T499, T500, T502), T11)
U11_ag(T484, T482, T485, T11, in_orderF_out_ag(T484, T240)) → in_orderF_out_ag(node(T484, T482, T485), T11)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

IN_ORDERF_IN_AG(void, T11) → U5_AG(T11, appD_in_aaag(X18, X31, X19, T11))
IN_ORDERF_IN_AG(void, T11) → APPD_IN_AAAG(X18, X31, X19, T11)
APPD_IN_AAAG(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_AAAG(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
APPD_IN_AAAG(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → APPA_IN_AAAG(X395, X396, X397, T179)
APPA_IN_AAAG(.(T203, X446), X447, X448, .(T203, T204)) → U1_AAAG(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
APPA_IN_AAAG(.(T203, X446), X447, X448, .(T203, T204)) → APPA_IN_AAAG(X446, X447, X448, T204)
IN_ORDERF_IN_AG(void, T11) → U6_AG(T11, appD_in_aaag(T17, T18, T19, T11))
U6_AG(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_AG(T11, T19, in_orderB_in_g(T17))
U6_AG(T11, appD_out_aaag(T17, T18, T19, T11)) → IN_ORDERB_IN_G(T17)
U7_AG(T11, T19, in_orderB_out_g(T17)) → U8_AG(T11, in_orderB_in_g(T19))
U7_AG(T11, T19, in_orderB_out_g(T17)) → IN_ORDERB_IN_G(T19)
IN_ORDERF_IN_AG(node(T234, T233, T235), T11) → U9_AG(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
IN_ORDERF_IN_AG(node(T234, T233, T235), T11) → APPE_IN_AAAG(X18, T233, X19, T11)
APPE_IN_AAAG(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_AAAG(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
APPE_IN_AAAG(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → APPC_IN_AAAG(X767, T437, X768, T436)
APPC_IN_AAAG(.(T464, X806), T466, X807, .(T464, T465)) → U2_AAAG(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
APPC_IN_AAAG(.(T464, X806), T466, X807, .(T464, T465)) → APPC_IN_AAAG(X806, T466, X807, T465)
IN_ORDERF_IN_AG(node(T484, T482, T485), T11) → U10_AG(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_AG(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_AG(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
U10_AG(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → IN_ORDERF_IN_AG(T484, T240)
IN_ORDERF_IN_AG(node(T499, T500, T502), T11) → U12_AG(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_AG(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_AG(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U12_AG(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → IN_ORDERF_IN_AG(T499, T240)
U13_AG(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_AG(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U13_AG(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → IN_ORDERF_IN_AG(T502, T241)

The TRS R consists of the following rules:

in_orderF_in_ag(void, []) → in_orderF_out_ag(void, [])
in_orderF_in_ag(void, T11) → U5_ag(T11, appD_in_aaag(X18, X31, X19, T11))
appD_in_aaag([], T32, T33, .(T32, T33)) → appD_out_aaag([], T32, T33, .(T32, T33))
appD_in_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53)))
appD_in_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73))))
appD_in_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93)))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133)))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173)))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
appA_in_aaag([], T197, T198, .(T197, T198)) → appA_out_aaag([], T197, T198, .(T197, T198))
appA_in_aaag(.(T203, X446), X447, X448, .(T203, T204)) → U1_aaag(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
U1_aaag(T203, X446, X447, X448, T204, appA_out_aaag(X446, X447, X448, T204)) → appA_out_aaag(.(T203, X446), X447, X448, .(T203, T204))
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_out_aaag(X395, X396, X397, T179)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))))
U5_ag(T11, appD_out_aaag(X18, X31, X19, T11)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(void, T11) → U6_ag(T11, appD_in_aaag(T17, T18, T19, T11))
U6_ag(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_ag(T11, T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g([])
U7_ag(T11, T19, in_orderB_out_g(T17)) → in_orderF_out_ag(void, T11)
U7_ag(T11, T19, in_orderB_out_g(T17)) → U8_ag(T11, in_orderB_in_g(T19))
U8_ag(T11, in_orderB_out_g(T19)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(node(T234, T233, T235), T11) → U9_ag(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
appE_in_aaag([], T258, T259, .(T258, T259)) → appE_out_aaag([], T258, T259, .(T258, T259))
appE_in_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283)))
appE_in_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307))))
appE_in_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331)))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379)))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427)))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
appC_in_aaag([], T455, T456, .(T455, T456)) → appC_out_aaag([], T455, T456, .(T455, T456))
appC_in_aaag(.(T464, X806), T466, X807, .(T464, T465)) → U2_aaag(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
U2_aaag(T464, X806, T466, X807, T465, appC_out_aaag(X806, T466, X807, T465)) → appC_out_aaag(.(T464, X806), T466, X807, .(T464, T465))
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_out_aaag(X767, T437, X768, T436)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))))
U9_ag(T234, T233, T235, T11, appE_out_aaag(X18, T233, X19, T11)) → in_orderF_out_ag(node(T234, T233, T235), T11)
in_orderF_in_ag(node(T484, T482, T485), T11) → U10_ag(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_ag(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_ag(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
in_orderF_in_ag(node(T499, T500, T502), T11) → U12_ag(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_ag(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_ag(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U13_ag(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_ag(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U14_ag(T499, T500, T502, T11, in_orderF_out_ag(T502, T241)) → in_orderF_out_ag(node(T499, T500, T502), T11)
U11_ag(T484, T482, T485, T11, in_orderF_out_ag(T484, T240)) → in_orderF_out_ag(node(T484, T482, T485), T11)

The argument filtering Pi contains the following mapping:
in_orderF_in_ag(x1, x2) = in_orderF_in_ag(x2)
[] = []
in_orderF_out_ag(x1, x2) = in_orderF_out_ag
U5_ag(x1, x2) = U5_ag(x2)
appD_in_aaag(x1, x2, x3, x4) = appD_in_aaag(x4)
.(x1, x2) = .(x1, x2)
appD_out_aaag(x1, x2, x3, x4) = appD_out_aaag(x1, x2, x3)
U3_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U3_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x13)
appA_in_aaag(x1, x2, x3, x4) = appA_in_aaag(x4)
appA_out_aaag(x1, x2, x3, x4) = appA_out_aaag(x1, x2, x3)
U1_aaag(x1, x2, x3, x4, x5, x6) = U1_aaag(x1, x6)
U6_ag(x1, x2) = U6_ag(x2)
U7_ag(x1, x2, x3) = U7_ag(x2, x3)
in_orderB_in_g(x1) = in_orderB_in_g(x1)
in_orderB_out_g(x1) = in_orderB_out_g
U8_ag(x1, x2) = U8_ag(x2)
U9_ag(x1, x2, x3, x4, x5) = U9_ag(x5)
appE_in_aaag(x1, x2, x3, x4) = appE_in_aaag(x4)
appE_out_aaag(x1, x2, x3, x4) = appE_out_aaag(x1, x2, x3)
U4_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U4_aaag(x1, x2, x3, x4, x5, x6, x7, x8, x13)
appC_in_aaag(x1, x2, x3, x4) = appC_in_aaag(x4)
appC_out_aaag(x1, x2, x3, x4) = appC_out_aaag(x1, x2, x3)
U2_aaag(x1, x2, x3, x4, x5, x6) = U2_aaag(x1, x6)
U10_ag(x1, x2, x3, x4, x5) = U10_ag(x5)
U11_ag(x1, x2, x3, x4, x5) = U11_ag(x5)
U12_ag(x1, x2, x3, x4, x5) = U12_ag(x5)
U13_ag(x1, x2, x3, x4, x5, x6) = U13_ag(x5, x6)
U14_ag(x1, x2, x3, x4, x5) = U14_ag(x5)
IN_ORDERF_IN_AG(x1, x2) = IN_ORDERF_IN_AG(x2)
U5_AG(x1, x2) = U5_AG(x2)
APPD_IN_AAAG(x1, x2, x3, x4) = APPD_IN_AAAG(x4)
U3_AAAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U3_AAAG(x1, x2, x3, x4, x5, x6, x7, x8, x13)
APPA_IN_AAAG(x1, x2, x3, x4) = APPA_IN_AAAG(x4)
U1_AAAG(x1, x2, x3, x4, x5, x6) = U1_AAAG(x1, x6)
U6_AG(x1, x2) = U6_AG(x2)
U7_AG(x1, x2, x3) = U7_AG(x2, x3)
IN_ORDERB_IN_G(x1) = IN_ORDERB_IN_G(x1)
U8_AG(x1, x2) = U8_AG(x2)
U9_AG(x1, x2, x3, x4, x5) = U9_AG(x5)
APPE_IN_AAAG(x1, x2, x3, x4) = APPE_IN_AAAG(x4)
U4_AAAG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) = U4_AAAG(x1, x2, x3, x4, x5, x6, x7, x8, x13)
APPC_IN_AAAG(x1, x2, x3, x4) = APPC_IN_AAAG(x4)
U2_AAAG(x1, x2, x3, x4, x5, x6) = U2_AAAG(x1, x6)
U10_AG(x1, x2, x3, x4, x5) = U10_AG(x5)
U11_AG(x1, x2, x3, x4, x5) = U11_AG(x5)
U12_AG(x1, x2, x3, x4, x5) = U12_AG(x5)
U13_AG(x1, x2, x3, x4, x5, x6) = U13_AG(x5, x6)
U14_AG(x1, x2, x3, x4, x5) = U14_AG(x5)

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

(6) Obligation:

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

IN_ORDERF_IN_AG(void, T11) → U5_AG(T11, appD_in_aaag(X18, X31, X19, T11))
IN_ORDERF_IN_AG(void, T11) → APPD_IN_AAAG(X18, X31, X19, T11)
APPD_IN_AAAG(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_AAAG(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
APPD_IN_AAAG(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → APPA_IN_AAAG(X395, X396, X397, T179)
APPA_IN_AAAG(.(T203, X446), X447, X448, .(T203, T204)) → U1_AAAG(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
APPA_IN_AAAG(.(T203, X446), X447, X448, .(T203, T204)) → APPA_IN_AAAG(X446, X447, X448, T204)
IN_ORDERF_IN_AG(void, T11) → U6_AG(T11, appD_in_aaag(T17, T18, T19, T11))
U6_AG(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_AG(T11, T19, in_orderB_in_g(T17))
U6_AG(T11, appD_out_aaag(T17, T18, T19, T11)) → IN_ORDERB_IN_G(T17)
U7_AG(T11, T19, in_orderB_out_g(T17)) → U8_AG(T11, in_orderB_in_g(T19))
U7_AG(T11, T19, in_orderB_out_g(T17)) → IN_ORDERB_IN_G(T19)
IN_ORDERF_IN_AG(node(T234, T233, T235), T11) → U9_AG(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
IN_ORDERF_IN_AG(node(T234, T233, T235), T11) → APPE_IN_AAAG(X18, T233, X19, T11)
APPE_IN_AAAG(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_AAAG(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
APPE_IN_AAAG(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → APPC_IN_AAAG(X767, T437, X768, T436)
APPC_IN_AAAG(.(T464, X806), T466, X807, .(T464, T465)) → U2_AAAG(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
APPC_IN_AAAG(.(T464, X806), T466, X807, .(T464, T465)) → APPC_IN_AAAG(X806, T466, X807, T465)
IN_ORDERF_IN_AG(node(T484, T482, T485), T11) → U10_AG(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_AG(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_AG(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
U10_AG(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → IN_ORDERF_IN_AG(T484, T240)
IN_ORDERF_IN_AG(node(T499, T500, T502), T11) → U12_AG(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_AG(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_AG(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U12_AG(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → IN_ORDERF_IN_AG(T499, T240)
U13_AG(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_AG(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U13_AG(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → IN_ORDERF_IN_AG(T502, T241)

The TRS R consists of the following rules:

in_orderF_in_ag(void, []) → in_orderF_out_ag(void, [])
in_orderF_in_ag(void, T11) → U5_ag(T11, appD_in_aaag(X18, X31, X19, T11))
appD_in_aaag([], T32, T33, .(T32, T33)) → appD_out_aaag([], T32, T33, .(T32, T33))
appD_in_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53)))
appD_in_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73))))
appD_in_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93)))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133)))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173)))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
appA_in_aaag([], T197, T198, .(T197, T198)) → appA_out_aaag([], T197, T198, .(T197, T198))
appA_in_aaag(.(T203, X446), X447, X448, .(T203, T204)) → U1_aaag(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
U1_aaag(T203, X446, X447, X448, T204, appA_out_aaag(X446, X447, X448, T204)) → appA_out_aaag(.(T203, X446), X447, X448, .(T203, T204))
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_out_aaag(X395, X396, X397, T179)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))))
U5_ag(T11, appD_out_aaag(X18, X31, X19, T11)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(void, T11) → U6_ag(T11, appD_in_aaag(T17, T18, T19, T11))
U6_ag(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_ag(T11, T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g([])
U7_ag(T11, T19, in_orderB_out_g(T17)) → in_orderF_out_ag(void, T11)
U7_ag(T11, T19, in_orderB_out_g(T17)) → U8_ag(T11, in_orderB_in_g(T19))
U8_ag(T11, in_orderB_out_g(T19)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(node(T234, T233, T235), T11) → U9_ag(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
appE_in_aaag([], T258, T259, .(T258, T259)) → appE_out_aaag([], T258, T259, .(T258, T259))
appE_in_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283)))
appE_in_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307))))
appE_in_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331)))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379)))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427)))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
appC_in_aaag([], T455, T456, .(T455, T456)) → appC_out_aaag([], T455, T456, .(T455, T456))
appC_in_aaag(.(T464, X806), T466, X807, .(T464, T465)) → U2_aaag(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
U2_aaag(T464, X806, T466, X807, T465, appC_out_aaag(X806, T466, X807, T465)) → appC_out_aaag(.(T464, X806), T466, X807, .(T464, T465))
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_out_aaag(X767, T437, X768, T436)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))))
U9_ag(T234, T233, T235, T11, appE_out_aaag(X18, T233, X19, T11)) → in_orderF_out_ag(node(T234, T233, T235), T11)
in_orderF_in_ag(node(T484, T482, T485), T11) → U10_ag(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_ag(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_ag(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
in_orderF_in_ag(node(T499, T500, T502), T11) → U12_ag(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_ag(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_ag(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U13_ag(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_ag(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U14_ag(T499, T500, T502, T11, in_orderF_out_ag(T502, T241)) → in_orderF_out_ag(node(T499, T500, T502), T11)
U11_ag(T484, T482, T485, T11, in_orderF_out_ag(T484, T240)) → in_orderF_out_ag(node(T484, T482, T485), T11)

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

APPC_IN_AAAG(.(T464, X806), T466, X807, .(T464, T465)) → APPC_IN_AAAG(X806, T466, X807, T465)

The TRS R consists of the following rules:

in_orderF_in_ag(void, []) → in_orderF_out_ag(void, [])
in_orderF_in_ag(void, T11) → U5_ag(T11, appD_in_aaag(X18, X31, X19, T11))
appD_in_aaag([], T32, T33, .(T32, T33)) → appD_out_aaag([], T32, T33, .(T32, T33))
appD_in_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53)))
appD_in_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73))))
appD_in_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93)))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133)))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173)))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
appA_in_aaag([], T197, T198, .(T197, T198)) → appA_out_aaag([], T197, T198, .(T197, T198))
appA_in_aaag(.(T203, X446), X447, X448, .(T203, T204)) → U1_aaag(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
U1_aaag(T203, X446, X447, X448, T204, appA_out_aaag(X446, X447, X448, T204)) → appA_out_aaag(.(T203, X446), X447, X448, .(T203, T204))
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_out_aaag(X395, X396, X397, T179)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))))
U5_ag(T11, appD_out_aaag(X18, X31, X19, T11)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(void, T11) → U6_ag(T11, appD_in_aaag(T17, T18, T19, T11))
U6_ag(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_ag(T11, T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g([])
U7_ag(T11, T19, in_orderB_out_g(T17)) → in_orderF_out_ag(void, T11)
U7_ag(T11, T19, in_orderB_out_g(T17)) → U8_ag(T11, in_orderB_in_g(T19))
U8_ag(T11, in_orderB_out_g(T19)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(node(T234, T233, T235), T11) → U9_ag(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
appE_in_aaag([], T258, T259, .(T258, T259)) → appE_out_aaag([], T258, T259, .(T258, T259))
appE_in_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283)))
appE_in_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307))))
appE_in_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331)))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379)))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427)))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
appC_in_aaag([], T455, T456, .(T455, T456)) → appC_out_aaag([], T455, T456, .(T455, T456))
appC_in_aaag(.(T464, X806), T466, X807, .(T464, T465)) → U2_aaag(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
U2_aaag(T464, X806, T466, X807, T465, appC_out_aaag(X806, T466, X807, T465)) → appC_out_aaag(.(T464, X806), T466, X807, .(T464, T465))
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_out_aaag(X767, T437, X768, T436)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))))
U9_ag(T234, T233, T235, T11, appE_out_aaag(X18, T233, X19, T11)) → in_orderF_out_ag(node(T234, T233, T235), T11)
in_orderF_in_ag(node(T484, T482, T485), T11) → U10_ag(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_ag(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_ag(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
in_orderF_in_ag(node(T499, T500, T502), T11) → U12_ag(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_ag(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_ag(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U13_ag(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_ag(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U14_ag(T499, T500, T502, T11, in_orderF_out_ag(T502, T241)) → in_orderF_out_ag(node(T499, T500, T502), T11)
U11_ag(T484, T482, T485, T11, in_orderF_out_ag(T484, T240)) → in_orderF_out_ag(node(T484, T482, T485), T11)

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

APPC_IN_AAAG(.(T464, X806), T466, X807, .(T464, T465)) → APPC_IN_AAAG(X806, T466, X807, T465)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

APPC_IN_AAAG(.(T464, T465)) → APPC_IN_AAAG(T465)

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

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

APPC_IN_AAAG(.(T464, T465)) → APPC_IN_AAAG(T465)
The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

APPA_IN_AAAG(.(T203, X446), X447, X448, .(T203, T204)) → APPA_IN_AAAG(X446, X447, X448, T204)

The TRS R consists of the following rules:

in_orderF_in_ag(void, []) → in_orderF_out_ag(void, [])
in_orderF_in_ag(void, T11) → U5_ag(T11, appD_in_aaag(X18, X31, X19, T11))
appD_in_aaag([], T32, T33, .(T32, T33)) → appD_out_aaag([], T32, T33, .(T32, T33))
appD_in_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53)))
appD_in_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73))))
appD_in_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93)))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133)))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173)))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
appA_in_aaag([], T197, T198, .(T197, T198)) → appA_out_aaag([], T197, T198, .(T197, T198))
appA_in_aaag(.(T203, X446), X447, X448, .(T203, T204)) → U1_aaag(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
U1_aaag(T203, X446, X447, X448, T204, appA_out_aaag(X446, X447, X448, T204)) → appA_out_aaag(.(T203, X446), X447, X448, .(T203, T204))
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_out_aaag(X395, X396, X397, T179)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))))
U5_ag(T11, appD_out_aaag(X18, X31, X19, T11)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(void, T11) → U6_ag(T11, appD_in_aaag(T17, T18, T19, T11))
U6_ag(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_ag(T11, T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g([])
U7_ag(T11, T19, in_orderB_out_g(T17)) → in_orderF_out_ag(void, T11)
U7_ag(T11, T19, in_orderB_out_g(T17)) → U8_ag(T11, in_orderB_in_g(T19))
U8_ag(T11, in_orderB_out_g(T19)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(node(T234, T233, T235), T11) → U9_ag(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
appE_in_aaag([], T258, T259, .(T258, T259)) → appE_out_aaag([], T258, T259, .(T258, T259))
appE_in_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283)))
appE_in_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307))))
appE_in_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331)))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379)))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427)))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
appC_in_aaag([], T455, T456, .(T455, T456)) → appC_out_aaag([], T455, T456, .(T455, T456))
appC_in_aaag(.(T464, X806), T466, X807, .(T464, T465)) → U2_aaag(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
U2_aaag(T464, X806, T466, X807, T465, appC_out_aaag(X806, T466, X807, T465)) → appC_out_aaag(.(T464, X806), T466, X807, .(T464, T465))
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_out_aaag(X767, T437, X768, T436)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))))
U9_ag(T234, T233, T235, T11, appE_out_aaag(X18, T233, X19, T11)) → in_orderF_out_ag(node(T234, T233, T235), T11)
in_orderF_in_ag(node(T484, T482, T485), T11) → U10_ag(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_ag(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_ag(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
in_orderF_in_ag(node(T499, T500, T502), T11) → U12_ag(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_ag(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_ag(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U13_ag(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_ag(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U14_ag(T499, T500, T502, T11, in_orderF_out_ag(T502, T241)) → in_orderF_out_ag(node(T499, T500, T502), T11)
U11_ag(T484, T482, T485, T11, in_orderF_out_ag(T484, T240)) → in_orderF_out_ag(node(T484, T482, T485), T11)

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

APPA_IN_AAAG(.(T203, X446), X447, X448, .(T203, T204)) → APPA_IN_AAAG(X446, X447, X448, T204)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

APPA_IN_AAAG(.(T203, T204)) → APPA_IN_AAAG(T204)

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

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

APPA_IN_AAAG(.(T203, T204)) → APPA_IN_AAAG(T204)
The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

IN_ORDERF_IN_AG(node(T484, T482, T485), T11) → U10_AG(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_AG(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → IN_ORDERF_IN_AG(T484, T240)
IN_ORDERF_IN_AG(node(T499, T500, T502), T11) → U12_AG(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_AG(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_AG(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U13_AG(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → IN_ORDERF_IN_AG(T502, T241)
U12_AG(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → IN_ORDERF_IN_AG(T499, T240)

The TRS R consists of the following rules:

in_orderF_in_ag(void, []) → in_orderF_out_ag(void, [])
in_orderF_in_ag(void, T11) → U5_ag(T11, appD_in_aaag(X18, X31, X19, T11))
appD_in_aaag([], T32, T33, .(T32, T33)) → appD_out_aaag([], T32, T33, .(T32, T33))
appD_in_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53, .(T38, .(T52, T53)))
appD_in_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73, .(T38, .(T58, .(T72, T73))))
appD_in_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93, .(T38, .(T58, .(T78, .(T92, T93)))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113, .(T38, .(T58, .(T78, .(T98, .(T112, T113))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133, .(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133)))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173)))))))))
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_in_aaag(X395, X396, X397, T179))
appA_in_aaag([], T197, T198, .(T197, T198)) → appA_out_aaag([], T197, T198, .(T197, T198))
appA_in_aaag(.(T203, X446), X447, X448, .(T203, T204)) → U1_aaag(T203, X446, X447, X448, T204, appA_in_aaag(X446, X447, X448, T204))
U1_aaag(T203, X446, X447, X448, T204, appA_out_aaag(X446, X447, X448, T204)) → appA_out_aaag(.(T203, X446), X447, X448, .(T203, T204))
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, X395, X396, X397, T179, appA_out_aaag(X395, X396, X397, T179)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397, .(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179)))))))))
U5_ag(T11, appD_out_aaag(X18, X31, X19, T11)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(void, T11) → U6_ag(T11, appD_in_aaag(T17, T18, T19, T11))
U6_ag(T11, appD_out_aaag(T17, T18, T19, T11)) → U7_ag(T11, T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g([])
U7_ag(T11, T19, in_orderB_out_g(T17)) → in_orderF_out_ag(void, T11)
U7_ag(T11, T19, in_orderB_out_g(T17)) → U8_ag(T11, in_orderB_in_g(T19))
U8_ag(T11, in_orderB_out_g(T19)) → in_orderF_out_ag(void, T11)
in_orderF_in_ag(node(T234, T233, T235), T11) → U9_ag(T234, T233, T235, T11, appE_in_aaag(X18, T233, X19, T11))
appE_in_aaag([], T258, T259, .(T258, T259)) → appE_out_aaag([], T258, T259, .(T258, T259))
appE_in_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283, .(T267, .(T282, T283)))
appE_in_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307, .(T267, .(T291, .(T306, T307))))
appE_in_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331, .(T267, .(T291, .(T315, .(T330, T331)))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355, .(T267, .(T291, .(T315, .(T339, .(T354, T355))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379, .(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379)))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427)))))))))
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_in_aaag(X767, T437, X768, T436))
appC_in_aaag([], T455, T456, .(T455, T456)) → appC_out_aaag([], T455, T456, .(T455, T456))
appC_in_aaag(.(T464, X806), T466, X807, .(T464, T465)) → U2_aaag(T464, X806, T466, X807, T465, appC_in_aaag(X806, T466, X807, T465))
U2_aaag(T464, X806, T466, X807, T465, appC_out_aaag(X806, T466, X807, T465)) → appC_out_aaag(.(T464, X806), T466, X807, .(T464, T465))
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, X767, T437, X768, T436, appC_out_aaag(X767, T437, X768, T436)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768, .(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436)))))))))
U9_ag(T234, T233, T235, T11, appE_out_aaag(X18, T233, X19, T11)) → in_orderF_out_ag(node(T234, T233, T235), T11)
in_orderF_in_ag(node(T484, T482, T485), T11) → U10_ag(T484, T482, T485, T11, appE_in_aaag(T240, T482, T241, T11))
U10_ag(T484, T482, T485, T11, appE_out_aaag(T240, T482, T241, T11)) → U11_ag(T484, T482, T485, T11, in_orderF_in_ag(T484, T240))
in_orderF_in_ag(node(T499, T500, T502), T11) → U12_ag(T499, T500, T502, T11, appE_in_aaag(T240, T500, T241, T11))
U12_ag(T499, T500, T502, T11, appE_out_aaag(T240, T500, T241, T11)) → U13_ag(T499, T500, T502, T11, T241, in_orderF_in_ag(T499, T240))
U13_ag(T499, T500, T502, T11, T241, in_orderF_out_ag(T499, T240)) → U14_ag(T499, T500, T502, T11, in_orderF_in_ag(T502, T241))
U14_ag(T499, T500, T502, T11, in_orderF_out_ag(T502, T241)) → in_orderF_out_ag(node(T499, T500, T502), T11)
U11_ag(T484, T482, T485, T11, in_orderF_out_ag(T484, T240)) → in_orderF_out_ag(node(T484, T482, T485), T11)

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

IN_ORDERF_IN_AG(T11) → U10_AG(appE_in_aaag(T11))
U10_AG(appE_out_aaag(T240, T482, T241)) → IN_ORDERF_IN_AG(T240)
IN_ORDERF_IN_AG(T11) → U12_AG(appE_in_aaag(T11))
U12_AG(appE_out_aaag(T240, T500, T241)) → U13_AG(T241, in_orderF_in_ag(T240))
U13_AG(T241, in_orderF_out_ag) → IN_ORDERF_IN_AG(T241)
U12_AG(appE_out_aaag(T240, T500, T241)) → IN_ORDERF_IN_AG(T240)

The TRS R consists of the following rules:

in_orderF_in_ag([]) → in_orderF_out_ag
in_orderF_in_ag(T11) → U5_ag(appD_in_aaag(T11))
appD_in_aaag(.(T32, T33)) → appD_out_aaag([], T32, T33)
appD_in_aaag(.(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53)
appD_in_aaag(.(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73)
appD_in_aaag(.(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, appA_in_aaag(T179))
appA_in_aaag(.(T197, T198)) → appA_out_aaag([], T197, T198)
appA_in_aaag(.(T203, T204)) → U1_aaag(T203, appA_in_aaag(T204))
U1_aaag(T203, appA_out_aaag(X446, X447, X448)) → appA_out_aaag(.(T203, X446), X447, X448)
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, appA_out_aaag(X395, X396, X397)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397)
U5_ag(appD_out_aaag(X18, X31, X19)) → in_orderF_out_ag
in_orderF_in_ag(T11) → U6_ag(appD_in_aaag(T11))
U6_ag(appD_out_aaag(T17, T18, T19)) → U7_ag(T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g
U7_ag(T19, in_orderB_out_g) → in_orderF_out_ag
U7_ag(T19, in_orderB_out_g) → U8_ag(in_orderB_in_g(T19))
U8_ag(in_orderB_out_g) → in_orderF_out_ag
in_orderF_in_ag(T11) → U9_ag(appE_in_aaag(T11))
appE_in_aaag(.(T258, T259)) → appE_out_aaag([], T258, T259)
appE_in_aaag(.(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283)
appE_in_aaag(.(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307)
appE_in_aaag(.(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, appC_in_aaag(T436))
appC_in_aaag(.(T455, T456)) → appC_out_aaag([], T455, T456)
appC_in_aaag(.(T464, T465)) → U2_aaag(T464, appC_in_aaag(T465))
U2_aaag(T464, appC_out_aaag(X806, T466, X807)) → appC_out_aaag(.(T464, X806), T466, X807)
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, appC_out_aaag(X767, T437, X768)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768)
U9_ag(appE_out_aaag(X18, T233, X19)) → in_orderF_out_ag
in_orderF_in_ag(T11) → U10_ag(appE_in_aaag(T11))
U10_ag(appE_out_aaag(T240, T482, T241)) → U11_ag(in_orderF_in_ag(T240))
in_orderF_in_ag(T11) → U12_ag(appE_in_aaag(T11))
U12_ag(appE_out_aaag(T240, T500, T241)) → U13_ag(T241, in_orderF_in_ag(T240))
U13_ag(T241, in_orderF_out_ag) → U14_ag(in_orderF_in_ag(T241))
U14_ag(in_orderF_out_ag) → in_orderF_out_ag
U11_ag(in_orderF_out_ag) → in_orderF_out_ag

The set Q consists of the following terms:

in_orderF_in_ag(x0)
appD_in_aaag(x0)
appA_in_aaag(x0)
U1_aaag(x0, x1)
U3_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8)
U5_ag(x0)
U6_ag(x0)
in_orderB_in_g(x0)
U7_ag(x0, x1)
U8_ag(x0)
appE_in_aaag(x0)
appC_in_aaag(x0)
U2_aaag(x0, x1)
U4_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8)
U9_ag(x0)
U10_ag(x0)
U12_ag(x0)
U13_ag(x0, x1)
U14_ag(x0)
U11_ag(x0)

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

(26) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

IN_ORDERF_IN_AG(T11) → U10_AG(appE_in_aaag(T11))
U10_AG(appE_out_aaag(T240, T482, T241)) → IN_ORDERF_IN_AG(T240)
IN_ORDERF_IN_AG(T11) → U12_AG(appE_in_aaag(T11))
U12_AG(appE_out_aaag(T240, T500, T241)) → U13_AG(T241, in_orderF_in_ag(T240))
U13_AG(T241, in_orderF_out_ag) → IN_ORDERF_IN_AG(T241)
U12_AG(appE_out_aaag(T240, T500, T241)) → IN_ORDERF_IN_AG(T240)

Strictly oriented rules of the TRS R:

in_orderF_in_ag([]) → in_orderF_out_ag
in_orderF_in_ag(T11) → U5_ag(appD_in_aaag(T11))
appD_in_aaag(.(T32, T33)) → appD_out_aaag([], T32, T33)
appD_in_aaag(.(T38, .(T52, T53))) → appD_out_aaag(.(T38, []), T52, T53)
appD_in_aaag(.(T38, .(T58, .(T72, T73)))) → appD_out_aaag(.(T38, .(T58, [])), T72, T73)
appD_in_aaag(.(T38, .(T58, .(T78, .(T92, T93))))) → appD_out_aaag(.(T38, .(T58, .(T78, []))), T92, T93)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T112, T113)))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, [])))), T112, T113)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T132, T133))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, []))))), T132, T133)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T152, T153)))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, [])))))), T152, T153)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T172, T173))))))))) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, []))))))), T172, T173)
appD_in_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, T179))))))))) → U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, appA_in_aaag(T179))
appA_in_aaag(.(T197, T198)) → appA_out_aaag([], T197, T198)
appA_in_aaag(.(T203, T204)) → U1_aaag(T203, appA_in_aaag(T204))
U1_aaag(T203, appA_out_aaag(X446, X447, X448)) → appA_out_aaag(.(T203, X446), X447, X448)
U3_aaag(T38, T58, T78, T98, T118, T138, T158, T178, appA_out_aaag(X395, X396, X397)) → appD_out_aaag(.(T38, .(T58, .(T78, .(T98, .(T118, .(T138, .(T158, .(T178, X395)))))))), X396, X397)
U5_ag(appD_out_aaag(X18, X31, X19)) → in_orderF_out_ag
in_orderF_in_ag(T11) → U6_ag(appD_in_aaag(T11))
U6_ag(appD_out_aaag(T17, T18, T19)) → U7_ag(T19, in_orderB_in_g(T17))
in_orderB_in_g([]) → in_orderB_out_g
U7_ag(T19, in_orderB_out_g) → in_orderF_out_ag
U7_ag(T19, in_orderB_out_g) → U8_ag(in_orderB_in_g(T19))
U8_ag(in_orderB_out_g) → in_orderF_out_ag
in_orderF_in_ag(T11) → U9_ag(appE_in_aaag(T11))
appE_in_aaag(.(T258, T259)) → appE_out_aaag([], T258, T259)
appE_in_aaag(.(T267, .(T282, T283))) → appE_out_aaag(.(T267, []), T282, T283)
appE_in_aaag(.(T267, .(T291, .(T306, T307)))) → appE_out_aaag(.(T267, .(T291, [])), T306, T307)
appE_in_aaag(.(T267, .(T291, .(T315, .(T330, T331))))) → appE_out_aaag(.(T267, .(T291, .(T315, []))), T330, T331)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T354, T355)))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, [])))), T354, T355)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T378, T379))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, []))))), T378, T379)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T402, T403)))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, [])))))), T402, T403)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T426, T427))))))))) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, []))))))), T426, T427)
appE_in_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, T436))))))))) → U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, appC_in_aaag(T436))
appC_in_aaag(.(T455, T456)) → appC_out_aaag([], T455, T456)
appC_in_aaag(.(T464, T465)) → U2_aaag(T464, appC_in_aaag(T465))
U2_aaag(T464, appC_out_aaag(X806, T466, X807)) → appC_out_aaag(.(T464, X806), T466, X807)
U4_aaag(T267, T291, T315, T339, T363, T387, T411, T435, appC_out_aaag(X767, T437, X768)) → appE_out_aaag(.(T267, .(T291, .(T315, .(T339, .(T363, .(T387, .(T411, .(T435, X767)))))))), T437, X768)
U9_ag(appE_out_aaag(X18, T233, X19)) → in_orderF_out_ag
in_orderF_in_ag(T11) → U10_ag(appE_in_aaag(T11))
U10_ag(appE_out_aaag(T240, T482, T241)) → U11_ag(in_orderF_in_ag(T240))
in_orderF_in_ag(T11) → U12_ag(appE_in_aaag(T11))
U12_ag(appE_out_aaag(T240, T500, T241)) → U13_ag(T241, in_orderF_in_ag(T240))
U13_ag(T241, in_orderF_out_ag) → U14_ag(in_orderF_in_ag(T241))
U14_ag(in_orderF_out_ag) → in_orderF_out_ag
U11_ag(in_orderF_out_ag) → in_orderF_out_ag

Used ordering: Knuth-Bendix order [KBO] with precedence:

appA_{in_aaag₁} > U7_ag₂ > U13_AG₂ > U12_AG₁ > U10_AG₁ > IN_{ORDERF_{IN_AG₁}} > U14_ag₁ > appC_{in_aaag₁} > U2_aaag₂ > appD_{out_aaag₃} > appD_{in_aaag₁} > in_{orderF_{in_ag₁}} > U12_ag₁ > in_{orderB_{in_g₁}} > U3_aaag₉ > U4_aaag₉ > .₂ > U13_ag₂ > U10_ag₁ > U11_ag₁ > appC_{out_aaag₃} > appE_{out_aaag₃} > appE_{in_aaag₁} > U8_ag₁ > U1_aaag₂ > appA_{out_aaag₃} > U5_ag₁ > [] > in_{orderF_{out_ag}} > in_{orderB_{out_g}} > U9_ag₁ > U6_ag₁

and weight map:

[]=3
in_orderF_out_ag=9
in_orderB_out_g=3
in_orderF_in_ag_1=6
U5_ag_1=3
appD_in_aaag_1=1
appA_in_aaag_1=1
U6_ag_1=4
in_orderB_in_g_1=1
U8_ag_1=7
U9_ag_1=4
appE_in_aaag_1=1
appC_in_aaag_1=1
U10_ag_1=5
U11_ag_1=4
U12_ag_1=5
U14_ag_1=5
IN_ORDERF_IN_AG_1=8
U10_AG_1=4
U12_AG_1=3
._2=8
appD_out_aaag_3=3
U3_aaag_9=63
appA_out_aaag_3=5
U1_aaag_2=8
U7_ag_2=6
appE_out_aaag_3=3
U4_aaag_9=61
appC_out_aaag_3=6
U2_aaag_2=8
U13_ag_2=3
U13_AG_2=0

The variable weight is 1

(27) Obligation:

Q DP problem:
P is empty.
R is empty.
The set Q consists of the following terms:

in_orderF_in_ag(x0)
appD_in_aaag(x0)
appA_in_aaag(x0)
U1_aaag(x0, x1)
U3_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8)
U5_ag(x0)
U6_ag(x0)
in_orderB_in_g(x0)
U7_ag(x0, x1)
U8_ag(x0)
appE_in_aaag(x0)
appC_in_aaag(x0)
U2_aaag(x0, x1)
U4_aaag(x0, x1, x2, x3, x4, x5, x6, x7, x8)
U9_ag(x0)
U10_ag(x0)
U12_ag(x0)
U13_ag(x0, x1)
U14_ag(x0)
U11_ag(x0)

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

(28) PisEmptyProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) YES

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) MRRProof (EQUIVALENT transformation)

(27) Obligation:

(28) PisEmptyProof (EQUIVALENT transformation)

(29) YES