Left Termination proof of /tmp/tmpoaqiKR/parse.pl

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇐)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇐)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇐)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇐)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔)

        ↳34 YES

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇐)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔)

        ↳41 YES

    ↳42 PiDP

        ↳43 UsableRulesProof (⇔)

        ↳44 PiDP

        ↳45 PiDPToQDPProof (⇐)

        ↳46 QDP

        ↳47 QDPSizeChangeProof (⇔)

        ↳48 YES

    ↳49 PiDP

        ↳50 UsableRulesProof (⇔)

        ↳51 PiDP

        ↳52 PiDPToQDPProof (⇐)

        ↳53 QDP

        ↳54 QDPOrderProof (⇔)

        ↳55 QDP

        ↳56 DependencyGraphProof (⇔)

        ↳57 QDP

        ↳58 UsableRulesProof (⇔)

        ↳59 QDP

        ↳60 QReductionProof (⇔)

        ↳61 QDP

        ↳62 QDPOrderProof (⇔)

        ↳63 QDP

        ↳64 DependencyGraphProof (⇔)

        ↳65 TRUE

(0) Obligation:

Clauses:

parse(Xs, T) :- ','(app(As, cons(a, cons(s(A, B, C), cons(b, Bs))), Xs), ','(app(As, cons(s(a, s(A, B, C), b), Bs), Ys), parse(Ys, T))).
parse(Xs, T) :- ','(app(As, cons(a, cons(s(A, B), cons(b, Bs))), Xs), ','(app(As, cons(s(a, s(A, B), b), Bs), Ys), parse(Ys, T))).
parse(Xs, T) :- ','(app(As, cons(a, cons(b, Bs)), Xs), ','(app(As, cons(s(a, b), Bs), Ys), parse(Ys, T))).
parse(cons(s(A, B), nil), s(A, B)).
parse(cons(s(A, B, C), nil), s(A, B, C)).
app(nil, X, X).
app(cons(X, Xs), Ys, cons(X, Zs)) :- app(Xs, Ys, Zs).

Queries:

