Left Termination proof of /tmp/tmpoBcGNB/btree.pl

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 UndefinedPredicateInTriplesTransformerProof (⇐)

↳4 TRIPLES

↳5 TriplesToPiDPProof (⇐)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 PiDP

↳9 PiDPToQDPProof (⇐)

↳10 QDP

↳11 QDPSizeChangeProof (⇔)

↳12 YES

(0) Obligation:

Clauses:

goal(X) :- ','(s2t(X, T), tree(T)).
tree(nil) :- !.
tree(X) :- ','(left(T, L), ','(right(T, R), ','(tree(L), tree(R)))).
s2t(0, L) :- ','(!, eq(L, nil)).
s2t(X, node(T, X1, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X2, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(T, X3, nil)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X4, nil)).
left(nil, nil).
left(node(L, X5, X6), L).
right(nil, nil).
right(node(X7, X8, R), R).
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(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: goal(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(s2t(T3, X11), tree(X11))\n\nT3 is ground\nX11 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 3 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 4 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX11 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(!_2, ','(eq(X17, nil), tree(X17))) | ','(s2t(0, X11), tree(X11)), SCOPE: 2, CLAUSE: 4 | ','(s2t(0, X11), tree(X11)), SCOPE: 2, CLAUSE: 5 | ','(s2t(0, X11), tree(X11)), SCOPE: 2, CLAUSE: 6 | ','(s2t(0, X11), tree(X11)), SCOPE: 2, CLAUSE: 7\n\nX11 is free\nX17 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 4 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX11 is free; \ns2t(T3, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(eq(X17, nil), tree(X17))\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(eq(X17, nil), tree(X17)), SCOPE: 3, CLAUSE: 14\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: tree(nil), SCOPE: 4, CLAUSE: 1 | tree(nil), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: !_4 | tree(nil), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX11 is free; \ns2t(T3, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX11 is free; \ns2t(T3, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(p(T8, X54), ','(s2t(X54, X55), tree(node(X55, X56, X55))))\n\nT8 is ground\nX55 is free; \nX56 is free; \nX54 is free; \ns2t(T8, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(p(T8, X54), ','(s2t(X54, X55), tree(node(X55, X56, X55)))), SCOPE: 5, CLAUSE: 12 | ','(p(T8, X54), ','(s2t(X54, X55), tree(node(X55, X56, X55)))), SCOPE: 5, CLAUSE: 13\n\nT8 is ground\nX55 is free; \nX56 is free; \nX54 is free; \ns2t(T8, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(p(T8, X54), ','(s2t(X54, X55), tree(node(X55, X56, X55)))), SCOPE: 5, CLAUSE: 13\n\nT8 is ground\nX55 is free; \nX56 is free; \nX54 is free; \ns2t(T8, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(s2t(T11, X55), tree(node(X55, X56, X55)))\n\nT11 is ground\nX55 is free; \nX56 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: s2t(T11, X55)\n\nT11 is ground\nX55 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: tree(node(T12, X56, T12))\n\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: s2t(T11, X55), SCOPE: 6, CLAUSE: 3 | s2t(T11, X55), SCOPE: 6, CLAUSE: 4 | s2t(T11, X55), SCOPE: 6, CLAUSE: 5 | s2t(T11, X55), SCOPE: 6, CLAUSE: 6 | s2t(T11, X55), SCOPE: 6, CLAUSE: 7\n\nT11 is ground\nX55 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(!_6, eq(X72, nil)) | s2t(0, X55), SCOPE: 6, CLAUSE: 4 | s2t(0, X55), SCOPE: 6, CLAUSE: 5 | s2t(0, X55), SCOPE: 6, CLAUSE: 6 | s2t(0, X55), SCOPE: 6, CLAUSE: 7\n\nX55 is free\nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: s2t(T11, X55), SCOPE: 6, CLAUSE: 4 | s2t(T11, X55), SCOPE: 6, CLAUSE: 5 | s2t(T11, X55), SCOPE: 6, CLAUSE: 6 | s2t(T11, X55), SCOPE: 6, CLAUSE: 7\n\nT11 is ground\nX55 is free; \ns2t(T11, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: eq(X72, nil)\n\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: eq(X72, nil), SCOPE: 7, CLAUSE: 14\n\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: s2t(T11, X55), SCOPE: 6, CLAUSE: 4\n\nT11 is ground\nX55 is free; \ns2t(T11, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: s2t(T11, X55), SCOPE: 6, CLAUSE: 5 | s2t(T11, X55), SCOPE: 6, CLAUSE: 6 | s2t(T11, X55), SCOPE: 6, CLAUSE: 7\n\nT11 is ground\nX55 is free; \ns2t(T11, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(p(T17, X109), s2t(X109, X110))\n\nT17 is ground\nX110 is free; \nX109 is free; \ns2t(T17, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(p(T17, X109), s2t(X109, X110)), SCOPE: 8, CLAUSE: 12 | ','(p(T17, X109), s2t(X109, X110)), SCOPE: 8, CLAUSE: 13\n\nT17 is ground\nX110 is free; \nX109 is free; \ns2t(T17, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(p(T17, X109), s2t(X109, X110)), SCOPE: 8, CLAUSE: 13\n\nT17 is ground\nX110 is free; \nX109 is free; \ns2t(T17, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: s2t(T20, X110)\n\nT20 is ground\nX110 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: s2t(T11, X55), SCOPE: 6, CLAUSE: 5\n\nT11 is ground\nX55 is free; \ns2t(T11, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: s2t(T11, X55), SCOPE: 6, CLAUSE: 6 | s2t(T11, X55), SCOPE: 6, CLAUSE: 7\n\nT11 is ground\nX55 is free; \ns2t(T11, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(p(T25, X149), s2t(X149, X151))\n\nT25 is ground\nX151 is free; \nX149 is free; \ns2t(T25, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(p(T25, X149), s2t(X149, X151)), SCOPE: 9, CLAUSE: 12 | ','(p(T25, X149), s2t(X149, X151)), SCOPE: 9, CLAUSE: 13\n\nT25 is ground\nX151 is free; \nX149 is free; \ns2t(T25, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(p(T25, X149), s2t(X149, X151)), SCOPE: 9, CLAUSE: 13\n\nT25 is ground\nX151 is free; \nX149 is free; \ns2t(T25, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: s2t(T28, X151)\n\nT28 is ground\nX151 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: s2t(T11, X55), SCOPE: 6, CLAUSE: 6\n\nT11 is ground\nX55 is free; \ns2t(T11, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: s2t(T11, X55), SCOPE: 6, CLAUSE: 7\n\nT11 is ground\nX55 is free; \ns2t(T11, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(p(T33, X189), s2t(X189, X190))\n\nT33 is ground\nX190 is free; \nX189 is free; \ns2t(T33, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(p(T33, X189), s2t(X189, X190)), SCOPE: 10, CLAUSE: 12 | ','(p(T33, X189), s2t(X189, X190)), SCOPE: 10, CLAUSE: 13\n\nT33 is ground\nX190 is free; \nX189 is free; \ns2t(T33, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(p(T33, X189), s2t(X189, X190)), SCOPE: 10, CLAUSE: 13\n\nT33 is ground\nX190 is free; \nX189 is free; \ns2t(T33, X55) !=? s2t(0, X71)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: s2t(T36, X190)\n\nT36 is ground\nX190 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: tree(node(T12, X56, T12)), SCOPE: 11, CLAUSE: 1 | tree(node(T12, X56, T12)), SCOPE: 11, CLAUSE: 2\n\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: tree(node(T12, X56, T12)), SCOPE: 11, CLAUSE: 2\n\nX56 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(left(X222, X223), ','(right(X222, X224), ','(tree(X223), tree(X224))))\n\nX222 is free\nX223 is free; \nX224 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(left(X222, X223), ','(right(X222, X224), ','(tree(X223), tree(X224)))), SCOPE: 12, CLAUSE: 8 | ','(left(X222, X223), ','(right(X222, X224), ','(tree(X223), tree(X224)))), SCOPE: 12, CLAUSE: 9\n\nX222 is free\nX223 is free; \nX224 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(left(X222, X223), ','(right(X222, X224), ','(tree(X223), tree(X224)))), SCOPE: 12, CLAUSE: 8\n\nX222 is free\nX223 is free; \nX224 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(left(X222, X223), ','(right(X222, X224), ','(tree(X223), tree(X224)))), SCOPE: 12, CLAUSE: 9\n\nX222 is free\nX223 is free; \nX224 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(right(nil, X224), ','(tree(nil), tree(X224)))\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(right(nil, X224), ','(tree(nil), tree(X224))), SCOPE: 13, CLAUSE: 10 | ','(right(nil, X224), ','(tree(nil), tree(X224))), SCOPE: 13, CLAUSE: 11\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(right(nil, X224), ','(tree(nil), tree(X224))), SCOPE: 13, CLAUSE: 10\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(right(nil, X224), ','(tree(nil), tree(X224))), SCOPE: 13, CLAUSE: 11\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(right(node(X244, X245, X246), X224), ','(tree(X244), tree(X224)))\n\nX224 is free\nX244 is free; \nX245 is free; \nX246 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(right(node(X244, X245, X246), X224), ','(tree(X244), tree(X224))), SCOPE: 14, CLAUSE: 10 | ','(right(node(X244, X245, X246), X224), ','(tree(X244), tree(X224))), SCOPE: 14, CLAUSE: 11\n\nX224 is free\nX244 is free; \nX245 is free; \nX246 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(right(node(X244, X245, X246), X224), ','(tree(X244), tree(X224))), SCOPE: 14, CLAUSE: 11\n\nX224 is free\nX244 is free; \nX245 is free; \nX246 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(tree(X262), tree(X264))\n\nX262 is free\nX264 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: tree(X262)\n\nX262 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: tree(X264)\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: tree(X264), SCOPE: 15, CLAUSE: 1 | tree(X264), SCOPE: 15, CLAUSE: 2\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: !_15 | tree(X264), SCOPE: 15, CLAUSE: 2\n\nX264 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 5\n\nT3 is ground\nX11 is free; \ns2t(T3, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX11 is free; \ns2t(T3, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(p(T49, X294), ','(s2t(X294, X296), tree(node(nil, X295, X296))))\n\nT49 is ground\nX295 is free; \nX296 is free; \nX294 is free; \ns2t(T49, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(p(T49, X294), ','(s2t(X294, X296), tree(node(nil, X295, X296)))), SCOPE: 16, CLAUSE: 12 | ','(p(T49, X294), ','(s2t(X294, X296), tree(node(nil, X295, X296)))), SCOPE: 16, CLAUSE: 13\n\nT49 is ground\nX295 is free; \nX296 is free; \nX294 is free; \ns2t(T49, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(p(T49, X294), ','(s2t(X294, X296), tree(node(nil, X295, X296)))), SCOPE: 16, CLAUSE: 13\n\nT49 is ground\nX295 is free; \nX296 is free; \nX294 is free; \ns2t(T49, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(s2t(T52, X296), tree(node(nil, X295, X296)))\n\nT52 is ground\nX295 is free; \nX296 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: s2t(T52, X296)\n\nT52 is ground\nX296 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: tree(node(nil, X295, T53))\n\nX295 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: tree(node(nil, X295, T53)), SCOPE: 17, CLAUSE: 1 | tree(node(nil, X295, T53)), SCOPE: 17, CLAUSE: 2\n\nX295 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: tree(node(nil, X295, T53)), SCOPE: 17, CLAUSE: 2\n\nX295 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(left(X320, X321), ','(right(X320, X322), ','(tree(X321), tree(X322))))\n\nX320 is free\nX321 is free; \nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(left(X320, X321), ','(right(X320, X322), ','(tree(X321), tree(X322)))), SCOPE: 18, CLAUSE: 8 | ','(left(X320, X321), ','(right(X320, X322), ','(tree(X321), tree(X322)))), SCOPE: 18, CLAUSE: 9\n\nX320 is free\nX321 is free; \nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(left(X320, X321), ','(right(X320, X322), ','(tree(X321), tree(X322)))), SCOPE: 18, CLAUSE: 8\n\nX320 is free\nX321 is free; \nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(left(X320, X321), ','(right(X320, X322), ','(tree(X321), tree(X322)))), SCOPE: 18, CLAUSE: 9\n\nX320 is free\nX321 is free; \nX322 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(right(nil, X322), ','(tree(nil), tree(X322)))\n\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(right(nil, X322), ','(tree(nil), tree(X322))), SCOPE: 19, CLAUSE: 10 | ','(right(nil, X322), ','(tree(nil), tree(X322))), SCOPE: 19, CLAUSE: 11\n\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(right(nil, X322), ','(tree(nil), tree(X322))), SCOPE: 19, CLAUSE: 10\n\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(right(nil, X322), ','(tree(nil), tree(X322))), SCOPE: 19, CLAUSE: 11\n\nX322 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(right(node(X342, X343, X344), X322), ','(tree(X342), tree(X322)))\n\nX322 is free\nX342 is free; \nX343 is free; \nX344 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(right(node(X342, X343, X344), X322), ','(tree(X342), tree(X322))), SCOPE: 20, CLAUSE: 10 | ','(right(node(X342, X343, X344), X322), ','(tree(X342), tree(X322))), SCOPE: 20, CLAUSE: 11\n\nX322 is free\nX342 is free; \nX343 is free; \nX344 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(right(node(X342, X343, X344), X322), ','(tree(X342), tree(X322))), SCOPE: 20, CLAUSE: 11\n\nX322 is free\nX342 is free; \nX343 is free; \nX344 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(tree(X360), tree(X362))\n\nX360 is free\nX362 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX11 is free; \ns2t(T3, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(s2t(T3, X11), tree(X11)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX11 is free; \ns2t(T3, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(p(T62, X392), ','(s2t(X392, X393), tree(node(X393, X394, nil))))\n\nT62 is ground\nX393 is free; \nX394 is free; \nX392 is free; \ns2t(T62, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(p(T62, X392), ','(s2t(X392, X393), tree(node(X393, X394, nil)))), SCOPE: 21, CLAUSE: 12 | ','(p(T62, X392), ','(s2t(X392, X393), tree(node(X393, X394, nil)))), SCOPE: 21, CLAUSE: 13\n\nT62 is ground\nX393 is free; \nX394 is free; \nX392 is free; \ns2t(T62, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(p(T62, X392), ','(s2t(X392, X393), tree(node(X393, X394, nil)))), SCOPE: 21, CLAUSE: 13\n\nT62 is ground\nX393 is free; \nX394 is free; \nX392 is free; \ns2t(T62, X11) !=? s2t(0, X16)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(s2t(T65, X393), tree(node(X393, X394, nil)))\n\nT65 is ground\nX393 is free; \nX394 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: s2t(T65, X393)\n\nT65 is ground\nX393 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: tree(node(T66, X394, nil))\n\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: tree(node(T66, X394, nil)), SCOPE: 22, CLAUSE: 1 | tree(node(T66, X394, nil)), SCOPE: 22, CLAUSE: 2\n\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: tree(node(T66, X394, nil)), SCOPE: 22, CLAUSE: 2\n\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(left(X418, X419), ','(right(X418, X420), ','(tree(X419), tree(X420))))\n\nX418 is free\nX419 is free; \nX420 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(left(X418, X419), ','(right(X418, X420), ','(tree(X419), tree(X420)))), SCOPE: 23, CLAUSE: 8 | ','(left(X418, X419), ','(right(X418, X420), ','(tree(X419), tree(X420)))), SCOPE: 23, CLAUSE: 9\n\nX418 is free\nX419 is free; \nX420 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(left(X418, X419), ','(right(X418, X420), ','(tree(X419), tree(X420)))), SCOPE: 23, CLAUSE: 8\n\nX418 is free\nX419 is free; \nX420 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(left(X418, X419), ','(right(X418, X420), ','(tree(X419), tree(X420)))), SCOPE: 23, CLAUSE: 9\n\nX418 is free\nX419 is free; \nX420 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(right(nil, X420), ','(tree(nil), tree(X420)))\n\nX420 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(right(nil, X420), ','(tree(nil), tree(X420))), SCOPE: 24, CLAUSE: 10 | ','(right(nil, X420), ','(tree(nil), tree(X420))), SCOPE: 24, CLAUSE: 11\n\nX420 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(right(nil, X420), ','(tree(nil), tree(X420))), SCOPE: 24, CLAUSE: 10\n\nX420 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(right(nil, X420), ','(tree(nil), tree(X420))), SCOPE: 24, CLAUSE: 11\n\nX420 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(right(node(X440, X441, X442), X420), ','(tree(X440), tree(X420)))\n\nX420 is free\nX440 is free; \nX441 is free; \nX442 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(right(node(X440, X441, X442), X420), ','(tree(X440), tree(X420))), SCOPE: 25, CLAUSE: 10 | ','(right(node(X440, X441, X442), X420), ','(tree(X440), tree(X420))), SCOPE: 25, CLAUSE: 11\n\nX420 is free\nX440 is free; \nX441 is free; \nX442 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(right(node(X440, X441, X442), X420), ','(tree(X440), tree(X420))), SCOPE: 25, CLAUSE: 11\n\nX420 is free\nX440 is free; \nX441 is free; \nX442 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(tree(X458), tree(X460))\n\nX458 is free\nX460 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: tree(node(nil, X474, nil))\n\nX474 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: tree(node(nil, X474, nil)), SCOPE: 26, CLAUSE: 1 | tree(node(nil, X474, nil)), SCOPE: 26, CLAUSE: 2\n\nX474 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: tree(node(nil, X474, nil)), SCOPE: 26, CLAUSE: 2\n\nX474 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(left(X488, X489), ','(right(X488, X490), ','(tree(X489), tree(X490))))\n\nX488 is free\nX489 is free; \nX490 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(left(X488, X489), ','(right(X488, X490), ','(tree(X489), tree(X490)))), SCOPE: 27, CLAUSE: 8 | ','(left(X488, X489), ','(right(X488, X490), ','(tree(X489), tree(X490)))), SCOPE: 27, CLAUSE: 9\n\nX488 is free\nX489 is free; \nX490 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(left(X488, X489), ','(right(X488, X490), ','(tree(X489), tree(X490)))), SCOPE: 27, CLAUSE: 8\n\nX488 is free\nX489 is free; \nX490 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(left(X488, X489), ','(right(X488, X490), ','(tree(X489), tree(X490)))), SCOPE: 27, CLAUSE: 9\n\nX488 is free\nX489 is free; \nX490 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(right(nil, X490), ','(tree(nil), tree(X490)))\n\nX490 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(right(nil, X490), ','(tree(nil), tree(X490))), SCOPE: 28, CLAUSE: 10 | ','(right(nil, X490), ','(tree(nil), tree(X490))), SCOPE: 28, CLAUSE: 11\n\nX490 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(right(nil, X490), ','(tree(nil), tree(X490))), SCOPE: 28, CLAUSE: 10\n\nX490 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(right(nil, X490), ','(tree(nil), tree(X490))), SCOPE: 28, CLAUSE: 11\n\nX490 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(right(node(X510, X511, X512), X490), ','(tree(X510), tree(X490)))\n\nX490 is free\nX510 is free; \nX511 is free; \nX512 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(right(node(X510, X511, X512), X490), ','(tree(X510), tree(X490))), SCOPE: 29, CLAUSE: 10 | ','(right(node(X510, X511, X512), X490), ','(tree(X510), tree(X490))), SCOPE: 29, CLAUSE: 11\n\nX490 is free\nX510 is free; \nX511 is free; \nX512 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(right(node(X510, X511, X512), X490), ','(tree(X510), tree(X490))), SCOPE: 29, CLAUSE: 11\n\nX490 is free\nX510 is free; \nX511 is free; \nX512 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(tree(X528), tree(X530))\n\nX528 is free\nX530 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 144 [arrowhead = none ];
144 -> 2;

145 [label="ONLY EVAL with clause\ngoal(X10) :- ','(s2t(X10, X11), tree(X11)).\nand substitution\nT1 -> T3\nX10 -> T3", fontsize=14, style = filled, fillcolor = white];
2 -> 145 [arrowhead = none ];
145 -> 3;

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

147 [label="EVAL with clause\ns2t(0, X16) :- ','(!_2, eq(X16, nil)).\nand substitution\nT3 -> 0\nX11 -> X17\nX16 -> X17", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 147 [arrowhead = none ];
147 -> 5;

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

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

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

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

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

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

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

155 [label="ONLY EVAL with clause\ntree(nil) :- !_4.\nand substitution", fontsize=14, style = filled, fillcolor = white];
10 -> 155 [arrowhead = none ];
155 -> 11;

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

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

158 [label="ONLY EVAL with clause\ns2t(X51, node(X52, X53, X52)) :- ','(p(X51, X54), s2t(X54, X52)).\nand substitution\nT3 -> T8\nX51 -> T8\nX52 -> X55\nX53 -> X56\nX11 -> node(X55, X56, X55)", fontsize=14, style = filled, fillcolor = white];
14 -> 158 [arrowhead = none ];
158 -> 16;

159 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
15 -> 159 [arrowhead = none ];
159 -> 77;

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

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

162 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T8, X11), s2t(0, X16))", fontsize=14, style = filled, fillcolor = white];
17 -> 162 [arrowhead = none ];
162 -> 18;

163 [label="EVAL with clause\np(s(X61), X61).\nand substitution\nX61 -> T11\nT8 -> s(T11)\nX54 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 163 [arrowhead = none ];
163 -> 19;

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

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

166 [label="SPLIT 2\nreplacements:\nX55 -> T12", fontsize=14, style = filled, fillcolor = violet];
19 -> 166 [arrowhead = none ];
166 -> 22;

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

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

169 [label="EVAL with clause\ns2t(0, X71) :- ','(!_6, eq(X71, nil)).\nand substitution\nT11 -> 0\nX55 -> X72\nX71 -> X72", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 169 [arrowhead = none ];
169 -> 24;

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

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

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

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

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

175 [label="ONLY EVAL with clause\neq(X78, X78).\nand substitution\nX72 -> nil\nX78 -> nil\nX79 -> nil", fontsize=14, style = filled, fillcolor = white];
27 -> 175 [arrowhead = none ];
175 -> 28;

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

177 [label="ONLY EVAL with clause\ns2t(X106, node(X107, X108, X107)) :- ','(p(X106, X109), s2t(X109, X107)).\nand substitution\nT11 -> T17\nX106 -> T17\nX107 -> X110\nX108 -> X111\nX55 -> node(X110, X111, X110)", fontsize=14, style = filled, fillcolor = white];
30 -> 177 [arrowhead = none ];
177 -> 32;

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

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

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

181 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T17, X55), s2t(0, X71))", fontsize=14, style = filled, fillcolor = white];
33 -> 181 [arrowhead = none ];
181 -> 34;

182 [label="EVAL with clause\np(s(X116), X116).\nand substitution\nX116 -> T20\nT17 -> s(T20)\nX109 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 182 [arrowhead = none ];
182 -> 35;

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

184 [label="INSTANCE with matching:\nT11 -> T20\nX55 -> X110", fontsize=14, style = filled, fillcolor = lightgrey];
35 -> 184 [arrowhead = none , style=dashed];
184 -> 21[style=dashed];

185 [label="ONLY EVAL with clause\ns2t(X146, node(nil, X147, X148)) :- ','(p(X146, X149), s2t(X149, X148)).\nand substitution\nT11 -> T25\nX146 -> T25\nX147 -> X150\nX148 -> X151\nX55 -> node(nil, X150, X151)", fontsize=14, style = filled, fillcolor = white];
37 -> 185 [arrowhead = none ];
185 -> 39;

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

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

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

189 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T25, X55), s2t(0, X71))", fontsize=14, style = filled, fillcolor = white];
40 -> 189 [arrowhead = none ];
189 -> 41;

190 [label="EVAL with clause\np(s(X156), X156).\nand substitution\nX156 -> T28\nT25 -> s(T28)\nX149 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 190 [arrowhead = none ];
190 -> 42;

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

192 [label="INSTANCE with matching:\nT11 -> T28\nX55 -> X151", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 192 [arrowhead = none , style=dashed];
192 -> 21[style=dashed];

193 [label="ONLY EVAL with clause\ns2t(X186, node(X187, X188, nil)) :- ','(p(X186, X189), s2t(X189, X187)).\nand substitution\nT11 -> T33\nX186 -> T33\nX187 -> X190\nX188 -> X191\nX55 -> node(X190, X191, nil)", fontsize=14, style = filled, fillcolor = white];
44 -> 193 [arrowhead = none ];
193 -> 46;

194 [label="ONLY EVAL with clause\ns2t(X206, node(nil, X207, nil)).\nand substitution\nT11 -> T39\nX206 -> T39\nX207 -> X208\nX55 -> node(nil, X208, nil)", fontsize=14, style = filled, fillcolor = white];
45 -> 194 [arrowhead = none ];
194 -> 51;

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

196 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T33, X55), s2t(0, X71))", fontsize=14, style = filled, fillcolor = white];
47 -> 196 [arrowhead = none ];
196 -> 48;

197 [label="EVAL with clause\np(s(X196), X196).\nand substitution\nX196 -> T36\nT33 -> s(T36)\nX189 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 197 [arrowhead = none ];
197 -> 49;

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

199 [label="INSTANCE with matching:\nT11 -> T36\nX55 -> X190", fontsize=14, style = filled, fillcolor = lightgrey];
49 -> 199 [arrowhead = none , style=dashed];
199 -> 21[style=dashed];

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

201 [label="BACKTRACK\nfor clause: tree(nil) :- !because of non-unification", fontsize=14, style = filled, fillcolor = white];
53 -> 201 [arrowhead = none ];
201 -> 54;

202 [label="ONLY EVAL with clause\ntree(X221) :- ','(left(X222, X223), ','(right(X222, X224), ','(tree(X223), tree(X224)))).\nand substitution\nT12 -> T43\nX56 -> X225\nX221 -> node(T43, X225, T43)", fontsize=14, style = filled, fillcolor = white];
54 -> 202 [arrowhead = none ];
202 -> 55;

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

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

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

206 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitution\nX222 -> nil\nX223 -> nil", fontsize=14, style = filled, fillcolor = white];
57 -> 206 [arrowhead = none ];
206 -> 59;

207 [label="ONLY EVAL with clause\nleft(node(X241, X242, X243), X241).\nand substitution\nX241 -> X244\nX242 -> X245\nX243 -> X246\nX222 -> node(X244, X245, X246)\nX223 -> X244", fontsize=14, style = filled, fillcolor = white];
58 -> 207 [arrowhead = none ];
207 -> 67;

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

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

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

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

212 [label="BACKTRACK\nfor clause: right(node(X7, X8, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = white];
62 -> 212 [arrowhead = none ];
212 -> 66;

213 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
63 -> 213 [arrowhead = none ];
213 -> 64;

214 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
63 -> 214 [arrowhead = none ];
214 -> 65;

215 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 215 [arrowhead = none , style=dashed];
215 -> 9[style=dashed];

216 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 216 [arrowhead = none , style=dashed];
216 -> 9[style=dashed];

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

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

219 [label="ONLY EVAL with clause\nright(node(X259, X260, X261), X261).\nand substitution\nX244 -> X262\nX259 -> X262\nX245 -> X263\nX260 -> X263\nX246 -> X264\nX261 -> X264\nX224 -> X264", fontsize=14, style = filled, fillcolor = white];
69 -> 219 [arrowhead = none ];
219 -> 70;

220 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
70 -> 220 [arrowhead = none ];
220 -> 71;

221 [label="SPLIT 2\nreplacements:\nX262 -> T44", fontsize=14, style = filled, fillcolor = violet];
70 -> 221 [arrowhead = none ];
221 -> 72;

222 [label="INSTANCE with matching:\nX264 -> X262", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 222 [arrowhead = none , style=dashed];
222 -> 72[style=dashed];

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

224 [label="ONLY EVAL with clause\ntree(nil) :- !_15.\nand substitution\nX264 -> nil", fontsize=14, style = filled, fillcolor = white];
73 -> 224 [arrowhead = none ];
224 -> 74;

225 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 225 [arrowhead = none ];
225 -> 75;

226 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 226 [arrowhead = none ];
226 -> 76;

227 [label="ONLY EVAL with clause\ns2t(X291, node(nil, X292, X293)) :- ','(p(X291, X294), s2t(X294, X293)).\nand substitution\nT3 -> T49\nX291 -> T49\nX292 -> X295\nX293 -> X296\nX11 -> node(nil, X295, X296)", fontsize=14, style = filled, fillcolor = white];
77 -> 227 [arrowhead = none ];
227 -> 79;

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

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

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

231 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T49, X11), s2t(0, X16))", fontsize=14, style = filled, fillcolor = white];
80 -> 231 [arrowhead = none ];
231 -> 81;

232 [label="EVAL with clause\np(s(X301), X301).\nand substitution\nX301 -> T52\nT49 -> s(T52)\nX294 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 232 [arrowhead = none ];
232 -> 82;

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

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

235 [label="SPLIT 2\nreplacements:\nX296 -> T53", fontsize=14, style = filled, fillcolor = violet];
82 -> 235 [arrowhead = none ];
235 -> 85;

236 [label="INSTANCE with matching:\nT11 -> T52\nX55 -> X296", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 236 [arrowhead = none , style=dashed];
236 -> 21[style=dashed];

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

238 [label="BACKTRACK\nfor clause: tree(nil) :- !because of non-unification", fontsize=14, style = filled, fillcolor = white];
86 -> 238 [arrowhead = none ];
238 -> 87;

239 [label="ONLY EVAL with clause\ntree(X319) :- ','(left(X320, X321), ','(right(X320, X322), ','(tree(X321), tree(X322)))).\nand substitution\nX295 -> X323\nT53 -> T57\nX319 -> node(nil, X323, T57)", fontsize=14, style = filled, fillcolor = white];
87 -> 239 [arrowhead = none ];
239 -> 88;

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

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

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

243 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitution\nX320 -> nil\nX321 -> nil", fontsize=14, style = filled, fillcolor = white];
90 -> 243 [arrowhead = none ];
243 -> 92;

244 [label="ONLY EVAL with clause\nleft(node(X339, X340, X341), X339).\nand substitution\nX339 -> X342\nX340 -> X343\nX341 -> X344\nX320 -> node(X342, X343, X344)\nX321 -> X342", fontsize=14, style = filled, fillcolor = white];
91 -> 244 [arrowhead = none ];
244 -> 98;

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

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

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

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

249 [label="BACKTRACK\nfor clause: right(node(X7, X8, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = white];
95 -> 249 [arrowhead = none ];
249 -> 97;

250 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
96 -> 250 [arrowhead = none , style=dashed];
250 -> 63[style=dashed];

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

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

253 [label="ONLY EVAL with clause\nright(node(X357, X358, X359), X359).\nand substitution\nX342 -> X360\nX357 -> X360\nX343 -> X361\nX358 -> X361\nX344 -> X362\nX359 -> X362\nX322 -> X362", fontsize=14, style = filled, fillcolor = white];
100 -> 253 [arrowhead = none ];
253 -> 101;

254 [label="INSTANCE with matching:\nX262 -> X360\nX264 -> X362", fontsize=14, style = filled, fillcolor = lightgrey];
101 -> 254 [arrowhead = none , style=dashed];
254 -> 70[style=dashed];

255 [label="ONLY EVAL with clause\ns2t(X389, node(X390, X391, nil)) :- ','(p(X389, X392), s2t(X392, X390)).\nand substitution\nT3 -> T62\nX389 -> T62\nX390 -> X393\nX391 -> X394\nX11 -> node(X393, X394, nil)", fontsize=14, style = filled, fillcolor = white];
102 -> 255 [arrowhead = none ];
255 -> 104;

256 [label="ONLY EVAL with clause\ns2t(X472, node(nil, X473, nil)).\nand substitution\nT3 -> T73\nX472 -> T73\nX473 -> X474\nX11 -> node(nil, X474, nil)", fontsize=14, style = filled, fillcolor = white];
103 -> 256 [arrowhead = none ];
256 -> 127;

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

258 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T62, X11), s2t(0, X16))", fontsize=14, style = filled, fillcolor = white];
105 -> 258 [arrowhead = none ];
258 -> 106;

259 [label="EVAL with clause\np(s(X399), X399).\nand substitution\nX399 -> T65\nT62 -> s(T65)\nX392 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 259 [arrowhead = none ];
259 -> 107;

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

261 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
107 -> 261 [arrowhead = none ];
261 -> 109;

262 [label="SPLIT 2\nreplacements:\nX393 -> T66", fontsize=14, style = filled, fillcolor = violet];
107 -> 262 [arrowhead = none ];
262 -> 110;

263 [label="INSTANCE with matching:\nT11 -> T65\nX55 -> X393", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 263 [arrowhead = none , style=dashed];
263 -> 21[style=dashed];

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

265 [label="BACKTRACK\nfor clause: tree(nil) :- !because of non-unification", fontsize=14, style = filled, fillcolor = white];
111 -> 265 [arrowhead = none ];
265 -> 112;

266 [label="ONLY EVAL with clause\ntree(X417) :- ','(left(X418, X419), ','(right(X418, X420), ','(tree(X419), tree(X420)))).\nand substitution\nT66 -> T70\nX394 -> X421\nX417 -> node(T70, X421, nil)", fontsize=14, style = filled, fillcolor = white];
112 -> 266 [arrowhead = none ];
266 -> 113;

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

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

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

270 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitution\nX418 -> nil\nX419 -> nil", fontsize=14, style = filled, fillcolor = white];
115 -> 270 [arrowhead = none ];
270 -> 117;

271 [label="ONLY EVAL with clause\nleft(node(X437, X438, X439), X437).\nand substitution\nX437 -> X440\nX438 -> X441\nX439 -> X442\nX418 -> node(X440, X441, X442)\nX419 -> X440", fontsize=14, style = filled, fillcolor = white];
116 -> 271 [arrowhead = none ];
271 -> 123;

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

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

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

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

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

277 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 277 [arrowhead = none , style=dashed];
277 -> 63[style=dashed];

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

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

280 [label="ONLY EVAL with clause\nright(node(X455, X456, X457), X457).\nand substitution\nX440 -> X458\nX455 -> X458\nX441 -> X459\nX456 -> X459\nX442 -> X460\nX457 -> X460\nX420 -> X460", fontsize=14, style = filled, fillcolor = white];
125 -> 280 [arrowhead = none ];
280 -> 126;

281 [label="INSTANCE with matching:\nX262 -> X458\nX264 -> X460", fontsize=14, style = filled, fillcolor = lightgrey];
126 -> 281 [arrowhead = none , style=dashed];
281 -> 70[style=dashed];

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

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

284 [label="ONLY EVAL with clause\ntree(X487) :- ','(left(X488, X489), ','(right(X488, X490), ','(tree(X489), tree(X490)))).\nand substitution\nX474 -> X491\nX487 -> node(nil, X491, nil)", fontsize=14, style = filled, fillcolor = white];
129 -> 284 [arrowhead = none ];
284 -> 130;

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

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

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

288 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitution\nX488 -> nil\nX489 -> nil", fontsize=14, style = filled, fillcolor = white];
132 -> 288 [arrowhead = none ];
288 -> 134;

289 [label="ONLY EVAL with clause\nleft(node(X507, X508, X509), X507).\nand substitution\nX507 -> X510\nX508 -> X511\nX509 -> X512\nX488 -> node(X510, X511, X512)\nX489 -> X510", fontsize=14, style = filled, fillcolor = white];
133 -> 289 [arrowhead = none ];
289 -> 140;

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

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

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

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

294 [label="BACKTRACK\nfor clause: right(node(X7, X8, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = white];
137 -> 294 [arrowhead = none ];
294 -> 139;

295 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
138 -> 295 [arrowhead = none , style=dashed];
295 -> 63[style=dashed];

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

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

298 [label="ONLY EVAL with clause\nright(node(X525, X526, X527), X527).\nand substitution\nX510 -> X528\nX525 -> X528\nX511 -> X529\nX526 -> X529\nX512 -> X530\nX527 -> X530\nX490 -> X530", fontsize=14, style = filled, fillcolor = white];
142 -> 298 [arrowhead = none ];
298 -> 143;

299 [label="INSTANCE with matching:\nX262 -> X528\nX264 -> X530", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 299 [arrowhead = none , style=dashed];
299 -> 70[style=dashed];

}

(2) Obligation:

Triples:

s2t21(s(T20), node(X110, X111, X110)) :- s2t21(T20, X110).
s2t21(s(T28), node(nil, X150, X151)) :- s2t21(T28, X151).
s2t21(s(T36), node(X190, X191, nil)) :- s2t21(T36, X190).
p63 :- tree9.
p63 :- ','(treec9, tree9).
p70(X262, X264) :- tree72(X262).
p70(T44, X264) :- ','(treec72(T44), tree72(X264)).
goal1(0) :- tree9.
goal1(s(T11)) :- s2t21(T11, X55).
goal1(s(T11)) :- ','(s2tc21(T11, T43), p63).
goal1(s(T11)) :- ','(s2tc21(T11, T43), p70(X262, X264)).
goal1(s(T52)) :- s2t21(T52, X296).
goal1(s(T52)) :- ','(s2tc21(T52, T57), p63).
goal1(s(T52)) :- ','(s2tc21(T52, T57), p70(X360, X362)).
goal1(s(T65)) :- s2t21(T65, X393).
goal1(s(T65)) :- ','(s2tc21(T65, T70), p63).
goal1(s(T65)) :- ','(s2tc21(T65, T70), p70(X458, X460)).
goal1(T73) :- p63.
goal1(T73) :- p70(X528, X530).

Clauses:

s2tc21(0, nil).
s2tc21(s(T20), node(X110, X111, X110)) :- s2tc21(T20, X110).
s2tc21(s(T28), node(nil, X150, X151)) :- s2tc21(T28, X151).
s2tc21(s(T36), node(X190, X191, nil)) :- s2tc21(T36, X190).
s2tc21(T39, node(nil, X208, nil)).
treec9.
treec72(nil).
qc63 :- ','(treec9, treec9).
qc70(T44, X264) :- ','(treec72(T44), treec72(X264)).

Afs:

goal1(x1) = goal1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

s2t21(s(T20), node(X110, X111, X110)) :- s2t21(T20, X110).
s2t21(s(T28), node(nil, X150, X151)) :- s2t21(T28, X151).
s2t21(s(T36), node(X190, X191, nil)) :- s2t21(T36, X190).
goal1(s(T11)) :- s2t21(T11, X55).
goal1(s(T52)) :- s2t21(T52, X296).
goal1(s(T65)) :- s2t21(T65, X393).

Clauses:

s2tc21(0, nil).
s2tc21(s(T20), node(X110, X111, X110)) :- s2tc21(T20, X110).
s2tc21(s(T28), node(nil, X150, X151)) :- s2tc21(T28, X151).
s2tc21(s(T36), node(X190, X191, nil)) :- s2tc21(T36, X190).
s2tc21(T39, node(nil, X208, nil)).
treec9.
treec72(nil).
qc63 :- ','(treec9, treec9).
qc70(T44, X264) :- ','(treec72(T44), treec72(X264)).

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

GOAL1_IN_G(s(T11)) → U4_G(T11, s2t21_in_ga(T11, X55))
GOAL1_IN_G(s(T11)) → S2T21_IN_GA(T11, X55)
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → U1_GA(T20, X110, X111, s2t21_in_ga(T20, X110))
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → S2T21_IN_GA(T20, X110)
S2T21_IN_GA(s(T28), node(nil, X150, X151)) → U2_GA(T28, X150, X151, s2t21_in_ga(T28, X151))
S2T21_IN_GA(s(T28), node(nil, X150, X151)) → S2T21_IN_GA(T28, X151)
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → U3_GA(T36, X190, X191, s2t21_in_ga(T36, X190))
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → S2T21_IN_GA(T36, X190)
GOAL1_IN_G(s(T52)) → U5_G(T52, s2t21_in_ga(T52, X296))
GOAL1_IN_G(s(T65)) → U6_G(T65, s2t21_in_ga(T65, X393))

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
s2t21_in_ga(x1, x2) = s2t21_in_ga(x1)
node(x1, x2, x3) = node(x1, x3)
nil = nil
GOAL1_IN_G(x1) = GOAL1_IN_G(x1)
U4_G(x1, x2) = U4_G(x1, x2)
S2T21_IN_GA(x1, x2) = S2T21_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)
U5_G(x1, x2) = U5_G(x1, x2)
U6_G(x1, x2) = U6_G(x1, x2)

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(T11)) → U4_G(T11, s2t21_in_ga(T11, X55))
GOAL1_IN_G(s(T11)) → S2T21_IN_GA(T11, X55)
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → U1_GA(T20, X110, X111, s2t21_in_ga(T20, X110))
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → S2T21_IN_GA(T20, X110)
S2T21_IN_GA(s(T28), node(nil, X150, X151)) → U2_GA(T28, X150, X151, s2t21_in_ga(T28, X151))
S2T21_IN_GA(s(T28), node(nil, X150, X151)) → S2T21_IN_GA(T28, X151)
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → U3_GA(T36, X190, X191, s2t21_in_ga(T36, X190))
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → S2T21_IN_GA(T36, X190)
GOAL1_IN_G(s(T52)) → U5_G(T52, s2t21_in_ga(T52, X296))
GOAL1_IN_G(s(T65)) → U6_G(T65, s2t21_in_ga(T65, X393))

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 7 less nodes.

(8) Obligation:

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

S2T21_IN_GA(s(T28), node(nil, X150, X151)) → S2T21_IN_GA(T28, X151)
S2T21_IN_GA(s(T20), node(X110, X111, X110)) → S2T21_IN_GA(T20, X110)
S2T21_IN_GA(s(T36), node(X190, X191, nil)) → S2T21_IN_GA(T36, X190)

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

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

(9) PiDPToQDPProof (SOUND transformation)

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

(10) Obligation:

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

S2T21_IN_GA(s(T28)) → S2T21_IN_GA(T28)

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

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

S2T21_IN_GA(s(T28)) → S2T21_IN_GA(T28)
The graph contains the following edges 1 > 1