Left Termination proof of /tmp/tmpkNVqDw/btapplast.pl

Left Termination of the query pattern goal_in_3(g, a, 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

(0) Obligation:

Clauses:

goal(A, B, C) :- ','(s2t(A, T), tapplast(T, B, C)).
tapplast(L, X, Last) :- ','(tappend(L, node(nil, X, nil), LX), tlast(Last, LX)).
tlast(X, node(nil, X, nil)).
tlast(X, node(L, H, R)) :- tlast(X, L).
tlast(X, node(L, H, R)) :- tlast(X, R).
tappend(nil, T, T).
tappend(node(nil, X, T2), T1, node(T1, X, T2)).
tappend(node(T1, X, nil), T2, node(T1, X, T2)).
tappend(node(T1, X, T2), T3, node(U, X, T2)) :- tappend(T1, T3, U).
tappend(node(T1, X, T2), T3, node(T1, X, U)) :- tappend(T2, T3, U).
s2t(s(X), node(T, Y, T)) :- s2t(X, T).
s2t(s(X), node(nil, Y, T)) :- s2t(X, T).
s2t(s(X), node(T, Y, nil)) :- s2t(X, T).
s2t(s(X), node(nil, Y, nil)).
s2t(0, nil).

Queries:

goal(g,a,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: goal(T4, T5, T6)\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: goal(T4, T5, T6), SCOPE: 1, CLAUSE: 0\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(s2t(T10, X7), tapplast(X7, T13, T14))\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 10 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 11 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 12 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 10\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 11 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 12 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(s2t(T19, X31), tapplast(node(X31, X32, X31), T13, T14))\n\nT19 is ground\nX31 is free; \nX32 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: s2t(T19, X31)\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: tapplast(node(T21, X32, T21), T13, T14)\n\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: s2t(T19, X31), SCOPE: 3, CLAUSE: 10 | s2t(T19, X31), SCOPE: 3, CLAUSE: 11 | s2t(T19, X31), SCOPE: 3, CLAUSE: 12 | s2t(T19, X31), SCOPE: 3, CLAUSE: 13 | s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: s2t(T19, X31), SCOPE: 3, CLAUSE: 10\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: s2t(T19, X31), SCOPE: 3, CLAUSE: 11 | s2t(T19, X31), SCOPE: 3, CLAUSE: 12 | s2t(T19, X31), SCOPE: 3, CLAUSE: 13 | s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: s2t(T27, X69)\n\nT27 is ground\nX69 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: s2t(T19, X31), SCOPE: 3, CLAUSE: 11\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: s2t(T19, X31), SCOPE: 3, CLAUSE: 12 | s2t(T19, X31), SCOPE: 3, CLAUSE: 13 | s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: s2t(T33, X103)\n\nT33 is ground\nX103 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: s2t(T19, X31), SCOPE: 3, CLAUSE: 12\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: s2t(T19, X31), SCOPE: 3, CLAUSE: 13 | s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: s2t(T39, X135)\n\nT39 is ground\nX135 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: s2t(T19, X31), SCOPE: 3, CLAUSE: 13\n\nT19 is ground\nX31 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: s2t(T19, X31), SCOPE: 3, CLAUSE: 14\n\nT19 is ground\nX31 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: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: tapplast(node(T21, X32, T21), T13, T14), SCOPE: 4, CLAUSE: 1\n\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(tappend(node(T63, X190, T63), node(nil, T64, nil), X189), tlast(T65, X189))\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: tappend(node(T63, X190, T63), node(nil, T64, nil), X189)\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: tlast(T70, T69)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 5 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 6 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 7 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 8 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 9\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 6 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 7 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 8 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 9\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 6\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 7 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 8 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 9\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 7\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 8 | tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 9\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 8\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: tappend(node(T63, X190, T63), node(nil, T64, nil), X189), SCOPE: 5, CLAUSE: 9\n\nX190 is free\nX189 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: tappend(T106, node(nil, T107, nil), X296)\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 5 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 6 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 7 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 8 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 9\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 5\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 6 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 7 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 8 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 9\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 6\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 7 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 8 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 9\n\nX296 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: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 7\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 8 | tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 9\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 8\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: tappend(T106, node(nil, T107, nil), X296), SCOPE: 6, CLAUSE: 9\n\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: tappend(T165, node(nil, T166, nil), X370)\n\nX370 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: tappend(T181, node(nil, T182, nil), X395)\n\nX395 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: tappend(T195, node(nil, T196, nil), X425)\n\nX425 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: tlast(T70, T69), SCOPE: 7, CLAUSE: 2 | tlast(T70, T69), SCOPE: 7, CLAUSE: 3 | tlast(T70, T69), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: tlast(T70, T69), SCOPE: 7, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: tlast(T70, T69), SCOPE: 7, CLAUSE: 3 | tlast(T70, T69), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: tlast(T70, T69), SCOPE: 7, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: tlast(T70, T69), SCOPE: 7, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: tlast(T226, T227)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: tlast(T242, T243)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 11\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 12 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(s2t(T250, X504), tapplast(node(nil, X503, X504), T13, T14))\n\nT250 is ground\nX503 is free; \nX504 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: s2t(T250, X504)\n\nT250 is ground\nX504 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: tapplast(node(nil, X503, T252), T13, T14)\n\nX503 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: tapplast(node(nil, X503, T252), T13, T14), SCOPE: 8, CLAUSE: 1\n\nX503 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(tappend(node(nil, X543, T272), node(nil, T273, nil), X542), tlast(T274, X542))\n\nX543 is free\nX542 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: tappend(node(nil, X543, T272), node(nil, T273, nil), X542)\n\nX543 is free\nX542 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: tlast(T280, T279)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 12\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13 | ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(s2t(T289, X582), tapplast(node(X582, X583, nil), T13, T14))\n\nT289 is ground\nX582 is free; \nX583 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: s2t(T289, X582)\n\nT289 is ground\nX582 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: tapplast(node(T291, X583, nil), T13, T14)\n\nX583 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: tapplast(node(T291, X583, nil), T13, T14), SCOPE: 9, CLAUSE: 1\n\nX583 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(tappend(node(T310, X625, nil), node(nil, T311, nil), X624), tlast(T312, X624))\n\nX625 is free\nX624 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: tappend(node(T310, X625, nil), node(nil, T311, nil), X624)\n\nX625 is free\nX624 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: tlast(T317, T316)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 13\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(s2t(T10, X7), tapplast(X7, T13, T14)), SCOPE: 2, CLAUSE: 14\n\nT10 is ground\nX7 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: tapplast(node(nil, X662, nil), T13, T14)\n\nX662 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: tapplast(node(nil, X662, nil), T13, T14), SCOPE: 10, CLAUSE: 1\n\nX662 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(tappend(node(nil, X690, nil), node(nil, T339, nil), X689), tlast(T340, X689))\n\nX690 is free\nX689 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: tapplast(nil, T13, T14)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: tapplast(nil, T13, T14), SCOPE: 11, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(tappend(nil, node(nil, T355, nil), X714), tlast(T356, X714))\n\nX714 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: tappend(nil, node(nil, T355, nil), X714)\n\nX714 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: tlast(T360, T359)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 118 [arrowhead = none ];
118 -> 2;

119 [label="ONLY EVAL with clause\ngoal(X4, X5, X6) :- ','(s2t(X4, X7), tapplast(X7, X5, X6)).\nand substitution\nT4 -> T10\nX4 -> T10\nT5 -> T13\nX5 -> T13\nT6 -> T14\nX6 -> T14\nT11 -> T13\nT12 -> T14", fontsize=14, style = filled, fillcolor = white];
2 -> 119 [arrowhead = none ];
119 -> 3;

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

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

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

123 [label="EVAL with clause\ns2t(s(X28), node(X29, X30, X29)) :- s2t(X28, X29).\nand substitution\nX28 -> T19\nT10 -> s(T19)\nX29 -> X31\nX30 -> X32\nX7 -> node(X31, X32, X31)", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 123 [arrowhead = none ];
123 -> 7;

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

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

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

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

128 [label="SPLIT 2\nreplacements:\nX31 -> T21", fontsize=14, style = filled, fillcolor = violet];
7 -> 128 [arrowhead = none ];
128 -> 10;

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

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

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

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

133 [label="EVAL with clause\ns2t(s(X66), node(X67, X68, X67)) :- s2t(X66, X67).\nand substitution\nX66 -> T27\nT19 -> s(T27)\nX67 -> X69\nX68 -> X70\nX31 -> node(X69, X70, X69)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 133 [arrowhead = none ];
133 -> 14;

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

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

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

137 [label="INSTANCE with matching:\nT19 -> T27\nX31 -> X69", fontsize=14, style = filled, fillcolor = lightgrey];
14 -> 137 [arrowhead = none , style=dashed];
137 -> 9[style=dashed];

138 [label="EVAL with clause\ns2t(s(X99), node(nil, X100, X101)) :- s2t(X99, X101).\nand substitution\nX99 -> T33\nT19 -> s(T33)\nX100 -> X102\nX101 -> X103\nX31 -> node(nil, X102, X103)", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 138 [arrowhead = none ];
138 -> 18;

139 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 139 [arrowhead = none ];
139 -> 19;

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

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

142 [label="INSTANCE with matching:\nT19 -> T33\nX31 -> X103", fontsize=14, style = filled, fillcolor = lightgrey];
18 -> 142 [arrowhead = none , style=dashed];
142 -> 9[style=dashed];

143 [label="EVAL with clause\ns2t(s(X132), node(X133, X134, nil)) :- s2t(X132, X133).\nand substitution\nX132 -> T39\nT19 -> s(T39)\nX133 -> X135\nX134 -> X136\nX31 -> node(X135, X136, nil)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 143 [arrowhead = none ];
143 -> 22;

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

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

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

147 [label="INSTANCE with matching:\nT19 -> T39\nX31 -> X135", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 147 [arrowhead = none , style=dashed];
147 -> 9[style=dashed];

148 [label="EVAL with clause\ns2t(s(X157), node(nil, X158, nil)).\nand substitution\nX157 -> T45\nT19 -> s(T45)\nX158 -> X159\nX31 -> node(nil, X159, nil)", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 148 [arrowhead = none ];
148 -> 26;

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

150 [label="EVAL with clause\ns2t(0, nil).\nand substitution\nT19 -> 0\nX31 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 150 [arrowhead = none ];
150 -> 29;

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

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

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

154 [label="ONLY EVAL with clause\ntapplast(X186, X187, X188) :- ','(tappend(X186, node(nil, X187, nil), X189), tlast(X188, X189)).\nand substitution\nT21 -> T63\nX32 -> X190\nX186 -> node(T63, X190, T63)\nT13 -> T64\nX187 -> T64\nT14 -> T65\nX188 -> T65\nT60 -> T63\nT61 -> T64\nT62 -> T65", fontsize=14, style = filled, fillcolor = white];
32 -> 154 [arrowhead = none ];
154 -> 33;

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

156 [label="SPLIT 2\nreplacements:\nX190 -> T68\nX189 -> T69\nT65 -> T70", fontsize=14, style = filled, fillcolor = violet];
33 -> 156 [arrowhead = none ];
156 -> 35;

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

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

159 [label="BACKTRACK\nfor clause: tappend(nil, T, T)because of non-unification", fontsize=14, style = filled, fillcolor = white];
36 -> 159 [arrowhead = none ];
159 -> 37;

160 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 160 [arrowhead = none ];
160 -> 38;

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

162 [label="EVAL with clause\ntappend(node(nil, X228, X229), X230, node(X230, X228, X229)).\nand substitution\nT63 -> nil\nX190 -> X231\nX228 -> X231\nX229 -> nil\nT64 -> T77\nX230 -> node(nil, T77, nil)\nX189 -> node(node(nil, T77, nil), X231, nil)", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 162 [arrowhead = none ];
162 -> 40;

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

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

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

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

167 [label="EVAL with clause\ntappend(node(X251, X252, nil), X253, node(X251, X252, X253)).\nand substitution\nT63 -> nil\nX251 -> nil\nX190 -> X254\nX252 -> X254\nT86 -> nil\nT64 -> T87\nX253 -> node(nil, T87, nil)\nX189 -> node(nil, X254, node(nil, T87, nil))", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 167 [arrowhead = none ];
167 -> 45;

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

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

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

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

172 [label="ONLY EVAL with clause\ntappend(node(X290, X291, X292), X293, node(X294, X291, X292)) :- tappend(X290, X293, X294).\nand substitution\nT63 -> T106\nX290 -> T106\nX190 -> X295\nX291 -> X295\nX292 -> T106\nT64 -> T107\nX293 -> node(nil, T107, nil)\nX294 -> X296\nX189 -> node(X296, X295, T106)\nT104 -> T106\nT105 -> T107", fontsize=14, style = filled, fillcolor = white];
48 -> 172 [arrowhead = none ];
172 -> 50;

173 [label="ONLY EVAL with clause\ntappend(node(X419, X420, X421), X422, node(X419, X420, X423)) :- tappend(X421, X422, X423).\nand substitution\nT63 -> T195\nX419 -> T195\nX190 -> X424\nX420 -> X424\nX421 -> T195\nT64 -> T196\nX422 -> node(nil, T196, nil)\nX423 -> X425\nX189 -> node(T195, X424, X425)\nT193 -> T195\nT194 -> T196", fontsize=14, style = filled, fillcolor = white];
49 -> 173 [arrowhead = none ];
173 -> 73;

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

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

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

177 [label="EVAL with clause\ntappend(nil, X303, X303).\nand substitution\nT106 -> nil\nT107 -> T114\nX303 -> node(nil, T114, nil)\nX296 -> node(nil, T114, nil)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 177 [arrowhead = none ];
177 -> 54;

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

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

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

181 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 181 [arrowhead = none ];
181 -> 56;

182 [label="EVAL with clause\ntappend(node(nil, X317, X318), X319, node(X319, X317, X318)).\nand substitution\nX317 -> T127\nX318 -> T128\nT106 -> node(nil, T127, T128)\nT107 -> T129\nX319 -> node(nil, T129, nil)\nX296 -> node(node(nil, T129, nil), T127, T128)", 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="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 184 [arrowhead = none ];
184 -> 62;

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

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

187 [label="EVAL with clause\ntappend(node(X335, X336, nil), X337, node(X335, X336, X337)).\nand substitution\nX335 -> T142\nX336 -> T143\nT106 -> node(T142, T143, nil)\nT107 -> T144\nX337 -> node(nil, T144, nil)\nX296 -> node(T142, T143, node(nil, T144, nil))", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 187 [arrowhead = none ];
187 -> 64;

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

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

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

191 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 191 [arrowhead = none ];
191 -> 66;

192 [label="EVAL with clause\ntappend(node(X365, X366, X367), X368, node(X369, X366, X367)) :- tappend(X365, X368, X369).\nand substitution\nX365 -> T165\nX366 -> T162\nX367 -> T163\nT106 -> node(T165, T162, T163)\nT107 -> T166\nX368 -> node(nil, T166, nil)\nX369 -> X370\nX296 -> node(X370, T162, T163)\nT161 -> T165\nT164 -> T166", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 192 [arrowhead = none ];
192 -> 69;

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

194 [label="EVAL with clause\ntappend(node(X390, X391, X392), X393, node(X390, X391, X394)) :- tappend(X392, X393, X394).\nand substitution\nX390 -> T177\nX391 -> T178\nX392 -> T181\nT106 -> node(T177, T178, T181)\nT107 -> T182\nX393 -> node(nil, T182, nil)\nX394 -> X395\nX296 -> node(T177, T178, X395)\nT179 -> T181\nT180 -> T182", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 194 [arrowhead = none ];
194 -> 71;

195 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 195 [arrowhead = none ];
195 -> 72;

196 [label="INSTANCE with matching:\nT106 -> T165\nT107 -> T166\nX296 -> X370", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 196 [arrowhead = none , style=dashed];
196 -> 50[style=dashed];

197 [label="INSTANCE with matching:\nT106 -> T181\nT107 -> T182\nX296 -> X395", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 197 [arrowhead = none , style=dashed];
197 -> 50[style=dashed];

198 [label="INSTANCE with matching:\nT106 -> T195\nT107 -> T196\nX296 -> X425", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 198 [arrowhead = none , style=dashed];
198 -> 50[style=dashed];

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

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

201 [label="EVAL with clause\ntlast(X434, node(nil, X434, nil)).\nand substitution\nT70 -> T205\nX434 -> T205\nT69 -> node(nil, T205, nil)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 201 [arrowhead = none ];
201 -> 77;

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

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

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

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

206 [label="EVAL with clause\ntlast(X452, node(X453, X454, X455)) :- tlast(X452, X453).\nand substitution\nT70 -> T226\nX452 -> T226\nX453 -> T227\nX454 -> T224\nX455 -> T225\nT69 -> node(T227, T224, T225)\nT222 -> T226\nT223 -> T227", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 206 [arrowhead = none ];
206 -> 82;

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

208 [label="EVAL with clause\ntlast(X470, node(X471, X472, X473)) :- tlast(X470, X473).\nand substitution\nT70 -> T242\nX470 -> T242\nX471 -> T239\nX472 -> T240\nX473 -> T243\nT69 -> node(T239, T240, T243)\nT238 -> T242\nT241 -> T243", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 208 [arrowhead = none ];
208 -> 84;

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

210 [label="INSTANCE with matching:\nT70 -> T226\nT69 -> T227", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 210 [arrowhead = none , style=dashed];
210 -> 35[style=dashed];

211 [label="INSTANCE with matching:\nT70 -> T242\nT69 -> T243", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 211 [arrowhead = none , style=dashed];
211 -> 35[style=dashed];

212 [label="EVAL with clause\ns2t(s(X500), node(nil, X501, X502)) :- s2t(X500, X502).\nand substitution\nX500 -> T250\nT10 -> s(T250)\nX501 -> X503\nX502 -> X504\nX7 -> node(nil, X503, X504)", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 212 [arrowhead = none ];
212 -> 88;

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

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

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

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

217 [label="SPLIT 2\nreplacements:\nX504 -> T252", fontsize=14, style = filled, fillcolor = violet];
88 -> 217 [arrowhead = none ];
217 -> 91;

218 [label="INSTANCE with matching:\nT19 -> T250\nX31 -> X504", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 218 [arrowhead = none , style=dashed];
218 -> 9[style=dashed];

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

220 [label="ONLY EVAL with clause\ntapplast(X539, X540, X541) :- ','(tappend(X539, node(nil, X540, nil), X542), tlast(X541, X542)).\nand substitution\nX503 -> X543\nT252 -> T272\nX539 -> node(nil, X543, T272)\nT13 -> T273\nX540 -> T273\nT14 -> T274\nX541 -> T274\nT269 -> T272\nT270 -> T273\nT271 -> T274", fontsize=14, style = filled, fillcolor = white];
92 -> 220 [arrowhead = none ];
220 -> 93;

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

222 [label="SPLIT 2\nreplacements:\nX543 -> T278\nX542 -> T279\nT274 -> T280", fontsize=14, style = filled, fillcolor = violet];
93 -> 222 [arrowhead = none ];
222 -> 95;

223 [label="INSTANCE with matching:\nT106 -> node(nil, X543, T272)\nT107 -> T273\nX296 -> X542", fontsize=14, style = filled, fillcolor = lightgrey];
94 -> 223 [arrowhead = none , style=dashed];
223 -> 50[style=dashed];

224 [label="INSTANCE with matching:\nT70 -> T280\nT69 -> T279", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 224 [arrowhead = none , style=dashed];
224 -> 35[style=dashed];

225 [label="EVAL with clause\ns2t(s(X579), node(X580, X581, nil)) :- s2t(X579, X580).\nand substitution\nX579 -> T289\nT10 -> s(T289)\nX580 -> X582\nX581 -> X583\nX7 -> node(X582, X583, nil)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 225 [arrowhead = none ];
225 -> 98;

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

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

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

229 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
98 -> 229 [arrowhead = none ];
229 -> 100;

230 [label="SPLIT 2\nreplacements:\nX582 -> T291", fontsize=14, style = filled, fillcolor = violet];
98 -> 230 [arrowhead = none ];
230 -> 101;

231 [label="INSTANCE with matching:\nT19 -> T289\nX31 -> X582", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 231 [arrowhead = none , style=dashed];
231 -> 9[style=dashed];

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

233 [label="ONLY EVAL with clause\ntapplast(X621, X622, X623) :- ','(tappend(X621, node(nil, X622, nil), X624), tlast(X623, X624)).\nand substitution\nT291 -> T310\nX583 -> X625\nX621 -> node(T310, X625, nil)\nT13 -> T311\nX622 -> T311\nT14 -> T312\nX623 -> T312\nT307 -> T310\nT308 -> T311\nT309 -> T312", fontsize=14, style = filled, fillcolor = white];
102 -> 233 [arrowhead = none ];
233 -> 103;

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

235 [label="SPLIT 2\nreplacements:\nX625 -> T315\nX624 -> T316\nT312 -> T317", fontsize=14, style = filled, fillcolor = violet];
103 -> 235 [arrowhead = none ];
235 -> 105;

236 [label="INSTANCE with matching:\nT106 -> node(T310, X625, nil)\nT107 -> T311\nX296 -> X624", fontsize=14, style = filled, fillcolor = lightgrey];
104 -> 236 [arrowhead = none , style=dashed];
236 -> 50[style=dashed];

237 [label="INSTANCE with matching:\nT70 -> T317\nT69 -> T316", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 237 [arrowhead = none , style=dashed];
237 -> 35[style=dashed];

238 [label="EVAL with clause\ns2t(s(X660), node(nil, X661, nil)).\nand substitution\nX660 -> T326\nT10 -> s(T326)\nX661 -> X662\nX7 -> node(nil, X662, nil)", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 238 [arrowhead = none ];
238 -> 108;

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

240 [label="EVAL with clause\ns2t(0, nil).\nand substitution\nT10 -> 0\nX7 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 240 [arrowhead = none ];
240 -> 112;

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

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

243 [label="ONLY EVAL with clause\ntapplast(X686, X687, X688) :- ','(tappend(X686, node(nil, X687, nil), X689), tlast(X688, X689)).\nand substitution\nX662 -> X690\nX686 -> node(nil, X690, nil)\nT13 -> T339\nX687 -> T339\nT14 -> T340\nX688 -> T340\nT337 -> T339\nT338 -> T340", fontsize=14, style = filled, fillcolor = white];
110 -> 243 [arrowhead = none ];
243 -> 111;

244 [label="INSTANCE with matching:\nT63 -> nil\nX190 -> X690\nT64 -> T339\nX189 -> X689\nT65 -> T340", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 244 [arrowhead = none , style=dashed];
244 -> 33[style=dashed];

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

246 [label="ONLY EVAL with clause\ntapplast(X711, X712, X713) :- ','(tappend(X711, node(nil, X712, nil), X714), tlast(X713, X714)).\nand substitution\nX711 -> nil\nT13 -> T355\nX712 -> T355\nT14 -> T356\nX713 -> T356\nT353 -> T355\nT354 -> T356", fontsize=14, style = filled, fillcolor = white];
114 -> 246 [arrowhead = none ];
246 -> 115;

247 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
115 -> 247 [arrowhead = none ];
247 -> 116;

248 [label="SPLIT 2\nreplacements:\nX714 -> T359\nT356 -> T360", fontsize=14, style = filled, fillcolor = violet];
115 -> 248 [arrowhead = none ];
248 -> 117;

249 [label="INSTANCE with matching:\nT106 -> nil\nT107 -> T355\nX296 -> X714", fontsize=14, style = filled, fillcolor = lightgrey];
116 -> 249 [arrowhead = none , style=dashed];
249 -> 50[style=dashed];

250 [label="INSTANCE with matching:\nT70 -> T360\nT69 -> T359", fontsize=14, style = filled, fillcolor = lightgrey];
117 -> 250 [arrowhead = none , style=dashed];
250 -> 35[style=dashed];

}

(2) Obligation:

Triples:

s2t9(s(T27), node(X69, X70, X69)) :- s2t9(T27, X69).
s2t9(s(T33), node(nil, X102, X103)) :- s2t9(T33, X103).
s2t9(s(T39), node(X135, X136, nil)) :- s2t9(T39, X135).
tappend50(node(T165, T162, T163), T166, node(X370, T162, T163)) :- tappend50(T165, T166, X370).
tappend50(node(T177, T178, T181), T182, node(T177, T178, X395)) :- tappend50(T181, T182, X395).
tlast35(T226, node(T227, T224, T225)) :- tlast35(T226, T227).
tlast35(T242, node(T239, T240, T243)) :- tlast35(T242, T243).
p33(T106, X295, T107, node(X296, X295, T106), T65) :- tappend50(T106, T107, X296).
p33(T195, X424, T196, node(T195, X424, X425), T65) :- tappend50(T195, T196, X425).
p33(T63, T68, T64, T69, T70) :- ','(tappendc34(T63, T68, T64, T69), tlast35(T70, T69)).
goal1(s(T19), T13, T14) :- s2t9(T19, X31).
goal1(s(T19), T64, T65) :- ','(s2tc9(T19, T63), p33(T63, X190, T64, X189, T65)).
goal1(s(T250), T13, T14) :- s2t9(T250, X504).
goal1(s(T250), T273, T274) :- ','(s2tc9(T250, T272), tappend50(node(nil, X543, T272), T273, X542)).
goal1(s(T250), T273, T280) :- ','(s2tc9(T250, T272), ','(tappendc50(node(nil, T278, T272), T273, T279), tlast35(T280, T279))).
goal1(s(T289), T13, T14) :- s2t9(T289, X582).
goal1(s(T289), T311, T312) :- ','(s2tc9(T289, T310), tappend50(node(T310, X625, nil), T311, X624)).
goal1(s(T289), T311, T317) :- ','(s2tc9(T289, T310), ','(tappendc50(node(T310, T315, nil), T311, T316), tlast35(T317, T316))).
goal1(s(T326), T339, T340) :- p33(nil, X690, T339, X689, T340).
goal1(0, T355, T356) :- tappend50(nil, T355, X714).
goal1(0, T355, T360) :- ','(tappendc50(nil, T355, T359), tlast35(T360, T359)).

Clauses:

s2tc9(s(T27), node(X69, X70, X69)) :- s2tc9(T27, X69).
s2tc9(s(T33), node(nil, X102, X103)) :- s2tc9(T33, X103).
s2tc9(s(T39), node(X135, X136, nil)) :- s2tc9(T39, X135).
s2tc9(s(T45), node(nil, X159, nil)).
s2tc9(0, nil).
tappendc50(nil, T114, node(nil, T114, nil)).
tappendc50(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128)).
tappendc50(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil))).
tappendc50(node(T165, T162, T163), T166, node(X370, T162, T163)) :- tappendc50(T165, T166, X370).
tappendc50(node(T177, T178, T181), T182, node(T177, T178, X395)) :- tappendc50(T181, T182, X395).
tlastc35(T205, node(nil, T205, nil)).
tlastc35(T226, node(T227, T224, T225)) :- tlastc35(T226, T227).
tlastc35(T242, node(T239, T240, T243)) :- tlastc35(T242, T243).
qc33(T63, T68, T64, T69, T70) :- ','(tappendc34(T63, T68, T64, T69), tlastc35(T70, T69)).
tappendc34(nil, X231, T77, node(node(nil, T77, nil), X231, nil)).
tappendc34(nil, X254, T87, node(nil, X254, node(nil, T87, nil))).
tappendc34(T106, X295, T107, node(X296, X295, T106)) :- tappendc50(T106, T107, X296).
tappendc34(T195, X424, T196, node(T195, X424, X425)) :- tappendc50(T195, T196, X425).

Afs:

goal1(x1, x2, x3) = goal1(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:
goal1_in: (b,f,f)
s2t9_in: (b,f)
s2tc9_in: (b,f)
p33_in: (b,f,f,f,f)
tappend50_in: (b,f,f)
tappendc34_in: (b,f,f,f)
tappendc50_in: (b,f,f)
tlast35_in: (f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOAL1_IN_GAA(s(T19), T13, T14) → U12_GAA(T19, T13, T14, s2t9_in_ga(T19, X31))
GOAL1_IN_GAA(s(T19), T13, T14) → S2T9_IN_GA(T19, X31)
S2T9_IN_GA(s(T27), node(X69, X70, X69)) → U1_GA(T27, X69, X70, s2t9_in_ga(T27, X69))
S2T9_IN_GA(s(T27), node(X69, X70, X69)) → S2T9_IN_GA(T27, X69)
S2T9_IN_GA(s(T33), node(nil, X102, X103)) → U2_GA(T33, X102, X103, s2t9_in_ga(T33, X103))
S2T9_IN_GA(s(T33), node(nil, X102, X103)) → S2T9_IN_GA(T33, X103)
S2T9_IN_GA(s(T39), node(X135, X136, nil)) → U3_GA(T39, X135, X136, s2t9_in_ga(T39, X135))
S2T9_IN_GA(s(T39), node(X135, X136, nil)) → S2T9_IN_GA(T39, X135)
GOAL1_IN_GAA(s(T19), T64, T65) → U13_GAA(T19, T64, T65, s2tc9_in_ga(T19, T63))
U13_GAA(T19, T64, T65, s2tc9_out_ga(T19, T63)) → U14_GAA(T19, T64, T65, p33_in_gaaaa(T63, X190, T64, X189, T65))
U13_GAA(T19, T64, T65, s2tc9_out_ga(T19, T63)) → P33_IN_GAAAA(T63, X190, T64, X189, T65)
P33_IN_GAAAA(T106, X295, T107, node(X296, X295, T106), T65) → U8_GAAAA(T106, X295, T107, X296, T65, tappend50_in_gaa(T106, T107, X296))
P33_IN_GAAAA(T106, X295, T107, node(X296, X295, T106), T65) → TAPPEND50_IN_GAA(T106, T107, X296)
TAPPEND50_IN_GAA(node(T165, T162, T163), T166, node(X370, T162, T163)) → U4_GAA(T165, T162, T163, T166, X370, tappend50_in_gaa(T165, T166, X370))
TAPPEND50_IN_GAA(node(T165, T162, T163), T166, node(X370, T162, T163)) → TAPPEND50_IN_GAA(T165, T166, X370)
TAPPEND50_IN_GAA(node(T177, T178, T181), T182, node(T177, T178, X395)) → U5_GAA(T177, T178, T181, T182, X395, tappend50_in_gaa(T181, T182, X395))
TAPPEND50_IN_GAA(node(T177, T178, T181), T182, node(T177, T178, X395)) → TAPPEND50_IN_GAA(T181, T182, X395)
P33_IN_GAAAA(T195, X424, T196, node(T195, X424, X425), T65) → U9_GAAAA(T195, X424, T196, X425, T65, tappend50_in_gaa(T195, T196, X425))
P33_IN_GAAAA(T195, X424, T196, node(T195, X424, X425), T65) → TAPPEND50_IN_GAA(T195, T196, X425)
P33_IN_GAAAA(T63, T68, T64, T69, T70) → U10_GAAAA(T63, T68, T64, T69, T70, tappendc34_in_gaaa(T63, T68, T64, T69))
U10_GAAAA(T63, T68, T64, T69, T70, tappendc34_out_gaaa(T63, T68, T64, T69)) → U11_GAAAA(T63, T68, T64, T69, T70, tlast35_in_ag(T70, T69))
U10_GAAAA(T63, T68, T64, T69, T70, tappendc34_out_gaaa(T63, T68, T64, T69)) → TLAST35_IN_AG(T70, T69)
TLAST35_IN_AG(T226, node(T227, T224, T225)) → U6_AG(T226, T227, T224, T225, tlast35_in_ag(T226, T227))
TLAST35_IN_AG(T226, node(T227, T224, T225)) → TLAST35_IN_AG(T226, T227)
TLAST35_IN_AG(T242, node(T239, T240, T243)) → U7_AG(T242, T239, T240, T243, tlast35_in_ag(T242, T243))
TLAST35_IN_AG(T242, node(T239, T240, T243)) → TLAST35_IN_AG(T242, T243)
GOAL1_IN_GAA(s(T250), T13, T14) → U15_GAA(T250, T13, T14, s2t9_in_ga(T250, X504))
GOAL1_IN_GAA(s(T250), T273, T274) → U16_GAA(T250, T273, T274, s2tc9_in_ga(T250, T272))
U16_GAA(T250, T273, T274, s2tc9_out_ga(T250, T272)) → U17_GAA(T250, T273, T274, tappend50_in_gaa(node(nil, X543, T272), T273, X542))
U16_GAA(T250, T273, T274, s2tc9_out_ga(T250, T272)) → TAPPEND50_IN_GAA(node(nil, X543, T272), T273, X542)
GOAL1_IN_GAA(s(T250), T273, T280) → U18_GAA(T250, T273, T280, s2tc9_in_ga(T250, T272))
U18_GAA(T250, T273, T280, s2tc9_out_ga(T250, T272)) → U19_GAA(T250, T273, T280, tappendc50_in_gaa(node(nil, T278, T272), T273, T279))
U19_GAA(T250, T273, T280, tappendc50_out_gaa(node(nil, T278, T272), T273, T279)) → U20_GAA(T250, T273, T280, tlast35_in_ag(T280, T279))
U19_GAA(T250, T273, T280, tappendc50_out_gaa(node(nil, T278, T272), T273, T279)) → TLAST35_IN_AG(T280, T279)
GOAL1_IN_GAA(s(T289), T13, T14) → U21_GAA(T289, T13, T14, s2t9_in_ga(T289, X582))
GOAL1_IN_GAA(s(T289), T311, T312) → U22_GAA(T289, T311, T312, s2tc9_in_ga(T289, T310))
U22_GAA(T289, T311, T312, s2tc9_out_ga(T289, T310)) → U23_GAA(T289, T311, T312, tappend50_in_gaa(node(T310, X625, nil), T311, X624))
U22_GAA(T289, T311, T312, s2tc9_out_ga(T289, T310)) → TAPPEND50_IN_GAA(node(T310, X625, nil), T311, X624)
GOAL1_IN_GAA(s(T289), T311, T317) → U24_GAA(T289, T311, T317, s2tc9_in_ga(T289, T310))
U24_GAA(T289, T311, T317, s2tc9_out_ga(T289, T310)) → U25_GAA(T289, T311, T317, tappendc50_in_gaa(node(T310, T315, nil), T311, T316))
U25_GAA(T289, T311, T317, tappendc50_out_gaa(node(T310, T315, nil), T311, T316)) → U26_GAA(T289, T311, T317, tlast35_in_ag(T317, T316))
U25_GAA(T289, T311, T317, tappendc50_out_gaa(node(T310, T315, nil), T311, T316)) → TLAST35_IN_AG(T317, T316)
GOAL1_IN_GAA(s(T326), T339, T340) → U27_GAA(T326, T339, T340, p33_in_gaaaa(nil, X690, T339, X689, T340))
GOAL1_IN_GAA(s(T326), T339, T340) → P33_IN_GAAAA(nil, X690, T339, X689, T340)
GOAL1_IN_GAA(0, T355, T356) → U28_GAA(T355, T356, tappend50_in_gaa(nil, T355, X714))
GOAL1_IN_GAA(0, T355, T356) → TAPPEND50_IN_GAA(nil, T355, X714)
GOAL1_IN_GAA(0, T355, T360) → U29_GAA(T355, T360, tappendc50_in_gaa(nil, T355, T359))
U29_GAA(T355, T360, tappendc50_out_gaa(nil, T355, T359)) → U30_GAA(T355, T360, tlast35_in_ag(T360, T359))
U29_GAA(T355, T360, tappendc50_out_gaa(nil, T355, T359)) → TLAST35_IN_AG(T360, T359)

The TRS R consists of the following rules:

s2tc9_in_ga(s(T27), node(X69, X70, X69)) → U32_ga(T27, X69, X70, s2tc9_in_ga(T27, X69))
s2tc9_in_ga(s(T33), node(nil, X102, X103)) → U33_ga(T33, X102, X103, s2tc9_in_ga(T33, X103))
s2tc9_in_ga(s(T39), node(X135, X136, nil)) → U34_ga(T39, X135, X136, s2tc9_in_ga(T39, X135))
s2tc9_in_ga(s(T45), node(nil, X159, nil)) → s2tc9_out_ga(s(T45), node(nil, X159, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U34_ga(T39, X135, X136, s2tc9_out_ga(T39, X135)) → s2tc9_out_ga(s(T39), node(X135, X136, nil))
U33_ga(T33, X102, X103, s2tc9_out_ga(T33, X103)) → s2tc9_out_ga(s(T33), node(nil, X102, X103))
U32_ga(T27, X69, X70, s2tc9_out_ga(T27, X69)) → s2tc9_out_ga(s(T27), node(X69, X70, X69))
tappendc34_in_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil)) → tappendc34_out_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil))
tappendc34_in_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil))) → tappendc34_out_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil)))
tappendc34_in_gaaa(T106, X295, T107, node(X296, X295, T106)) → U41_gaaa(T106, X295, T107, X296, tappendc50_in_gaa(T106, T107, X296))
tappendc50_in_gaa(nil, T114, node(nil, T114, nil)) → tappendc50_out_gaa(nil, T114, node(nil, T114, nil))
tappendc50_in_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128)) → tappendc50_out_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128))
tappendc50_in_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil))) → tappendc50_out_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil)))
tappendc50_in_gaa(node(T165, T162, T163), T166, node(X370, T162, T163)) → U35_gaa(T165, T162, T163, T166, X370, tappendc50_in_gaa(T165, T166, X370))
tappendc50_in_gaa(node(T177, T178, T181), T182, node(T177, T178, X395)) → U36_gaa(T177, T178, T181, T182, X395, tappendc50_in_gaa(T181, T182, X395))
U36_gaa(T177, T178, T181, T182, X395, tappendc50_out_gaa(T181, T182, X395)) → tappendc50_out_gaa(node(T177, T178, T181), T182, node(T177, T178, X395))
U35_gaa(T165, T162, T163, T166, X370, tappendc50_out_gaa(T165, T166, X370)) → tappendc50_out_gaa(node(T165, T162, T163), T166, node(X370, T162, T163))
U41_gaaa(T106, X295, T107, X296, tappendc50_out_gaa(T106, T107, X296)) → tappendc34_out_gaaa(T106, X295, T107, node(X296, X295, T106))
tappendc34_in_gaaa(T195, X424, T196, node(T195, X424, X425)) → U42_gaaa(T195, X424, T196, X425, tappendc50_in_gaa(T195, T196, X425))
U42_gaaa(T195, X424, T196, X425, tappendc50_out_gaa(T195, T196, X425)) → tappendc34_out_gaaa(T195, X424, T196, node(T195, X424, X425))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
s2t9_in_ga(x1, x2) = s2t9_in_ga(x1)
node(x1, x2, x3) = node(x1, x3)
s2tc9_in_ga(x1, x2) = s2tc9_in_ga(x1)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
U33_ga(x1, x2, x3, x4) = U33_ga(x1, x4)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x4)
s2tc9_out_ga(x1, x2) = s2tc9_out_ga(x1, x2)
0 = 0
p33_in_gaaaa(x1, x2, x3, x4, x5) = p33_in_gaaaa(x1)
tappend50_in_gaa(x1, x2, x3) = tappend50_in_gaa(x1)
tappendc34_in_gaaa(x1, x2, x3, x4) = tappendc34_in_gaaa(x1)
nil = nil
tappendc34_out_gaaa(x1, x2, x3, x4) = tappendc34_out_gaaa(x1, x4)
U41_gaaa(x1, x2, x3, x4, x5) = U41_gaaa(x1, x5)
tappendc50_in_gaa(x1, x2, x3) = tappendc50_in_gaa(x1)
tappendc50_out_gaa(x1, x2, x3) = tappendc50_out_gaa(x1, x3)
U35_gaa(x1, x2, x3, x4, x5, x6) = U35_gaa(x1, x3, x6)
U36_gaa(x1, x2, x3, x4, x5, x6) = U36_gaa(x1, x3, x6)
U42_gaaa(x1, x2, x3, x4, x5) = U42_gaaa(x1, x5)
tlast35_in_ag(x1, x2) = tlast35_in_ag(x2)
GOAL1_IN_GAA(x1, x2, x3) = GOAL1_IN_GAA(x1)
U12_GAA(x1, x2, x3, x4) = U12_GAA(x1, x4)
S2T9_IN_GA(x1, x2) = S2T9_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x1, x4)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x4)
U3_GA(x1, x2, x3, x4) = U3_GA(x1, x4)
U13_GAA(x1, x2, x3, x4) = U13_GAA(x1, x4)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x1, x4)
P33_IN_GAAAA(x1, x2, x3, x4, x5) = P33_IN_GAAAA(x1)
U8_GAAAA(x1, x2, x3, x4, x5, x6) = U8_GAAAA(x1, x6)
TAPPEND50_IN_GAA(x1, x2, x3) = TAPPEND50_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6) = U4_GAA(x1, x3, x6)
U5_GAA(x1, x2, x3, x4, x5, x6) = U5_GAA(x1, x3, x6)
U9_GAAAA(x1, x2, x3, x4, x5, x6) = U9_GAAAA(x1, x6)
U10_GAAAA(x1, x2, x3, x4, x5, x6) = U10_GAAAA(x1, x6)
U11_GAAAA(x1, x2, x3, x4, x5, x6) = U11_GAAAA(x1, x4, x6)
TLAST35_IN_AG(x1, x2) = TLAST35_IN_AG(x2)
U6_AG(x1, x2, x3, x4, x5) = U6_AG(x2, x4, x5)
U7_AG(x1, x2, x3, x4, x5) = U7_AG(x2, x4, x5)
U15_GAA(x1, x2, x3, x4) = U15_GAA(x1, x4)
U16_GAA(x1, x2, x3, x4) = U16_GAA(x1, x4)
U17_GAA(x1, x2, x3, x4) = U17_GAA(x1, x4)
U18_GAA(x1, x2, x3, x4) = U18_GAA(x1, x4)
U19_GAA(x1, x2, x3, x4) = U19_GAA(x1, x4)
U20_GAA(x1, x2, x3, x4) = U20_GAA(x1, x4)
U21_GAA(x1, x2, x3, x4) = U21_GAA(x1, x4)
U22_GAA(x1, x2, x3, x4) = U22_GAA(x1, x4)
U23_GAA(x1, x2, x3, x4) = U23_GAA(x1, x4)
U24_GAA(x1, x2, x3, x4) = U24_GAA(x1, x4)
U25_GAA(x1, x2, x3, x4) = U25_GAA(x1, x4)
U26_GAA(x1, x2, x3, x4) = U26_GAA(x1, x4)
U27_GAA(x1, x2, x3, x4) = U27_GAA(x1, x4)
U28_GAA(x1, x2, x3) = U28_GAA(x3)
U29_GAA(x1, x2, x3) = U29_GAA(x3)
U30_GAA(x1, x2, x3) = U30_GAA(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:

GOAL1_IN_GAA(s(T19), T13, T14) → U12_GAA(T19, T13, T14, s2t9_in_ga(T19, X31))
GOAL1_IN_GAA(s(T19), T13, T14) → S2T9_IN_GA(T19, X31)
S2T9_IN_GA(s(T27), node(X69, X70, X69)) → U1_GA(T27, X69, X70, s2t9_in_ga(T27, X69))
S2T9_IN_GA(s(T27), node(X69, X70, X69)) → S2T9_IN_GA(T27, X69)
S2T9_IN_GA(s(T33), node(nil, X102, X103)) → U2_GA(T33, X102, X103, s2t9_in_ga(T33, X103))
S2T9_IN_GA(s(T33), node(nil, X102, X103)) → S2T9_IN_GA(T33, X103)
S2T9_IN_GA(s(T39), node(X135, X136, nil)) → U3_GA(T39, X135, X136, s2t9_in_ga(T39, X135))
S2T9_IN_GA(s(T39), node(X135, X136, nil)) → S2T9_IN_GA(T39, X135)
GOAL1_IN_GAA(s(T19), T64, T65) → U13_GAA(T19, T64, T65, s2tc9_in_ga(T19, T63))
U13_GAA(T19, T64, T65, s2tc9_out_ga(T19, T63)) → U14_GAA(T19, T64, T65, p33_in_gaaaa(T63, X190, T64, X189, T65))
U13_GAA(T19, T64, T65, s2tc9_out_ga(T19, T63)) → P33_IN_GAAAA(T63, X190, T64, X189, T65)
P33_IN_GAAAA(T106, X295, T107, node(X296, X295, T106), T65) → U8_GAAAA(T106, X295, T107, X296, T65, tappend50_in_gaa(T106, T107, X296))
P33_IN_GAAAA(T106, X295, T107, node(X296, X295, T106), T65) → TAPPEND50_IN_GAA(T106, T107, X296)
TAPPEND50_IN_GAA(node(T165, T162, T163), T166, node(X370, T162, T163)) → U4_GAA(T165, T162, T163, T166, X370, tappend50_in_gaa(T165, T166, X370))
TAPPEND50_IN_GAA(node(T165, T162, T163), T166, node(X370, T162, T163)) → TAPPEND50_IN_GAA(T165, T166, X370)
TAPPEND50_IN_GAA(node(T177, T178, T181), T182, node(T177, T178, X395)) → U5_GAA(T177, T178, T181, T182, X395, tappend50_in_gaa(T181, T182, X395))
TAPPEND50_IN_GAA(node(T177, T178, T181), T182, node(T177, T178, X395)) → TAPPEND50_IN_GAA(T181, T182, X395)
P33_IN_GAAAA(T195, X424, T196, node(T195, X424, X425), T65) → U9_GAAAA(T195, X424, T196, X425, T65, tappend50_in_gaa(T195, T196, X425))
P33_IN_GAAAA(T195, X424, T196, node(T195, X424, X425), T65) → TAPPEND50_IN_GAA(T195, T196, X425)
P33_IN_GAAAA(T63, T68, T64, T69, T70) → U10_GAAAA(T63, T68, T64, T69, T70, tappendc34_in_gaaa(T63, T68, T64, T69))
U10_GAAAA(T63, T68, T64, T69, T70, tappendc34_out_gaaa(T63, T68, T64, T69)) → U11_GAAAA(T63, T68, T64, T69, T70, tlast35_in_ag(T70, T69))
U10_GAAAA(T63, T68, T64, T69, T70, tappendc34_out_gaaa(T63, T68, T64, T69)) → TLAST35_IN_AG(T70, T69)
TLAST35_IN_AG(T226, node(T227, T224, T225)) → U6_AG(T226, T227, T224, T225, tlast35_in_ag(T226, T227))
TLAST35_IN_AG(T226, node(T227, T224, T225)) → TLAST35_IN_AG(T226, T227)
TLAST35_IN_AG(T242, node(T239, T240, T243)) → U7_AG(T242, T239, T240, T243, tlast35_in_ag(T242, T243))
TLAST35_IN_AG(T242, node(T239, T240, T243)) → TLAST35_IN_AG(T242, T243)
GOAL1_IN_GAA(s(T250), T13, T14) → U15_GAA(T250, T13, T14, s2t9_in_ga(T250, X504))
GOAL1_IN_GAA(s(T250), T273, T274) → U16_GAA(T250, T273, T274, s2tc9_in_ga(T250, T272))
U16_GAA(T250, T273, T274, s2tc9_out_ga(T250, T272)) → U17_GAA(T250, T273, T274, tappend50_in_gaa(node(nil, X543, T272), T273, X542))
U16_GAA(T250, T273, T274, s2tc9_out_ga(T250, T272)) → TAPPEND50_IN_GAA(node(nil, X543, T272), T273, X542)
GOAL1_IN_GAA(s(T250), T273, T280) → U18_GAA(T250, T273, T280, s2tc9_in_ga(T250, T272))
U18_GAA(T250, T273, T280, s2tc9_out_ga(T250, T272)) → U19_GAA(T250, T273, T280, tappendc50_in_gaa(node(nil, T278, T272), T273, T279))
U19_GAA(T250, T273, T280, tappendc50_out_gaa(node(nil, T278, T272), T273, T279)) → U20_GAA(T250, T273, T280, tlast35_in_ag(T280, T279))
U19_GAA(T250, T273, T280, tappendc50_out_gaa(node(nil, T278, T272), T273, T279)) → TLAST35_IN_AG(T280, T279)
GOAL1_IN_GAA(s(T289), T13, T14) → U21_GAA(T289, T13, T14, s2t9_in_ga(T289, X582))
GOAL1_IN_GAA(s(T289), T311, T312) → U22_GAA(T289, T311, T312, s2tc9_in_ga(T289, T310))
U22_GAA(T289, T311, T312, s2tc9_out_ga(T289, T310)) → U23_GAA(T289, T311, T312, tappend50_in_gaa(node(T310, X625, nil), T311, X624))
U22_GAA(T289, T311, T312, s2tc9_out_ga(T289, T310)) → TAPPEND50_IN_GAA(node(T310, X625, nil), T311, X624)
GOAL1_IN_GAA(s(T289), T311, T317) → U24_GAA(T289, T311, T317, s2tc9_in_ga(T289, T310))
U24_GAA(T289, T311, T317, s2tc9_out_ga(T289, T310)) → U25_GAA(T289, T311, T317, tappendc50_in_gaa(node(T310, T315, nil), T311, T316))
U25_GAA(T289, T311, T317, tappendc50_out_gaa(node(T310, T315, nil), T311, T316)) → U26_GAA(T289, T311, T317, tlast35_in_ag(T317, T316))
U25_GAA(T289, T311, T317, tappendc50_out_gaa(node(T310, T315, nil), T311, T316)) → TLAST35_IN_AG(T317, T316)
GOAL1_IN_GAA(s(T326), T339, T340) → U27_GAA(T326, T339, T340, p33_in_gaaaa(nil, X690, T339, X689, T340))
GOAL1_IN_GAA(s(T326), T339, T340) → P33_IN_GAAAA(nil, X690, T339, X689, T340)
GOAL1_IN_GAA(0, T355, T356) → U28_GAA(T355, T356, tappend50_in_gaa(nil, T355, X714))
GOAL1_IN_GAA(0, T355, T356) → TAPPEND50_IN_GAA(nil, T355, X714)
GOAL1_IN_GAA(0, T355, T360) → U29_GAA(T355, T360, tappendc50_in_gaa(nil, T355, T359))
U29_GAA(T355, T360, tappendc50_out_gaa(nil, T355, T359)) → U30_GAA(T355, T360, tlast35_in_ag(T360, T359))
U29_GAA(T355, T360, tappendc50_out_gaa(nil, T355, T359)) → TLAST35_IN_AG(T360, T359)

The TRS R consists of the following rules:

s2tc9_in_ga(s(T27), node(X69, X70, X69)) → U32_ga(T27, X69, X70, s2tc9_in_ga(T27, X69))
s2tc9_in_ga(s(T33), node(nil, X102, X103)) → U33_ga(T33, X102, X103, s2tc9_in_ga(T33, X103))
s2tc9_in_ga(s(T39), node(X135, X136, nil)) → U34_ga(T39, X135, X136, s2tc9_in_ga(T39, X135))
s2tc9_in_ga(s(T45), node(nil, X159, nil)) → s2tc9_out_ga(s(T45), node(nil, X159, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U34_ga(T39, X135, X136, s2tc9_out_ga(T39, X135)) → s2tc9_out_ga(s(T39), node(X135, X136, nil))
U33_ga(T33, X102, X103, s2tc9_out_ga(T33, X103)) → s2tc9_out_ga(s(T33), node(nil, X102, X103))
U32_ga(T27, X69, X70, s2tc9_out_ga(T27, X69)) → s2tc9_out_ga(s(T27), node(X69, X70, X69))
tappendc34_in_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil)) → tappendc34_out_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil))
tappendc34_in_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil))) → tappendc34_out_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil)))
tappendc34_in_gaaa(T106, X295, T107, node(X296, X295, T106)) → U41_gaaa(T106, X295, T107, X296, tappendc50_in_gaa(T106, T107, X296))
tappendc50_in_gaa(nil, T114, node(nil, T114, nil)) → tappendc50_out_gaa(nil, T114, node(nil, T114, nil))
tappendc50_in_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128)) → tappendc50_out_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128))
tappendc50_in_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil))) → tappendc50_out_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil)))
tappendc50_in_gaa(node(T165, T162, T163), T166, node(X370, T162, T163)) → U35_gaa(T165, T162, T163, T166, X370, tappendc50_in_gaa(T165, T166, X370))
tappendc50_in_gaa(node(T177, T178, T181), T182, node(T177, T178, X395)) → U36_gaa(T177, T178, T181, T182, X395, tappendc50_in_gaa(T181, T182, X395))
U36_gaa(T177, T178, T181, T182, X395, tappendc50_out_gaa(T181, T182, X395)) → tappendc50_out_gaa(node(T177, T178, T181), T182, node(T177, T178, X395))
U35_gaa(T165, T162, T163, T166, X370, tappendc50_out_gaa(T165, T166, X370)) → tappendc50_out_gaa(node(T165, T162, T163), T166, node(X370, T162, T163))
U41_gaaa(T106, X295, T107, X296, tappendc50_out_gaa(T106, T107, X296)) → tappendc34_out_gaaa(T106, X295, T107, node(X296, X295, T106))
tappendc34_in_gaaa(T195, X424, T196, node(T195, X424, X425)) → U42_gaaa(T195, X424, T196, X425, tappendc50_in_gaa(T195, T196, X425))
U42_gaaa(T195, X424, T196, X425, tappendc50_out_gaa(T195, T196, X425)) → tappendc34_out_gaaa(T195, X424, T196, node(T195, X424, X425))

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