parse(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: parse(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: parse(T1, T2), SCOPE: 1, CLAUSE: 0 | parse(T1, T2), SCOPE: 1, CLAUSE: 1 | parse(T1, T2), SCOPE: 1, CLAUSE: 2 | parse(T1, T2), SCOPE: 1, CLAUSE: 3 | parse(T1, T2), SCOPE: 1, CLAUSE: 4\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(app(X5, cons(a, cons(s(X6, X7, X8), cons(b, X9))), T5), ','(app(X5, cons(s(a, s(X6, X7, X8), b), X9), X10), parse(X10, T7))) | parse(T5, T2), SCOPE: 1, CLAUSE: 1 | parse(T5, T2), SCOPE: 1, CLAUSE: 2 | parse(T5, T2), SCOPE: 1, CLAUSE: 3 | parse(T5, T2), SCOPE: 1, CLAUSE: 4\n\nT5 is ground\nX5 is free; \nX6 is free; \nX7 is free; \nX8 is free; \nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(app(X5, cons(a, cons(s(X6, X7, X8), cons(b, X9))), T5), ','(app(X5, cons(s(a, s(X6, X7, X8), b), X9), X10), parse(X10, T7))), SCOPE: 2, CLAUSE: 5 | ','(app(X5, cons(a, cons(s(X6, X7, X8), cons(b, X9))), T5), ','(app(X5, cons(s(a, s(X6, X7, X8), b), X9), X10), parse(X10, T7))), SCOPE: 2, CLAUSE: 6 | ?_2 | parse(T5, T2), SCOPE: 1, CLAUSE: 1 | parse(T5, T2), SCOPE: 1, CLAUSE: 2 | parse(T5, T2), SCOPE: 1, CLAUSE: 3 | parse(T5, T2), SCOPE: 1, CLAUSE: 4\n\nT5 is ground\nX5 is free; \nX6 is free; \nX7 is free; \nX8 is free; \nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(app(X5, cons(a, cons(s(X6, X7, X8), cons(b, X9))), T5), ','(app(X5, cons(s(a, s(X6, X7, X8), b), X9), X10), parse(X10, T7))), SCOPE: 2, CLAUSE: 5\n\nT5 is ground\nX5 is free; \nX6 is free; \nX7 is free; \nX8 is free; \nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(app(X5, cons(a, cons(s(X6, X7, X8), cons(b, X9))), T5), ','(app(X5, cons(s(a, s(X6, X7, X8), b), X9), X10), parse(X10, T7))), SCOPE: 2, CLAUSE: 6 | ?_2 | parse(T5, T2), SCOPE: 1, CLAUSE: 1 | parse(T5, T2), SCOPE: 1, CLAUSE: 2 | parse(T5, T2), SCOPE: 1, CLAUSE: 3 | parse(T5, T2), SCOPE: 1, CLAUSE: 4\n\nT5 is ground\nX5 is free; \nX6 is free; \nX7 is free; \nX8 is free; \nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(app(nil, cons(s(a, s(X32, X33, X34), b), X35), X10), parse(X10, T7))\n\nX10 is free\nX32 is free; \nX33 is free; \nX34 is free; \nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: app(nil, cons(s(a, s(X32, X33, X34), b), X35), X10)\n\nX10 is free\nX32 is free; \nX33 is free; \nX34 is free; \nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: parse(T13, T7)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: app(nil, cons(s(a, s(X32, X33, X34), b), X35), X10), SCOPE: 3, CLAUSE: 5 | app(nil, cons(s(a, s(X32, X33, X34), b), X35), X10), SCOPE: 3, CLAUSE: 6\n\nX10 is free\nX32 is free; \nX33 is free; \nX34 is free; \nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: app(nil, cons(s(a, s(X32, X33, X34), b), X35), X10), SCOPE: 3, CLAUSE: 5\n\nX10 is free\nX32 is free; \nX33 is free; \nX34 is free; \nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: app(nil, cons(s(a, s(X32, X33, X34), b), X35), X10), SCOPE: 3, CLAUSE: 6\n\nX10 is free\nX32 is free; \nX33 is free; \nX34 is free; \nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: parse(T13, T7), SCOPE: 4, CLAUSE: 0 | parse(T13, T7), SCOPE: 4, CLAUSE: 1 | parse(T13, T7), SCOPE: 4, CLAUSE: 2 | parse(T13, T7), SCOPE: 4, CLAUSE: 3 | parse(T13, T7), SCOPE: 4, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: parse(T13, T7), SCOPE: 4, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: parse(T13, T7), SCOPE: 4, CLAUSE: 1 | parse(T13, T7), SCOPE: 4, CLAUSE: 2 | parse(T13, T7), SCOPE: 4, CLAUSE: 3 | parse(T13, T7), SCOPE: 4, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(app(X135, cons(a, cons(s(X136, X137, X138), cons(b, X139))), T30), ','(app(X135, cons(s(a, s(X136, X137, X138), b), X139), X140), parse(X140, T31)))\n\nX135 is free\nX136 is free; \nX137 is free; \nX138 is free; \nX139 is free; \nX140 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: app(X135, cons(a, cons(s(X136, X137, X138), cons(b, X139))), T30)\n\nX135 is free\nX136 is free; \nX137 is free; \nX138 is free; \nX139 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(app(T32, cons(s(a, s(T33, T34, T35), b), T36), X140), parse(X140, T37))\n\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: app(X135, cons(a, cons(s(X136, X137, X138), cons(b, X139))), T30), SCOPE: 5, CLAUSE: 5 | app(X135, cons(a, cons(s(X136, X137, X138), cons(b, X139))), T30), SCOPE: 5, CLAUSE: 6\n\nX135 is free\nX136 is free; \nX137 is free; \nX138 is free; \nX139 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: app(X135, cons(a, cons(s(X136, X137, X138), cons(b, X139))), T30), SCOPE: 5, CLAUSE: 5\n\nX135 is free\nX136 is free; \nX137 is free; \nX138 is free; \nX139 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: app(X135, cons(a, cons(s(X136, X137, X138), cons(b, X139))), T30), SCOPE: 5, CLAUSE: 6\n\nX135 is free\nX136 is free; \nX137 is free; \nX138 is free; \nX139 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: app(X212, cons(a, cons(s(X213, X214, X215), cons(b, X216))), T41)\n\nX212 is free\nX213 is free; \nX214 is free; \nX215 is free; \nX216 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: app(T32, cons(s(a, s(T33, T34, T35), b), T36), X140)\n\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: parse(T50, T51)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: app(T32, cons(s(a, s(T33, T34, T35), b), T36), X140), SCOPE: 6, CLAUSE: 5 | app(T32, cons(s(a, s(T33, T34, T35), b), T36), X140), SCOPE: 6, CLAUSE: 6\n\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: app(T32, cons(s(a, s(T33, T34, T35), b), T36), X140), SCOPE: 6, CLAUSE: 5\n\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: app(T32, cons(s(a, s(T33, T34, T35), b), T36), X140), SCOPE: 6, CLAUSE: 6\n\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: app(T98, cons(s(a, s(T100, T101, T102), b), T99), X255)\n\nX255 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: parse(T13, T7), SCOPE: 4, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: parse(T13, T7), SCOPE: 4, CLAUSE: 2 | parse(T13, T7), SCOPE: 4, CLAUSE: 3 | parse(T13, T7), SCOPE: 4, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(app(X306, cons(a, cons(s(X307, X308), cons(b, X309))), T127), ','(app(X306, cons(s(a, s(X307, X308), b), X309), X310), parse(X310, T128)))\n\nX306 is free\nX307 is free; \nX308 is free; \nX309 is free; \nX310 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: app(X306, cons(a, cons(s(X307, X308), cons(b, X309))), T127)\n\nX306 is free\nX307 is free; \nX308 is free; \nX309 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(app(T129, cons(s(a, s(T130, T131), b), T132), X310), parse(X310, T133))\n\nX310 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: app(X306, cons(a, cons(s(X307, X308), cons(b, X309))), T127), SCOPE: 7, CLAUSE: 5 | app(X306, cons(a, cons(s(X307, X308), cons(b, X309))), T127), SCOPE: 7, CLAUSE: 6\n\nX306 is free\nX307 is free; \nX308 is free; \nX309 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: app(X306, cons(a, cons(s(X307, X308), cons(b, X309))), T127), SCOPE: 7, CLAUSE: 5\n\nX306 is free\nX307 is free; \nX308 is free; \nX309 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: app(X306, cons(a, cons(s(X307, X308), cons(b, X309))), T127), SCOPE: 7, CLAUSE: 6\n\nX306 is free\nX307 is free; \nX308 is free; \nX309 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: app(X371, cons(a, cons(s(X372, X373), cons(b, X374))), T137)\n\nX371 is free\nX372 is free; \nX373 is free; \nX374 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: app(T129, cons(s(a, s(T130, T131), b), T132), X310)\n\nX310 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: parse(T144, T145)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: app(T129, cons(s(a, s(T130, T131), b), T132), X310), SCOPE: 8, CLAUSE: 5 | app(T129, cons(s(a, s(T130, T131), b), T132), X310), SCOPE: 8, CLAUSE: 6\n\nX310 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: app(T129, cons(s(a, s(T130, T131), b), T132), X310), SCOPE: 8, CLAUSE: 5\n\nX310 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: app(T129, cons(s(a, s(T130, T131), b), T132), X310), SCOPE: 8, CLAUSE: 6\n\nX310 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: app(T182, cons(s(a, s(T184, T185), b), T183), X411)\n\nX411 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: parse(T13, T7), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: parse(T13, T7), SCOPE: 4, CLAUSE: 3 | parse(T13, T7), SCOPE: 4, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(app(X450, cons(a, cons(b, X451)), T208), ','(app(X450, cons(s(a, b), X451), X452), parse(X452, T209)))\n\nX450 is free\nX451 is free; \nX452 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: app(X450, cons(a, cons(b, X451)), T208)\n\nX450 is free\nX451 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(app(T210, cons(s(a, b), T211), X452), parse(X452, T212))\n\nX452 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: app(X450, cons(a, cons(b, X451)), T208), SCOPE: 9, CLAUSE: 5 | app(X450, cons(a, cons(b, X451)), T208), SCOPE: 9, CLAUSE: 6\n\nX450 is free\nX451 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: app(X450, cons(a, cons(b, X451)), T208), SCOPE: 9, CLAUSE: 5\n\nX450 is free\nX451 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: app(X450, cons(a, cons(b, X451)), T208), SCOPE: 9, CLAUSE: 6\n\nX450 is free\nX451 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: app(X491, cons(a, cons(b, X492)), T216)\n\nX491 is free\nX492 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: app(T210, cons(s(a, b), T211), X452)\n\nX452 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: parse(T219, T220)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: app(T210, cons(s(a, b), T211), X452), SCOPE: 10, CLAUSE: 5 | app(T210, cons(s(a, b), T211), X452), SCOPE: 10, CLAUSE: 6\n\nX452 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: app(T210, cons(s(a, b), T211), X452), SCOPE: 10, CLAUSE: 5\n\nX452 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: app(T210, cons(s(a, b), T211), X452), SCOPE: 10, CLAUSE: 6\n\nX452 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: app(T237, cons(s(a, b), T238), X525)\n\nX525 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: parse(T13, T7), SCOPE: 4, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: parse(T13, T7), SCOPE: 4, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(app(X5, cons(a, cons(s(X6, X7, X8), cons(b, X9))), T5), ','(app(X5, cons(s(a, s(X6, X7, X8), b), X9), X10), parse(X10, T7))), SCOPE: 2, CLAUSE: 6\n\nT5 is ground\nX5 is free; \nX6 is free; \nX7 is free; \nX8 is free; \nX9 is free; \nX10 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ?_2 | parse(T5, T2), SCOPE: 1, CLAUSE: 1 | parse(T5, T2), SCOPE: 1, CLAUSE: 2 | parse(T5, T2), SCOPE: 1, CLAUSE: 3 | parse(T5, T2), SCOPE: 1, CLAUSE: 4\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(app(X609, cons(a, cons(s(X610, X611, X612), cons(b, X613))), T266), ','(app(cons(X608, X609), cons(s(a, s(X610, X611, X612), b), X613), X10), parse(X10, T7)))\n\nT266 is ground\nX10 is free; \nX608 is free; \nX609 is free; \nX610 is free; \nX611 is free; \nX612 is free; \nX613 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: app(X609, cons(a, cons(s(X610, X611, X612), cons(b, X613))), T266)\n\nT266 is ground\nX609 is free; \nX610 is free; \nX611 is free; \nX612 is free; \nX613 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(app(cons(X608, T267), cons(s(a, s(T268, T269, T270), b), T271), X10), parse(X10, T7))\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT271 is ground\nX10 is free; \nX608 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: parse(T5, T2), SCOPE: 1, CLAUSE: 1 | parse(T5, T2), SCOPE: 1, CLAUSE: 2 | parse(T5, T2), SCOPE: 1, CLAUSE: 3 | parse(T5, T2), SCOPE: 1, CLAUSE: 4\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: parse(T5, T2), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: parse(T5, T2), SCOPE: 1, CLAUSE: 2 | parse(T5, T2), SCOPE: 1, CLAUSE: 3 | parse(T5, T2), SCOPE: 1, CLAUSE: 4\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(app(X682, cons(a, cons(s(X683, X684), cons(b, X685))), T287), ','(app(X682, cons(s(a, s(X683, X684), b), X685), X686), parse(X686, T289)))\n\nT287 is ground\nX682 is free; \nX683 is free; \nX684 is free; \nX685 is free; \nX686 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: parse(T5, T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: parse(T5, T2), SCOPE: 1, CLAUSE: 3 | parse(T5, T2), SCOPE: 1, CLAUSE: 4\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(app(X719, cons(a, cons(b, X720)), T300), ','(app(X719, cons(s(a, b), X720), X721), parse(X721, T302)))\n\nT300 is ground\nX719 is free; \nX720 is free; \nX721 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: parse(T5, T2), SCOPE: 1, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: parse(T5, T2), SCOPE: 1, CLAUSE: 4\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 116 [arrowhead = none ];
116 -> 2;

117 [label="ONLY EVAL with clause\nparse(X3, X4) :- ','(app(X5, cons(a, cons(s(X6, X7, X8), cons(b, X9))), X3), ','(app(X5, cons(s(a, s(X6, X7, X8), b), X9), X10), parse(X10, X4))).\nand substitution\nT1 -> T5\nX3 -> T5\nT2 -> T7\nX4 -> T7\nT6 -> T7", fontsize=14, style = filled, fillcolor = white];
2 -> 117 [arrowhead = none ];
117 -> 3;

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

119 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 119 [arrowhead = none ];
119 -> 5;

120 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 120 [arrowhead = none ];
120 -> 6;

121 [label="EVAL with clause\napp(nil, X31, X31).\nand substitution\nX5 -> nil\nX6 -> X32\nX7 -> X33\nX8 -> X34\nX9 -> X35\nX31 -> cons(a, cons(s(X32, X33, X34), cons(b, X35)))\nT5 -> cons(a, cons(s(X32, X33, X34), cons(b, X35)))", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 121 [arrowhead = none ];
121 -> 7;

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

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

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

125 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
7 -> 125 [arrowhead = none ];
125 -> 9;

126 [label="SPLIT 2\nreplacements:\nX32 -> T9\nX33 -> T10\nX34 -> T11\nX35 -> T12\nX10 -> T13", fontsize=14, style = filled, fillcolor = violet];
7 -> 126 [arrowhead = none ];
126 -> 10;

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

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

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

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

131 [label="ONLY EVAL with clause\napp(nil, X76, X76).\nand substitution\nX32 -> X77\nX33 -> X78\nX34 -> X79\nX35 -> X80\nX76 -> cons(s(a, s(X77, X78, X79), b), X80)\nX10 -> cons(s(a, s(X77, X78, X79), b), X80)", fontsize=14, style = filled, fillcolor = white];
12 -> 131 [arrowhead = none ];
131 -> 14;

132 [label="BACKTRACK\nfor clause: app(cons(X, Xs), Ys, cons(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = white];
13 -> 132 [arrowhead = none ];
132 -> 16;

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

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

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

136 [label="ONLY EVAL with clause\nparse(X133, X134) :- ','(app(X135, cons(a, cons(s(X136, X137, X138), cons(b, X139))), X133), ','(app(X135, cons(s(a, s(X136, X137, X138), b), X139), X140), parse(X140, X134))).\nand substitution\nT13 -> T30\nX133 -> T30\nT7 -> T31\nX134 -> T31\nT28 -> T30\nT29 -> T31", fontsize=14, style = filled, fillcolor = white];
18 -> 136 [arrowhead = none ];
136 -> 20;

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

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

139 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 139 [arrowhead = none ];
139 -> 21;

140 [label="SPLIT 2\nreplacements:\nX135 -> T32\nX136 -> T33\nX137 -> T34\nX138 -> T35\nX139 -> T36\nT31 -> T37", fontsize=14, style = filled, fillcolor = violet];
20 -> 140 [arrowhead = none ];
140 -> 22;

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

142 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
22 -> 142 [arrowhead = none ];
142 -> 31;

143 [label="SPLIT 2\nreplacements:\nX140 -> T50\nT37 -> T51", fontsize=14, style = filled, fillcolor = violet];
22 -> 143 [arrowhead = none ];
143 -> 32;

144 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
23 -> 144 [arrowhead = none ];
144 -> 24;

145 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
23 -> 145 [arrowhead = none ];
145 -> 25;

146 [label="EVAL with clause\napp(nil, X181, X181).\nand substitution\nX135 -> nil\nX136 -> X182\nX137 -> X183\nX138 -> X184\nX139 -> X185\nX181 -> cons(a, cons(s(X182, X183, X184), cons(b, X185)))\nT30 -> cons(a, cons(s(X182, X183, X184), cons(b, X185)))", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 146 [arrowhead = none ];
146 -> 26;

147 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 147 [arrowhead = none ];
147 -> 27;

148 [label="EVAL with clause\napp(cons(X207, X208), X209, cons(X207, X210)) :- app(X208, X209, X210).\nand substitution\nX207 -> X211\nX208 -> X212\nX135 -> cons(X211, X212)\nX136 -> X213\nX137 -> X214\nX138 -> X215\nX139 -> X216\nX209 -> cons(a, cons(s(X213, X214, X215), cons(b, X216)))\nX210 -> T41\nT30 -> cons(X211, T41)\nT40 -> T41", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 148 [arrowhead = none ];
148 -> 29;

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

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

151 [label="INSTANCE with matching:\nX135 -> X212\nX136 -> X213\nX137 -> X214\nX138 -> X215\nX139 -> X216\nT30 -> T41", fontsize=14, style = filled, fillcolor = lightgrey];
29 -> 151 [arrowhead = none , style=dashed];
151 -> 21[style=dashed];

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

153 [label="INSTANCE with matching:\nT13 -> T50\nT7 -> T51", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 153 [arrowhead = none , style=dashed];
153 -> 10[style=dashed];

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

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

156 [label="EVAL with clause\napp(nil, X239, X239).\nand substitution\nT32 -> nil\nT33 -> T76\nT34 -> T77\nT35 -> T78\nT36 -> T79\nX239 -> cons(s(a, s(T76, T77, T78), b), T79)\nX140 -> cons(s(a, s(T76, T77, T78), b), T79)", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 156 [arrowhead = none ];
156 -> 36;

157 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 157 [arrowhead = none ];
157 -> 37;

158 [label="EVAL with clause\napp(cons(X251, X252), X253, cons(X251, X254)) :- app(X252, X253, X254).\nand substitution\nX251 -> T92\nX252 -> T98\nT32 -> cons(T92, T98)\nT33 -> T100\nT34 -> T101\nT35 -> T102\nT36 -> T99\nX253 -> cons(s(a, s(T100, T101, T102), b), T99)\nX254 -> X255\nX140 -> cons(T92, X255)\nT93 -> T98\nT97 -> T99\nT94 -> T100\nT95 -> T101\nT96 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 158 [arrowhead = none ];
158 -> 39;

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

160 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 160 [arrowhead = none ];
160 -> 38;

161 [label="INSTANCE with matching:\nT32 -> T98\nT33 -> T100\nT34 -> T101\nT35 -> T102\nT36 -> T99\nX140 -> X255", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 161 [arrowhead = none , style=dashed];
161 -> 31[style=dashed];

162 [label="ONLY EVAL with clause\nparse(X304, X305) :- ','(app(X306, cons(a, cons(s(X307, X308), cons(b, X309))), X304), ','(app(X306, cons(s(a, s(X307, X308), b), X309), X310), parse(X310, X305))).\nand substitution\nT13 -> T127\nX304 -> T127\nT7 -> T128\nX305 -> T128\nT125 -> T127\nT126 -> T128", fontsize=14, style = filled, fillcolor = white];
41 -> 162 [arrowhead = none ];
162 -> 43;

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

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

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

166 [label="SPLIT 2\nreplacements:\nX306 -> T129\nX307 -> T130\nX308 -> T131\nX309 -> T132\nT128 -> T133", fontsize=14, style = filled, fillcolor = violet];
43 -> 166 [arrowhead = none ];
166 -> 45;

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

168 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
45 -> 168 [arrowhead = none ];
168 -> 54;

169 [label="SPLIT 2\nreplacements:\nX310 -> T144\nT133 -> T145", fontsize=14, style = filled, fillcolor = violet];
45 -> 169 [arrowhead = none ];
169 -> 55;

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

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

172 [label="EVAL with clause\napp(nil, X343, X343).\nand substitution\nX306 -> nil\nX307 -> X344\nX308 -> X345\nX309 -> X346\nX343 -> cons(a, cons(s(X344, X345), cons(b, X346)))\nT127 -> cons(a, cons(s(X344, X345), cons(b, X346)))", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 172 [arrowhead = none ];
172 -> 49;

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

174 [label="EVAL with clause\napp(cons(X366, X367), X368, cons(X366, X369)) :- app(X367, X368, X369).\nand substitution\nX366 -> X370\nX367 -> X371\nX306 -> cons(X370, X371)\nX307 -> X372\nX308 -> X373\nX309 -> X374\nX368 -> cons(a, cons(s(X372, X373), cons(b, X374)))\nX369 -> T137\nT127 -> cons(X370, T137)\nT136 -> T137", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 174 [arrowhead = none ];
174 -> 52;

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

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

177 [label="INSTANCE with matching:\nX306 -> X371\nX307 -> X372\nX308 -> X373\nX309 -> X374\nT127 -> T137", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 177 [arrowhead = none , style=dashed];
177 -> 44[style=dashed];

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

179 [label="INSTANCE with matching:\nT13 -> T144\nT7 -> T145", fontsize=14, style = filled, fillcolor = lightgrey];
55 -> 179 [arrowhead = none , style=dashed];
179 -> 10[style=dashed];

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

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

182 [label="EVAL with clause\napp(nil, X395, X395).\nand substitution\nT129 -> nil\nT130 -> T164\nT131 -> T165\nT132 -> T166\nX395 -> cons(s(a, s(T164, T165), b), T166)\nX310 -> cons(s(a, s(T164, T165), b), T166)", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 182 [arrowhead = none ];
182 -> 59;

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

184 [label="EVAL with clause\napp(cons(X407, X408), X409, cons(X407, X410)) :- app(X408, X409, X410).\nand substitution\nX407 -> T177\nX408 -> T182\nT129 -> cons(T177, T182)\nT130 -> T184\nT131 -> T185\nT132 -> T183\nX409 -> cons(s(a, s(T184, T185), b), T183)\nX410 -> X411\nX310 -> cons(T177, X411)\nT178 -> T182\nT181 -> T183\nT179 -> T184\nT180 -> T185", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 184 [arrowhead = none ];
184 -> 62;

185 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 185 [arrowhead = none ];
185 -> 63;

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

187 [label="INSTANCE with matching:\nT129 -> T182\nT130 -> T184\nT131 -> T185\nT132 -> T183\nX310 -> X411", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 187 [arrowhead = none , style=dashed];
187 -> 54[style=dashed];

188 [label="ONLY EVAL with clause\nparse(X448, X449) :- ','(app(X450, cons(a, cons(b, X451)), X448), ','(app(X450, cons(s(a, b), X451), X452), parse(X452, X449))).\nand substitution\nT13 -> T208\nX448 -> T208\nT7 -> T209\nX449 -> T209\nT206 -> T208\nT207 -> T209", fontsize=14, style = filled, fillcolor = white];
64 -> 188 [arrowhead = none ];
188 -> 66;

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

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

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

192 [label="SPLIT 2\nreplacements:\nX450 -> T210\nX451 -> T211\nT209 -> T212", fontsize=14, style = filled, fillcolor = violet];
66 -> 192 [arrowhead = none ];
192 -> 68;

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

194 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
68 -> 194 [arrowhead = none ];
194 -> 77;

195 [label="SPLIT 2\nreplacements:\nX452 -> T219\nT212 -> T220", fontsize=14, style = filled, fillcolor = violet];
68 -> 195 [arrowhead = none ];
195 -> 78;

196 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
69 -> 196 [arrowhead = none ];
196 -> 70;

197 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
69 -> 197 [arrowhead = none ];
197 -> 71;

198 [label="EVAL with clause\napp(nil, X469, X469).\nand substitution\nX450 -> nil\nX451 -> X470\nX469 -> cons(a, cons(b, X470))\nT208 -> cons(a, cons(b, X470))", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 198 [arrowhead = none ];
198 -> 72;

199 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 199 [arrowhead = none ];
199 -> 73;

200 [label="EVAL with clause\napp(cons(X486, X487), X488, cons(X486, X489)) :- app(X487, X488, X489).\nand substitution\nX486 -> X490\nX487 -> X491\nX450 -> cons(X490, X491)\nX451 -> X492\nX488 -> cons(a, cons(b, X492))\nX489 -> T216\nT208 -> cons(X490, T216)\nT215 -> T216", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 200 [arrowhead = none ];
200 -> 75;

201 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 201 [arrowhead = none ];
201 -> 76;

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

203 [label="INSTANCE with matching:\nX450 -> X491\nX451 -> X492\nT208 -> T216", fontsize=14, style = filled, fillcolor = lightgrey];
75 -> 203 [arrowhead = none , style=dashed];
203 -> 67[style=dashed];

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

205 [label="INSTANCE with matching:\nT13 -> T219\nT7 -> T220", fontsize=14, style = filled, fillcolor = lightgrey];
78 -> 205 [arrowhead = none , style=dashed];
205 -> 10[style=dashed];

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

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

208 [label="EVAL with clause\napp(nil, X509, X509).\nand substitution\nT210 -> nil\nT211 -> T227\nX509 -> cons(s(a, b), T227)\nX452 -> cons(s(a, b), T227)", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 208 [arrowhead = none ];
208 -> 82;

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

210 [label="EVAL with clause\napp(cons(X521, X522), X523, cons(X521, X524)) :- app(X522, X523, X524).\nand substitution\nX521 -> T234\nX522 -> T237\nT210 -> cons(T234, T237)\nT211 -> T238\nX523 -> cons(s(a, b), T238)\nX524 -> X525\nX452 -> cons(T234, X525)\nT235 -> T237\nT236 -> T238", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 210 [arrowhead = none ];
210 -> 85;

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

212 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 212 [arrowhead = none ];
212 -> 84;

213 [label="INSTANCE with matching:\nT210 -> T237\nT211 -> T238\nX452 -> X525", fontsize=14, style = filled, fillcolor = lightgrey];
85 -> 213 [arrowhead = none , style=dashed];
213 -> 77[style=dashed];

214 [label="EVAL with clause\nparse(cons(s(X548, X549), nil), s(X548, X549)).\nand substitution\nX548 -> T251\nX549 -> T252\nT13 -> cons(s(T251, T252), nil)\nT7 -> s(T251, T252)", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 214 [arrowhead = none ];
214 -> 89;

215 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 215 [arrowhead = none ];
215 -> 90;

216 [label="EVAL with clause\nparse(cons(s(X558, X559, X560), nil), s(X558, X559, X560)).\nand substitution\nX558 -> T259\nX559 -> T260\nX560 -> T261\nT13 -> cons(s(T259, T260, T261), nil)\nT7 -> s(T259, T260, T261)", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 216 [arrowhead = none ];
216 -> 92;

217 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 217 [arrowhead = none ];
217 -> 93;

218 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 218 [arrowhead = none ];
218 -> 91;

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

220 [label="EVAL with clause\napp(cons(X604, X605), X606, cons(X604, X607)) :- app(X605, X606, X607).\nand substitution\nX604 -> X608\nX605 -> X609\nX5 -> cons(X608, X609)\nX6 -> X610\nX7 -> X611\nX8 -> X612\nX9 -> X613\nX606 -> cons(a, cons(s(X610, X611, X612), cons(b, X613)))\nX607 -> T266\nT5 -> cons(X608, T266)", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 220 [arrowhead = none ];
220 -> 97;

221 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 221 [arrowhead = none ];
221 -> 98;

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

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

224 [label="SPLIT 2\nnew knowledge:\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT271 is ground\nreplacements:\nX609 -> T267\nX610 -> T268\nX611 -> T269\nX612 -> T270\nX613 -> T271", fontsize=14, style = filled, fillcolor = violet];
97 -> 224 [arrowhead = none ];
224 -> 100;

225 [label="INSTANCE with matching:\nX135 -> X609\nX136 -> X610\nX137 -> X611\nX138 -> X612\nX139 -> X613\nT30 -> T266", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 225 [arrowhead = none , style=dashed];
225 -> 21[style=dashed];

226 [label="INSTANCE with matching:\nT32 -> cons(X608, T267)\nT33 -> T268\nT34 -> T269\nT35 -> T270\nT36 -> T271\nX140 -> X10\nT37 -> T7", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 226 [arrowhead = none , style=dashed];
226 -> 22[style=dashed];

227 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
101 -> 227 [arrowhead = none ];
227 -> 102;

228 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
101 -> 228 [arrowhead = none ];
228 -> 103;

229 [label="ONLY EVAL with clause\nparse(X680, X681) :- ','(app(X682, cons(a, cons(s(X683, X684), cons(b, X685))), X680), ','(app(X682, cons(s(a, s(X683, X684), b), X685), X686), parse(X686, X681))).\nand substitution\nT5 -> T287\nX680 -> T287\nT2 -> T289\nX681 -> T289\nT288 -> T289", fontsize=14, style = filled, fillcolor = white];
102 -> 229 [arrowhead = none ];
229 -> 104;

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

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

232 [label="INSTANCE with matching:\nX306 -> X682\nX307 -> X683\nX308 -> X684\nX309 -> X685\nT127 -> T287\nX310 -> X686\nT128 -> T289", fontsize=14, style = filled, fillcolor = lightgrey];
104 -> 232 [arrowhead = none , style=dashed];
232 -> 43[style=dashed];

233 [label="ONLY EVAL with clause\nparse(X717, X718) :- ','(app(X719, cons(a, cons(b, X720)), X717), ','(app(X719, cons(s(a, b), X720), X721), parse(X721, X718))).\nand substitution\nT5 -> T300\nX717 -> T300\nT2 -> T302\nX718 -> T302\nT301 -> T302", fontsize=14, style = filled, fillcolor = white];
105 -> 233 [arrowhead = none ];
233 -> 107;

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

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

236 [label="INSTANCE with matching:\nX450 -> X719\nX451 -> X720\nT208 -> T300\nX452 -> X721\nT209 -> T302", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 236 [arrowhead = none , style=dashed];
236 -> 66[style=dashed];

237 [label="EVAL with clause\nparse(cons(s(X734, X735), nil), s(X734, X735)).\nand substitution\nX734 -> T311\nX735 -> T312\nT5 -> cons(s(T311, T312), nil)\nT2 -> s(T311, T312)", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 237 [arrowhead = none ];
237 -> 110;

238 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 238 [arrowhead = none ];
238 -> 111;

239 [label="EVAL with clause\nparse(cons(s(X744, X745, X746), nil), s(X744, X745, X746)).\nand substitution\nX744 -> T319\nX745 -> T320\nX746 -> T321\nT5 -> cons(s(T319, T320, T321), nil)\nT2 -> s(T319, T320, T321)", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 239 [arrowhead = none ];
239 -> 113;

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

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

242 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 242 [arrowhead = none ];
242 -> 115;

}

(2) Obligation:

Triples:

app21(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) :- app21(X212, X213, X214, X215, X216, T41).
parse10(T30, T31) :- app21(X135, X136, X137, X138, X139, T30).
parse10(T30, T37) :- ','(appc21(T32, T33, T34, T35, T36, T30), p22(T32, T33, T34, T35, T36, X140, T37)).
parse10(T127, T128) :- p43(X306, X307, X308, X309, T127, X310, T128).
parse10(T208, T209) :- p66(X450, X451, T208, X452, T209).
app31(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) :- app31(T98, T100, T101, T102, T99, X255).
app44(cons(X370, X371), X372, X373, X374, cons(X370, T137)) :- app44(X371, X372, X373, X374, T137).
app54(cons(T177, T182), T184, T185, T183, cons(T177, X411)) :- app54(T182, T184, T185, T183, X411).
app67(cons(X490, X491), X492, cons(X490, T216)) :- app67(X491, X492, T216).
app77(cons(T234, T237), T238, cons(T234, X525)) :- app77(T237, T238, X525).
p22(T32, T33, T34, T35, T36, X140, T37) :- app31(T32, T33, T34, T35, T36, X140).
p22(T32, T33, T34, T35, T36, T50, T51) :- ','(appc31(T32, T33, T34, T35, T36, T50), parse10(T50, T51)).
p43(X306, X307, X308, X309, T127, X310, T128) :- app44(X306, X307, X308, X309, T127).
p43(T129, T130, T131, T132, T127, X310, T133) :- ','(appc44(T129, T130, T131, T132, T127), app54(T129, T130, T131, T132, X310)).
p43(T129, T130, T131, T132, T127, T144, T145) :- ','(appc44(T129, T130, T131, T132, T127), ','(appc54(T129, T130, T131, T132, T144), parse10(T144, T145))).
p66(X450, X451, T208, X452, T209) :- app67(X450, X451, T208).
p66(T210, T211, T208, X452, T212) :- ','(appc67(T210, T211, T208), app77(T210, T211, X452)).
p66(T210, T211, T208, T219, T220) :- ','(appc67(T210, T211, T208), ','(appc77(T210, T211, T219), parse10(T219, T220))).
parse1(cons(a, cons(s(T9, T10, T11), cons(b, T12))), T7) :- ','(appc9(T9, T10, T11, T12, T13), parse10(T13, T7)).
parse1(cons(X608, T266), T7) :- app21(X609, X610, X611, X612, X613, T266).
parse1(cons(X608, T266), T7) :- ','(appc21(T267, T268, T269, T270, T271, T266), p22(cons(X608, T267), T268, T269, T270, T271, X10, T7)).
parse1(T287, T289) :- p43(X682, X683, X684, X685, T287, X686, T289).
parse1(T300, T302) :- p66(X719, X720, T300, X721, T302).

Clauses:

appc21(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))).
appc21(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) :- appc21(X212, X213, X214, X215, X216, T41).
parsec10(T30, T37) :- ','(appc21(T32, T33, T34, T35, T36, T30), qc22(T32, T33, T34, T35, T36, X140, T37)).
parsec10(T127, T128) :- qc43(X306, X307, X308, X309, T127, X310, T128).
parsec10(T208, T209) :- qc66(X450, X451, T208, X452, T209).
parsec10(cons(s(T251, T252), nil), s(T251, T252)).
parsec10(cons(s(T259, T260, T261), nil), s(T259, T260, T261)).
appc31(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)).
appc31(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) :- appc31(T98, T100, T101, T102, T99, X255).
appc44(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))).
appc44(cons(X370, X371), X372, X373, X374, cons(X370, T137)) :- appc44(X371, X372, X373, X374, T137).
appc54(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)).
appc54(cons(T177, T182), T184, T185, T183, cons(T177, X411)) :- appc54(T182, T184, T185, T183, X411).
appc67(nil, X470, cons(a, cons(b, X470))).
appc67(cons(X490, X491), X492, cons(X490, T216)) :- appc67(X491, X492, T216).
appc77(nil, T227, cons(s(a, b), T227)).
appc77(cons(T234, T237), T238, cons(T234, X525)) :- appc77(T237, T238, X525).
qc22(T32, T33, T34, T35, T36, T50, T51) :- ','(appc31(T32, T33, T34, T35, T36, T50), parsec10(T50, T51)).
qc43(T129, T130, T131, T132, T127, T144, T145) :- ','(appc44(T129, T130, T131, T132, T127), ','(appc54(T129, T130, T131, T132, T144), parsec10(T144, T145))).
qc66(T210, T211, T208, T219, T220) :- ','(appc67(T210, T211, T208), ','(appc77(T210, T211, T219), parsec10(T219, T220))).
appc9(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)).

Afs:

parse1(x1, x2) = parse1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
parse1_in: (b,f)
parse10_in: (b,f)
app21_in: (f,f,f,f,f,b)
appc21_in: (f,f,f,f,f,b)
p22_in: (b,b,b,b,b,f,f)
app31_in: (b,b,b,b,b,f)
appc31_in: (b,b,b,b,b,f)
p43_in: (f,f,f,f,b,f,f)
app44_in: (f,f,f,f,b)
appc44_in: (f,f,f,f,b)
app54_in: (b,b,b,b,f)
appc54_in: (b,b,b,b,f)
p66_in: (f,f,b,f,f)
app67_in: (f,f,b)
appc67_in: (f,f,b)
app77_in: (b,b,f)
appc77_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PARSE1_IN_GA(cons(a, cons(s(T9, T10, T11), cons(b, T12))), T7) → U27_GA(T9, T10, T11, T12, T7, appc9_in_gggga(T9, T10, T11, T12, T13))
U27_GA(T9, T10, T11, T12, T7, appc9_out_gggga(T9, T10, T11, T12, T13)) → U28_GA(T9, T10, T11, T12, T7, parse10_in_ga(T13, T7))
U27_GA(T9, T10, T11, T12, T7, appc9_out_gggga(T9, T10, T11, T12, T13)) → PARSE10_IN_GA(T13, T7)
PARSE10_IN_GA(T30, T31) → U2_GA(T30, T31, app21_in_aaaaag(X135, X136, X137, X138, X139, T30))
PARSE10_IN_GA(T30, T31) → APP21_IN_AAAAAG(X135, X136, X137, X138, X139, T30)
APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U1_AAAAAG(X211, X212, X213, X214, X215, X216, T41, app21_in_aaaaag(X212, X213, X214, X215, X216, T41))
APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → APP21_IN_AAAAAG(X212, X213, X214, X215, X216, T41)
PARSE10_IN_GA(T30, T37) → U3_GA(T30, T37, appc21_in_aaaaag(T32, T33, T34, T35, T36, T30))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → U4_GA(T30, T37, p22_in_gggggaa(T32, T33, T34, T35, T36, X140, T37))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37) → U12_GGGGGAA(T32, T33, T34, T35, T36, X140, T37, app31_in_ggggga(T32, T33, T34, T35, T36, X140))
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37) → APP31_IN_GGGGGA(T32, T33, T34, T35, T36, X140)
APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U7_GGGGGA(T92, T98, T100, T101, T102, T99, X255, app31_in_ggggga(T98, T100, T101, T102, T99, X255))
APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99, X255)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, T50, T51) → U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_in_ggggga(T32, T33, T34, T35, T36, T50))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → U14_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, parse10_in_ga(T50, T51))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50, T51)
PARSE10_IN_GA(T127, T128) → U5_GA(T127, T128, p43_in_aaaagaa(X306, X307, X308, X309, T127, X310, T128))
PARSE10_IN_GA(T127, T128) → P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128)
P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128) → U15_AAAAGAA(X306, X307, X308, X309, T127, X310, T128, app44_in_aaaag(X306, X307, X308, X309, T127))
P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128) → APP44_IN_AAAAG(X306, X307, X308, X309, T127)
APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U8_AAAAG(X370, X371, X372, X373, X374, T137, app44_in_aaaag(X371, X372, X373, X374, T137))
APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → APP44_IN_AAAAG(X371, X372, X373, X374, T137)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, X310, T133) → U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_in_aaaag(T129, T130, T131, T132, T127))
U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U17_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, app54_in_gggga(T129, T130, T131, T132, X310))
U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_out_aaaag(T129, T130, T131, T132, T127)) → APP54_IN_GGGGA(T129, T130, T131, T132, X310)
APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U9_GGGGA(T177, T182, T184, T185, T183, X411, app54_in_gggga(T182, T184, T185, T183, X411))
APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → APP54_IN_GGGGA(T182, T184, T185, T183, X411)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, T144, T145) → U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_in_aaaag(T129, T130, T131, T132, T127))
U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_in_gggga(T129, T130, T131, T132, T144))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → U20_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, parse10_in_ga(T144, T145))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144, T145)
PARSE10_IN_GA(T208, T209) → U6_GA(T208, T209, p66_in_aagaa(X450, X451, T208, X452, T209))
PARSE10_IN_GA(T208, T209) → P66_IN_AAGAA(X450, X451, T208, X452, T209)
P66_IN_AAGAA(X450, X451, T208, X452, T209) → U21_AAGAA(X450, X451, T208, X452, T209, app67_in_aag(X450, X451, T208))
P66_IN_AAGAA(X450, X451, T208, X452, T209) → APP67_IN_AAG(X450, X451, T208)
APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → U10_AAG(X490, X491, X492, T216, app67_in_aag(X491, X492, T216))
APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → APP67_IN_AAG(X491, X492, T216)
P66_IN_AAGAA(T210, T211, T208, X452, T212) → U22_AAGAA(T210, T211, T208, X452, T212, appc67_in_aag(T210, T211, T208))
U22_AAGAA(T210, T211, T208, X452, T212, appc67_out_aag(T210, T211, T208)) → U23_AAGAA(T210, T211, T208, X452, T212, app77_in_gga(T210, T211, X452))
U22_AAGAA(T210, T211, T208, X452, T212, appc67_out_aag(T210, T211, T208)) → APP77_IN_GGA(T210, T211, X452)
APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → U11_GGA(T234, T237, T238, X525, app77_in_gga(T237, T238, X525))
APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → APP77_IN_GGA(T237, T238, X525)
P66_IN_AAGAA(T210, T211, T208, T219, T220) → U24_AAGAA(T210, T211, T208, T219, T220, appc67_in_aag(T210, T211, T208))
U24_AAGAA(T210, T211, T208, T219, T220, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, T219, T220, appc77_in_gga(T210, T211, T219))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → U26_AAGAA(T210, T211, T208, T219, T220, parse10_in_ga(T219, T220))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219, T220)
PARSE1_IN_GA(cons(X608, T266), T7) → U29_GA(X608, T266, T7, app21_in_aaaaag(X609, X610, X611, X612, X613, T266))
PARSE1_IN_GA(cons(X608, T266), T7) → APP21_IN_AAAAAG(X609, X610, X611, X612, X613, T266)
PARSE1_IN_GA(cons(X608, T266), T7) → U30_GA(X608, T266, T7, appc21_in_aaaaag(T267, T268, T269, T270, T271, T266))
U30_GA(X608, T266, T7, appc21_out_aaaaag(T267, T268, T269, T270, T271, T266)) → U31_GA(X608, T266, T7, p22_in_gggggaa(cons(X608, T267), T268, T269, T270, T271, X10, T7))
U30_GA(X608, T266, T7, appc21_out_aaaaag(T267, T268, T269, T270, T271, T266)) → P22_IN_GGGGGAA(cons(X608, T267), T268, T269, T270, T271, X10, T7)
PARSE1_IN_GA(T287, T289) → U32_GA(T287, T289, p43_in_aaaagaa(X682, X683, X684, X685, T287, X686, T289))
PARSE1_IN_GA(T287, T289) → P43_IN_AAAAGAA(X682, X683, X684, X685, T287, X686, T289)
PARSE1_IN_GA(T300, T302) → U33_GA(T300, T302, p66_in_aagaa(X719, X720, T300, X721, T302))
PARSE1_IN_GA(T300, T302) → P66_IN_AAGAA(X719, X720, T300, X721, T302)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
a = a
s(x1, x2, x3) = s(x1, x2, x3)
b = b
appc9_in_gggga(x1, x2, x3, x4, x5) = appc9_in_gggga(x1, x2, x3, x4)
appc9_out_gggga(x1, x2, x3, x4, x5) = appc9_out_gggga(x1, x2, x3, x4, x5)
parse10_in_ga(x1, x2) = parse10_in_ga(x1)
app21_in_aaaaag(x1, x2, x3, x4, x5, x6) = app21_in_aaaaag(x6)
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6) = appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6) = appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8) = U35_aaaaag(x1, x7, x8)
p22_in_gggggaa(x1, x2, x3, x4, x5, x6, x7) = p22_in_gggggaa(x1, x2, x3, x4, x5)
app31_in_ggggga(x1, x2, x3, x4, x5, x6) = app31_in_ggggga(x1, x2, x3, x4, x5)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6) = appc31_in_ggggga(x1, x2, x3, x4, x5)
nil = nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6) = appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8) = U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
p43_in_aaaagaa(x1, x2, x3, x4, x5, x6, x7) = p43_in_aaaagaa(x5)
app44_in_aaaag(x1, x2, x3, x4, x5) = app44_in_aaaag(x5)
appc44_in_aaaag(x1, x2, x3, x4, x5) = appc44_in_aaaag(x5)
s(x1, x2) = s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5) = appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7) = U41_aaaag(x1, x6, x7)
app54_in_gggga(x1, x2, x3, x4, x5) = app54_in_gggga(x1, x2, x3, x4)
appc54_in_gggga(x1, x2, x3, x4, x5) = appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5) = appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7) = U42_gggga(x1, x2, x3, x4, x5, x7)
p66_in_aagaa(x1, x2, x3, x4, x5) = p66_in_aagaa(x3)
app67_in_aag(x1, x2, x3) = app67_in_aag(x3)
appc67_in_aag(x1, x2, x3) = appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3) = appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5) = U43_aag(x1, x4, x5)
app77_in_gga(x1, x2, x3) = app77_in_gga(x1, x2)
appc77_in_gga(x1, x2, x3) = appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3) = appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5) = U44_gga(x1, x2, x3, x5)
PARSE1_IN_GA(x1, x2) = PARSE1_IN_GA(x1)
U27_GA(x1, x2, x3, x4, x5, x6) = U27_GA(x1, x2, x3, x4, x6)
U28_GA(x1, x2, x3, x4, x5, x6) = U28_GA(x1, x2, x3, x4, x6)
PARSE10_IN_GA(x1, x2) = PARSE10_IN_GA(x1)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
APP21_IN_AAAAAG(x1, x2, x3, x4, x5, x6) = APP21_IN_AAAAAG(x6)
U1_AAAAAG(x1, x2, x3, x4, x5, x6, x7, x8) = U1_AAAAAG(x1, x7, x8)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
P22_IN_GGGGGAA(x1, x2, x3, x4, x5, x6, x7) = P22_IN_GGGGGAA(x1, x2, x3, x4, x5)
U12_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U12_GGGGGAA(x1, x2, x3, x4, x5, x8)
APP31_IN_GGGGGA(x1, x2, x3, x4, x5, x6) = APP31_IN_GGGGGA(x1, x2, x3, x4, x5)
U7_GGGGGA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_GGGGGA(x1, x2, x3, x4, x5, x6, x8)
U13_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U13_GGGGGAA(x1, x2, x3, x4, x5, x8)
U14_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U14_GGGGGAA(x1, x2, x3, x4, x5, x6, x8)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
P43_IN_AAAAGAA(x1, x2, x3, x4, x5, x6, x7) = P43_IN_AAAAGAA(x5)
U15_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U15_AAAAGAA(x5, x8)
APP44_IN_AAAAG(x1, x2, x3, x4, x5) = APP44_IN_AAAAG(x5)
U8_AAAAG(x1, x2, x3, x4, x5, x6, x7) = U8_AAAAG(x1, x6, x7)
U16_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U16_AAAAGAA(x5, x8)
U17_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U17_AAAAGAA(x1, x2, x3, x4, x5, x8)
APP54_IN_GGGGA(x1, x2, x3, x4, x5) = APP54_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6, x7) = U9_GGGGA(x1, x2, x3, x4, x5, x7)
U18_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U18_AAAAGAA(x5, x8)
U19_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U19_AAAAGAA(x1, x2, x3, x4, x5, x8)
U20_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U20_AAAAGAA(x1, x2, x3, x4, x5, x8)
U6_GA(x1, x2, x3) = U6_GA(x1, x3)
P66_IN_AAGAA(x1, x2, x3, x4, x5) = P66_IN_AAGAA(x3)
U21_AAGAA(x1, x2, x3, x4, x5, x6) = U21_AAGAA(x3, x6)
APP67_IN_AAG(x1, x2, x3) = APP67_IN_AAG(x3)
U10_AAG(x1, x2, x3, x4, x5) = U10_AAG(x1, x4, x5)
U22_AAGAA(x1, x2, x3, x4, x5, x6) = U22_AAGAA(x3, x6)
U23_AAGAA(x1, x2, x3, x4, x5, x6) = U23_AAGAA(x1, x2, x3, x6)
APP77_IN_GGA(x1, x2, x3) = APP77_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4, x5) = U11_GGA(x1, x2, x3, x5)
U24_AAGAA(x1, x2, x3, x4, x5, x6) = U24_AAGAA(x3, x6)
U25_AAGAA(x1, x2, x3, x4, x5, x6) = U25_AAGAA(x1, x2, x3, x6)
U26_AAGAA(x1, x2, x3, x4, x5, x6) = U26_AAGAA(x1, x2, x3, x6)
U29_GA(x1, x2, x3, x4) = U29_GA(x1, x2, x4)
U30_GA(x1, x2, x3, x4) = U30_GA(x1, x2, x4)
U31_GA(x1, x2, x3, x4) = U31_GA(x1, x2, x4)
U32_GA(x1, x2, x3) = U32_GA(x1, x3)
U33_GA(x1, x2, x3) = U33_GA(x1, x3)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

