Left Termination proof of /tmp/tmpiKX

Left Termination of the query pattern goal_in_1(g) w.r.t. the given Prolog program could not be shown:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 UndefinedPredicateInTriplesTransformerProof (⇐)

↳4 TRIPLES

↳5 TriplesToPiDPProof (⇐)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔)

        ↳11 PiDP

        ↳12 PiDPToQDPProof (⇐)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇐)

        ↳20 QDP

        ↳21 NonTerminationProof (⇔)

        ↳22 NO

    ↳23 PiDP

        ↳24 UsableRulesProof (⇔)

        ↳25 PiDP

        ↳26 PiDPToQDPProof (⇐)

        ↳27 QDP

        ↳28 QDPSizeChangeProof (⇔)

        ↳29 YES

(0) Obligation:

Clauses:

goal(X) :- ','(s2t(X, T), tappend(T, X1, X2)).
tappend(nil, Y, Z) :- ','(!, eq(Y, Z)).
tappend(T, T1, node(T1, X, T2)) :- ','(left(T, nil), ','(right(T, T2), value(T, X))).
tappend(T, T2, node(T1, X, T2)) :- ','(left(T, T1), ','(right(T, nil), value(T, X))).
tappend(T, T3, node(U, X, T2)) :- ','(left(T, T1), ','(right(T, T2), ','(value(T, X), tappend(T1, T3, U)))).
tappend(T, T1, node(T1, X, U)) :- ','(left(T, T1), ','(right(T, T2), ','(value(T, X), tappend(T2, T3, U)))).
s2t(0, L) :- ','(!, eq(L, nil)).
s2t(X, node(T, X3, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X4, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(T, X5, nil)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X6, nil)).
left(nil, nil).
left(node(L, X7, X8), L).
right(nil, nil).
right(node(X9, X10, R), R).
value(nil, nil).
value(node(X11, X, X12), X).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