TLAST35_IN_AG(T242, node(T239, T240, T243)) → TLAST35_IN_AG(T242, T243)
TLAST35_IN_AG(T226, node(T227, T224, T225)) → TLAST35_IN_AG(T226, T227)

The TRS R consists of the following rules:

s2tc9_in_ga(s(T27), node(X69, X70, X69)) → U32_ga(T27, X69, X70, s2tc9_in_ga(T27, X69))
s2tc9_in_ga(s(T33), node(nil, X102, X103)) → U33_ga(T33, X102, X103, s2tc9_in_ga(T33, X103))
s2tc9_in_ga(s(T39), node(X135, X136, nil)) → U34_ga(T39, X135, X136, s2tc9_in_ga(T39, X135))
s2tc9_in_ga(s(T45), node(nil, X159, nil)) → s2tc9_out_ga(s(T45), node(nil, X159, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U34_ga(T39, X135, X136, s2tc9_out_ga(T39, X135)) → s2tc9_out_ga(s(T39), node(X135, X136, nil))
U33_ga(T33, X102, X103, s2tc9_out_ga(T33, X103)) → s2tc9_out_ga(s(T33), node(nil, X102, X103))
U32_ga(T27, X69, X70, s2tc9_out_ga(T27, X69)) → s2tc9_out_ga(s(T27), node(X69, X70, X69))
tappendc34_in_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil)) → tappendc34_out_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil))
tappendc34_in_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil))) → tappendc34_out_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil)))
tappendc34_in_gaaa(T106, X295, T107, node(X296, X295, T106)) → U41_gaaa(T106, X295, T107, X296, tappendc50_in_gaa(T106, T107, X296))
tappendc50_in_gaa(nil, T114, node(nil, T114, nil)) → tappendc50_out_gaa(nil, T114, node(nil, T114, nil))
tappendc50_in_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128)) → tappendc50_out_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128))
tappendc50_in_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil))) → tappendc50_out_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil)))
tappendc50_in_gaa(node(T165, T162, T163), T166, node(X370, T162, T163)) → U35_gaa(T165, T162, T163, T166, X370, tappendc50_in_gaa(T165, T166, X370))
tappendc50_in_gaa(node(T177, T178, T181), T182, node(T177, T178, X395)) → U36_gaa(T177, T178, T181, T182, X395, tappendc50_in_gaa(T181, T182, X395))
U36_gaa(T177, T178, T181, T182, X395, tappendc50_out_gaa(T181, T182, X395)) → tappendc50_out_gaa(node(T177, T178, T181), T182, node(T177, T178, X395))
U35_gaa(T165, T162, T163, T166, X370, tappendc50_out_gaa(T165, T166, X370)) → tappendc50_out_gaa(node(T165, T162, T163), T166, node(X370, T162, T163))
U41_gaaa(T106, X295, T107, X296, tappendc50_out_gaa(T106, T107, X296)) → tappendc34_out_gaaa(T106, X295, T107, node(X296, X295, T106))
tappendc34_in_gaaa(T195, X424, T196, node(T195, X424, X425)) → U42_gaaa(T195, X424, T196, X425, tappendc50_in_gaa(T195, T196, X425))
U42_gaaa(T195, X424, T196, X425, tappendc50_out_gaa(T195, T196, X425)) → tappendc34_out_gaaa(T195, X424, T196, node(T195, X424, X425))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
node(x1, x2, x3) = node(x1, x3)
s2tc9_in_ga(x1, x2) = s2tc9_in_ga(x1)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
U33_ga(x1, x2, x3, x4) = U33_ga(x1, x4)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x4)
s2tc9_out_ga(x1, x2) = s2tc9_out_ga(x1, x2)
0 = 0
tappendc34_in_gaaa(x1, x2, x3, x4) = tappendc34_in_gaaa(x1)
nil = nil
tappendc34_out_gaaa(x1, x2, x3, x4) = tappendc34_out_gaaa(x1, x4)
U41_gaaa(x1, x2, x3, x4, x5) = U41_gaaa(x1, x5)
tappendc50_in_gaa(x1, x2, x3) = tappendc50_in_gaa(x1)
tappendc50_out_gaa(x1, x2, x3) = tappendc50_out_gaa(x1, x3)
U35_gaa(x1, x2, x3, x4, x5, x6) = U35_gaa(x1, x3, x6)
U36_gaa(x1, x2, x3, x4, x5, x6) = U36_gaa(x1, x3, x6)
U42_gaaa(x1, x2, x3, x4, x5) = U42_gaaa(x1, x5)
TLAST35_IN_AG(x1, x2) = TLAST35_IN_AG(x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

TLAST35_IN_AG(T242, node(T239, T240, T243)) → TLAST35_IN_AG(T242, T243)
TLAST35_IN_AG(T226, node(T227, T224, T225)) → TLAST35_IN_AG(T226, T227)

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

TLAST35_IN_AG(node(T239, T243)) → TLAST35_IN_AG(T243)
TLAST35_IN_AG(node(T227, T225)) → TLAST35_IN_AG(T227)

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:

TLAST35_IN_AG(node(T239, T243)) → TLAST35_IN_AG(T243)
The graph contains the following edges 1 > 1
TLAST35_IN_AG(node(T227, T225)) → TLAST35_IN_AG(T227)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

TAPPEND50_IN_GAA(node(T177, T178, T181), T182, node(T177, T178, X395)) → TAPPEND50_IN_GAA(T181, T182, X395)
TAPPEND50_IN_GAA(node(T165, T162, T163), T166, node(X370, T162, T163)) → TAPPEND50_IN_GAA(T165, T166, X370)

The TRS R consists of the following rules:

s2tc9_in_ga(s(T27), node(X69, X70, X69)) → U32_ga(T27, X69, X70, s2tc9_in_ga(T27, X69))
s2tc9_in_ga(s(T33), node(nil, X102, X103)) → U33_ga(T33, X102, X103, s2tc9_in_ga(T33, X103))
s2tc9_in_ga(s(T39), node(X135, X136, nil)) → U34_ga(T39, X135, X136, s2tc9_in_ga(T39, X135))
s2tc9_in_ga(s(T45), node(nil, X159, nil)) → s2tc9_out_ga(s(T45), node(nil, X159, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U34_ga(T39, X135, X136, s2tc9_out_ga(T39, X135)) → s2tc9_out_ga(s(T39), node(X135, X136, nil))
U33_ga(T33, X102, X103, s2tc9_out_ga(T33, X103)) → s2tc9_out_ga(s(T33), node(nil, X102, X103))
U32_ga(T27, X69, X70, s2tc9_out_ga(T27, X69)) → s2tc9_out_ga(s(T27), node(X69, X70, X69))
tappendc34_in_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil)) → tappendc34_out_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil))
tappendc34_in_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil))) → tappendc34_out_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil)))
tappendc34_in_gaaa(T106, X295, T107, node(X296, X295, T106)) → U41_gaaa(T106, X295, T107, X296, tappendc50_in_gaa(T106, T107, X296))
tappendc50_in_gaa(nil, T114, node(nil, T114, nil)) → tappendc50_out_gaa(nil, T114, node(nil, T114, nil))
tappendc50_in_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128)) → tappendc50_out_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128))
tappendc50_in_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil))) → tappendc50_out_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil)))
tappendc50_in_gaa(node(T165, T162, T163), T166, node(X370, T162, T163)) → U35_gaa(T165, T162, T163, T166, X370, tappendc50_in_gaa(T165, T166, X370))
tappendc50_in_gaa(node(T177, T178, T181), T182, node(T177, T178, X395)) → U36_gaa(T177, T178, T181, T182, X395, tappendc50_in_gaa(T181, T182, X395))
U36_gaa(T177, T178, T181, T182, X395, tappendc50_out_gaa(T181, T182, X395)) → tappendc50_out_gaa(node(T177, T178, T181), T182, node(T177, T178, X395))
U35_gaa(T165, T162, T163, T166, X370, tappendc50_out_gaa(T165, T166, X370)) → tappendc50_out_gaa(node(T165, T162, T163), T166, node(X370, T162, T163))
U41_gaaa(T106, X295, T107, X296, tappendc50_out_gaa(T106, T107, X296)) → tappendc34_out_gaaa(T106, X295, T107, node(X296, X295, T106))
tappendc34_in_gaaa(T195, X424, T196, node(T195, X424, X425)) → U42_gaaa(T195, X424, T196, X425, tappendc50_in_gaa(T195, T196, X425))
U42_gaaa(T195, X424, T196, X425, tappendc50_out_gaa(T195, T196, X425)) → tappendc34_out_gaaa(T195, X424, T196, node(T195, X424, X425))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
node(x1, x2, x3) = node(x1, x3)
s2tc9_in_ga(x1, x2) = s2tc9_in_ga(x1)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
U33_ga(x1, x2, x3, x4) = U33_ga(x1, x4)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x4)
s2tc9_out_ga(x1, x2) = s2tc9_out_ga(x1, x2)
0 = 0
tappendc34_in_gaaa(x1, x2, x3, x4) = tappendc34_in_gaaa(x1)
nil = nil
tappendc34_out_gaaa(x1, x2, x3, x4) = tappendc34_out_gaaa(x1, x4)
U41_gaaa(x1, x2, x3, x4, x5) = U41_gaaa(x1, x5)
tappendc50_in_gaa(x1, x2, x3) = tappendc50_in_gaa(x1)
tappendc50_out_gaa(x1, x2, x3) = tappendc50_out_gaa(x1, x3)
U35_gaa(x1, x2, x3, x4, x5, x6) = U35_gaa(x1, x3, x6)
U36_gaa(x1, x2, x3, x4, x5, x6) = U36_gaa(x1, x3, x6)
U42_gaaa(x1, x2, x3, x4, x5) = U42_gaaa(x1, x5)
TAPPEND50_IN_GAA(x1, x2, x3) = TAPPEND50_IN_GAA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