PARSE1_IN_GA(cons(a, cons(s(T9, T10, T11), cons(b, T12))), T7) → U27_GA(T9, T10, T11, T12, T7, appc9_in_gggga(T9, T10, T11, T12, T13))
U27_GA(T9, T10, T11, T12, T7, appc9_out_gggga(T9, T10, T11, T12, T13)) → U28_GA(T9, T10, T11, T12, T7, parse10_in_ga(T13, T7))
U27_GA(T9, T10, T11, T12, T7, appc9_out_gggga(T9, T10, T11, T12, T13)) → PARSE10_IN_GA(T13, T7)
PARSE10_IN_GA(T30, T31) → U2_GA(T30, T31, app21_in_aaaaag(X135, X136, X137, X138, X139, T30))
PARSE10_IN_GA(T30, T31) → APP21_IN_AAAAAG(X135, X136, X137, X138, X139, T30)
APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U1_AAAAAG(X211, X212, X213, X214, X215, X216, T41, app21_in_aaaaag(X212, X213, X214, X215, X216, T41))
APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → APP21_IN_AAAAAG(X212, X213, X214, X215, X216, T41)
PARSE10_IN_GA(T30, T37) → U3_GA(T30, T37, appc21_in_aaaaag(T32, T33, T34, T35, T36, T30))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → U4_GA(T30, T37, p22_in_gggggaa(T32, T33, T34, T35, T36, X140, T37))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37) → U12_GGGGGAA(T32, T33, T34, T35, T36, X140, T37, app31_in_ggggga(T32, T33, T34, T35, T36, X140))
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37) → APP31_IN_GGGGGA(T32, T33, T34, T35, T36, X140)
APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U7_GGGGGA(T92, T98, T100, T101, T102, T99, X255, app31_in_ggggga(T98, T100, T101, T102, T99, X255))
APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99, X255)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, T50, T51) → U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_in_ggggga(T32, T33, T34, T35, T36, T50))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → U14_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, parse10_in_ga(T50, T51))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50, T51)
PARSE10_IN_GA(T127, T128) → U5_GA(T127, T128, p43_in_aaaagaa(X306, X307, X308, X309, T127, X310, T128))
PARSE10_IN_GA(T127, T128) → P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128)
P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128) → U15_AAAAGAA(X306, X307, X308, X309, T127, X310, T128, app44_in_aaaag(X306, X307, X308, X309, T127))
P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128) → APP44_IN_AAAAG(X306, X307, X308, X309, T127)
APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U8_AAAAG(X370, X371, X372, X373, X374, T137, app44_in_aaaag(X371, X372, X373, X374, T137))
APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → APP44_IN_AAAAG(X371, X372, X373, X374, T137)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, X310, T133) → U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_in_aaaag(T129, T130, T131, T132, T127))
U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U17_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, app54_in_gggga(T129, T130, T131, T132, X310))
U16_AAAAGAA(T129, T130, T131, T132, T127, X310, T133, appc44_out_aaaag(T129, T130, T131, T132, T127)) → APP54_IN_GGGGA(T129, T130, T131, T132, X310)
APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U9_GGGGA(T177, T182, T184, T185, T183, X411, app54_in_gggga(T182, T184, T185, T183, X411))
APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → APP54_IN_GGGGA(T182, T184, T185, T183, X411)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, T144, T145) → U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_in_aaaag(T129, T130, T131, T132, T127))
U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_in_gggga(T129, T130, T131, T132, T144))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → U20_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, parse10_in_ga(T144, T145))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144, T145)
PARSE10_IN_GA(T208, T209) → U6_GA(T208, T209, p66_in_aagaa(X450, X451, T208, X452, T209))
PARSE10_IN_GA(T208, T209) → P66_IN_AAGAA(X450, X451, T208, X452, T209)
P66_IN_AAGAA(X450, X451, T208, X452, T209) → U21_AAGAA(X450, X451, T208, X452, T209, app67_in_aag(X450, X451, T208))
P66_IN_AAGAA(X450, X451, T208, X452, T209) → APP67_IN_AAG(X450, X451, T208)
APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → U10_AAG(X490, X491, X492, T216, app67_in_aag(X491, X492, T216))
APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → APP67_IN_AAG(X491, X492, T216)
P66_IN_AAGAA(T210, T211, T208, X452, T212) → U22_AAGAA(T210, T211, T208, X452, T212, appc67_in_aag(T210, T211, T208))
U22_AAGAA(T210, T211, T208, X452, T212, appc67_out_aag(T210, T211, T208)) → U23_AAGAA(T210, T211, T208, X452, T212, app77_in_gga(T210, T211, X452))
U22_AAGAA(T210, T211, T208, X452, T212, appc67_out_aag(T210, T211, T208)) → APP77_IN_GGA(T210, T211, X452)
APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → U11_GGA(T234, T237, T238, X525, app77_in_gga(T237, T238, X525))
APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → APP77_IN_GGA(T237, T238, X525)
P66_IN_AAGAA(T210, T211, T208, T219, T220) → U24_AAGAA(T210, T211, T208, T219, T220, appc67_in_aag(T210, T211, T208))
U24_AAGAA(T210, T211, T208, T219, T220, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, T219, T220, appc77_in_gga(T210, T211, T219))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → U26_AAGAA(T210, T211, T208, T219, T220, parse10_in_ga(T219, T220))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219, T220)
PARSE1_IN_GA(cons(X608, T266), T7) → U29_GA(X608, T266, T7, app21_in_aaaaag(X609, X610, X611, X612, X613, T266))
PARSE1_IN_GA(cons(X608, T266), T7) → APP21_IN_AAAAAG(X609, X610, X611, X612, X613, T266)
PARSE1_IN_GA(cons(X608, T266), T7) → U30_GA(X608, T266, T7, appc21_in_aaaaag(T267, T268, T269, T270, T271, T266))
U30_GA(X608, T266, T7, appc21_out_aaaaag(T267, T268, T269, T270, T271, T266)) → U31_GA(X608, T266, T7, p22_in_gggggaa(cons(X608, T267), T268, T269, T270, T271, X10, T7))
U30_GA(X608, T266, T7, appc21_out_aaaaag(T267, T268, T269, T270, T271, T266)) → P22_IN_GGGGGAA(cons(X608, T267), T268, T269, T270, T271, X10, T7)
PARSE1_IN_GA(T287, T289) → U32_GA(T287, T289, p43_in_aaaagaa(X682, X683, X684, X685, T287, X686, T289))
PARSE1_IN_GA(T287, T289) → P43_IN_AAAAGAA(X682, X683, X684, X685, T287, X686, T289)
PARSE1_IN_GA(T300, T302) → U33_GA(T300, T302, p66_in_aagaa(X719, X720, T300, X721, T302))
PARSE1_IN_GA(T300, T302) → P66_IN_AAGAA(X719, X720, T300, X721, T302)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 7 SCCs with 38 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → APP77_IN_GGA(T237, T238, X525)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