goal(g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: goal(T4)\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: goal(T4), SCOPE: 1, CLAUSE: 0\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(s2t(T6, X15), tappend(X15, X16, X17))\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 7 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 8 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 9 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 10\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(!_2, ','(eq(X23, nil), tappend(X23, X16, X17))) | ','(s2t(0, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 7 | ','(s2t(0, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 8 | ','(s2t(0, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 9 | ','(s2t(0, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 10\n\nX15 is free\nX16 is free; \nX17 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 7 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 8 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 9 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 10\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; \ns2t(T6, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(eq(X23, nil), tappend(X23, X16, X17))\n\nX16 is free\nX17 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(eq(X23, nil), tappend(X23, X16, X17)), SCOPE: 3, CLAUSE: 19\n\nX16 is free\nX17 is free; \nX23 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: tappend(nil, X16, X17)\n\nX16 is free\nX17 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 1 | tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 2 | tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 3 | tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 4 | tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 5\n\nX16 is free\nX17 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(!_4, eq(X53, X54)) | tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 2 | tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 3 | tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 4 | tappend(nil, X16, X17), SCOPE: 4, CLAUSE: 5\n\nX16 is free\nX17 is free; \nX53 is free; \nX54 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: eq(X53, X54)\n\nX53 is free\nX54 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: eq(X53, X54), SCOPE: 5, CLAUSE: 19\n\nX53 is free\nX54 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: ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 7\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; \ns2t(T6, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 8 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 9 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 10\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; \ns2t(T6, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(p(T11, X90), ','(s2t(X90, X91), tappend(node(X91, X92, X91), X16, X17)))\n\nT11 is ground\nX16 is free; \nX17 is free; \nX91 is free; \nX92 is free; \nX90 is free; \ns2t(T11, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(p(T11, X90), ','(s2t(X90, X91), tappend(node(X91, X92, X91), X16, X17))), SCOPE: 6, CLAUSE: 17 | ','(p(T11, X90), ','(s2t(X90, X91), tappend(node(X91, X92, X91), X16, X17))), SCOPE: 6, CLAUSE: 18\n\nT11 is ground\nX16 is free; \nX17 is free; \nX91 is free; \nX92 is free; \nX90 is free; \ns2t(T11, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(p(T11, X90), ','(s2t(X90, X91), tappend(node(X91, X92, X91), X16, X17))), SCOPE: 6, CLAUSE: 18\n\nT11 is ground\nX16 is free; \nX17 is free; \nX91 is free; \nX92 is free; \nX90 is free; \ns2t(T11, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(s2t(T14, X91), tappend(node(X91, X92, X91), X16, X17))\n\nT14 is ground\nX16 is free; \nX17 is free; \nX91 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: s2t(T14, X91)\n\nT14 is ground\nX91 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: tappend(node(T15, X92, T15), X16, X17)\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: s2t(T14, X91), SCOPE: 7, CLAUSE: 6 | s2t(T14, X91), SCOPE: 7, CLAUSE: 7 | s2t(T14, X91), SCOPE: 7, CLAUSE: 8 | s2t(T14, X91), SCOPE: 7, CLAUSE: 9 | s2t(T14, X91), SCOPE: 7, CLAUSE: 10\n\nT14 is ground\nX91 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(!_7, eq(X108, nil)) | s2t(0, X91), SCOPE: 7, CLAUSE: 7 | s2t(0, X91), SCOPE: 7, CLAUSE: 8 | s2t(0, X91), SCOPE: 7, CLAUSE: 9 | s2t(0, X91), SCOPE: 7, CLAUSE: 10\n\nX91 is free\nX108 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: s2t(T14, X91), SCOPE: 7, CLAUSE: 7 | s2t(T14, X91), SCOPE: 7, CLAUSE: 8 | s2t(T14, X91), SCOPE: 7, CLAUSE: 9 | s2t(T14, X91), SCOPE: 7, CLAUSE: 10\n\nT14 is ground\nX91 is free; \ns2t(T14, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: eq(X108, nil)\n\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: eq(X108, nil), SCOPE: 8, CLAUSE: 19\n\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: s2t(T14, X91), SCOPE: 7, CLAUSE: 7\n\nT14 is ground\nX91 is free; \ns2t(T14, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: s2t(T14, X91), SCOPE: 7, CLAUSE: 8 | s2t(T14, X91), SCOPE: 7, CLAUSE: 9 | s2t(T14, X91), SCOPE: 7, CLAUSE: 10\n\nT14 is ground\nX91 is free; \ns2t(T14, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(p(T20, X145), s2t(X145, X146))\n\nT20 is ground\nX146 is free; \nX145 is free; \ns2t(T20, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(p(T20, X145), s2t(X145, X146)), SCOPE: 9, CLAUSE: 17 | ','(p(T20, X145), s2t(X145, X146)), SCOPE: 9, CLAUSE: 18\n\nT20 is ground\nX146 is free; \nX145 is free; \ns2t(T20, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(p(T20, X145), s2t(X145, X146)), SCOPE: 9, CLAUSE: 18\n\nT20 is ground\nX146 is free; \nX145 is free; \ns2t(T20, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: s2t(T23, X146)\n\nT23 is ground\nX146 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: s2t(T14, X91), SCOPE: 7, CLAUSE: 8\n\nT14 is ground\nX91 is free; \ns2t(T14, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: s2t(T14, X91), SCOPE: 7, CLAUSE: 9 | s2t(T14, X91), SCOPE: 7, CLAUSE: 10\n\nT14 is ground\nX91 is free; \ns2t(T14, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(p(T28, X185), s2t(X185, X187))\n\nT28 is ground\nX187 is free; \nX185 is free; \ns2t(T28, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(p(T28, X185), s2t(X185, X187)), SCOPE: 10, CLAUSE: 17 | ','(p(T28, X185), s2t(X185, X187)), SCOPE: 10, CLAUSE: 18\n\nT28 is ground\nX187 is free; \nX185 is free; \ns2t(T28, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(p(T28, X185), s2t(X185, X187)), SCOPE: 10, CLAUSE: 18\n\nT28 is ground\nX187 is free; \nX185 is free; \ns2t(T28, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: s2t(T31, X187)\n\nT31 is ground\nX187 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: s2t(T14, X91), SCOPE: 7, CLAUSE: 9\n\nT14 is ground\nX91 is free; \ns2t(T14, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: s2t(T14, X91), SCOPE: 7, CLAUSE: 10\n\nT14 is ground\nX91 is free; \ns2t(T14, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(p(T36, X225), s2t(X225, X226))\n\nT36 is ground\nX226 is free; \nX225 is free; \ns2t(T36, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(p(T36, X225), s2t(X225, X226)), SCOPE: 11, CLAUSE: 17 | ','(p(T36, X225), s2t(X225, X226)), SCOPE: 11, CLAUSE: 18\n\nT36 is ground\nX226 is free; \nX225 is free; \ns2t(T36, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(p(T36, X225), s2t(X225, X226)), SCOPE: 11, CLAUSE: 18\n\nT36 is ground\nX226 is free; \nX225 is free; \ns2t(T36, X91) !=? s2t(0, X107)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: s2t(T39, X226)\n\nT39 is ground\nX226 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 1 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 2 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 3 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 4 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 5\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 2 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 3 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 4 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 5\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 2\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 3 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 4 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 5\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(left(node(T51, X293, T51), nil), ','(right(node(T51, X293, T51), X296), value(node(T51, X293, T51), X295)))\n\nX293 is free\nX295 is free; \nX296 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(left(node(T51, X293, T51), nil), ','(right(node(T51, X293, T51), X296), value(node(T51, X293, T51), X295))), SCOPE: 13, CLAUSE: 11 | ','(left(node(T51, X293, T51), nil), ','(right(node(T51, X293, T51), X296), value(node(T51, X293, T51), X295))), SCOPE: 13, CLAUSE: 12\n\nX293 is free\nX295 is free; \nX296 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(left(node(T51, X293, T51), nil), ','(right(node(T51, X293, T51), X296), value(node(T51, X293, T51), X295))), SCOPE: 13, CLAUSE: 12\n\nX293 is free\nX295 is free; \nX296 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(right(node(nil, X308, nil), X296), value(node(nil, X308, nil), X295))\n\nX295 is free\nX296 is free; \nX308 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(right(node(nil, X308, nil), X296), value(node(nil, X308, nil), X295)), SCOPE: 14, CLAUSE: 13 | ','(right(node(nil, X308, nil), X296), value(node(nil, X308, nil), X295)), SCOPE: 14, CLAUSE: 14\n\nX295 is free\nX296 is free; \nX308 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(right(node(nil, X308, nil), X296), value(node(nil, X308, nil), X295)), SCOPE: 14, CLAUSE: 14\n\nX295 is free\nX296 is free; \nX308 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: value(node(nil, X323, nil), X295)\n\nX295 is free\nX323 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: value(node(nil, X323, nil), X295), SCOPE: 15, CLAUSE: 15 | value(node(nil, X323, nil), X295), SCOPE: 15, CLAUSE: 16\n\nX295 is free\nX323 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: value(node(nil, X323, nil), X295), SCOPE: 15, CLAUSE: 16\n\nX295 is free\nX323 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 3\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 4 | tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 5\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(left(node(T62, X372, T62), X374), ','(right(node(T62, X372, T62), nil), value(node(T62, X372, T62), X375)))\n\nX372 is free\nX374 is free; \nX375 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(left(node(T62, X372, T62), X374), ','(right(node(T62, X372, T62), nil), value(node(T62, X372, T62), X375))), SCOPE: 16, CLAUSE: 11 | ','(left(node(T62, X372, T62), X374), ','(right(node(T62, X372, T62), nil), value(node(T62, X372, T62), X375))), SCOPE: 16, CLAUSE: 12\n\nX372 is free\nX374 is free; \nX375 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(left(node(T62, X372, T62), X374), ','(right(node(T62, X372, T62), nil), value(node(T62, X372, T62), X375))), SCOPE: 16, CLAUSE: 12\n\nX372 is free\nX374 is free; \nX375 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(right(node(T67, X387, T67), nil), value(node(T67, X387, T67), X375))\n\nX375 is free\nX387 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(right(node(T67, X387, T67), nil), value(node(T67, X387, T67), X375)), SCOPE: 17, CLAUSE: 13 | ','(right(node(T67, X387, T67), nil), value(node(T67, X387, T67), X375)), SCOPE: 17, CLAUSE: 14\n\nX375 is free\nX387 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(right(node(T67, X387, T67), nil), value(node(T67, X387, T67), X375)), SCOPE: 17, CLAUSE: 14\n\nX375 is free\nX387 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: value(node(nil, X399, nil), X375)\n\nX375 is free\nX399 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: value(node(nil, X399, nil), X375), SCOPE: 18, CLAUSE: 15 | value(node(nil, X399, nil), X375), SCOPE: 18, CLAUSE: 16\n\nX375 is free\nX399 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: value(node(nil, X399, nil), X375), SCOPE: 18, CLAUSE: 16\n\nX375 is free\nX399 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 4\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: tappend(node(T15, X92, T15), X16, X17), SCOPE: 12, CLAUSE: 5\n\nX16 is free\nX17 is free; \nX92 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(left(node(T78, X471, T78), X470), ','(right(node(T78, X471, T78), X475), ','(value(node(T78, X471, T78), X474), tappend(X470, X472, X473))))\n\nX471 is free\nX472 is free; \nX473 is free; \nX474 is free; \nX475 is free; \nX470 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(left(node(T78, X471, T78), X470), ','(right(node(T78, X471, T78), X475), ','(value(node(T78, X471, T78), X474), tappend(X470, X472, X473)))), SCOPE: 19, CLAUSE: 11 | ','(left(node(T78, X471, T78), X470), ','(right(node(T78, X471, T78), X475), ','(value(node(T78, X471, T78), X474), tappend(X470, X472, X473)))), SCOPE: 19, CLAUSE: 12\n\nX471 is free\nX472 is free; \nX473 is free; \nX474 is free; \nX475 is free; \nX470 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(left(node(T78, X471, T78), X470), ','(right(node(T78, X471, T78), X475), ','(value(node(T78, X471, T78), X474), tappend(X470, X472, X473)))), SCOPE: 19, CLAUSE: 12\n\nX471 is free\nX472 is free; \nX473 is free; \nX474 is free; \nX475 is free; \nX470 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(right(node(T83, X495, T83), X475), ','(value(node(T83, X495, T83), X474), tappend(T83, X472, X473)))\n\nX472 is free\nX473 is free; \nX474 is free; \nX475 is free; \nX495 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(right(node(T83, X495, T83), X475), ','(value(node(T83, X495, T83), X474), tappend(T83, X472, X473))), SCOPE: 20, CLAUSE: 13 | ','(right(node(T83, X495, T83), X475), ','(value(node(T83, X495, T83), X474), tappend(T83, X472, X473))), SCOPE: 20, CLAUSE: 14\n\nX472 is free\nX473 is free; \nX474 is free; \nX475 is free; \nX495 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(right(node(T83, X495, T83), X475), ','(value(node(T83, X495, T83), X474), tappend(T83, X472, X473))), SCOPE: 20, CLAUSE: 14\n\nX472 is free\nX473 is free; \nX474 is free; \nX475 is free; \nX495 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(value(node(T88, X515, T88), X474), tappend(T88, X472, X473))\n\nX472 is free\nX473 is free; \nX474 is free; \nX515 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(value(node(T88, X515, T88), X474), tappend(T88, X472, X473)), SCOPE: 21, CLAUSE: 15 | ','(value(node(T88, X515, T88), X474), tappend(T88, X472, X473)), SCOPE: 21, CLAUSE: 16\n\nX472 is free\nX473 is free; \nX474 is free; \nX515 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(value(node(T88, X515, T88), X474), tappend(T88, X472, X473)), SCOPE: 21, CLAUSE: 16\n\nX472 is free\nX473 is free; \nX474 is free; \nX515 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: tappend(T93, X472, X473)\n\nX472 is free\nX473 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 1 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 2 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 3 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 4 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 5\n\nX472 is free\nX473 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(!_22, eq(X550, X551)) | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 2 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 3 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 4 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 5\n\nX472 is free\nX473 is free; \nX550 is free; \nX551 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 2 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 3 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 4 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 5\n\nX472 is free\nX473 is free; \ntappend(T93, X472, X473) !=? tappend(nil, X548, X549)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: eq(X550, X551)\n\nX550 is free\nX551 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: eq(X550, X551), SCOPE: 23, CLAUSE: 19\n\nX550 is free\nX551 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 2\n\nX472 is free\nX473 is free; \ntappend(T93, X472, X473) !=? tappend(nil, X548, X549)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 3 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 4 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 5\n\nX472 is free\nX473 is free; \ntappend(T93, X472, X473) !=? tappend(nil, X548, X549)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(left(T101, nil), ','(right(T101, X594), value(T101, X593)))\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(left(T101, nil), ','(right(T101, X594), value(T101, X593))), SCOPE: 24, CLAUSE: 11 | ','(left(T101, nil), ','(right(T101, X594), value(T101, X593))), SCOPE: 24, CLAUSE: 12\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(left(T101, nil), ','(right(T101, X594), value(T101, X593))), SCOPE: 24, CLAUSE: 11\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(left(T101, nil), ','(right(T101, X594), value(T101, X593))), SCOPE: 24, CLAUSE: 12\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(right(nil, X594), value(nil, X593))\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(right(nil, X594), value(nil, X593)), SCOPE: 25, CLAUSE: 13 | ','(right(nil, X594), value(nil, X593)), SCOPE: 25, CLAUSE: 14\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(right(nil, X594), value(nil, X593)), SCOPE: 25, CLAUSE: 13\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(right(nil, X594), value(nil, X593)), SCOPE: 25, CLAUSE: 14\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: value(nil, X593)\n\nX593 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: value(nil, X593), SCOPE: 26, CLAUSE: 15 | value(nil, X593), SCOPE: 26, CLAUSE: 16\n\nX593 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: value(nil, X593), SCOPE: 26, CLAUSE: 15\n\nX593 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: value(nil, X593), SCOPE: 26, CLAUSE: 16\n\nX593 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(right(node(nil, T111, T112), X594), value(node(nil, T111, T112), X593))\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(right(node(nil, T111, T112), X594), value(node(nil, T111, T112), X593)), SCOPE: 27, CLAUSE: 13 | ','(right(node(nil, T111, T112), X594), value(node(nil, T111, T112), X593)), SCOPE: 27, CLAUSE: 14\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(right(node(nil, T111, T112), X594), value(node(nil, T111, T112), X593)), SCOPE: 27, CLAUSE: 14\n\nX593 is free\nX594 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: value(node(nil, T121, T122), X593)\n\nX593 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: value(node(nil, T121, T122), X593), SCOPE: 28, CLAUSE: 15 | value(node(nil, T121, T122), X593), SCOPE: 28, CLAUSE: 16\n\nX593 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: value(node(nil, T121, T122), X593), SCOPE: 28, CLAUSE: 16\n\nX593 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 3\n\nX472 is free\nX473 is free; \ntappend(T93, X472, X473) !=? tappend(nil, X548, X549)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 4 | tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 5\n\nX472 is free\nX473 is free; \ntappend(T93, X472, X473) !=? tappend(nil, X548, X549)", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(left(T136, X664), ','(right(T136, nil), value(T136, X665)))\n\nX664 is free\nX665 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(left(T136, X664), ','(right(T136, nil), value(T136, X665))), SCOPE: 29, CLAUSE: 11 | ','(left(T136, X664), ','(right(T136, nil), value(T136, X665))), SCOPE: 29, CLAUSE: 12\n\nX664 is free\nX665 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(left(T136, X664), ','(right(T136, nil), value(T136, X665))), SCOPE: 29, CLAUSE: 11\n\nX664 is free\nX665 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(left(T136, X664), ','(right(T136, nil), value(T136, X665))), SCOPE: 29, CLAUSE: 12\n\nX664 is free\nX665 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(right(nil, nil), value(nil, X665))\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(right(nil, nil), value(nil, X665)), SCOPE: 30, CLAUSE: 13 | ','(right(nil, nil), value(nil, X665)), SCOPE: 30, CLAUSE: 14\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(right(nil, nil), value(nil, X665)), SCOPE: 30, CLAUSE: 13\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(right(nil, nil), value(nil, X665)), SCOPE: 30, CLAUSE: 14\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: value(nil, X665)\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: value(nil, X665), SCOPE: 31, CLAUSE: 15 | value(nil, X665), SCOPE: 31, CLAUSE: 16\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: value(nil, X665), SCOPE: 31, CLAUSE: 15\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: value(nil, X665), SCOPE: 31, CLAUSE: 16\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(right(node(T146, T147, T148), nil), value(node(T146, T147, T148), X665))\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(right(node(T146, T147, T148), nil), value(node(T146, T147, T148), X665)), SCOPE: 32, CLAUSE: 13 | ','(right(node(T146, T147, T148), nil), value(node(T146, T147, T148), X665)), SCOPE: 32, CLAUSE: 14\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(right(node(T146, T147, T148), nil), value(node(T146, T147, T148), X665)), SCOPE: 32, CLAUSE: 14\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: value(node(T158, T159, nil), X665)\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: value(node(T158, T159, nil), X665), SCOPE: 33, CLAUSE: 15 | value(node(T158, T159, nil), X665), SCOPE: 33, CLAUSE: 16\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: value(node(T158, T159, nil), X665), SCOPE: 33, CLAUSE: 16\n\nX665 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 4\n\nX472 is free\nX473 is free; \ntappend(T93, X472, X473) !=? tappend(nil, X548, X549)", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: tappend(T93, X472, X473), SCOPE: 22, CLAUSE: 5\n\nX472 is free\nX473 is free; \ntappend(T93, X472, X473) !=? tappend(nil, X548, X549)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(left(T173, X756), ','(right(T173, X760), ','(value(T173, X759), tappend(X756, X757, X758))))\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; \nX756 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(left(T173, X756), ','(right(T173, X760), ','(value(T173, X759), tappend(X756, X757, X758)))), SCOPE: 34, CLAUSE: 11 | ','(left(T173, X756), ','(right(T173, X760), ','(value(T173, X759), tappend(X756, X757, X758)))), SCOPE: 34, CLAUSE: 12\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; \nX756 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(left(T173, X756), ','(right(T173, X760), ','(value(T173, X759), tappend(X756, X757, X758)))), SCOPE: 34, CLAUSE: 11\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; \nX756 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(left(T173, X756), ','(right(T173, X760), ','(value(T173, X759), tappend(X756, X757, X758)))), SCOPE: 34, CLAUSE: 12\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; \nX756 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(right(nil, X760), ','(value(nil, X759), tappend(nil, X757, X758)))\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(right(nil, X760), ','(value(nil, X759), tappend(nil, X757, X758))), SCOPE: 35, CLAUSE: 13 | ','(right(nil, X760), ','(value(nil, X759), tappend(nil, X757, X758))), SCOPE: 35, CLAUSE: 14\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(right(nil, X760), ','(value(nil, X759), tappend(nil, X757, X758))), SCOPE: 35, CLAUSE: 13\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ','(right(nil, X760), ','(value(nil, X759), tappend(nil, X757, X758))), SCOPE: 35, CLAUSE: 14\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(value(nil, X759), tappend(nil, X757, X758))\n\nX757 is free\nX758 is free; \nX759 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: ','(value(nil, X759), tappend(nil, X757, X758)), SCOPE: 36, CLAUSE: 15 | ','(value(nil, X759), tappend(nil, X757, X758)), SCOPE: 36, CLAUSE: 16\n\nX757 is free\nX758 is free; \nX759 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ','(value(nil, X759), tappend(nil, X757, X758)), SCOPE: 36, CLAUSE: 15\n\nX757 is free\nX758 is free; \nX759 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ','(value(nil, X759), tappend(nil, X757, X758)), SCOPE: 36, CLAUSE: 16\n\nX757 is free\nX758 is free; \nX759 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: tappend(nil, X757, X758)\n\nX757 is free\nX758 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(right(node(T183, T184, T185), X760), ','(value(node(T183, T184, T185), X759), tappend(T183, X757, X758)))\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ','(right(node(T183, T184, T185), X760), ','(value(node(T183, T184, T185), X759), tappend(T183, X757, X758))), SCOPE: 37, CLAUSE: 13 | ','(right(node(T183, T184, T185), X760), ','(value(node(T183, T184, T185), X759), tappend(T183, X757, X758))), SCOPE: 37, CLAUSE: 14\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ','(right(node(T183, T184, T185), X760), ','(value(node(T183, T184, T185), X759), tappend(T183, X757, X758))), SCOPE: 37, CLAUSE: 14\n\nX757 is free\nX758 is free; \nX759 is free; \nX760 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ','(value(node(T198, T199, T200), X759), tappend(T198, X757, X758))\n\nX757 is free\nX758 is free; \nX759 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ','(value(node(T198, T199, T200), X759), tappend(T198, X757, X758)), SCOPE: 38, CLAUSE: 15 | ','(value(node(T198, T199, T200), X759), tappend(T198, X757, X758)), SCOPE: 38, CLAUSE: 16\n\nX757 is free\nX758 is free; \nX759 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(value(node(T198, T199, T200), X759), tappend(T198, X757, X758)), SCOPE: 38, CLAUSE: 16\n\nX757 is free\nX758 is free; \nX759 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: tappend(T211, X757, X758)\n\nX757 is free\nX758 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(left(T216, X875), ','(right(T216, X873), ','(value(T216, X876), tappend(X873, X874, X877))))\n\nX875 is free\nX876 is free; \nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(left(T216, X875), ','(right(T216, X873), ','(value(T216, X876), tappend(X873, X874, X877)))), SCOPE: 39, CLAUSE: 11 | ','(left(T216, X875), ','(right(T216, X873), ','(value(T216, X876), tappend(X873, X874, X877)))), SCOPE: 39, CLAUSE: 12\n\nX875 is free\nX876 is free; \nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(left(T216, X875), ','(right(T216, X873), ','(value(T216, X876), tappend(X873, X874, X877)))), SCOPE: 39, CLAUSE: 11\n\nX875 is free\nX876 is free; \nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(left(T216, X875), ','(right(T216, X873), ','(value(T216, X876), tappend(X873, X874, X877)))), SCOPE: 39, CLAUSE: 12\n\nX875 is free\nX876 is free; \nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(right(nil, X873), ','(value(nil, X876), tappend(X873, X874, X877)))\n\nX876 is free\nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(right(nil, X873), ','(value(nil, X876), tappend(X873, X874, X877))), SCOPE: 40, CLAUSE: 13 | ','(right(nil, X873), ','(value(nil, X876), tappend(X873, X874, X877))), SCOPE: 40, CLAUSE: 14\n\nX876 is free\nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(right(nil, X873), ','(value(nil, X876), tappend(X873, X874, X877))), SCOPE: 40, CLAUSE: 13\n\nX876 is free\nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(right(nil, X873), ','(value(nil, X876), tappend(X873, X874, X877))), SCOPE: 40, CLAUSE: 14\n\nX876 is free\nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(value(nil, X876), tappend(nil, X874, X877))\n\nX876 is free\nX877 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(value(nil, X876), tappend(nil, X874, X877)), SCOPE: 41, CLAUSE: 15 | ','(value(nil, X876), tappend(nil, X874, X877)), SCOPE: 41, CLAUSE: 16\n\nX876 is free\nX877 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(value(nil, X876), tappend(nil, X874, X877)), SCOPE: 41, CLAUSE: 15\n\nX876 is free\nX877 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(value(nil, X876), tappend(nil, X874, X877)), SCOPE: 41, CLAUSE: 16\n\nX876 is free\nX877 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: tappend(nil, X874, X877)\n\nX877 is free\nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ','(right(node(T226, T227, T228), X873), ','(value(node(T226, T227, T228), X876), tappend(X873, X874, X877)))\n\nX876 is free\nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(right(node(T226, T227, T228), X873), ','(value(node(T226, T227, T228), X876), tappend(X873, X874, X877))), SCOPE: 42, CLAUSE: 13 | ','(right(node(T226, T227, T228), X873), ','(value(node(T226, T227, T228), X876), tappend(X873, X874, X877))), SCOPE: 42, CLAUSE: 14\n\nX876 is free\nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(right(node(T226, T227, T228), X873), ','(value(node(T226, T227, T228), X876), tappend(X873, X874, X877))), SCOPE: 42, CLAUSE: 14\n\nX876 is free\nX877 is free; \nX873 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(value(node(T241, T242, T243), X876), tappend(T243, X874, X877))\n\nX876 is free\nX877 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(value(node(T241, T242, T243), X876), tappend(T243, X874, X877)), SCOPE: 43, CLAUSE: 15 | ','(value(node(T241, T242, T243), X876), tappend(T243, X874, X877)), SCOPE: 43, CLAUSE: 16\n\nX876 is free\nX877 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(value(node(T241, T242, T243), X876), tappend(T243, X874, X877)), SCOPE: 43, CLAUSE: 16\n\nX876 is free\nX877 is free; \nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: tappend(T254, X874, X877)\n\nX877 is free\nX874 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ','(left(node(T259, X994, T259), X995), ','(right(node(T259, X994, T259), X992), ','(value(node(T259, X994, T259), X996), tappend(X992, X993, X997))))\n\nX994 is free\nX995 is free; \nX996 is free; \nX997 is free; \nX992 is free; \nX993 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ','(left(node(T259, X994, T259), X995), ','(right(node(T259, X994, T259), X992), ','(value(node(T259, X994, T259), X996), tappend(X992, X993, X997)))), SCOPE: 44, CLAUSE: 11 | ','(left(node(T259, X994, T259), X995), ','(right(node(T259, X994, T259), X992), ','(value(node(T259, X994, T259), X996), tappend(X992, X993, X997)))), SCOPE: 44, CLAUSE: 12\n\nX994 is free\nX995 is free; \nX996 is free; \nX997 is free; \nX992 is free; \nX993 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(left(node(T259, X994, T259), X995), ','(right(node(T259, X994, T259), X992), ','(value(node(T259, X994, T259), X996), tappend(X992, X993, X997)))), SCOPE: 44, CLAUSE: 12\n\nX994 is free\nX995 is free; \nX996 is free; \nX997 is free; \nX992 is free; \nX993 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(right(node(T264, X1017, T264), X992), ','(value(node(T264, X1017, T264), X996), tappend(X992, X993, X997)))\n\nX996 is free\nX997 is free; \nX992 is free; \nX993 is free; \nX1017 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(right(node(T264, X1017, T264), X992), ','(value(node(T264, X1017, T264), X996), tappend(X992, X993, X997))), SCOPE: 45, CLAUSE: 13 | ','(right(node(T264, X1017, T264), X992), ','(value(node(T264, X1017, T264), X996), tappend(X992, X993, X997))), SCOPE: 45, CLAUSE: 14\n\nX996 is free\nX997 is free; \nX992 is free; \nX993 is free; \nX1017 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(right(node(T264, X1017, T264), X992), ','(value(node(T264, X1017, T264), X996), tappend(X992, X993, X997))), SCOPE: 45, CLAUSE: 14\n\nX996 is free\nX997 is free; \nX992 is free; \nX993 is free; \nX1017 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(value(node(T269, X1037, T269), X996), tappend(T269, X993, X997))\n\nX996 is free\nX997 is free; \nX993 is free; \nX1037 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(value(node(T269, X1037, T269), X996), tappend(T269, X993, X997)), SCOPE: 46, CLAUSE: 15 | ','(value(node(T269, X1037, T269), X996), tappend(T269, X993, X997)), SCOPE: 46, CLAUSE: 16\n\nX996 is free\nX997 is free; \nX993 is free; \nX1037 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: ','(value(node(T269, X1037, T269), X996), tappend(T269, X993, X997)), SCOPE: 46, CLAUSE: 16\n\nX996 is free\nX997 is free; \nX993 is free; \nX1037 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: tappend(T274, X993, X997)\n\nX997 is free\nX993 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 8\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; \ns2t(T6, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 9 | ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 10\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; \ns2t(T6, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: ','(p(T279, X1091), ','(s2t(X1091, X1093), tappend(node(nil, X1092, X1093), X16, X17)))\n\nT279 is ground\nX16 is free; \nX17 is free; \nX1092 is free; \nX1093 is free; \nX1091 is free; \ns2t(T279, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ','(p(T279, X1091), ','(s2t(X1091, X1093), tappend(node(nil, X1092, X1093), X16, X17))), SCOPE: 47, CLAUSE: 17 | ','(p(T279, X1091), ','(s2t(X1091, X1093), tappend(node(nil, X1092, X1093), X16, X17))), SCOPE: 47, CLAUSE: 18\n\nT279 is ground\nX16 is free; \nX17 is free; \nX1092 is free; \nX1093 is free; \nX1091 is free; \ns2t(T279, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(p(T279, X1091), ','(s2t(X1091, X1093), tappend(node(nil, X1092, X1093), X16, X17))), SCOPE: 47, CLAUSE: 18\n\nT279 is ground\nX16 is free; \nX17 is free; \nX1092 is free; \nX1093 is free; \nX1091 is free; \ns2t(T279, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: ','(s2t(T282, X1093), tappend(node(nil, X1092, X1093), X16, X17))\n\nT282 is ground\nX16 is free; \nX17 is free; \nX1092 is free; \nX1093 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: s2t(T282, X1093)\n\nT282 is ground\nX1093 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: tappend(node(nil, X1092, T283), X16, X17)\n\nX16 is free\nX17 is free; \nX1092 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 9\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; \ns2t(T6, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: ','(s2t(T6, X15), tappend(X15, X16, X17)), SCOPE: 2, CLAUSE: 10\n\nT6 is ground\nX15 is free; \nX16 is free; \nX17 is free; \ns2t(T6, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(p(T289, X1143), ','(s2t(X1143, X1144), tappend(node(X1144, X1145, nil), X16, X17)))\n\nT289 is ground\nX16 is free; \nX17 is free; \nX1144 is free; \nX1145 is free; \nX1143 is free; \ns2t(T289, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: ','(p(T289, X1143), ','(s2t(X1143, X1144), tappend(node(X1144, X1145, nil), X16, X17))), SCOPE: 48, CLAUSE: 17 | ','(p(T289, X1143), ','(s2t(X1143, X1144), tappend(node(X1144, X1145, nil), X16, X17))), SCOPE: 48, CLAUSE: 18\n\nT289 is ground\nX16 is free; \nX17 is free; \nX1144 is free; \nX1145 is free; \nX1143 is free; \ns2t(T289, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(p(T289, X1143), ','(s2t(X1143, X1144), tappend(node(X1144, X1145, nil), X16, X17))), SCOPE: 48, CLAUSE: 18\n\nT289 is ground\nX16 is free; \nX17 is free; \nX1144 is free; \nX1145 is free; \nX1143 is free; \ns2t(T289, X15) !=? s2t(0, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: ','(s2t(T292, X1144), tappend(node(X1144, X1145, nil), X16, X17))\n\nT292 is ground\nX16 is free; \nX17 is free; \nX1144 is free; \nX1145 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: s2t(T292, X1144)\n\nT292 is ground\nX1144 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: tappend(node(T293, X1145, nil), X16, X17)\n\nX16 is free\nX17 is free; \nX1145 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: tappend(node(nil, X1184, nil), X16, X17)\n\nX16 is free\nX17 is free; \nX1184 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 240 [arrowhead = none ];
240 -> 2;

241 [label="ONLY EVAL with clause\ngoal(X14) :- ','(s2t(X14, X15), tappend(X15, X16, X17)).\nand substitution\nT4 -> T6\nX14 -> T6", fontsize=14, style = filled, fillcolor = white];
2 -> 241 [arrowhead = none ];
241 -> 3;

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

243 [label="EVAL with clause\ns2t(0, X22) :- ','(!_2, eq(X22, nil)).\nand substitution\nT6 -> 0\nX15 -> X23\nX22 -> X23", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 243 [arrowhead = none ];
243 -> 5;

244 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 244 [arrowhead = none ];
244 -> 6;

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

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

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

248 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 248 [arrowhead = none ];
248 -> 8;

249 [label="ONLY EVAL with clause\neq(X37, X37).\nand substitution\nX23 -> nil\nX37 -> nil\nX38 -> nil", fontsize=14, style = filled, fillcolor = white];
8 -> 249 [arrowhead = none ];
249 -> 9;

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

251 [label="ONLY EVAL with clause\ntappend(nil, X51, X52) :- ','(!_4, eq(X51, X52)).\nand substitution\nX16 -> X53\nX51 -> X53\nX17 -> X54\nX52 -> X54", fontsize=14, style = filled, fillcolor = white];
10 -> 251 [arrowhead = none ];
251 -> 11;

252 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 252 [arrowhead = none ];
252 -> 12;

253 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 253 [arrowhead = none ];
253 -> 13;

254 [label="ONLY EVAL with clause\neq(X59, X59).\nand substitution\nX53 -> X60\nX59 -> X60\nX54 -> X60", fontsize=14, style = filled, fillcolor = white];
13 -> 254 [arrowhead = none ];
254 -> 14;

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

256 [label="ONLY EVAL with clause\ns2t(X87, node(X88, X89, X88)) :- ','(p(X87, X90), s2t(X90, X88)).\nand substitution\nT6 -> T11\nX87 -> T11\nX88 -> X91\nX89 -> X92\nX15 -> node(X91, X92, X91)", fontsize=14, style = filled, fillcolor = white];
16 -> 256 [arrowhead = none ];
256 -> 18;

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

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

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

260 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T11, X15), s2t(0, X22))", fontsize=14, style = filled, fillcolor = white];
19 -> 260 [arrowhead = none ];
260 -> 20;

261 [label="EVAL with clause\np(s(X97), X97).\nand substitution\nX97 -> T14\nT11 -> s(T14)\nX90 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 261 [arrowhead = none ];
261 -> 21;

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

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

264 [label="SPLIT 2\nreplacements:\nX91 -> T15", fontsize=14, style = filled, fillcolor = violet];
21 -> 264 [arrowhead = none ];
264 -> 24;

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

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

267 [label="EVAL with clause\ns2t(0, X107) :- ','(!_7, eq(X107, nil)).\nand substitution\nT14 -> 0\nX91 -> X108\nX107 -> X108", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 267 [arrowhead = none ];
267 -> 26;

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

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

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

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

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

273 [label="ONLY EVAL with clause\neq(X114, X114).\nand substitution\nX108 -> nil\nX114 -> nil\nX115 -> nil", fontsize=14, style = filled, fillcolor = white];
29 -> 273 [arrowhead = none ];
273 -> 30;

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

275 [label="ONLY EVAL with clause\ns2t(X142, node(X143, X144, X143)) :- ','(p(X142, X145), s2t(X145, X143)).\nand substitution\nT14 -> T20\nX142 -> T20\nX143 -> X146\nX144 -> X147\nX91 -> node(X146, X147, X146)", fontsize=14, style = filled, fillcolor = white];
32 -> 275 [arrowhead = none ];
275 -> 34;

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

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

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

279 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T20, X91), s2t(0, X107))", fontsize=14, style = filled, fillcolor = white];
35 -> 279 [arrowhead = none ];
279 -> 36;

280 [label="EVAL with clause\np(s(X152), X152).\nand substitution\nX152 -> T23\nT20 -> s(T23)\nX145 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 280 [arrowhead = none ];
280 -> 37;

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

282 [label="INSTANCE with matching:\nT14 -> T23\nX91 -> X146", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 282 [arrowhead = none , style=dashed];
282 -> 23[style=dashed];

283 [label="ONLY EVAL with clause\ns2t(X182, node(nil, X183, X184)) :- ','(p(X182, X185), s2t(X185, X184)).\nand substitution\nT14 -> T28\nX182 -> T28\nX183 -> X186\nX184 -> X187\nX91 -> node(nil, X186, X187)", fontsize=14, style = filled, fillcolor = white];
39 -> 283 [arrowhead = none ];
283 -> 41;

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

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

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

287 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T28, X91), s2t(0, X107))", fontsize=14, style = filled, fillcolor = white];
42 -> 287 [arrowhead = none ];
287 -> 43;

288 [label="EVAL with clause\np(s(X192), X192).\nand substitution\nX192 -> T31\nT28 -> s(T31)\nX185 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 288 [arrowhead = none ];
288 -> 44;

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

290 [label="INSTANCE with matching:\nT14 -> T31\nX91 -> X187", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 290 [arrowhead = none , style=dashed];
290 -> 23[style=dashed];

291 [label="ONLY EVAL with clause\ns2t(X222, node(X223, X224, nil)) :- ','(p(X222, X225), s2t(X225, X223)).\nand substitution\nT14 -> T36\nX222 -> T36\nX223 -> X226\nX224 -> X227\nX91 -> node(X226, X227, nil)", fontsize=14, style = filled, fillcolor = white];
46 -> 291 [arrowhead = none ];
291 -> 48;

292 [label="ONLY EVAL with clause\ns2t(X242, node(nil, X243, nil)).\nand substitution\nT14 -> T42\nX242 -> T42\nX243 -> X244\nX91 -> node(nil, X244, nil)", fontsize=14, style = filled, fillcolor = white];
47 -> 292 [arrowhead = none ];
292 -> 53;

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

294 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T36, X91), s2t(0, X107))", fontsize=14, style = filled, fillcolor = white];
49 -> 294 [arrowhead = none ];
294 -> 50;

295 [label="EVAL with clause\np(s(X232), X232).\nand substitution\nX232 -> T39\nT36 -> s(T39)\nX225 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 295 [arrowhead = none ];
295 -> 51;

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

297 [label="INSTANCE with matching:\nT14 -> T39\nX91 -> X226", fontsize=14, style = filled, fillcolor = lightgrey];
51 -> 297 [arrowhead = none , style=dashed];
297 -> 23[style=dashed];

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

299 [label="BACKTRACK\nfor clause: tappend(nil, Y, Z) :- ','(!, eq(Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = white];
55 -> 299 [arrowhead = none ];
299 -> 56;

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

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

302 [label="ONLY EVAL with clause\ntappend(X289, X290, node(X290, X291, X292)) :- ','(left(X289, nil), ','(right(X289, X292), value(X289, X291))).\nand substitution\nT15 -> T51\nX92 -> X293\nX289 -> node(T51, X293, T51)\nX16 -> X294\nX290 -> X294\nX291 -> X295\nX292 -> X296\nX17 -> node(X294, X295, X296)\nT50 -> T51", fontsize=14, style = filled, fillcolor = white];
57 -> 302 [arrowhead = none ];
302 -> 59;

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

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

305 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 305 [arrowhead = none ];
305 -> 60;

306 [label="BACKTRACK\nfor clause: left(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
60 -> 306 [arrowhead = none ];
306 -> 61;

307 [label="EVAL with clause\nleft(node(X305, X306, X307), X305).\nand substitution\nT51 -> nil\nX305 -> nil\nX293 -> X308\nX306 -> X308\nX307 -> nil\nT54 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 307 [arrowhead = none ];
307 -> 62;

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

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

310 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
64 -> 310 [arrowhead = none ];
310 -> 65;

311 [label="ONLY EVAL with clause\nright(node(X320, X321, X322), X322).\nand substitution\nX320 -> nil\nX308 -> X323\nX321 -> X323\nX322 -> nil\nX296 -> nil", fontsize=14, style = filled, fillcolor = white];
65 -> 311 [arrowhead = none ];
311 -> 66;

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

313 [label="BACKTRACK\nfor clause: value(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
67 -> 313 [arrowhead = none ];
313 -> 68;

314 [label="ONLY EVAL with clause\nvalue(node(X332, X333, X334), X333).\nand substitution\nX332 -> nil\nX323 -> X335\nX333 -> X335\nX334 -> nil\nX295 -> X335", fontsize=14, style = filled, fillcolor = white];
68 -> 314 [arrowhead = none ];
314 -> 69;

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

316 [label="ONLY EVAL with clause\ntappend(X368, X369, node(X370, X371, X369)) :- ','(left(X368, X370), ','(right(X368, nil), value(X368, X371))).\nand substitution\nT15 -> T62\nX92 -> X372\nX368 -> node(T62, X372, T62)\nX16 -> X373\nX369 -> X373\nX370 -> X374\nX371 -> X375\nX17 -> node(X374, X375, X373)\nT61 -> T62", fontsize=14, style = filled, fillcolor = white];
71 -> 316 [arrowhead = none ];
316 -> 73;

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

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

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

320 [label="BACKTRACK\nfor clause: left(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
74 -> 320 [arrowhead = none ];
320 -> 75;

321 [label="ONLY EVAL with clause\nleft(node(X384, X385, X386), X384).\nand substitution\nT62 -> T67\nX384 -> T67\nX372 -> X387\nX385 -> X387\nX386 -> T67\nX374 -> T67\nT66 -> T67", fontsize=14, style = filled, fillcolor = white];
75 -> 321 [arrowhead = none ];
321 -> 76;

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

323 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
77 -> 323 [arrowhead = none ];
323 -> 78;

324 [label="EVAL with clause\nright(node(X396, X397, X398), X398).\nand substitution\nT67 -> nil\nX396 -> nil\nX387 -> X399\nX397 -> X399\nX398 -> nil\nT70 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 324 [arrowhead = none ];
324 -> 79;

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

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

327 [label="BACKTRACK\nfor clause: value(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
81 -> 327 [arrowhead = none ];
327 -> 82;

328 [label="ONLY EVAL with clause\nvalue(node(X411, X412, X413), X412).\nand substitution\nX411 -> nil\nX399 -> X414\nX412 -> X414\nX413 -> nil\nX375 -> X414", fontsize=14, style = filled, fillcolor = white];
82 -> 328 [arrowhead = none ];
328 -> 83;

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

330 [label="ONLY EVAL with clause\ntappend(X465, X466, node(X467, X468, X469)) :- ','(left(X465, X470), ','(right(X465, X469), ','(value(X465, X468), tappend(X470, X466, X467)))).\nand substitution\nT15 -> T78\nX92 -> X471\nX465 -> node(T78, X471, T78)\nX16 -> X472\nX466 -> X472\nX467 -> X473\nX468 -> X474\nX469 -> X475\nX17 -> node(X473, X474, X475)\nT77 -> T78", fontsize=14, style = filled, fillcolor = white];
85 -> 330 [arrowhead = none ];
330 -> 87;

331 [label="ONLY EVAL with clause\ntappend(X988, X989, node(X989, X990, X991)) :- ','(left(X988, X989), ','(right(X988, X992), ','(value(X988, X990), tappend(X992, X993, X991)))).\nand substitution\nT15 -> T259\nX92 -> X994\nX988 -> node(T259, X994, T259)\nX16 -> X995\nX989 -> X995\nX990 -> X996\nX991 -> X997\nX17 -> node(X995, X996, X997)\nT258 -> T259", fontsize=14, style = filled, fillcolor = white];
86 -> 331 [arrowhead = none ];
331 -> 211;

332 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
87 -> 332 [arrowhead = none ];
332 -> 88;

333 [label="BACKTRACK\nfor clause: left(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
88 -> 333 [arrowhead = none ];
333 -> 89;

334 [label="ONLY EVAL with clause\nleft(node(X492, X493, X494), X492).\nand substitution\nT78 -> T83\nX492 -> T83\nX471 -> X495\nX493 -> X495\nX494 -> T83\nX470 -> T83\nT82 -> T83", fontsize=14, style = filled, fillcolor = white];
89 -> 334 [arrowhead = none ];
334 -> 90;

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

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

337 [label="ONLY EVAL with clause\nright(node(X512, X513, X514), X514).\nand substitution\nT83 -> T88\nX512 -> T88\nX495 -> X515\nX513 -> X515\nX514 -> T88\nX475 -> T88\nT87 -> T88", fontsize=14, style = filled, fillcolor = white];
92 -> 337 [arrowhead = none ];
337 -> 93;

338 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
93 -> 338 [arrowhead = none ];
338 -> 94;

339 [label="BACKTRACK\nfor clause: value(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
94 -> 339 [arrowhead = none ];
339 -> 95;

340 [label="ONLY EVAL with clause\nvalue(node(X532, X533, X534), X533).\nand substitution\nT88 -> T93\nX532 -> T93\nX515 -> X535\nX533 -> X535\nX534 -> T93\nX474 -> X535\nT92 -> T93", fontsize=14, style = filled, fillcolor = white];
95 -> 340 [arrowhead = none ];
340 -> 96;

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

342 [label="EVAL with clause\ntappend(nil, X548, X549) :- ','(!_22, eq(X548, X549)).\nand substitution\nT93 -> nil\nX472 -> X550\nX548 -> X550\nX473 -> X551\nX549 -> X551", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 342 [arrowhead = none ];
342 -> 98;

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

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

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

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

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

348 [label="ONLY EVAL with clause\neq(X558, X558).\nand substitution\nX550 -> X559\nX558 -> X559\nX551 -> X559", fontsize=14, style = filled, fillcolor = white];
101 -> 348 [arrowhead = none ];
348 -> 102;

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

350 [label="ONLY EVAL with clause\ntappend(X588, X589, node(X589, X590, X591)) :- ','(left(X588, nil), ','(right(X588, X591), value(X588, X590))).\nand substitution\nT93 -> T101\nX588 -> T101\nX472 -> X592\nX589 -> X592\nX590 -> X593\nX591 -> X594\nX473 -> node(X592, X593, X594)\nT100 -> T101", fontsize=14, style = filled, fillcolor = white];
104 -> 350 [arrowhead = none ];
350 -> 106;

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

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

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

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

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

356 [label="EVAL with clause\nleft(nil, nil).\nand substitution\nT101 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 356 [arrowhead = none ];
356 -> 110;

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

358 [label="EVAL with clause\nleft(node(X607, X608, X609), X607).\nand substitution\nX607 -> nil\nX608 -> T111\nX609 -> T112\nT101 -> node(nil, T111, T112)\nT108 -> nil\nT109 -> T111\nT110 -> T112", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 358 [arrowhead = none ];
358 -> 123;

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

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

361 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 361 [arrowhead = none ];
361 -> 113;

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

363 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitution\nX594 -> nil", fontsize=14, style = filled, fillcolor = white];
113 -> 363 [arrowhead = none ];
363 -> 115;

364 [label="BACKTRACK\nfor clause: right(node(X9, X10, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = white];
114 -> 364 [arrowhead = none ];
364 -> 122;

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

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

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

368 [label="ONLY EVAL with clause\nvalue(nil, nil).\nand substitution\nX593 -> nil", fontsize=14, style = filled, fillcolor = white];
117 -> 368 [arrowhead = none ];
368 -> 119;

369 [label="BACKTRACK\nfor clause: value(node(X11, X, X12), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
118 -> 369 [arrowhead = none ];
369 -> 121;

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

371 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
123 -> 371 [arrowhead = none ];
371 -> 125;

372 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
125 -> 372 [arrowhead = none ];
372 -> 126;

373 [label="ONLY EVAL with clause\nright(node(X619, X620, X621), X621).\nand substitution\nX619 -> nil\nT111 -> T121\nX620 -> T121\nT112 -> T122\nX621 -> T122\nX594 -> T122\nT119 -> T121\nT120 -> T122", fontsize=14, style = filled, fillcolor = white];
126 -> 373 [arrowhead = none ];
373 -> 127;

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

375 [label="BACKTRACK\nfor clause: value(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
128 -> 375 [arrowhead = none ];
375 -> 129;

376 [label="ONLY EVAL with clause\nvalue(node(X628, X629, X630), X629).\nand substitution\nX628 -> nil\nT121 -> T127\nX629 -> T127\nT122 -> T128\nX630 -> T128\nX593 -> T127", fontsize=14, style = filled, fillcolor = white];
129 -> 376 [arrowhead = none ];
376 -> 130;

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

378 [label="ONLY EVAL with clause\ntappend(X659, X660, node(X661, X662, X660)) :- ','(left(X659, X661), ','(right(X659, nil), value(X659, X662))).\nand substitution\nT93 -> T136\nX659 -> T136\nX472 -> X663\nX660 -> X663\nX661 -> X664\nX662 -> X665\nX473 -> node(X664, X665, X663)\nT135 -> T136", fontsize=14, style = filled, fillcolor = white];
132 -> 378 [arrowhead = none ];
378 -> 134;

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

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

381 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
134 -> 381 [arrowhead = none ];
381 -> 135;

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

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

384 [label="EVAL with clause\nleft(nil, nil).\nand substitution\nT136 -> nil\nX664 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 384 [arrowhead = none ];
384 -> 138;

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

386 [label="EVAL with clause\nleft(node(X678, X679, X680), X678).\nand substitution\nX678 -> T146\nX679 -> T147\nX680 -> T148\nT136 -> node(T146, T147, T148)\nX664 -> T146\nT143 -> T146\nT144 -> T147\nT145 -> T148", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 386 [arrowhead = none ];
386 -> 151;

387 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 387 [arrowhead = none ];
387 -> 152;

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

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

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

391 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitution", fontsize=14, style = filled, fillcolor = white];
141 -> 391 [arrowhead = none ];
391 -> 143;

392 [label="BACKTRACK\nfor clause: right(node(X9, X10, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = white];
142 -> 392 [arrowhead = none ];
392 -> 150;

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

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

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

396 [label="ONLY EVAL with clause\nvalue(nil, nil).\nand substitution\nX665 -> nil", fontsize=14, style = filled, fillcolor = white];
145 -> 396 [arrowhead = none ];
396 -> 147;

397 [label="BACKTRACK\nfor clause: value(node(X11, X, X12), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
146 -> 397 [arrowhead = none ];
397 -> 149;

398 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 398 [arrowhead = none ];
398 -> 148;

399 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
151 -> 399 [arrowhead = none ];
399 -> 153;

400 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
153 -> 400 [arrowhead = none ];
400 -> 154;

401 [label="EVAL with clause\nright(node(X690, X691, X692), X692).\nand substitution\nT146 -> T158\nX690 -> T158\nT147 -> T159\nX691 -> T159\nT148 -> nil\nX692 -> nil\nT157 -> nil\nT155 -> T158\nT156 -> T159", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 401 [arrowhead = none ];
401 -> 155;

402 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 402 [arrowhead = none ];
402 -> 156;

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

404 [label="BACKTRACK\nfor clause: value(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
157 -> 404 [arrowhead = none ];
404 -> 158;

405 [label="ONLY EVAL with clause\nvalue(node(X702, X703, X704), X703).\nand substitution\nT158 -> T164\nX702 -> T164\nT159 -> T165\nX703 -> T165\nX704 -> nil\nX665 -> T165", fontsize=14, style = filled, fillcolor = white];
158 -> 405 [arrowhead = none ];
405 -> 159;

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

407 [label="ONLY EVAL with clause\ntappend(X751, X752, node(X753, X754, X755)) :- ','(left(X751, X756), ','(right(X751, X755), ','(value(X751, X754), tappend(X756, X752, X753)))).\nand substitution\nT93 -> T173\nX751 -> T173\nX472 -> X757\nX752 -> X757\nX753 -> X758\nX754 -> X759\nX755 -> X760\nX473 -> node(X758, X759, X760)\nT172 -> T173", fontsize=14, style = filled, fillcolor = white];
161 -> 407 [arrowhead = none ];
407 -> 163;

408 [label="ONLY EVAL with clause\ntappend(X869, X870, node(X870, X871, X872)) :- ','(left(X869, X870), ','(right(X869, X873), ','(value(X869, X871), tappend(X873, X874, X872)))).\nand substitution\nT93 -> T216\nX869 -> T216\nX472 -> X875\nX870 -> X875\nX871 -> X876\nX872 -> X877\nX473 -> node(X875, X876, X877)\nT215 -> T216", fontsize=14, style = filled, fillcolor = white];
162 -> 408 [arrowhead = none ];
408 -> 187;

409 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
163 -> 409 [arrowhead = none ];
409 -> 164;

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

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

412 [label="EVAL with clause\nleft(nil, nil).\nand substitution\nT173 -> nil\nX756 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 412 [arrowhead = none ];
412 -> 167;

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

414 [label="EVAL with clause\nleft(node(X805, X806, X807), X805).\nand substitution\nX805 -> T183\nX806 -> T184\nX807 -> T185\nT173 -> node(T183, T184, T185)\nX756 -> T183\nT180 -> T183\nT181 -> T184\nT182 -> T185", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 414 [arrowhead = none ];
414 -> 179;

415 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 415 [arrowhead = none ];
415 -> 180;

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

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

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

419 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitution\nX760 -> nil", fontsize=14, style = filled, fillcolor = white];
170 -> 419 [arrowhead = none ];
419 -> 172;

420 [label="BACKTRACK\nfor clause: right(node(X9, X10, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = white];
171 -> 420 [arrowhead = none ];
420 -> 178;

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

422 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
173 -> 422 [arrowhead = none ];
422 -> 174;

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

424 [label="ONLY EVAL with clause\nvalue(nil, nil).\nand substitution\nX759 -> nil", fontsize=14, style = filled, fillcolor = white];
174 -> 424 [arrowhead = none ];
424 -> 176;

425 [label="BACKTRACK\nfor clause: value(node(X11, X, X12), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
175 -> 425 [arrowhead = none ];
425 -> 177;

426 [label="INSTANCE with matching:\nX16 -> X757\nX17 -> X758", fontsize=14, style = filled, fillcolor = lightgrey];
176 -> 426 [arrowhead = none , style=dashed];
426 -> 9[style=dashed];

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

428 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
181 -> 428 [arrowhead = none ];
428 -> 182;

429 [label="ONLY EVAL with clause\nright(node(X825, X826, X827), X827).\nand substitution\nT183 -> T198\nX825 -> T198\nT184 -> T199\nX826 -> T199\nT185 -> T200\nX827 -> T200\nX760 -> T200\nT195 -> T198\nT196 -> T199\nT197 -> T200", fontsize=14, style = filled, fillcolor = white];
182 -> 429 [arrowhead = none ];
429 -> 183;

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

431 [label="BACKTRACK\nfor clause: value(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
184 -> 431 [arrowhead = none ];
431 -> 185;

432 [label="ONLY EVAL with clause\nvalue(node(X842, X843, X844), X843).\nand substitution\nT198 -> T211\nX842 -> T211\nT199 -> T209\nX843 -> T209\nT200 -> T210\nX844 -> T210\nX759 -> T209\nT208 -> T211", fontsize=14, style = filled, fillcolor = white];
185 -> 432 [arrowhead = none ];
432 -> 186;

433 [label="INSTANCE with matching:\nT93 -> T211\nX472 -> X757\nX473 -> X758", fontsize=14, style = filled, fillcolor = lightgrey];
186 -> 433 [arrowhead = none , style=dashed];
433 -> 96[style=dashed];

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

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

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

437 [label="EVAL with clause\nleft(nil, nil).\nand substitution\nT216 -> nil\nX875 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 437 [arrowhead = none ];
437 -> 191;

438 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 438 [arrowhead = none ];
438 -> 192;

439 [label="EVAL with clause\nleft(node(X922, X923, X924), X922).\nand substitution\nX922 -> T226\nX923 -> T227\nX924 -> T228\nT216 -> node(T226, T227, T228)\nX875 -> T226\nT223 -> T226\nT224 -> T227\nT225 -> T228", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 439 [arrowhead = none ];
439 -> 203;

440 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 440 [arrowhead = none ];
440 -> 204;

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

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

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

444 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitution\nX873 -> nil", fontsize=14, style = filled, fillcolor = white];
194 -> 444 [arrowhead = none ];
444 -> 196;

445 [label="BACKTRACK\nfor clause: right(node(X9, X10, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = white];
195 -> 445 [arrowhead = none ];
445 -> 202;

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

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

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

449 [label="ONLY EVAL with clause\nvalue(nil, nil).\nand substitution\nX876 -> nil", fontsize=14, style = filled, fillcolor = white];
198 -> 449 [arrowhead = none ];
449 -> 200;

450 [label="BACKTRACK\nfor clause: value(node(X11, X, X12), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
199 -> 450 [arrowhead = none ];
450 -> 201;

451 [label="INSTANCE with matching:\nX16 -> X874\nX17 -> X877", fontsize=14, style = filled, fillcolor = lightgrey];
200 -> 451 [arrowhead = none , style=dashed];
451 -> 9[style=dashed];

452 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
203 -> 452 [arrowhead = none ];
452 -> 205;

453 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
205 -> 453 [arrowhead = none ];
453 -> 206;

454 [label="ONLY EVAL with clause\nright(node(X942, X943, X944), X944).\nand substitution\nT226 -> T241\nX942 -> T241\nT227 -> T242\nX943 -> T242\nT228 -> T243\nX944 -> T243\nX873 -> T243\nT238 -> T241\nT239 -> T242\nT240 -> T243", fontsize=14, style = filled, fillcolor = white];
206 -> 454 [arrowhead = none ];
454 -> 207;

455 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
207 -> 455 [arrowhead = none ];
455 -> 208;

456 [label="BACKTRACK\nfor clause: value(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
208 -> 456 [arrowhead = none ];
456 -> 209;

457 [label="ONLY EVAL with clause\nvalue(node(X959, X960, X961), X960).\nand substitution\nT241 -> T251\nX959 -> T251\nT242 -> T252\nX960 -> T252\nT243 -> T254\nX961 -> T254\nX876 -> T252\nT253 -> T254", fontsize=14, style = filled, fillcolor = white];
209 -> 457 [arrowhead = none ];
457 -> 210;

458 [label="INSTANCE with matching:\nT93 -> T254\nX472 -> X874\nX473 -> X877", fontsize=14, style = filled, fillcolor = lightgrey];
210 -> 458 [arrowhead = none , style=dashed];
458 -> 96[style=dashed];

459 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
211 -> 459 [arrowhead = none ];
459 -> 212;

460 [label="BACKTRACK\nfor clause: left(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
212 -> 460 [arrowhead = none ];
460 -> 213;

461 [label="ONLY EVAL with clause\nleft(node(X1014, X1015, X1016), X1014).\nand substitution\nT259 -> T264\nX1014 -> T264\nX994 -> X1017\nX1015 -> X1017\nX1016 -> T264\nX995 -> T264\nT263 -> T264", fontsize=14, style = filled, fillcolor = white];
213 -> 461 [arrowhead = none ];
461 -> 214;

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

463 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
215 -> 463 [arrowhead = none ];
463 -> 216;

464 [label="ONLY EVAL with clause\nright(node(X1034, X1035, X1036), X1036).\nand substitution\nT264 -> T269\nX1034 -> T269\nX1017 -> X1037\nX1035 -> X1037\nX1036 -> T269\nX992 -> T269\nT268 -> T269", fontsize=14, style = filled, fillcolor = white];
216 -> 464 [arrowhead = none ];
464 -> 217;

465 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
217 -> 465 [arrowhead = none ];
465 -> 218;

466 [label="BACKTRACK\nfor clause: value(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = white];
218 -> 466 [arrowhead = none ];
466 -> 219;

467 [label="ONLY EVAL with clause\nvalue(node(X1054, X1055, X1056), X1055).\nand substitution\nT269 -> T274\nX1054 -> T274\nX1037 -> X1057\nX1055 -> X1057\nX1056 -> T274\nX996 -> X1057\nT273 -> T274", fontsize=14, style = filled, fillcolor = white];
219 -> 467 [arrowhead = none ];
467 -> 220;

468 [label="INSTANCE with matching:\nT93 -> T274\nX472 -> X993\nX473 -> X997", fontsize=14, style = filled, fillcolor = lightgrey];
220 -> 468 [arrowhead = none , style=dashed];
468 -> 96[style=dashed];

469 [label="ONLY EVAL with clause\ns2t(X1088, node(nil, X1089, X1090)) :- ','(p(X1088, X1091), s2t(X1091, X1090)).\nand substitution\nT6 -> T279\nX1088 -> T279\nX1089 -> X1092\nX1090 -> X1093\nX15 -> node(nil, X1092, X1093)", fontsize=14, style = filled, fillcolor = white];
221 -> 469 [arrowhead = none ];
469 -> 223;

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

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

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

473 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T279, X15), s2t(0, X22))", fontsize=14, style = filled, fillcolor = white];
224 -> 473 [arrowhead = none ];
473 -> 225;

474 [label="EVAL with clause\np(s(X1098), X1098).\nand substitution\nX1098 -> T282\nT279 -> s(T282)\nX1091 -> T282", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 474 [arrowhead = none ];
474 -> 226;

475 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 475 [arrowhead = none ];
475 -> 227;

476 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
226 -> 476 [arrowhead = none ];
476 -> 228;

477 [label="SPLIT 2\nreplacements:\nX1093 -> T283", fontsize=14, style = filled, fillcolor = violet];
226 -> 477 [arrowhead = none ];
477 -> 229;

478 [label="INSTANCE with matching:\nT14 -> T282\nX91 -> X1093", fontsize=14, style = filled, fillcolor = lightgrey];
228 -> 478 [arrowhead = none , style=dashed];
478 -> 23[style=dashed];

479 [label="INSTANCE with matching:\nT93 -> node(nil, X1092, T283)\nX472 -> X16\nX473 -> X17", fontsize=14, style = filled, fillcolor = lightgrey];
229 -> 479 [arrowhead = none , style=dashed];
479 -> 96[style=dashed];

480 [label="ONLY EVAL with clause\ns2t(X1140, node(X1141, X1142, nil)) :- ','(p(X1140, X1143), s2t(X1143, X1141)).\nand substitution\nT6 -> T289\nX1140 -> T289\nX1141 -> X1144\nX1142 -> X1145\nX15 -> node(X1144, X1145, nil)", fontsize=14, style = filled, fillcolor = white];
230 -> 480 [arrowhead = none ];
480 -> 232;

481 [label="ONLY EVAL with clause\ns2t(X1182, node(nil, X1183, nil)).\nand substitution\nT6 -> T297\nX1182 -> T297\nX1183 -> X1184\nX15 -> node(nil, X1184, nil)", fontsize=14, style = filled, fillcolor = white];
231 -> 481 [arrowhead = none ];
481 -> 239;

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

483 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T289, X15), s2t(0, X22))", fontsize=14, style = filled, fillcolor = white];
233 -> 483 [arrowhead = none ];
483 -> 234;

484 [label="EVAL with clause\np(s(X1150), X1150).\nand substitution\nX1150 -> T292\nT289 -> s(T292)\nX1143 -> T292", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 484 [arrowhead = none ];
484 -> 235;

485 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 485 [arrowhead = none ];
485 -> 236;

486 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
235 -> 486 [arrowhead = none ];
486 -> 237;

487 [label="SPLIT 2\nreplacements:\nX1144 -> T293", fontsize=14, style = filled, fillcolor = violet];
235 -> 487 [arrowhead = none ];
487 -> 238;

488 [label="INSTANCE with matching:\nT14 -> T292\nX91 -> X1144", fontsize=14, style = filled, fillcolor = lightgrey];
237 -> 488 [arrowhead = none , style=dashed];
488 -> 23[style=dashed];

489 [label="INSTANCE with matching:\nT93 -> node(T293, X1145, nil)\nX472 -> X16\nX473 -> X17", fontsize=14, style = filled, fillcolor = lightgrey];
238 -> 489 [arrowhead = none , style=dashed];
489 -> 96[style=dashed];

490 [label="INSTANCE with matching:\nT15 -> nil\nX92 -> X1184", fontsize=14, style = filled, fillcolor = lightgrey];
239 -> 490 [arrowhead = none , style=dashed];
490 -> 24[style=dashed];

}

(2) Obligation:

Triples:

s2t23(s(T23), node(X146, X147, X146)) :- s2t23(T23, X146).
s2t23(s(T31), node(nil, X186, X187)) :- s2t23(T31, X187).
s2t23(s(T39), node(X226, X227, nil)) :- s2t23(T39, X226).
tappend96(nil, X757, node(X758, nil, nil)) :- tappend9(X757, X758).
tappend96(node(T211, T209, T210), X757, node(X758, T209, T210)) :- tappend96(T211, X757, X758).
tappend96(nil, nil, node(nil, nil, X877)) :- tappend9(X874, X877).
tappend96(node(T251, T252, T254), T251, node(T251, T252, X877)) :- tappend96(T254, X874, X877).
tappend24(T93, X535, X472, node(X473, X535, T93)) :- tappend96(T93, X472, X473).
tappend24(T274, X1057, T274, node(T274, X1057, X997)) :- tappend96(T274, X993, X997).
goal1(0) :- tappend9(X16, X17).
goal1(s(T14)) :- s2t23(T14, X91).
goal1(s(T14)) :- ','(s2tc23(T14, T15), tappend24(T15, X92, X16, X17)).
goal1(s(T282)) :- s2t23(T282, X1093).
goal1(s(T282)) :- ','(s2tc23(T282, T283), tappend96(node(nil, X1092, T283), X16, X17)).
goal1(s(T292)) :- s2t23(T292, X1144).
goal1(s(T292)) :- ','(s2tc23(T292, T293), tappend96(node(T293, X1145, nil), X16, X17)).
goal1(T297) :- tappend24(nil, X1184, X16, X17).

Clauses:

s2tc23(0, nil).
s2tc23(s(T23), node(X146, X147, X146)) :- s2tc23(T23, X146).
s2tc23(s(T31), node(nil, X186, X187)) :- s2tc23(T31, X187).
s2tc23(s(T39), node(X226, X227, nil)) :- s2tc23(T39, X226).
s2tc23(T42, node(nil, X244, nil)).
tappendc9(X60, X60).
tappendc96(nil, X559, X559).
tappendc96(nil, X592, node(X592, nil, nil)).
tappendc96(node(nil, T127, T128), X592, node(X592, T127, T128)).
tappendc96(nil, X663, node(nil, nil, X663)).
tappendc96(node(T164, T165, nil), X663, node(T164, T165, X663)).
tappendc96(nil, X757, node(X758, nil, nil)) :- tappendc9(X757, X758).
tappendc96(node(T211, T209, T210), X757, node(X758, T209, T210)) :- tappendc96(T211, X757, X758).
tappendc96(nil, nil, node(nil, nil, X877)) :- tappendc9(X874, X877).
tappendc96(node(T251, T252, T254), T251, node(T251, T252, X877)) :- tappendc96(T254, X874, X877).
tappendc24(nil, X335, X294, node(X294, X335, nil)).
tappendc24(nil, X414, X373, node(nil, X414, X373)).
tappendc24(T93, X535, X472, node(X473, X535, T93)) :- tappendc96(T93, X472, X473).
tappendc24(T274, X1057, T274, node(T274, X1057, X997)) :- tappendc96(T274, X993, X997).

Afs:

goal1(x1) = goal1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

s2t23(s(T23), node(X146, X147, X146)) :- s2t23(T23, X146).
s2t23(s(T31), node(nil, X186, X187)) :- s2t23(T31, X187).
s2t23(s(T39), node(X226, X227, nil)) :- s2t23(T39, X226).
tappend96(node(T211, T209, T210), X757, node(X758, T209, T210)) :- tappend96(T211, X757, X758).
tappend96(node(T251, T252, T254), T251, node(T251, T252, X877)) :- tappend96(T254, X874, X877).
tappend24(T93, X535, X472, node(X473, X535, T93)) :- tappend96(T93, X472, X473).
tappend24(T274, X1057, T274, node(T274, X1057, X997)) :- tappend96(T274, X993, X997).
goal1(s(T14)) :- s2t23(T14, X91).
goal1(s(T14)) :- ','(s2tc23(T14, T15), tappend24(T15, X92, X16, X17)).
goal1(s(T282)) :- s2t23(T282, X1093).
goal1(s(T282)) :- ','(s2tc23(T282, T283), tappend96(node(nil, X1092, T283), X16, X17)).
goal1(s(T292)) :- s2t23(T292, X1144).
goal1(s(T292)) :- ','(s2tc23(T292, T293), tappend96(node(T293, X1145, nil), X16, X17)).
goal1(T297) :- tappend24(nil, X1184, X16, X17).

Clauses:

s2tc23(0, nil).
s2tc23(s(T23), node(X146, X147, X146)) :- s2tc23(T23, X146).
s2tc23(s(T31), node(nil, X186, X187)) :- s2tc23(T31, X187).
s2tc23(s(T39), node(X226, X227, nil)) :- s2tc23(T39, X226).
s2tc23(T42, node(nil, X244, nil)).
tappendc9(X60, X60).
tappendc96(nil, X559, X559).
tappendc96(nil, X592, node(X592, nil, nil)).
tappendc96(node(nil, T127, T128), X592, node(X592, T127, T128)).
tappendc96(nil, X663, node(nil, nil, X663)).
tappendc96(node(T164, T165, nil), X663, node(T164, T165, X663)).
tappendc96(nil, X757, node(X758, nil, nil)) :- tappendc9(X757, X758).
tappendc96(node(T211, T209, T210), X757, node(X758, T209, T210)) :- tappendc96(T211, X757, X758).
tappendc96(nil, nil, node(nil, nil, X877)) :- tappendc9(X874, X877).
tappendc96(node(T251, T252, T254), T251, node(T251, T252, X877)) :- tappendc96(T254, X874, X877).
tappendc24(nil, X335, X294, node(X294, X335, nil)).
tappendc24(nil, X414, X373, node(nil, X414, X373)).
tappendc24(T93, X535, X472, node(X473, X535, T93)) :- tappendc96(T93, X472, X473).
tappendc24(T274, X1057, T274, node(T274, X1057, X997)) :- tappendc96(T274, X993, X997).

Afs:

goal1(x1) = goal1(x1)

(5) 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)
s2t23_in: (b,f)
s2tc23_in: (b,f)
tappend24_in: (f,f,f,f) (b,f,f,f)
tappend96_in: (f,f,f) (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOAL1_IN_G(s(T14)) → U8_G(T14, s2t23_in_ga(T14, X91))
GOAL1_IN_G(s(T14)) → S2T23_IN_GA(T14, X91)
S2T23_IN_GA(s(T23), node(X146, X147, X146)) → U1_GA(T23, X146, X147, s2t23_in_ga(T23, X146))
S2T23_IN_GA(s(T23), node(X146, X147, X146)) → S2T23_IN_GA(T23, X146)
S2T23_IN_GA(s(T31), node(nil, X186, X187)) → U2_GA(T31, X186, X187, s2t23_in_ga(T31, X187))
S2T23_IN_GA(s(T31), node(nil, X186, X187)) → S2T23_IN_GA(T31, X187)
S2T23_IN_GA(s(T39), node(X226, X227, nil)) → U3_GA(T39, X226, X227, s2t23_in_ga(T39, X226))
S2T23_IN_GA(s(T39), node(X226, X227, nil)) → S2T23_IN_GA(T39, X226)
GOAL1_IN_G(s(T14)) → U9_G(T14, s2tc23_in_ga(T14, T15))
U9_G(T14, s2tc23_out_ga(T14, T15)) → U10_G(T14, tappend24_in_aaaa(T15, X92, X16, X17))
U9_G(T14, s2tc23_out_ga(T14, T15)) → TAPPEND24_IN_AAAA(T15, X92, X16, X17)
TAPPEND24_IN_AAAA(T93, X535, X472, node(X473, X535, T93)) → U6_AAAA(T93, X535, X472, X473, tappend96_in_aaa(T93, X472, X473))
TAPPEND24_IN_AAAA(T93, X535, X472, node(X473, X535, T93)) → TAPPEND96_IN_AAA(T93, X472, X473)
TAPPEND96_IN_AAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → U4_AAA(T211, T209, T210, X757, X758, tappend96_in_aaa(T211, X757, X758))
TAPPEND96_IN_AAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → TAPPEND96_IN_AAA(T211, X757, X758)
TAPPEND96_IN_AAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → U5_AAA(T251, T252, T254, X877, tappend96_in_aaa(T254, X874, X877))
TAPPEND96_IN_AAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → TAPPEND96_IN_AAA(T254, X874, X877)
TAPPEND24_IN_AAAA(T274, X1057, T274, node(T274, X1057, X997)) → U7_AAAA(T274, X1057, X997, tappend96_in_aaa(T274, X993, X997))
TAPPEND24_IN_AAAA(T274, X1057, T274, node(T274, X1057, X997)) → TAPPEND96_IN_AAA(T274, X993, X997)
GOAL1_IN_G(s(T282)) → U11_G(T282, s2t23_in_ga(T282, X1093))
GOAL1_IN_G(s(T282)) → U12_G(T282, s2tc23_in_ga(T282, T283))
U12_G(T282, s2tc23_out_ga(T282, T283)) → U13_G(T282, tappend96_in_aaa(node(nil, X1092, T283), X16, X17))
U12_G(T282, s2tc23_out_ga(T282, T283)) → TAPPEND96_IN_AAA(node(nil, X1092, T283), X16, X17)
GOAL1_IN_G(s(T292)) → U14_G(T292, s2t23_in_ga(T292, X1144))
GOAL1_IN_G(s(T292)) → U15_G(T292, s2tc23_in_ga(T292, T293))
U15_G(T292, s2tc23_out_ga(T292, T293)) → U16_G(T292, tappend96_in_aaa(node(T293, X1145, nil), X16, X17))
U15_G(T292, s2tc23_out_ga(T292, T293)) → TAPPEND96_IN_AAA(node(T293, X1145, nil), X16, X17)
GOAL1_IN_G(T297) → U17_G(T297, tappend24_in_gaaa(nil, X1184, X16, X17))
GOAL1_IN_G(T297) → TAPPEND24_IN_GAAA(nil, X1184, X16, X17)
TAPPEND24_IN_GAAA(T93, X535, X472, node(X473, X535, T93)) → U6_GAAA(T93, X535, X472, X473, tappend96_in_gaa(T93, X472, X473))
TAPPEND24_IN_GAAA(T93, X535, X472, node(X473, X535, T93)) → TAPPEND96_IN_GAA(T93, X472, X473)
TAPPEND96_IN_GAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → U4_GAA(T211, T209, T210, X757, X758, tappend96_in_gaa(T211, X757, X758))
TAPPEND96_IN_GAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → TAPPEND96_IN_GAA(T211, X757, X758)
TAPPEND96_IN_GAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → U5_GAA(T251, T252, T254, X877, tappend96_in_gaa(T254, X874, X877))
TAPPEND96_IN_GAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → TAPPEND96_IN_GAA(T254, X874, X877)
TAPPEND24_IN_GAAA(T274, X1057, T274, node(T274, X1057, X997)) → U7_GAAA(T274, X1057, X997, tappend96_in_gaa(T274, X993, X997))
TAPPEND24_IN_GAAA(T274, X1057, T274, node(T274, X1057, X997)) → TAPPEND96_IN_GAA(T274, X993, X997)

The TRS R consists of the following rules:

s2tc23_in_ga(0, nil) → s2tc23_out_ga(0, nil)
s2tc23_in_ga(s(T23), node(X146, X147, X146)) → U19_ga(T23, X146, X147, s2tc23_in_ga(T23, X146))
s2tc23_in_ga(s(T31), node(nil, X186, X187)) → U20_ga(T31, X186, X187, s2tc23_in_ga(T31, X187))
s2tc23_in_ga(s(T39), node(X226, X227, nil)) → U21_ga(T39, X226, X227, s2tc23_in_ga(T39, X226))
s2tc23_in_ga(T42, node(nil, X244, nil)) → s2tc23_out_ga(T42, node(nil, X244, nil))
U21_ga(T39, X226, X227, s2tc23_out_ga(T39, X226)) → s2tc23_out_ga(s(T39), node(X226, X227, nil))
U20_ga(T31, X186, X187, s2tc23_out_ga(T31, X187)) → s2tc23_out_ga(s(T31), node(nil, X186, X187))
U19_ga(T23, X146, X147, s2tc23_out_ga(T23, X146)) → s2tc23_out_ga(s(T23), node(X146, X147, X146))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
s2t23_in_ga(x1, x2) = s2t23_in_ga(x1)
s2tc23_in_ga(x1, x2) = s2tc23_in_ga(x1)
0 = 0
s2tc23_out_ga(x1, x2) = s2tc23_out_ga(x1)
U19_ga(x1, x2, x3, x4) = U19_ga(x1, x4)
U20_ga(x1, x2, x3, x4) = U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4) = U21_ga(x1, x4)
tappend24_in_aaaa(x1, x2, x3, x4) = tappend24_in_aaaa
tappend96_in_aaa(x1, x2, x3) = tappend96_in_aaa
tappend24_in_gaaa(x1, x2, x3, x4) = tappend24_in_gaaa(x1)
tappend96_in_gaa(x1, x2, x3) = tappend96_in_gaa(x1)
node(x1, x2, x3) = node(x1, x2, x3)
nil = nil
GOAL1_IN_G(x1) = GOAL1_IN_G(x1)
U8_G(x1, x2) = U8_G(x1, x2)
S2T23_IN_GA(x1, x2) = S2T23_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)
U9_G(x1, x2) = U9_G(x1, x2)
U10_G(x1, x2) = U10_G(x1, x2)
TAPPEND24_IN_AAAA(x1, x2, x3, x4) = TAPPEND24_IN_AAAA
U6_AAAA(x1, x2, x3, x4, x5) = U6_AAAA(x5)
TAPPEND96_IN_AAA(x1, x2, x3) = TAPPEND96_IN_AAA
U4_AAA(x1, x2, x3, x4, x5, x6) = U4_AAA(x6)
U5_AAA(x1, x2, x3, x4, x5) = U5_AAA(x5)
U7_AAAA(x1, x2, x3, x4) = U7_AAAA(x4)
U11_G(x1, x2) = U11_G(x1, x2)
U12_G(x1, x2) = U12_G(x1, x2)
U13_G(x1, x2) = U13_G(x1, x2)
U14_G(x1, x2) = U14_G(x1, x2)
U15_G(x1, x2) = U15_G(x1, x2)
U16_G(x1, x2) = U16_G(x1, x2)
U17_G(x1, x2) = U17_G(x1, x2)
TAPPEND24_IN_GAAA(x1, x2, x3, x4) = TAPPEND24_IN_GAAA(x1)
U6_GAAA(x1, x2, x3, x4, x5) = U6_GAAA(x1, x5)
TAPPEND96_IN_GAA(x1, x2, x3) = TAPPEND96_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5, x6) = U4_GAA(x1, x2, x3, x6)
U5_GAA(x1, x2, x3, x4, x5) = U5_GAA(x1, x2, x3, x5)
U7_GAAA(x1, x2, x3, x4) = U7_GAAA(x1, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

GOAL1_IN_G(s(T14)) → U8_G(T14, s2t23_in_ga(T14, X91))
GOAL1_IN_G(s(T14)) → S2T23_IN_GA(T14, X91)
S2T23_IN_GA(s(T23), node(X146, X147, X146)) → U1_GA(T23, X146, X147, s2t23_in_ga(T23, X146))
S2T23_IN_GA(s(T23), node(X146, X147, X146)) → S2T23_IN_GA(T23, X146)
S2T23_IN_GA(s(T31), node(nil, X186, X187)) → U2_GA(T31, X186, X187, s2t23_in_ga(T31, X187))
S2T23_IN_GA(s(T31), node(nil, X186, X187)) → S2T23_IN_GA(T31, X187)
S2T23_IN_GA(s(T39), node(X226, X227, nil)) → U3_GA(T39, X226, X227, s2t23_in_ga(T39, X226))
S2T23_IN_GA(s(T39), node(X226, X227, nil)) → S2T23_IN_GA(T39, X226)
GOAL1_IN_G(s(T14)) → U9_G(T14, s2tc23_in_ga(T14, T15))
U9_G(T14, s2tc23_out_ga(T14, T15)) → U10_G(T14, tappend24_in_aaaa(T15, X92, X16, X17))
U9_G(T14, s2tc23_out_ga(T14, T15)) → TAPPEND24_IN_AAAA(T15, X92, X16, X17)
TAPPEND24_IN_AAAA(T93, X535, X472, node(X473, X535, T93)) → U6_AAAA(T93, X535, X472, X473, tappend96_in_aaa(T93, X472, X473))
TAPPEND24_IN_AAAA(T93, X535, X472, node(X473, X535, T93)) → TAPPEND96_IN_AAA(T93, X472, X473)
TAPPEND96_IN_AAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → U4_AAA(T211, T209, T210, X757, X758, tappend96_in_aaa(T211, X757, X758))
TAPPEND96_IN_AAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → TAPPEND96_IN_AAA(T211, X757, X758)
TAPPEND96_IN_AAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → U5_AAA(T251, T252, T254, X877, tappend96_in_aaa(T254, X874, X877))
TAPPEND96_IN_AAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → TAPPEND96_IN_AAA(T254, X874, X877)
TAPPEND24_IN_AAAA(T274, X1057, T274, node(T274, X1057, X997)) → U7_AAAA(T274, X1057, X997, tappend96_in_aaa(T274, X993, X997))
TAPPEND24_IN_AAAA(T274, X1057, T274, node(T274, X1057, X997)) → TAPPEND96_IN_AAA(T274, X993, X997)
GOAL1_IN_G(s(T282)) → U11_G(T282, s2t23_in_ga(T282, X1093))
GOAL1_IN_G(s(T282)) → U12_G(T282, s2tc23_in_ga(T282, T283))
U12_G(T282, s2tc23_out_ga(T282, T283)) → U13_G(T282, tappend96_in_aaa(node(nil, X1092, T283), X16, X17))
U12_G(T282, s2tc23_out_ga(T282, T283)) → TAPPEND96_IN_AAA(node(nil, X1092, T283), X16, X17)
GOAL1_IN_G(s(T292)) → U14_G(T292, s2t23_in_ga(T292, X1144))
GOAL1_IN_G(s(T292)) → U15_G(T292, s2tc23_in_ga(T292, T293))
U15_G(T292, s2tc23_out_ga(T292, T293)) → U16_G(T292, tappend96_in_aaa(node(T293, X1145, nil), X16, X17))
U15_G(T292, s2tc23_out_ga(T292, T293)) → TAPPEND96_IN_AAA(node(T293, X1145, nil), X16, X17)
GOAL1_IN_G(T297) → U17_G(T297, tappend24_in_gaaa(nil, X1184, X16, X17))
GOAL1_IN_G(T297) → TAPPEND24_IN_GAAA(nil, X1184, X16, X17)
TAPPEND24_IN_GAAA(T93, X535, X472, node(X473, X535, T93)) → U6_GAAA(T93, X535, X472, X473, tappend96_in_gaa(T93, X472, X473))
TAPPEND24_IN_GAAA(T93, X535, X472, node(X473, X535, T93)) → TAPPEND96_IN_GAA(T93, X472, X473)
TAPPEND96_IN_GAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → U4_GAA(T211, T209, T210, X757, X758, tappend96_in_gaa(T211, X757, X758))
TAPPEND96_IN_GAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → TAPPEND96_IN_GAA(T211, X757, X758)
TAPPEND96_IN_GAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → U5_GAA(T251, T252, T254, X877, tappend96_in_gaa(T254, X874, X877))
TAPPEND96_IN_GAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → TAPPEND96_IN_GAA(T254, X874, X877)
TAPPEND24_IN_GAAA(T274, X1057, T274, node(T274, X1057, X997)) → U7_GAAA(T274, X1057, X997, tappend96_in_gaa(T274, X993, X997))
TAPPEND24_IN_GAAA(T274, X1057, T274, node(T274, X1057, X997)) → TAPPEND96_IN_GAA(T274, X993, X997)

The TRS R consists of the following rules:

s2tc23_in_ga(0, nil) → s2tc23_out_ga(0, nil)
s2tc23_in_ga(s(T23), node(X146, X147, X146)) → U19_ga(T23, X146, X147, s2tc23_in_ga(T23, X146))
s2tc23_in_ga(s(T31), node(nil, X186, X187)) → U20_ga(T31, X186, X187, s2tc23_in_ga(T31, X187))
s2tc23_in_ga(s(T39), node(X226, X227, nil)) → U21_ga(T39, X226, X227, s2tc23_in_ga(T39, X226))
s2tc23_in_ga(T42, node(nil, X244, nil)) → s2tc23_out_ga(T42, node(nil, X244, nil))
U21_ga(T39, X226, X227, s2tc23_out_ga(T39, X226)) → s2tc23_out_ga(s(T39), node(X226, X227, nil))
U20_ga(T31, X186, X187, s2tc23_out_ga(T31, X187)) → s2tc23_out_ga(s(T31), node(nil, X186, X187))
U19_ga(T23, X146, X147, s2tc23_out_ga(T23, X146)) → s2tc23_out_ga(s(T23), node(X146, X147, X146))

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

TAPPEND96_IN_GAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → TAPPEND96_IN_GAA(T254, X874, X877)
TAPPEND96_IN_GAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → TAPPEND96_IN_GAA(T211, X757, X758)

The TRS R consists of the following rules:

s2tc23_in_ga(0, nil) → s2tc23_out_ga(0, nil)
s2tc23_in_ga(s(T23), node(X146, X147, X146)) → U19_ga(T23, X146, X147, s2tc23_in_ga(T23, X146))
s2tc23_in_ga(s(T31), node(nil, X186, X187)) → U20_ga(T31, X186, X187, s2tc23_in_ga(T31, X187))
s2tc23_in_ga(s(T39), node(X226, X227, nil)) → U21_ga(T39, X226, X227, s2tc23_in_ga(T39, X226))
s2tc23_in_ga(T42, node(nil, X244, nil)) → s2tc23_out_ga(T42, node(nil, X244, nil))
U21_ga(T39, X226, X227, s2tc23_out_ga(T39, X226)) → s2tc23_out_ga(s(T39), node(X226, X227, nil))
U20_ga(T31, X186, X187, s2tc23_out_ga(T31, X187)) → s2tc23_out_ga(s(T31), node(nil, X186, X187))
U19_ga(T23, X146, X147, s2tc23_out_ga(T23, X146)) → s2tc23_out_ga(s(T23), node(X146, X147, X146))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
s2tc23_in_ga(x1, x2) = s2tc23_in_ga(x1)
0 = 0
s2tc23_out_ga(x1, x2) = s2tc23_out_ga(x1)
U19_ga(x1, x2, x3, x4) = U19_ga(x1, x4)
U20_ga(x1, x2, x3, x4) = U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4) = U21_ga(x1, x4)
node(x1, x2, x3) = node(x1, x2, x3)
nil = nil
TAPPEND96_IN_GAA(x1, x2, x3) = TAPPEND96_IN_GAA(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

TAPPEND96_IN_GAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → TAPPEND96_IN_GAA(T254, X874, X877)
TAPPEND96_IN_GAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → TAPPEND96_IN_GAA(T211, X757, X758)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

TAPPEND96_IN_GAA(node(T251, T252, T254)) → TAPPEND96_IN_GAA(T254)
TAPPEND96_IN_GAA(node(T211, T209, T210)) → TAPPEND96_IN_GAA(T211)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

TAPPEND96_IN_GAA(node(T251, T252, T254)) → TAPPEND96_IN_GAA(T254)
The graph contains the following edges 1 > 1
TAPPEND96_IN_GAA(node(T211, T209, T210)) → TAPPEND96_IN_GAA(T211)
The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

TAPPEND96_IN_AAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → TAPPEND96_IN_AAA(T254, X874, X877)
TAPPEND96_IN_AAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → TAPPEND96_IN_AAA(T211, X757, X758)

The TRS R consists of the following rules:

s2tc23_in_ga(0, nil) → s2tc23_out_ga(0, nil)
s2tc23_in_ga(s(T23), node(X146, X147, X146)) → U19_ga(T23, X146, X147, s2tc23_in_ga(T23, X146))
s2tc23_in_ga(s(T31), node(nil, X186, X187)) → U20_ga(T31, X186, X187, s2tc23_in_ga(T31, X187))
s2tc23_in_ga(s(T39), node(X226, X227, nil)) → U21_ga(T39, X226, X227, s2tc23_in_ga(T39, X226))
s2tc23_in_ga(T42, node(nil, X244, nil)) → s2tc23_out_ga(T42, node(nil, X244, nil))
U21_ga(T39, X226, X227, s2tc23_out_ga(T39, X226)) → s2tc23_out_ga(s(T39), node(X226, X227, nil))
U20_ga(T31, X186, X187, s2tc23_out_ga(T31, X187)) → s2tc23_out_ga(s(T31), node(nil, X186, X187))
U19_ga(T23, X146, X147, s2tc23_out_ga(T23, X146)) → s2tc23_out_ga(s(T23), node(X146, X147, X146))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
s2tc23_in_ga(x1, x2) = s2tc23_in_ga(x1)
0 = 0
s2tc23_out_ga(x1, x2) = s2tc23_out_ga(x1)
U19_ga(x1, x2, x3, x4) = U19_ga(x1, x4)
U20_ga(x1, x2, x3, x4) = U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4) = U21_ga(x1, x4)
node(x1, x2, x3) = node(x1, x2, x3)
nil = nil
TAPPEND96_IN_AAA(x1, x2, x3) = TAPPEND96_IN_AAA

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

TAPPEND96_IN_AAA(node(T251, T252, T254), T251, node(T251, T252, X877)) → TAPPEND96_IN_AAA(T254, X874, X877)
TAPPEND96_IN_AAA(node(T211, T209, T210), X757, node(X758, T209, T210)) → TAPPEND96_IN_AAA(T211, X757, X758)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

TAPPEND96_IN_AAA → TAPPEND96_IN_AAA

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

(21) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = TAPPEND96_IN_AAA evaluates to t =TAPPEND96_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from TAPPEND96_IN_AAA to TAPPEND96_IN_AAA.

(22) NO

(23) Obligation:

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

S2T23_IN_GA(s(T31), node(nil, X186, X187)) → S2T23_IN_GA(T31, X187)
S2T23_IN_GA(s(T23), node(X146, X147, X146)) → S2T23_IN_GA(T23, X146)
S2T23_IN_GA(s(T39), node(X226, X227, nil)) → S2T23_IN_GA(T39, X226)

The TRS R consists of the following rules:

s2tc23_in_ga(0, nil) → s2tc23_out_ga(0, nil)
s2tc23_in_ga(s(T23), node(X146, X147, X146)) → U19_ga(T23, X146, X147, s2tc23_in_ga(T23, X146))
s2tc23_in_ga(s(T31), node(nil, X186, X187)) → U20_ga(T31, X186, X187, s2tc23_in_ga(T31, X187))
s2tc23_in_ga(s(T39), node(X226, X227, nil)) → U21_ga(T39, X226, X227, s2tc23_in_ga(T39, X226))
s2tc23_in_ga(T42, node(nil, X244, nil)) → s2tc23_out_ga(T42, node(nil, X244, nil))
U21_ga(T39, X226, X227, s2tc23_out_ga(T39, X226)) → s2tc23_out_ga(s(T39), node(X226, X227, nil))
U20_ga(T31, X186, X187, s2tc23_out_ga(T31, X187)) → s2tc23_out_ga(s(T31), node(nil, X186, X187))
U19_ga(T23, X146, X147, s2tc23_out_ga(T23, X146)) → s2tc23_out_ga(s(T23), node(X146, X147, X146))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
s2tc23_in_ga(x1, x2) = s2tc23_in_ga(x1)
0 = 0
s2tc23_out_ga(x1, x2) = s2tc23_out_ga(x1)
U19_ga(x1, x2, x3, x4) = U19_ga(x1, x4)
U20_ga(x1, x2, x3, x4) = U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4) = U21_ga(x1, x4)
node(x1, x2, x3) = node(x1, x2, x3)
nil = nil
S2T23_IN_GA(x1, x2) = S2T23_IN_GA(x1)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

S2T23_IN_GA(s(T31), node(nil, X186, X187)) → S2T23_IN_GA(T31, X187)
S2T23_IN_GA(s(T23), node(X146, X147, X146)) → S2T23_IN_GA(T23, X146)
S2T23_IN_GA(s(T39), node(X226, X227, nil)) → S2T23_IN_GA(T39, X226)

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

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

S2T23_IN_GA(s(T31)) → S2T23_IN_GA(T31)

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

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

S2T23_IN_GA(s(T31)) → S2T23_IN_GA(T31)
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

(4) Obligation:

(5) TriplesToPiDPProof (SOUND transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) NonTerminationProof (EQUIVALENT transformation)

(22) NO

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) QDPSizeChangeProof (EQUIVALENT transformation)

(29) YES