TAPPEND50_IN_GAA(node(T177, T178, T181), T182, node(T177, T178, X395)) → TAPPEND50_IN_GAA(T181, T182, X395)
TAPPEND50_IN_GAA(node(T165, T162, T163), T166, node(X370, T162, T163)) → TAPPEND50_IN_GAA(T165, T166, X370)

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

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:

TAPPEND50_IN_GAA(node(T177, T181)) → TAPPEND50_IN_GAA(T181)
TAPPEND50_IN_GAA(node(T165, T163)) → TAPPEND50_IN_GAA(T165)

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:

TAPPEND50_IN_GAA(node(T177, T181)) → TAPPEND50_IN_GAA(T181)
The graph contains the following edges 1 > 1
TAPPEND50_IN_GAA(node(T165, T163)) → TAPPEND50_IN_GAA(T165)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

S2T9_IN_GA(s(T33), node(nil, X102, X103)) → S2T9_IN_GA(T33, X103)
S2T9_IN_GA(s(T27), node(X69, X70, X69)) → S2T9_IN_GA(T27, X69)
S2T9_IN_GA(s(T39), node(X135, X136, nil)) → S2T9_IN_GA(T39, X135)

The TRS R consists of the following rules:

s2tc9_in_ga(s(T27), node(X69, X70, X69)) → U32_ga(T27, X69, X70, s2tc9_in_ga(T27, X69))
s2tc9_in_ga(s(T33), node(nil, X102, X103)) → U33_ga(T33, X102, X103, s2tc9_in_ga(T33, X103))
s2tc9_in_ga(s(T39), node(X135, X136, nil)) → U34_ga(T39, X135, X136, s2tc9_in_ga(T39, X135))
s2tc9_in_ga(s(T45), node(nil, X159, nil)) → s2tc9_out_ga(s(T45), node(nil, X159, nil))
s2tc9_in_ga(0, nil) → s2tc9_out_ga(0, nil)
U34_ga(T39, X135, X136, s2tc9_out_ga(T39, X135)) → s2tc9_out_ga(s(T39), node(X135, X136, nil))
U33_ga(T33, X102, X103, s2tc9_out_ga(T33, X103)) → s2tc9_out_ga(s(T33), node(nil, X102, X103))
U32_ga(T27, X69, X70, s2tc9_out_ga(T27, X69)) → s2tc9_out_ga(s(T27), node(X69, X70, X69))
tappendc34_in_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil)) → tappendc34_out_gaaa(nil, X231, T77, node(node(nil, T77, nil), X231, nil))
tappendc34_in_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil))) → tappendc34_out_gaaa(nil, X254, T87, node(nil, X254, node(nil, T87, nil)))
tappendc34_in_gaaa(T106, X295, T107, node(X296, X295, T106)) → U41_gaaa(T106, X295, T107, X296, tappendc50_in_gaa(T106, T107, X296))
tappendc50_in_gaa(nil, T114, node(nil, T114, nil)) → tappendc50_out_gaa(nil, T114, node(nil, T114, nil))
tappendc50_in_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128)) → tappendc50_out_gaa(node(nil, T127, T128), T129, node(node(nil, T129, nil), T127, T128))
tappendc50_in_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil))) → tappendc50_out_gaa(node(T142, T143, nil), T144, node(T142, T143, node(nil, T144, nil)))
tappendc50_in_gaa(node(T165, T162, T163), T166, node(X370, T162, T163)) → U35_gaa(T165, T162, T163, T166, X370, tappendc50_in_gaa(T165, T166, X370))
tappendc50_in_gaa(node(T177, T178, T181), T182, node(T177, T178, X395)) → U36_gaa(T177, T178, T181, T182, X395, tappendc50_in_gaa(T181, T182, X395))
U36_gaa(T177, T178, T181, T182, X395, tappendc50_out_gaa(T181, T182, X395)) → tappendc50_out_gaa(node(T177, T178, T181), T182, node(T177, T178, X395))
U35_gaa(T165, T162, T163, T166, X370, tappendc50_out_gaa(T165, T166, X370)) → tappendc50_out_gaa(node(T165, T162, T163), T166, node(X370, T162, T163))
U41_gaaa(T106, X295, T107, X296, tappendc50_out_gaa(T106, T107, X296)) → tappendc34_out_gaaa(T106, X295, T107, node(X296, X295, T106))
tappendc34_in_gaaa(T195, X424, T196, node(T195, X424, X425)) → U42_gaaa(T195, X424, T196, X425, tappendc50_in_gaa(T195, T196, X425))
U42_gaaa(T195, X424, T196, X425, tappendc50_out_gaa(T195, T196, X425)) → tappendc34_out_gaaa(T195, X424, T196, node(T195, X424, X425))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
node(x1, x2, x3) = node(x1, x3)
s2tc9_in_ga(x1, x2) = s2tc9_in_ga(x1)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x4)
U33_ga(x1, x2, x3, x4) = U33_ga(x1, x4)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x4)
s2tc9_out_ga(x1, x2) = s2tc9_out_ga(x1, x2)
0 = 0
tappendc34_in_gaaa(x1, x2, x3, x4) = tappendc34_in_gaaa(x1)
nil = nil
tappendc34_out_gaaa(x1, x2, x3, x4) = tappendc34_out_gaaa(x1, x4)
U41_gaaa(x1, x2, x3, x4, x5) = U41_gaaa(x1, x5)
tappendc50_in_gaa(x1, x2, x3) = tappendc50_in_gaa(x1)
tappendc50_out_gaa(x1, x2, x3) = tappendc50_out_gaa(x1, x3)
U35_gaa(x1, x2, x3, x4, x5, x6) = U35_gaa(x1, x3, x6)
U36_gaa(x1, x2, x3, x4, x5, x6) = U36_gaa(x1, x3, x6)
U42_gaaa(x1, x2, x3, x4, x5) = U42_gaaa(x1, x5)
S2T9_IN_GA(x1, x2) = S2T9_IN_GA(x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

S2T9_IN_GA(s(T33), node(nil, X102, X103)) → S2T9_IN_GA(T33, X103)
S2T9_IN_GA(s(T27), node(X69, X70, X69)) → S2T9_IN_GA(T27, X69)
S2T9_IN_GA(s(T39), node(X135, X136, nil)) → S2T9_IN_GA(T39, X135)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
node(x1, x2, x3) = node(x1, x3)
nil = nil
S2T9_IN_GA(x1, x2) = S2T9_IN_GA(x1)

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:

S2T9_IN_GA(s(T33)) → S2T9_IN_GA(T33)

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:

S2T9_IN_GA(s(T33)) → S2T9_IN_GA(T33)
The graph contains the following edges 1 > 1

(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