APP77_IN_GGA(cons(T234, T237), T238, cons(T234, X525)) → APP77_IN_GGA(T237, T238, X525)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

APP77_IN_GGA(cons(T234, T237), T238) → APP77_IN_GGA(T237, T238)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APP77_IN_GGA(cons(T234, T237), T238) → APP77_IN_GGA(T237, T238)
The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → APP67_IN_AAG(X491, X492, T216)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

APP67_IN_AAG(cons(X490, X491), X492, cons(X490, T216)) → APP67_IN_AAG(X491, X492, T216)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

APP67_IN_AAG(cons(X490, T216)) → APP67_IN_AAG(T216)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APP67_IN_AAG(cons(X490, T216)) → APP67_IN_AAG(T216)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → APP54_IN_GGGGA(T182, T184, T185, T183, X411)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → APP54_IN_GGGGA(T182, T184, T185, T183, X411)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183) → APP54_IN_GGGGA(T182, T184, T185, T183)

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

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

APP54_IN_GGGGA(cons(T177, T182), T184, T185, T183) → APP54_IN_GGGGA(T182, T184, T185, T183)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4

(27) YES

(28) Obligation:

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

APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → APP44_IN_AAAAG(X371, X372, X373, X374, T137)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

APP44_IN_AAAAG(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → APP44_IN_AAAAG(X371, X372, X373, X374, T137)

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

APP44_IN_AAAAG(cons(X370, T137)) → APP44_IN_AAAAG(T137)

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

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

APP44_IN_AAAAG(cons(X370, T137)) → APP44_IN_AAAAG(T137)
The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

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

APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99, X255)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99, X255)

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

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99)

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

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

APP31_IN_GGGGGA(cons(T92, T98), T100, T101, T102, T99) → APP31_IN_GGGGGA(T98, T100, T101, T102, T99)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5

(41) YES

(42) Obligation:

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

APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → APP21_IN_AAAAAG(X212, X213, X214, X215, X216, T41)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

APP21_IN_AAAAAG(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → APP21_IN_AAAAAG(X212, X213, X214, X215, X216, T41)

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

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

APP21_IN_AAAAAG(cons(X211, T41)) → APP21_IN_AAAAAG(T41)

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

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

APP21_IN_AAAAAG(cons(X211, T41)) → APP21_IN_AAAAAG(T41)
The graph contains the following edges 1 > 1

(48) YES

(49) Obligation:

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

PARSE10_IN_GA(T30, T37) → U3_GA(T30, T37, appc21_in_aaaaag(T32, T33, T34, T35, T36, T30))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, T50, T51) → U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_in_ggggga(T32, T33, T34, T35, T36, T50))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50, T51)
PARSE10_IN_GA(T127, T128) → P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, T144, T145) → U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_in_aaaag(T129, T130, T131, T132, T127))
U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_in_gggga(T129, T130, T131, T132, T144))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144, T145)
PARSE10_IN_GA(T208, T209) → P66_IN_AAGAA(X450, X451, T208, X452, T209)
P66_IN_AAGAA(T210, T211, T208, T219, T220) → U24_AAGAA(T210, T211, T208, T219, T220, appc67_in_aag(T210, T211, T208))
U24_AAGAA(T210, T211, T208, T219, T220, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, T219, T220, appc77_in_gga(T210, T211, T219))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219, T220)

The TRS R consists of the following rules:

appc9_in_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80)) → appc9_out_gggga(X77, X78, X79, X80, cons(s(a, s(X77, X78, X79), b), X80))
appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(50) UsableRulesProof (EQUIVALENT transformation)

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

(51) Obligation:

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

PARSE10_IN_GA(T30, T37) → U3_GA(T30, T37, appc21_in_aaaaag(T32, T33, T34, T35, T36, T30))
U3_GA(T30, T37, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36, X140, T37)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36, T50, T51) → U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_in_ggggga(T32, T33, T34, T35, T36, T50))
U13_GGGGGAA(T32, T33, T34, T35, T36, T50, T51, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50, T51)
PARSE10_IN_GA(T127, T128) → P43_IN_AAAAGAA(X306, X307, X308, X309, T127, X310, T128)
P43_IN_AAAAGAA(T129, T130, T131, T132, T127, T144, T145) → U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_in_aaaag(T129, T130, T131, T132, T127))
U18_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_in_gggga(T129, T130, T131, T132, T144))
U19_AAAAGAA(T129, T130, T131, T132, T127, T144, T145, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144, T145)
PARSE10_IN_GA(T208, T209) → P66_IN_AAGAA(X450, X451, T208, X452, T209)
P66_IN_AAGAA(T210, T211, T208, T219, T220) → U24_AAGAA(T210, T211, T208, T219, T220, appc67_in_aag(T210, T211, T208))
U24_AAGAA(T210, T211, T208, T219, T220, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, T219, T220, appc77_in_gga(T210, T211, T219))
U25_AAGAA(T210, T211, T208, T219, T220, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219, T220)

The TRS R consists of the following rules:

appc21_in_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41)) → U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_in_aaaaag(X212, X213, X214, X215, X216, T41))
appc31_in_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79)) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255)) → U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_in_ggggga(T98, T100, T101, T102, T99, X255))
appc44_in_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137)) → U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_in_aaaag(X371, X372, X373, X374, T137))
appc54_in_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166)) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411)) → U42_gggga(T177, T182, T184, T185, T183, X411, appc54_in_gggga(T182, T184, T185, T183, X411))
appc67_in_aag(nil, X470, cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, X491), X492, cons(X490, T216)) → U43_aag(X490, X491, X492, T216, appc67_in_aag(X491, X492, T216))
appc77_in_gga(nil, T227, cons(s(a, b), T227)) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238, cons(T234, X525)) → U44_gga(T234, T237, T238, X525, appc77_in_gga(T237, T238, X525))
U35_aaaaag(X211, X212, X213, X214, X215, X216, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, X255, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, X371, X372, X373, X374, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, X411, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, X491, X492, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, X525, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The argument filtering Pi contains the following mapping:
cons(x1, x2) = cons(x1, x2)
a = a
s(x1, x2, x3) = s(x1, x2, x3)
b = b
appc21_in_aaaaag(x1, x2, x3, x4, x5, x6) = appc21_in_aaaaag(x6)
appc21_out_aaaaag(x1, x2, x3, x4, x5, x6) = appc21_out_aaaaag(x1, x2, x3, x4, x5, x6)
U35_aaaaag(x1, x2, x3, x4, x5, x6, x7, x8) = U35_aaaaag(x1, x7, x8)
appc31_in_ggggga(x1, x2, x3, x4, x5, x6) = appc31_in_ggggga(x1, x2, x3, x4, x5)
nil = nil
appc31_out_ggggga(x1, x2, x3, x4, x5, x6) = appc31_out_ggggga(x1, x2, x3, x4, x5, x6)
U40_ggggga(x1, x2, x3, x4, x5, x6, x7, x8) = U40_ggggga(x1, x2, x3, x4, x5, x6, x8)
appc44_in_aaaag(x1, x2, x3, x4, x5) = appc44_in_aaaag(x5)
s(x1, x2) = s(x1, x2)
appc44_out_aaaag(x1, x2, x3, x4, x5) = appc44_out_aaaag(x1, x2, x3, x4, x5)
U41_aaaag(x1, x2, x3, x4, x5, x6, x7) = U41_aaaag(x1, x6, x7)
appc54_in_gggga(x1, x2, x3, x4, x5) = appc54_in_gggga(x1, x2, x3, x4)
appc54_out_gggga(x1, x2, x3, x4, x5) = appc54_out_gggga(x1, x2, x3, x4, x5)
U42_gggga(x1, x2, x3, x4, x5, x6, x7) = U42_gggga(x1, x2, x3, x4, x5, x7)
appc67_in_aag(x1, x2, x3) = appc67_in_aag(x3)
appc67_out_aag(x1, x2, x3) = appc67_out_aag(x1, x2, x3)
U43_aag(x1, x2, x3, x4, x5) = U43_aag(x1, x4, x5)
appc77_in_gga(x1, x2, x3) = appc77_in_gga(x1, x2)
appc77_out_gga(x1, x2, x3) = appc77_out_gga(x1, x2, x3)
U44_gga(x1, x2, x3, x4, x5) = U44_gga(x1, x2, x3, x5)
PARSE10_IN_GA(x1, x2) = PARSE10_IN_GA(x1)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
P22_IN_GGGGGAA(x1, x2, x3, x4, x5, x6, x7) = P22_IN_GGGGGAA(x1, x2, x3, x4, x5)
U13_GGGGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U13_GGGGGAA(x1, x2, x3, x4, x5, x8)
P43_IN_AAAAGAA(x1, x2, x3, x4, x5, x6, x7) = P43_IN_AAAAGAA(x5)
U18_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U18_AAAAGAA(x5, x8)
U19_AAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U19_AAAAGAA(x1, x2, x3, x4, x5, x8)
P66_IN_AAGAA(x1, x2, x3, x4, x5) = P66_IN_AAGAA(x3)
U24_AAGAA(x1, x2, x3, x4, x5, x6) = U24_AAGAA(x3, x6)
U25_AAGAA(x1, x2, x3, x4, x5, x6) = U25_AAGAA(x1, x2, x3, x6)

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

(52) PiDPToQDPProof (SOUND transformation)

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

(53) Obligation:

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

PARSE10_IN_GA(T30) → U3_GA(T30, appc21_in_aaaaag(T30))
U3_GA(T30, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36)
P22_IN_GGGGGAA(T32, T33, T34, T35, T36) → U13_GGGGGAA(T32, T33, T34, T35, T36, appc31_in_ggggga(T32, T33, T34, T35, T36))
U13_GGGGGAA(T32, T33, T34, T35, T36, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50)
PARSE10_IN_GA(T127) → P43_IN_AAAAGAA(T127)
P43_IN_AAAAGAA(T127) → U18_AAAAGAA(T127, appc44_in_aaaag(T127))
U18_AAAAGAA(T127, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, appc54_in_gggga(T129, T130, T131, T132))
U19_AAAAGAA(T129, T130, T131, T132, T127, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144)
PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc21_in_aaaaag(cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, T41)) → U35_aaaaag(X211, T41, appc21_in_aaaaag(T41))
appc31_in_ggggga(nil, T76, T77, T78, T79) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99) → U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_in_ggggga(T98, T100, T101, T102, T99))
appc44_in_aaaag(cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, T137)) → U41_aaaag(X370, T137, appc44_in_aaaag(T137))
appc54_in_gggga(nil, T164, T165, T166) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183) → U42_gggga(T177, T182, T184, T185, T183, appc54_in_gggga(T182, T184, T185, T183))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U35_aaaaag(X211, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The set Q consists of the following terms:

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

P22_IN_GGGGGAA(T32, T33, T34, T35, T36) → U13_GGGGGAA(T32, T33, T34, T35, T36, appc31_in_ggggga(T32, T33, T34, T35, T36))
U18_AAAAGAA(T127, appc44_out_aaaag(T129, T130, T131, T132, T127)) → U19_AAAAGAA(T129, T130, T131, T132, T127, appc54_in_gggga(T129, T130, T131, T132))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(P22_IN_GGGGGAA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ + x₅
POL(P43_IN_AAAAGAA(x₁)) = x₁
POL(P66_IN_AAGAA(x₁)) = x₁
POL(PARSE10_IN_GA(x₁)) = x₁
POL(U13_GGGGGAA(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆
POL(U18_AAAAGAA(x₁, x₂)) = x₂
POL(U19_AAAAGAA(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆
POL(U24_AAGAA(x₁, x₂)) = x₂
POL(U25_AAGAA(x₁, x₂, x₃, x₄)) = x₄
POL(U35_aaaaag(x₁, x₂, x₃)) = 1 + x₃
POL(U3_GA(x₁, x₂)) = x₂
POL(U40_ggggga(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 1 + x₇
POL(U41_aaaag(x₁, x₂, x₃)) = 1 + x₃
POL(U42_gggga(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₆
POL(U43_aag(x₁, x₂, x₃)) = 1 + x₃
POL(U44_gga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(a) = 0
POL(appc21_in_aaaaag(x₁)) = x₁
POL(appc21_out_aaaaag(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₁ + x₅
POL(appc31_in_ggggga(x₁, x₂, x₃, x₄, x₅)) = x₁ + x₅
POL(appc31_out_ggggga(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆
POL(appc44_in_aaaag(x₁)) = x₁
POL(appc44_out_aaaag(x₁, x₂, x₃, x₄, x₅)) = 1 + x₁ + x₄
POL(appc54_in_gggga(x₁, x₂, x₃, x₄)) = x₁ + x₄
POL(appc54_out_gggga(x₁, x₂, x₃, x₄, x₅)) = x₅
POL(appc67_in_aag(x₁)) = x₁
POL(appc67_out_aag(x₁, x₂, x₃)) = x₁ + x₂
POL(appc77_in_gga(x₁, x₂)) = x₁ + x₂
POL(appc77_out_gga(x₁, x₂, x₃)) = x₃
POL(b) = 0
POL(cons(x₁, x₂)) = 1 + x₂
POL(nil) = 1
POL(s(x₁, x₂)) = 0
POL(s(x₁, x₂, x₃)) = 0

The following usable rules [FROCOS05] were oriented:

appc21_in_aaaaag(cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, T41)) → U35_aaaaag(X211, T41, appc21_in_aaaaag(T41))
appc31_in_ggggga(nil, T76, T77, T78, T79) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99) → U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_in_ggggga(T98, T100, T101, T102, T99))
appc44_in_aaaag(cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, T137)) → U41_aaaag(X370, T137, appc44_in_aaaag(T137))
appc54_in_gggga(nil, T164, T165, T166) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183) → U42_gggga(T177, T182, T184, T185, T183, appc54_in_gggga(T182, T184, T185, T183))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U35_aaaaag(X211, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

(55) Obligation:

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

PARSE10_IN_GA(T30) → U3_GA(T30, appc21_in_aaaaag(T30))
U3_GA(T30, appc21_out_aaaaag(T32, T33, T34, T35, T36, T30)) → P22_IN_GGGGGAA(T32, T33, T34, T35, T36)
U13_GGGGGAA(T32, T33, T34, T35, T36, appc31_out_ggggga(T32, T33, T34, T35, T36, T50)) → PARSE10_IN_GA(T50)
PARSE10_IN_GA(T127) → P43_IN_AAAAGAA(T127)
P43_IN_AAAAGAA(T127) → U18_AAAAGAA(T127, appc44_in_aaaag(T127))
U19_AAAAGAA(T129, T130, T131, T132, T127, appc54_out_gggga(T129, T130, T131, T132, T144)) → PARSE10_IN_GA(T144)
PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc21_in_aaaaag(cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, T41)) → U35_aaaaag(X211, T41, appc21_in_aaaaag(T41))
appc31_in_ggggga(nil, T76, T77, T78, T79) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99) → U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_in_ggggga(T98, T100, T101, T102, T99))
appc44_in_aaaag(cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, T137)) → U41_aaaag(X370, T137, appc44_in_aaaag(T137))
appc54_in_gggga(nil, T164, T165, T166) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183) → U42_gggga(T177, T182, T184, T185, T183, appc54_in_gggga(T182, T184, T185, T183))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U35_aaaaag(X211, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The set Q consists of the following terms:

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(56) DependencyGraphProof (EQUIVALENT transformation)

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

(57) Obligation:

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

PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc21_in_aaaaag(cons(a, cons(s(X182, X183, X184), cons(b, X185)))) → appc21_out_aaaaag(nil, X182, X183, X184, X185, cons(a, cons(s(X182, X183, X184), cons(b, X185))))
appc21_in_aaaaag(cons(X211, T41)) → U35_aaaaag(X211, T41, appc21_in_aaaaag(T41))
appc31_in_ggggga(nil, T76, T77, T78, T79) → appc31_out_ggggga(nil, T76, T77, T78, T79, cons(s(a, s(T76, T77, T78), b), T79))
appc31_in_ggggga(cons(T92, T98), T100, T101, T102, T99) → U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_in_ggggga(T98, T100, T101, T102, T99))
appc44_in_aaaag(cons(a, cons(s(X344, X345), cons(b, X346)))) → appc44_out_aaaag(nil, X344, X345, X346, cons(a, cons(s(X344, X345), cons(b, X346))))
appc44_in_aaaag(cons(X370, T137)) → U41_aaaag(X370, T137, appc44_in_aaaag(T137))
appc54_in_gggga(nil, T164, T165, T166) → appc54_out_gggga(nil, T164, T165, T166, cons(s(a, s(T164, T165), b), T166))
appc54_in_gggga(cons(T177, T182), T184, T185, T183) → U42_gggga(T177, T182, T184, T185, T183, appc54_in_gggga(T182, T184, T185, T183))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U35_aaaaag(X211, T41, appc21_out_aaaaag(X212, X213, X214, X215, X216, T41)) → appc21_out_aaaaag(cons(X211, X212), X213, X214, X215, X216, cons(X211, T41))
U40_ggggga(T92, T98, T100, T101, T102, T99, appc31_out_ggggga(T98, T100, T101, T102, T99, X255)) → appc31_out_ggggga(cons(T92, T98), T100, T101, T102, T99, cons(T92, X255))
U41_aaaag(X370, T137, appc44_out_aaaag(X371, X372, X373, X374, T137)) → appc44_out_aaaag(cons(X370, X371), X372, X373, X374, cons(X370, T137))
U42_gggga(T177, T182, T184, T185, T183, appc54_out_gggga(T182, T184, T185, T183, X411)) → appc54_out_gggga(cons(T177, T182), T184, T185, T183, cons(T177, X411))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))

The set Q consists of the following terms:

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(58) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(59) Obligation:

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

PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))

The set Q consists of the following terms:

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(60) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

appc21_in_aaaaag(x0)
appc31_in_ggggga(x0, x1, x2, x3, x4)
appc44_in_aaaag(x0)
appc54_in_gggga(x0, x1, x2, x3)
U35_aaaaag(x0, x1, x2)
U40_ggggga(x0, x1, x2, x3, x4, x5, x6)
U41_aaaag(x0, x1, x2)
U42_gggga(x0, x1, x2, x3, x4, x5)

(61) Obligation:

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

PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))

The set Q consists of the following terms:

appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(62) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

U24_AAGAA(T208, appc67_out_aag(T210, T211, T208)) → U25_AAGAA(T210, T211, T208, appc77_in_gga(T210, T211))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(P66_IN_AAGAA(x₁)) = x₁
POL(PARSE10_IN_GA(x₁)) = x₁
POL(U24_AAGAA(x₁, x₂)) = x₂
POL(U25_AAGAA(x₁, x₂, x₃, x₄)) = x₄
POL(U43_aag(x₁, x₂, x₃)) = 1 + x₃
POL(U44_gga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(a) = 0
POL(appc67_in_aag(x₁)) = x₁
POL(appc67_out_aag(x₁, x₂, x₃)) = 1 + x₁ + x₂
POL(appc77_in_gga(x₁, x₂)) = x₁ + x₂
POL(appc77_out_gga(x₁, x₂, x₃)) = x₃
POL(b) = 0
POL(cons(x₁, x₂)) = 1 + x₂
POL(nil) = 1
POL(s(x₁, x₂)) = 0

The following usable rules [FROCOS05] were oriented:

appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))

(63) Obligation:

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

PARSE10_IN_GA(T208) → P66_IN_AAGAA(T208)
P66_IN_AAGAA(T208) → U24_AAGAA(T208, appc67_in_aag(T208))
U25_AAGAA(T210, T211, T208, appc77_out_gga(T210, T211, T219)) → PARSE10_IN_GA(T219)

The TRS R consists of the following rules:

appc77_in_gga(nil, T227) → appc77_out_gga(nil, T227, cons(s(a, b), T227))
appc77_in_gga(cons(T234, T237), T238) → U44_gga(T234, T237, T238, appc77_in_gga(T237, T238))
U44_gga(T234, T237, T238, appc77_out_gga(T237, T238, X525)) → appc77_out_gga(cons(T234, T237), T238, cons(T234, X525))
appc67_in_aag(cons(a, cons(b, X470))) → appc67_out_aag(nil, X470, cons(a, cons(b, X470)))
appc67_in_aag(cons(X490, T216)) → U43_aag(X490, T216, appc67_in_aag(T216))
U43_aag(X490, T216, appc67_out_aag(X491, X492, T216)) → appc67_out_aag(cons(X490, X491), X492, cons(X490, T216))

The set Q consists of the following terms:

appc67_in_aag(x0)
appc77_in_gga(x0, x1)
U43_aag(x0, x1, x2)
U44_gga(x0, x1, x2, x3)

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

(64) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES

(42) Obligation:

(43) UsableRulesProof (EQUIVALENT transformation)

(44) Obligation:

(45) PiDPToQDPProof (SOUND transformation)

(46) Obligation:

(47) QDPSizeChangeProof (EQUIVALENT transformation)

(48) YES

(49) Obligation:

(50) UsableRulesProof (EQUIVALENT transformation)

(51) Obligation:

(52) PiDPToQDPProof (SOUND transformation)

(53) Obligation:

(54) QDPOrderProof (EQUIVALENT transformation)

(55) Obligation:

(56) DependencyGraphProof (EQUIVALENT transformation)

(57) Obligation:

(58) UsableRulesProof (EQUIVALENT transformation)

(59) Obligation:

(60) QReductionProof (EQUIVALENT transformation)

(61) Obligation:

(62) QDPOrderProof (EQUIVALENT transformation)

(63) Obligation:

(64) DependencyGraphProof (EQUIVALENT transformation)

(65) TRUE