Left Termination proof of /tmp/tmpGVTauC/btree2.pl

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇒, 373 ms)

↳2 Prolog

↳3 PrologToPiTRSProof (⇒, 19 ms)

↳4 PiTRS

↳5 DependencyPairsProof (⇔, 133 ms)

↳6 PiDP

↳7 DependencyGraphProof (⇔, 0 ms)

↳8 PiDP

↳9 UsableRulesProof (⇔, 0 ms)

↳10 PiDP

↳11 PiDPToQDPProof (⇒, 0 ms)

↳12 QDP

↳13 QDPSizeChangeProof (⇔, 0 ms)

↳14 YES

(0) Obligation:

Clauses:

goal(X) :- ','(s2t(X, T), tree(T)).
tree(nil).
tree(X) :- ','(no(empty(X)), ','(left(T, L), ','(right(T, R), ','(tree(L), tree(R))))).
s2t(0, nil).
s2t(X, node(T, X1, T)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(nil, X2, T)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(T, X3, nil)) :- ','(no(zero(X)), ','(p(X, P), s2t(P, T))).
s2t(X, node(nil, X4, nil)) :- no(zero(X)).
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).
empty(nil).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X9).
failure(b).

Query: goal(g)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

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, X12), tree(X12))\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 3 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 4 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 4 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: tree(nil), SCOPE: 3, CLAUSE: 1 | tree(nil), SCOPE: 3, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: tree(nil), SCOPE: 3, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: tree(nil), SCOPE: 3, 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: ','(no(empty(nil)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21)))))\n\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(no(empty(nil)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))), SCOPE: 4, CLAUSE: 16 | ','(no(empty(nil)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))), SCOPE: 4, CLAUSE: 17\n\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(','(call(empty(nil)), ','(!_4, failure(a))), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))) | ','(no(empty(nil)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))), SCOPE: 4, CLAUSE: 17\n\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(empty(nil), ','(','(!_4, failure(a)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21)))))) | ?_5 | ','(no(empty(nil)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))), SCOPE: 4, CLAUSE: 17\n\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(empty(nil), ','(','(!_4, failure(a)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21)))))), SCOPE: 6, CLAUSE: 14 | ?_6 | ?_5 | ','(no(empty(nil)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))), SCOPE: 4, CLAUSE: 17\n\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(','(!_4, failure(a)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))) | ?_6 | ?_5 | ','(no(empty(nil)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))), SCOPE: 4, CLAUSE: 17\n\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(failure(a), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21)))))\n\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(failure(a), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))), SCOPE: 7, CLAUSE: 18\n\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(','(no(zero(T8)), ','(p(T8, X50), s2t(X50, X51))), tree(node(X51, X52, X51)))\n\nT8 is ground\nX51 is free\nX52 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(','(no(zero(T8)), ','(p(T8, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 16 | ','(','(no(zero(T8)), ','(p(T8, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 17\n\nT8 is ground\nX51 is free\nX52 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(','(call(zero(T11)), ','(!_8, failure(a))), ','(','(p(T11, X50), s2t(X50, X51)), tree(node(X51, X52, X51)))) | ','(','(no(zero(T11)), ','(p(T11, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 17\n\nT11 is ground\nX51 is free\nX52 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(zero(T11), ','(','(!_8, failure(a)), ','(','(p(T11, X50), s2t(X50, X51)), tree(node(X51, X52, X51))))) | ?_9 | ','(','(no(zero(T11)), ','(p(T11, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 17\n\nT11 is ground\nX51 is free\nX52 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(zero(T11), ','(','(!_8, failure(a)), ','(','(p(T11, X50), s2t(X50, X51)), tree(node(X51, X52, X51))))), SCOPE: 10, CLAUSE: 15 | ?_10 | ?_9 | ','(','(no(zero(T11)), ','(p(T11, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 17\n\nT11 is ground\nX51 is free\nX52 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(','(!_8, failure(a)), ','(','(p(0, X50), s2t(X50, X51)), tree(node(X51, X52, X51)))) | ?_10 | ?_9 | ','(','(no(zero(0)), ','(p(0, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 17\n\nX51 is free\nX52 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ?_10 | ?_9 | ','(','(no(zero(T11)), ','(p(T11, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 17\n\nT11 is ground\nX51 is free\nX52 is free\nX50 is free\nzero(T11) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(failure(a), ','(','(p(0, X50), s2t(X50, X51)), tree(node(X51, X52, X51))))\n\nX51 is free\nX52 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(failure(a), ','(','(p(0, X50), s2t(X50, X51)), tree(node(X51, X52, X51)))), SCOPE: 11, CLAUSE: 18\n\nX51 is free\nX52 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ?_9 | ','(','(no(zero(T11)), ','(p(T11, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 17\n\nT11 is ground\nX51 is free\nX52 is free\nX50 is free\nzero(T11) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(','(no(zero(T11)), ','(p(T11, X50), s2t(X50, X51))), tree(node(X51, X52, X51))), SCOPE: 8, CLAUSE: 17\n\nT11 is ground\nX51 is free\nX52 is free\nX50 is free\nzero(T11) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(','(p(T14, X50), s2t(X50, X51)), tree(node(X51, X52, X51)))\n\nT14 is ground\nX51 is free\nX52 is free\nX50 is free\nzero(T14) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(','(p(T14, X50), s2t(X50, X51)), tree(node(X51, X52, X51))), SCOPE: 12, CLAUSE: 12 | ','(','(p(T14, X50), s2t(X50, X51)), tree(node(X51, X52, X51))), SCOPE: 12, CLAUSE: 13\n\nT14 is ground\nX51 is free\nX52 is free\nX50 is free\nzero(T14) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(','(p(T14, X50), s2t(X50, X51)), tree(node(X51, X52, X51))), SCOPE: 12, CLAUSE: 13\n\nT14 is ground\nX51 is free\nX52 is free\nX50 is free\nzero(T14) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(s2t(T17, X51), tree(node(X51, X52, X51)))\n\nT17 is ground\nX51 is free\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: s2t(T17, X51)\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: tree(node(T18, X52, T18))\n\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: s2t(T17, X51), SCOPE: 13, CLAUSE: 3 | s2t(T17, X51), SCOPE: 13, CLAUSE: 4 | s2t(T17, X51), SCOPE: 13, CLAUSE: 5 | s2t(T17, X51), SCOPE: 13, CLAUSE: 6 | s2t(T17, X51), SCOPE: 13, CLAUSE: 7\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: s2t(T17, X51), SCOPE: 13, CLAUSE: 3\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: s2t(T17, X51), SCOPE: 13, CLAUSE: 4 | s2t(T17, X51), SCOPE: 13, CLAUSE: 5 | s2t(T17, X51), SCOPE: 13, CLAUSE: 6 | s2t(T17, X51), SCOPE: 13, CLAUSE: 7\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: s2t(T17, X51), SCOPE: 13, CLAUSE: 4\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: s2t(T17, X51), SCOPE: 13, CLAUSE: 5 | s2t(T17, X51), SCOPE: 13, CLAUSE: 6 | s2t(T17, X51), SCOPE: 13, CLAUSE: 7\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(no(zero(T23)), ','(p(T23, X87), s2t(X87, X88)))\n\nT23 is ground\nX88 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(no(zero(T23)), ','(p(T23, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 16 | ','(no(zero(T23)), ','(p(T23, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 17\n\nT23 is ground\nX88 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(','(call(zero(T26)), ','(!_14, failure(a))), ','(p(T26, X87), s2t(X87, X88))) | ','(no(zero(T26)), ','(p(T26, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 17\n\nT26 is ground\nX88 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(zero(T26), ','(','(!_14, failure(a)), ','(p(T26, X87), s2t(X87, X88)))) | ?_15 | ','(no(zero(T26)), ','(p(T26, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 17\n\nT26 is ground\nX88 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(zero(T26), ','(','(!_14, failure(a)), ','(p(T26, X87), s2t(X87, X88)))), SCOPE: 16, CLAUSE: 15 | ?_16 | ?_15 | ','(no(zero(T26)), ','(p(T26, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 17\n\nT26 is ground\nX88 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(','(!_14, failure(a)), ','(p(0, X87), s2t(X87, X88))) | ?_16 | ?_15 | ','(no(zero(0)), ','(p(0, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 17\n\nX88 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ?_16 | ?_15 | ','(no(zero(T26)), ','(p(T26, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 17\n\nT26 is ground\nX88 is free\nX87 is free\nzero(T26) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(failure(a), ','(p(0, X87), s2t(X87, X88)))\n\nX88 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(failure(a), ','(p(0, X87), s2t(X87, X88))), SCOPE: 17, CLAUSE: 18\n\nX88 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ?_15 | ','(no(zero(T26)), ','(p(T26, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 17\n\nT26 is ground\nX88 is free\nX87 is free\nzero(T26) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(no(zero(T26)), ','(p(T26, X87), s2t(X87, X88))), SCOPE: 14, CLAUSE: 17\n\nT26 is ground\nX88 is free\nX87 is free\nzero(T26) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(p(T29, X87), s2t(X87, X88))\n\nT29 is ground\nX88 is free\nX87 is free\nzero(T29) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(p(T29, X87), s2t(X87, X88)), SCOPE: 18, CLAUSE: 12 | ','(p(T29, X87), s2t(X87, X88)), SCOPE: 18, CLAUSE: 13\n\nT29 is ground\nX88 is free\nX87 is free\nzero(T29) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(p(T29, X87), s2t(X87, X88)), SCOPE: 18, CLAUSE: 13\n\nT29 is ground\nX88 is free\nX87 is free\nzero(T29) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: s2t(T32, X88)\n\nT32 is ground\nX88 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: s2t(T17, X51), SCOPE: 13, CLAUSE: 5\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: s2t(T17, X51), SCOPE: 13, CLAUSE: 6 | s2t(T17, X51), SCOPE: 13, CLAUSE: 7\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(no(zero(T37)), ','(p(T37, X124), s2t(X124, X126)))\n\nT37 is ground\nX126 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(no(zero(T37)), ','(p(T37, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 16 | ','(no(zero(T37)), ','(p(T37, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 17\n\nT37 is ground\nX126 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(','(call(zero(T40)), ','(!_19, failure(a))), ','(p(T40, X124), s2t(X124, X126))) | ','(no(zero(T40)), ','(p(T40, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 17\n\nT40 is ground\nX126 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(zero(T40), ','(','(!_19, failure(a)), ','(p(T40, X124), s2t(X124, X126)))) | ?_20 | ','(no(zero(T40)), ','(p(T40, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 17\n\nT40 is ground\nX126 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(zero(T40), ','(','(!_19, failure(a)), ','(p(T40, X124), s2t(X124, X126)))), SCOPE: 21, CLAUSE: 15 | ?_21 | ?_20 | ','(no(zero(T40)), ','(p(T40, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 17\n\nT40 is ground\nX126 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(','(!_19, failure(a)), ','(p(0, X124), s2t(X124, X126))) | ?_21 | ?_20 | ','(no(zero(0)), ','(p(0, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 17\n\nX126 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ?_21 | ?_20 | ','(no(zero(T40)), ','(p(T40, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 17\n\nT40 is ground\nX126 is free\nX124 is free\nzero(T40) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(failure(a), ','(p(0, X124), s2t(X124, X126)))\n\nX126 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(failure(a), ','(p(0, X124), s2t(X124, X126))), SCOPE: 22, CLAUSE: 18\n\nX126 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ?_20 | ','(no(zero(T40)), ','(p(T40, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 17\n\nT40 is ground\nX126 is free\nX124 is free\nzero(T40) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(no(zero(T40)), ','(p(T40, X124), s2t(X124, X126))), SCOPE: 19, CLAUSE: 17\n\nT40 is ground\nX126 is free\nX124 is free\nzero(T40) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(p(T43, X124), s2t(X124, X126))\n\nT43 is ground\nX126 is free\nX124 is free\nzero(T43) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(p(T43, X124), s2t(X124, X126)), SCOPE: 23, CLAUSE: 12 | ','(p(T43, X124), s2t(X124, X126)), SCOPE: 23, CLAUSE: 13\n\nT43 is ground\nX126 is free\nX124 is free\nzero(T43) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(p(T43, X124), s2t(X124, X126)), SCOPE: 23, CLAUSE: 13\n\nT43 is ground\nX126 is free\nX124 is free\nzero(T43) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: s2t(T46, X126)\n\nT46 is ground\nX126 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: s2t(T17, X51), SCOPE: 13, CLAUSE: 6\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: s2t(T17, X51), SCOPE: 13, CLAUSE: 7\n\nT17 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(no(zero(T51)), ','(p(T51, X161), s2t(X161, X162)))\n\nT51 is ground\nX162 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(no(zero(T51)), ','(p(T51, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 16 | ','(no(zero(T51)), ','(p(T51, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 17\n\nT51 is ground\nX162 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(','(call(zero(T54)), ','(!_24, failure(a))), ','(p(T54, X161), s2t(X161, X162))) | ','(no(zero(T54)), ','(p(T54, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 17\n\nT54 is ground\nX162 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(zero(T54), ','(','(!_24, failure(a)), ','(p(T54, X161), s2t(X161, X162)))) | ?_25 | ','(no(zero(T54)), ','(p(T54, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 17\n\nT54 is ground\nX162 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(zero(T54), ','(','(!_24, failure(a)), ','(p(T54, X161), s2t(X161, X162)))), SCOPE: 26, CLAUSE: 15 | ?_26 | ?_25 | ','(no(zero(T54)), ','(p(T54, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 17\n\nT54 is ground\nX162 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(','(!_24, failure(a)), ','(p(0, X161), s2t(X161, X162))) | ?_26 | ?_25 | ','(no(zero(0)), ','(p(0, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 17\n\nX162 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ?_26 | ?_25 | ','(no(zero(T54)), ','(p(T54, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 17\n\nT54 is ground\nX162 is free\nX161 is free\nzero(T54) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(failure(a), ','(p(0, X161), s2t(X161, X162)))\n\nX162 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(failure(a), ','(p(0, X161), s2t(X161, X162))), SCOPE: 27, CLAUSE: 18\n\nX162 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ?_25 | ','(no(zero(T54)), ','(p(T54, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 17\n\nT54 is ground\nX162 is free\nX161 is free\nzero(T54) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(no(zero(T54)), ','(p(T54, X161), s2t(X161, X162))), SCOPE: 24, CLAUSE: 17\n\nT54 is ground\nX162 is free\nX161 is free\nzero(T54) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(p(T57, X161), s2t(X161, X162))\n\nT57 is ground\nX162 is free\nX161 is free\nzero(T57) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(p(T57, X161), s2t(X161, X162)), SCOPE: 28, CLAUSE: 12 | ','(p(T57, X161), s2t(X161, X162)), SCOPE: 28, CLAUSE: 13\n\nT57 is ground\nX162 is free\nX161 is free\nzero(T57) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(p(T57, X161), s2t(X161, X162)), SCOPE: 28, CLAUSE: 13\n\nT57 is ground\nX162 is free\nX161 is free\nzero(T57) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: s2t(T60, X162)\n\nT60 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: no(zero(T63))\n\nT63 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: no(zero(T63)), SCOPE: 29, CLAUSE: 16 | no(zero(T63)), SCOPE: 29, CLAUSE: 17\n\nT63 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(call(zero(T66)), ','(!_29, failure(a))) | no(zero(T66)), SCOPE: 29, CLAUSE: 17\n\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(zero(T66), ','(!_29, failure(a))) | ?_30 | no(zero(T66)), SCOPE: 29, CLAUSE: 17\n\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(zero(T66), ','(!_29, failure(a))), SCOPE: 31, CLAUSE: 15 | ?_31 | ?_30 | no(zero(T66)), SCOPE: 29, CLAUSE: 17\n\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(!_29, failure(a)) | ?_31 | ?_30 | no(zero(0)), SCOPE: 29, CLAUSE: 17\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ?_31 | ?_30 | no(zero(T66)), SCOPE: 29, CLAUSE: 17\n\nT66 is ground\nzero(T66) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: failure(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: failure(a), SCOPE: 32, CLAUSE: 18\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ?_30 | no(zero(T66)), SCOPE: 29, CLAUSE: 17\n\nT66 is ground\nzero(T66) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: no(zero(T66)), SCOPE: 29, CLAUSE: 17\n\nT66 is ground\nzero(T66) !=? zero(0)", 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: tree(node(T18, X52, T18)), SCOPE: 33, CLAUSE: 1 | tree(node(T18, X52, T18)), SCOPE: 33, CLAUSE: 2\n\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: tree(node(T18, X52, T18)), SCOPE: 33, CLAUSE: 2\n\nX52 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198)))))\n\nX199 is free\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))), SCOPE: 34, CLAUSE: 16 | ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))), SCOPE: 34, CLAUSE: 17\n\nX199 is free\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(','(call(empty(node(T79, X205, T79))), ','(!_34, failure(a))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))) | ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))), SCOPE: 34, CLAUSE: 17\n\nX199 is free\nX196 is free\nX197 is free\nX198 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(empty(node(T79, X205, T79)), ','(','(!_34, failure(a)), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198)))))) | ?_35 | ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))), SCOPE: 34, CLAUSE: 17\n\nX199 is free\nX196 is free\nX197 is free\nX198 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(empty(node(T79, X205, T79)), ','(','(!_34, failure(a)), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198)))))), SCOPE: 36, CLAUSE: 14 | ?_36 | ?_35 | ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))), SCOPE: 34, CLAUSE: 17\n\nX199 is free\nX196 is free\nX197 is free\nX198 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ?_36 | ?_35 | ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))), SCOPE: 34, CLAUSE: 17\n\nX199 is free\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ?_35 | ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))), SCOPE: 34, CLAUSE: 17\n\nX199 is free\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(no(empty(node(T74, X199, T74))), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))), SCOPE: 34, CLAUSE: 17\n\nX199 is free\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))\n\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198)))), SCOPE: 37, CLAUSE: 8 | ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198)))), SCOPE: 37, CLAUSE: 9\n\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198)))), SCOPE: 37, CLAUSE: 8\n\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198)))), SCOPE: 37, CLAUSE: 9\n\nX196 is free\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(right(nil, X198), ','(tree(nil), tree(X198)))\n\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(right(nil, X198), ','(tree(nil), tree(X198))), SCOPE: 38, CLAUSE: 10 | ','(right(nil, X198), ','(tree(nil), tree(X198))), SCOPE: 38, CLAUSE: 11\n\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(right(nil, X198), ','(tree(nil), tree(X198))), SCOPE: 38, CLAUSE: 10\n\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(right(nil, X198), ','(tree(nil), tree(X198))), SCOPE: 38, CLAUSE: 11\n\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(right(node(X230, X231, X232), X198), ','(tree(X230), tree(X198)))\n\nX198 is free\nX230 is free\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(right(node(X230, X231, X232), X198), ','(tree(X230), tree(X198))), SCOPE: 39, CLAUSE: 10 | ','(right(node(X230, X231, X232), X198), ','(tree(X230), tree(X198))), SCOPE: 39, CLAUSE: 11\n\nX198 is free\nX230 is free\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(right(node(X230, X231, X232), X198), ','(tree(X230), tree(X198))), SCOPE: 39, CLAUSE: 11\n\nX198 is free\nX230 is free\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(tree(X248), tree(X250))\n\nX248 is free\nX250 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: tree(X248)\n\nX248 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: tree(X250)\n\nX250 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: tree(X250), SCOPE: 40, CLAUSE: 1 | tree(X250), SCOPE: 40, CLAUSE: 2\n\nX250 is free", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: tree(X250), SCOPE: 40, CLAUSE: 1\n\nX250 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: tree(X250), SCOPE: 40, CLAUSE: 2\n\nX250 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(no(empty(X262)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261)))))\n\nX262 is free\nX259 is free\nX260 is free\nX261 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(no(empty(X262)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))), SCOPE: 41, CLAUSE: 16 | ','(no(empty(X262)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))), SCOPE: 41, CLAUSE: 17\n\nX262 is free\nX259 is free\nX260 is free\nX261 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(','(call(empty(X268)), ','(!_41, failure(a))), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))) | ','(no(empty(X262)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))), SCOPE: 41, CLAUSE: 17\n\nX262 is free\nX259 is free\nX260 is free\nX261 is free\nX268 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(empty(X268), ','(','(!_41, failure(a)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261)))))) | ?_42 | ','(no(empty(X262)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))), SCOPE: 41, CLAUSE: 17\n\nX262 is free\nX259 is free\nX260 is free\nX261 is free\nX268 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ','(empty(X268), ','(','(!_41, failure(a)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261)))))), SCOPE: 43, CLAUSE: 14 | ?_43 | ?_42 | ','(no(empty(X262)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))), SCOPE: 41, CLAUSE: 17\n\nX262 is free\nX259 is free\nX260 is free\nX261 is free\nX268 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(','(!_41, failure(a)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))) | ?_43 | ?_42 | ','(no(empty(X262)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))), SCOPE: 41, CLAUSE: 17\n\nX262 is free\nX259 is free\nX260 is free\nX261 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(failure(a), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261)))))\n\nX259 is free\nX260 is free\nX261 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(failure(a), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))), SCOPE: 44, CLAUSE: 18\n\nX259 is free\nX260 is free\nX261 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 5\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 6 | ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(','(no(zero(T88)), ','(p(T88, X294), s2t(X294, X296))), tree(node(nil, X295, X296)))\n\nT88 is ground\nX295 is free\nX296 is free\nX294 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(','(no(zero(T88)), ','(p(T88, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 16 | ','(','(no(zero(T88)), ','(p(T88, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 17\n\nT88 is ground\nX295 is free\nX296 is free\nX294 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(','(call(zero(T91)), ','(!_45, failure(a))), ','(','(p(T91, X294), s2t(X294, X296)), tree(node(nil, X295, X296)))) | ','(','(no(zero(T91)), ','(p(T91, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 17\n\nT91 is ground\nX295 is free\nX296 is free\nX294 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(zero(T91), ','(','(!_45, failure(a)), ','(','(p(T91, X294), s2t(X294, X296)), tree(node(nil, X295, X296))))) | ?_46 | ','(','(no(zero(T91)), ','(p(T91, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 17\n\nT91 is ground\nX295 is free\nX296 is free\nX294 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(zero(T91), ','(','(!_45, failure(a)), ','(','(p(T91, X294), s2t(X294, X296)), tree(node(nil, X295, X296))))), SCOPE: 47, CLAUSE: 15 | ?_47 | ?_46 | ','(','(no(zero(T91)), ','(p(T91, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 17\n\nT91 is ground\nX295 is free\nX296 is free\nX294 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(','(!_45, failure(a)), ','(','(p(0, X294), s2t(X294, X296)), tree(node(nil, X295, X296)))) | ?_47 | ?_46 | ','(','(no(zero(0)), ','(p(0, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 17\n\nX295 is free\nX296 is free\nX294 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ?_47 | ?_46 | ','(','(no(zero(T91)), ','(p(T91, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 17\n\nT91 is ground\nX295 is free\nX296 is free\nX294 is free\nzero(T91) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(failure(a), ','(','(p(0, X294), s2t(X294, X296)), tree(node(nil, X295, X296))))\n\nX295 is free\nX296 is free\nX294 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: ','(failure(a), ','(','(p(0, X294), s2t(X294, X296)), tree(node(nil, X295, X296)))), SCOPE: 48, CLAUSE: 18\n\nX295 is free\nX296 is free\nX294 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ?_46 | ','(','(no(zero(T91)), ','(p(T91, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 17\n\nT91 is ground\nX295 is free\nX296 is free\nX294 is free\nzero(T91) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(','(no(zero(T91)), ','(p(T91, X294), s2t(X294, X296))), tree(node(nil, X295, X296))), SCOPE: 45, CLAUSE: 17\n\nT91 is ground\nX295 is free\nX296 is free\nX294 is free\nzero(T91) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(','(p(T94, X294), s2t(X294, X296)), tree(node(nil, X295, X296)))\n\nT94 is ground\nX295 is free\nX296 is free\nX294 is free\nzero(T94) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ','(','(p(T94, X294), s2t(X294, X296)), tree(node(nil, X295, X296))), SCOPE: 49, CLAUSE: 12 | ','(','(p(T94, X294), s2t(X294, X296)), tree(node(nil, X295, X296))), SCOPE: 49, CLAUSE: 13\n\nT94 is ground\nX295 is free\nX296 is free\nX294 is free\nzero(T94) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(','(p(T94, X294), s2t(X294, X296)), tree(node(nil, X295, X296))), SCOPE: 49, CLAUSE: 13\n\nT94 is ground\nX295 is free\nX296 is free\nX294 is free\nzero(T94) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: ','(s2t(T97, X296), tree(node(nil, X295, X296)))\n\nT97 is ground\nX295 is free\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: s2t(T97, X296)\n\nT97 is ground\nX296 is free", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: tree(node(nil, X295, T98))\n\nX295 is free", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: tree(node(nil, X295, T98)), SCOPE: 50, CLAUSE: 1 | tree(node(nil, X295, T98)), SCOPE: 50, CLAUSE: 2\n\nX295 is free", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: tree(node(nil, X295, T98)), SCOPE: 50, CLAUSE: 2\n\nX295 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316)))))\n\nX317 is free\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))), SCOPE: 51, CLAUSE: 16 | ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))), SCOPE: 51, CLAUSE: 17\n\nX317 is free\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(','(call(empty(node(nil, X323, T108))), ','(!_51, failure(a))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))) | ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))), SCOPE: 51, CLAUSE: 17\n\nX317 is free\nX314 is free\nX315 is free\nX316 is free\nX323 is free", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(empty(node(nil, X323, T108)), ','(','(!_51, failure(a)), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316)))))) | ?_52 | ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))), SCOPE: 51, CLAUSE: 17\n\nX317 is free\nX314 is free\nX315 is free\nX316 is free\nX323 is free", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(empty(node(nil, X323, T108)), ','(','(!_51, failure(a)), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316)))))), SCOPE: 53, CLAUSE: 14 | ?_53 | ?_52 | ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))), SCOPE: 51, CLAUSE: 17\n\nX317 is free\nX314 is free\nX315 is free\nX316 is free\nX323 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ?_53 | ?_52 | ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))), SCOPE: 51, CLAUSE: 17\n\nX317 is free\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ?_52 | ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))), SCOPE: 51, CLAUSE: 17\n\nX317 is free\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(no(empty(node(nil, X317, T103))), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))), SCOPE: 51, CLAUSE: 17\n\nX317 is free\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))\n\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316)))), SCOPE: 54, CLAUSE: 8 | ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316)))), SCOPE: 54, CLAUSE: 9\n\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316)))), SCOPE: 54, CLAUSE: 8\n\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316)))), SCOPE: 54, CLAUSE: 9\n\nX314 is free\nX315 is free\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(right(nil, X316), ','(tree(nil), tree(X316)))\n\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(right(nil, X316), ','(tree(nil), tree(X316))), SCOPE: 55, CLAUSE: 10 | ','(right(nil, X316), ','(tree(nil), tree(X316))), SCOPE: 55, CLAUSE: 11\n\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ','(right(nil, X316), ','(tree(nil), tree(X316))), SCOPE: 55, CLAUSE: 10\n\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(right(nil, X316), ','(tree(nil), tree(X316))), SCOPE: 55, CLAUSE: 11\n\nX316 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: ','(right(node(X348, X349, X350), X316), ','(tree(X348), tree(X316)))\n\nX316 is free\nX348 is free\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(right(node(X348, X349, X350), X316), ','(tree(X348), tree(X316))), SCOPE: 56, CLAUSE: 10 | ','(right(node(X348, X349, X350), X316), ','(tree(X348), tree(X316))), SCOPE: 56, CLAUSE: 11\n\nX316 is free\nX348 is free\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(right(node(X348, X349, X350), X316), ','(tree(X348), tree(X316))), SCOPE: 56, CLAUSE: 11\n\nX316 is free\nX348 is free\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(tree(X366), tree(X368))\n\nX366 is free\nX368 is free", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(s2t(T3, X12), tree(X12)), SCOPE: 2, CLAUSE: 7\n\nT3 is ground\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(','(no(zero(T116)), ','(p(T116, X394), s2t(X394, X395))), tree(node(X395, X396, nil)))\n\nT116 is ground\nX395 is free\nX396 is free\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ','(','(no(zero(T116)), ','(p(T116, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 16 | ','(','(no(zero(T116)), ','(p(T116, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 17\n\nT116 is ground\nX395 is free\nX396 is free\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ','(','(call(zero(T119)), ','(!_57, failure(a))), ','(','(p(T119, X394), s2t(X394, X395)), tree(node(X395, X396, nil)))) | ','(','(no(zero(T119)), ','(p(T119, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 17\n\nT119 is ground\nX395 is free\nX396 is free\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(zero(T119), ','(','(!_57, failure(a)), ','(','(p(T119, X394), s2t(X394, X395)), tree(node(X395, X396, nil))))) | ?_58 | ','(','(no(zero(T119)), ','(p(T119, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 17\n\nT119 is ground\nX395 is free\nX396 is free\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(zero(T119), ','(','(!_57, failure(a)), ','(','(p(T119, X394), s2t(X394, X395)), tree(node(X395, X396, nil))))), SCOPE: 59, CLAUSE: 15 | ?_59 | ?_58 | ','(','(no(zero(T119)), ','(p(T119, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 17\n\nT119 is ground\nX395 is free\nX396 is free\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(','(!_57, failure(a)), ','(','(p(0, X394), s2t(X394, X395)), tree(node(X395, X396, nil)))) | ?_59 | ?_58 | ','(','(no(zero(0)), ','(p(0, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 17\n\nX395 is free\nX396 is free\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ?_59 | ?_58 | ','(','(no(zero(T119)), ','(p(T119, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 17\n\nT119 is ground\nX395 is free\nX396 is free\nX394 is free\nzero(T119) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(failure(a), ','(','(p(0, X394), s2t(X394, X395)), tree(node(X395, X396, nil))))\n\nX395 is free\nX396 is free\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(failure(a), ','(','(p(0, X394), s2t(X394, X395)), tree(node(X395, X396, nil)))), SCOPE: 60, CLAUSE: 18\n\nX395 is free\nX396 is free\nX394 is free", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: ?_58 | ','(','(no(zero(T119)), ','(p(T119, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 17\n\nT119 is ground\nX395 is free\nX396 is free\nX394 is free\nzero(T119) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(','(no(zero(T119)), ','(p(T119, X394), s2t(X394, X395))), tree(node(X395, X396, nil))), SCOPE: 57, CLAUSE: 17\n\nT119 is ground\nX395 is free\nX396 is free\nX394 is free\nzero(T119) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: ','(','(p(T122, X394), s2t(X394, X395)), tree(node(X395, X396, nil)))\n\nT122 is ground\nX395 is free\nX396 is free\nX394 is free\nzero(T122) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: ','(','(p(T122, X394), s2t(X394, X395)), tree(node(X395, X396, nil))), SCOPE: 61, CLAUSE: 12 | ','(','(p(T122, X394), s2t(X394, X395)), tree(node(X395, X396, nil))), SCOPE: 61, CLAUSE: 13\n\nT122 is ground\nX395 is free\nX396 is free\nX394 is free\nzero(T122) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ','(','(p(T122, X394), s2t(X394, X395)), tree(node(X395, X396, nil))), SCOPE: 61, CLAUSE: 13\n\nT122 is ground\nX395 is free\nX396 is free\nX394 is free\nzero(T122) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(s2t(T125, X395), tree(node(X395, X396, nil)))\n\nT125 is ground\nX395 is free\nX396 is free", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: s2t(T125, X395)\n\nT125 is ground\nX395 is free", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: tree(node(T126, X396, nil))\n\nX396 is free", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: tree(node(T126, X396, nil)), SCOPE: 62, CLAUSE: 1 | tree(node(T126, X396, nil)), SCOPE: 62, CLAUSE: 2\n\nX396 is free", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: tree(node(T126, X396, nil)), SCOPE: 62, CLAUSE: 2\n\nX396 is free", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416)))))\n\nX417 is free\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))), SCOPE: 63, CLAUSE: 16 | ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))), SCOPE: 63, CLAUSE: 17\n\nX417 is free\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: ','(','(call(empty(node(T136, X423, nil))), ','(!_63, failure(a))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))) | ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))), SCOPE: 63, CLAUSE: 17\n\nX417 is free\nX414 is free\nX415 is free\nX416 is free\nX423 is free", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(empty(node(T136, X423, nil)), ','(','(!_63, failure(a)), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416)))))) | ?_64 | ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))), SCOPE: 63, CLAUSE: 17\n\nX417 is free\nX414 is free\nX415 is free\nX416 is free\nX423 is free", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: ','(empty(node(T136, X423, nil)), ','(','(!_63, failure(a)), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416)))))), SCOPE: 65, CLAUSE: 14 | ?_65 | ?_64 | ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))), SCOPE: 63, CLAUSE: 17\n\nX417 is free\nX414 is free\nX415 is free\nX416 is free\nX423 is free", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: ?_65 | ?_64 | ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))), SCOPE: 63, CLAUSE: 17\n\nX417 is free\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: ?_64 | ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))), SCOPE: 63, CLAUSE: 17\n\nX417 is free\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ','(no(empty(node(T131, X417, nil))), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))), SCOPE: 63, CLAUSE: 17\n\nX417 is free\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))\n\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416)))), SCOPE: 66, CLAUSE: 8 | ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416)))), SCOPE: 66, CLAUSE: 9\n\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416)))), SCOPE: 66, CLAUSE: 8\n\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416)))), SCOPE: 66, CLAUSE: 9\n\nX414 is free\nX415 is free\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: ','(right(nil, X416), ','(tree(nil), tree(X416)))\n\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: ','(right(nil, X416), ','(tree(nil), tree(X416))), SCOPE: 67, CLAUSE: 10 | ','(right(nil, X416), ','(tree(nil), tree(X416))), SCOPE: 67, CLAUSE: 11\n\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: ','(right(nil, X416), ','(tree(nil), tree(X416))), SCOPE: 67, CLAUSE: 10\n\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: ','(right(nil, X416), ','(tree(nil), tree(X416))), SCOPE: 67, CLAUSE: 11\n\nX416 is free", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(right(node(X448, X449, X450), X416), ','(tree(X448), tree(X416)))\n\nX416 is free\nX448 is free\nX449 is free\nX450 is free", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ','(right(node(X448, X449, X450), X416), ','(tree(X448), tree(X416))), SCOPE: 68, CLAUSE: 10 | ','(right(node(X448, X449, X450), X416), ','(tree(X448), tree(X416))), SCOPE: 68, CLAUSE: 11\n\nX416 is free\nX448 is free\nX449 is free\nX450 is free", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: ','(right(node(X448, X449, X450), X416), ','(tree(X448), tree(X416))), SCOPE: 68, CLAUSE: 11\n\nX416 is free\nX448 is free\nX449 is free\nX450 is free", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: ','(tree(X466), tree(X468))\n\nX466 is free\nX468 is free", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: ','(no(zero(T142)), tree(node(nil, X477, nil)))\n\nT142 is ground\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: ','(no(zero(T142)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 16 | ','(no(zero(T142)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 17\n\nT142 is ground\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: ','(','(call(zero(T145)), ','(!_69, failure(a))), tree(node(nil, X477, nil))) | ','(no(zero(T145)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 17\n\nT145 is ground\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: ','(zero(T145), ','(','(!_69, failure(a)), tree(node(nil, X477, nil)))) | ?_70 | ','(no(zero(T145)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 17\n\nT145 is ground\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: ','(zero(T145), ','(','(!_69, failure(a)), tree(node(nil, X477, nil)))), SCOPE: 71, CLAUSE: 15 | ?_71 | ?_70 | ','(no(zero(T145)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 17\n\nT145 is ground\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: ','(','(!_69, failure(a)), tree(node(nil, X477, nil))) | ?_71 | ?_70 | ','(no(zero(0)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 17\n\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: ?_71 | ?_70 | ','(no(zero(T145)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 17\n\nT145 is ground\nX477 is free\nzero(T145) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: ','(failure(a), tree(node(nil, X477, nil)))\n\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(failure(a), tree(node(nil, X477, nil))), SCOPE: 72, CLAUSE: 18\n\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: ?_70 | ','(no(zero(T145)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 17\n\nT145 is ground\nX477 is free\nzero(T145) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: ','(no(zero(T145)), tree(node(nil, X477, nil))), SCOPE: 69, CLAUSE: 17\n\nT145 is ground\nX477 is free\nzero(T145) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: tree(node(nil, X477, nil))\n\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: tree(node(nil, X477, nil)), SCOPE: 73, CLAUSE: 1 | tree(node(nil, X477, nil)), SCOPE: 73, CLAUSE: 2\n\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: tree(node(nil, X477, nil)), SCOPE: 73, CLAUSE: 2\n\nX477 is free", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494)))))\n\nX495 is free\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))), SCOPE: 74, CLAUSE: 16 | ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))), SCOPE: 74, CLAUSE: 17\n\nX495 is free\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: ','(','(call(empty(node(nil, X501, nil))), ','(!_74, failure(a))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))) | ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))), SCOPE: 74, CLAUSE: 17\n\nX495 is free\nX492 is free\nX493 is free\nX494 is free\nX501 is free", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: ','(empty(node(nil, X501, nil)), ','(','(!_74, failure(a)), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494)))))) | ?_75 | ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))), SCOPE: 74, CLAUSE: 17\n\nX495 is free\nX492 is free\nX493 is free\nX494 is free\nX501 is free", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: ','(empty(node(nil, X501, nil)), ','(','(!_74, failure(a)), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494)))))), SCOPE: 76, CLAUSE: 14 | ?_76 | ?_75 | ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))), SCOPE: 74, CLAUSE: 17\n\nX495 is free\nX492 is free\nX493 is free\nX494 is free\nX501 is free", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: ?_76 | ?_75 | ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))), SCOPE: 74, CLAUSE: 17\n\nX495 is free\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: ?_75 | ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))), SCOPE: 74, CLAUSE: 17\n\nX495 is free\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: ','(no(empty(node(nil, X495, nil))), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))), SCOPE: 74, CLAUSE: 17\n\nX495 is free\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))\n\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494)))), SCOPE: 77, CLAUSE: 8 | ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494)))), SCOPE: 77, CLAUSE: 9\n\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494)))), SCOPE: 77, CLAUSE: 8\n\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494)))), SCOPE: 77, CLAUSE: 9\n\nX492 is free\nX493 is free\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: ','(right(nil, X494), ','(tree(nil), tree(X494)))\n\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: ','(right(nil, X494), ','(tree(nil), tree(X494))), SCOPE: 78, CLAUSE: 10 | ','(right(nil, X494), ','(tree(nil), tree(X494))), SCOPE: 78, CLAUSE: 11\n\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: ','(right(nil, X494), ','(tree(nil), tree(X494))), SCOPE: 78, CLAUSE: 10\n\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: ','(right(nil, X494), ','(tree(nil), tree(X494))), SCOPE: 78, CLAUSE: 11\n\nX494 is free", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: ','(right(node(X526, X527, X528), X494), ','(tree(X526), tree(X494)))\n\nX494 is free\nX526 is free\nX527 is free\nX528 is free", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: ','(right(node(X526, X527, X528), X494), ','(tree(X526), tree(X494))), SCOPE: 79, CLAUSE: 10 | ','(right(node(X526, X527, X528), X494), ','(tree(X526), tree(X494))), SCOPE: 79, CLAUSE: 11\n\nX494 is free\nX526 is free\nX527 is free\nX528 is free", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: ','(right(node(X526, X527, X528), X494), ','(tree(X526), tree(X494))), SCOPE: 79, CLAUSE: 11\n\nX494 is free\nX526 is free\nX527 is free\nX528 is free", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: ','(tree(X544), tree(X546))\n\nX544 is free\nX546 is free", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 290 [arrowhead = none ];
290 -> 2;

291 [label="ONLY EVAL with clause\ngoal(X11) :- ','(s2t(X11, X12), tree(X12)).\nand substitutionT1 -> T3,\nX11 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 291 [arrowhead = none ];
291 -> 3;

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

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

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

295 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT3 -> 0,\nX12 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 295 [arrowhead = none ];
295 -> 7;

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

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

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

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

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

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

302 [label="ONLY EVAL with clause\ntree(nil).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 302 [arrowhead = none ];
302 -> 12;

303 [label="ONLY EVAL with clause\ntree(X18) :- ','(no(empty(X18)), ','(left(X19, X20), ','(right(X19, X21), ','(tree(X20), tree(X21))))).\nand substitutionX18 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 303 [arrowhead = none ];
303 -> 14;

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

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

306 [label="ONLY EVAL with clause\nno(X24) :- ','(call(X24), ','(!_4, failure(a))).\nand substitutionX24 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 306 [arrowhead = none ];
306 -> 16;

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

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

309 [label="ONLY EVAL with clause\nempty(nil).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 309 [arrowhead = none ];
309 -> 19;

310 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 310 [arrowhead = none ];
310 -> 20;

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

312 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 312 [arrowhead = none ];
312 -> 22;

313 [label="ONLY EVAL with clause\ns2t(X47, node(X48, X49, X48)) :- ','(no(zero(X47)), ','(p(X47, X50), s2t(X50, X48))).\nand substitutionT3 -> T8,\nX47 -> T8,\nX48 -> X51,\nX49 -> X52,\nX12 -> node(X51, X52, X51)", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 313 [arrowhead = none ];
313 -> 25;

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

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

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

317 [label="ONLY EVAL with clause\nno(X55) :- ','(call(X55), ','(!_8, failure(a))).\nand substitutionT8 -> T11,\nX55 -> zero(T11)", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 317 [arrowhead = none ];
317 -> 27;

318 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
27 -> 318 [arrowhead = none ];
318 -> 28;

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

320 [label="EVAL with clause\nzero(0).\nand substitutionT11 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 320 [arrowhead = none ];
320 -> 30;

321 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 321 [arrowhead = none ];
321 -> 31;

322 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 322 [arrowhead = none ];
322 -> 32;

323 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 323 [arrowhead = none ];
323 -> 35;

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

325 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 325 [arrowhead = none ];
325 -> 34;

326 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 326 [arrowhead = none ];
326 -> 36;

327 [label="ONLY EVAL with clause\nno(X58).\nand substitutionT11 -> T14,\nX58 -> zero(T14)", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 327 [arrowhead = none ];
327 -> 37;

328 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
37 -> 328 [arrowhead = none ];
328 -> 38;

329 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T14), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 329 [arrowhead = none ];
329 -> 39;

330 [label="EVAL with clause\np(s(X61), X61).\nand substitutionX61 -> T17,\nT14 -> s(T17),\nX50 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 330 [arrowhead = none ];
330 -> 40;

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

332 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 332 [arrowhead = none ];
332 -> 42;

333 [label="SPLIT 2\nnew knowledge:\nT17 is ground\nreplacements:X51 -> T18", fontsize=14, style = filled, fillcolor = violet];
40 -> 333 [arrowhead = none ];
333 -> 43;

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

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

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

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

338 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT17 -> 0,\nX51 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 338 [arrowhead = none ];
338 -> 47;

339 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 339 [arrowhead = none ];
339 -> 48;

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

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

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

343 [label="ONLY EVAL with clause\ns2t(X84, node(X85, X86, X85)) :- ','(no(zero(X84)), ','(p(X84, X87), s2t(X87, X85))).\nand substitutionT17 -> T23,\nX84 -> T23,\nX85 -> X88,\nX86 -> X89,\nX51 -> node(X88, X89, X88)", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 343 [arrowhead = none ];
343 -> 52;

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

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

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

347 [label="ONLY EVAL with clause\nno(X92) :- ','(call(X92), ','(!_14, failure(a))).\nand substitutionT23 -> T26,\nX92 -> zero(T26)", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 347 [arrowhead = none ];
347 -> 54;

348 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
54 -> 348 [arrowhead = none ];
348 -> 55;

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

350 [label="EVAL with clause\nzero(0).\nand substitutionT26 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 350 [arrowhead = none ];
350 -> 57;

351 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 351 [arrowhead = none ];
351 -> 58;

352 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 352 [arrowhead = none ];
352 -> 59;

353 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 353 [arrowhead = none ];
353 -> 62;

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

355 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 355 [arrowhead = none ];
355 -> 61;

356 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 356 [arrowhead = none ];
356 -> 63;

357 [label="ONLY EVAL with clause\nno(X95).\nand substitutionT26 -> T29,\nX95 -> zero(T29)", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 357 [arrowhead = none ];
357 -> 64;

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

359 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T29), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 359 [arrowhead = none ];
359 -> 66;

360 [label="EVAL with clause\np(s(X98), X98).\nand substitutionX98 -> T32,\nT29 -> s(T32),\nX87 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 360 [arrowhead = none ];
360 -> 67;

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

362 [label="INSTANCE with matching:\nT17 -> T32\nX51 -> X88", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 362 [arrowhead = none , style=dashed];
362 -> 42[style=dashed];

363 [label="ONLY EVAL with clause\ns2t(X121, node(nil, X122, X123)) :- ','(no(zero(X121)), ','(p(X121, X124), s2t(X124, X123))).\nand substitutionT17 -> T37,\nX121 -> T37,\nX122 -> X125,\nX123 -> X126,\nX51 -> node(nil, X125, X126)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 363 [arrowhead = none ];
363 -> 71;

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

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

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

367 [label="ONLY EVAL with clause\nno(X129) :- ','(call(X129), ','(!_19, failure(a))).\nand substitutionT37 -> T40,\nX129 -> zero(T40)", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 367 [arrowhead = none ];
367 -> 73;

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

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

370 [label="EVAL with clause\nzero(0).\nand substitutionT40 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 370 [arrowhead = none ];
370 -> 76;

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

372 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 372 [arrowhead = none ];
372 -> 78;

373 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 373 [arrowhead = none ];
373 -> 81;

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

375 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 375 [arrowhead = none ];
375 -> 80;

376 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 376 [arrowhead = none ];
376 -> 82;

377 [label="ONLY EVAL with clause\nno(X132).\nand substitutionT40 -> T43,\nX132 -> zero(T43)", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 377 [arrowhead = none ];
377 -> 83;

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

379 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T43), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 379 [arrowhead = none ];
379 -> 85;

380 [label="EVAL with clause\np(s(X135), X135).\nand substitutionX135 -> T46,\nT43 -> s(T46),\nX124 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 380 [arrowhead = none ];
380 -> 86;

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

382 [label="INSTANCE with matching:\nT17 -> T46\nX51 -> X126", fontsize=14, style = filled, fillcolor = lightgrey];
86 -> 382 [arrowhead = none , style=dashed];
382 -> 42[style=dashed];

383 [label="ONLY EVAL with clause\ns2t(X158, node(X159, X160, nil)) :- ','(no(zero(X158)), ','(p(X158, X161), s2t(X161, X159))).\nand substitutionT17 -> T51,\nX158 -> T51,\nX159 -> X162,\nX160 -> X163,\nX51 -> node(X162, X163, nil)", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 383 [arrowhead = none ];
383 -> 90;

384 [label="ONLY EVAL with clause\ns2t(X179, node(nil, X180, nil)) :- no(zero(X179)).\nand substitutionT17 -> T63,\nX179 -> T63,\nX180 -> X181,\nX51 -> node(nil, X181, nil)", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 384 [arrowhead = none ];
384 -> 107;

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

386 [label="ONLY EVAL with clause\nno(X166) :- ','(call(X166), ','(!_24, failure(a))).\nand substitutionT51 -> T54,\nX166 -> zero(T54)", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 386 [arrowhead = none ];
386 -> 92;

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

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

389 [label="EVAL with clause\nzero(0).\nand substitutionT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 389 [arrowhead = none ];
389 -> 95;

390 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 390 [arrowhead = none ];
390 -> 96;

391 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 391 [arrowhead = none ];
391 -> 97;

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

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

394 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 394 [arrowhead = none ];
394 -> 99;

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

396 [label="ONLY EVAL with clause\nno(X169).\nand substitutionT54 -> T57,\nX169 -> zero(T57)", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 396 [arrowhead = none ];
396 -> 102;

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

398 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T57), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 398 [arrowhead = none ];
398 -> 104;

399 [label="EVAL with clause\np(s(X172), X172).\nand substitutionX172 -> T60,\nT57 -> s(T60),\nX161 -> T60", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 399 [arrowhead = none ];
399 -> 105;

400 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 400 [arrowhead = none ];
400 -> 106;

401 [label="INSTANCE with matching:\nT17 -> T60\nX51 -> X162", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 401 [arrowhead = none , style=dashed];
401 -> 42[style=dashed];

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

403 [label="ONLY EVAL with clause\nno(X184) :- ','(call(X184), ','(!_29, failure(a))).\nand substitutionT63 -> T66,\nX184 -> zero(T66)", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 403 [arrowhead = none ];
403 -> 109;

404 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
109 -> 404 [arrowhead = none ];
404 -> 110;

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

406 [label="EVAL with clause\nzero(0).\nand substitutionT66 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 406 [arrowhead = none ];
406 -> 112;

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

408 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 408 [arrowhead = none ];
408 -> 114;

409 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 409 [arrowhead = none ];
409 -> 117;

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

411 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 411 [arrowhead = none ];
411 -> 116;

412 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 412 [arrowhead = none ];
412 -> 118;

413 [label="ONLY EVAL with clause\nno(X187).\nand substitutionT66 -> T69,\nX187 -> zero(T69)", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 413 [arrowhead = none ];
413 -> 119;

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

415 [label="BACKTRACK\nfor clause: tree(nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
121 -> 415 [arrowhead = none ];
415 -> 122;

416 [label="ONLY EVAL with clause\ntree(X195) :- ','(no(empty(X195)), ','(left(X196, X197), ','(right(X196, X198), ','(tree(X197), tree(X198))))).\nand substitutionT18 -> T74,\nX52 -> X199,\nX195 -> node(T74, X199, T74),\nT73 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 416 [arrowhead = none ];
416 -> 123;

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

418 [label="ONLY EVAL with clause\nno(X204) :- ','(call(X204), ','(!_34, failure(a))).\nand substitutionT74 -> T79,\nX199 -> X205,\nX204 -> empty(node(T79, X205, T79)),\nT78 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 418 [arrowhead = none ];
418 -> 125;

419 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
125 -> 419 [arrowhead = none ];
419 -> 126;

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

421 [label="BACKTRACK\nfor clause: empty(nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 421 [arrowhead = none ];
421 -> 128;

422 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 422 [arrowhead = none ];
422 -> 129;

423 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 423 [arrowhead = none ];
423 -> 130;

424 [label="ONLY EVAL with clause\nno(X210).\nand substitutionT74 -> T82,\nX199 -> X211,\nX210 -> empty(node(T82, X211, T82))", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 424 [arrowhead = none ];
424 -> 131;

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

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

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

428 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitutionX196 -> nil,\nX197 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 428 [arrowhead = none ];
428 -> 135;

429 [label="ONLY EVAL with clause\nleft(node(X227, X228, X229), X227).\nand substitutionX227 -> X230,\nX228 -> X231,\nX229 -> X232,\nX196 -> node(X230, X231, X232),\nX197 -> X230", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 429 [arrowhead = none ];
429 -> 143;

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

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

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

433 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitutionX198 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 433 [arrowhead = none ];
433 -> 139;

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

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

436 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
139 -> 436 [arrowhead = none ];
436 -> 141;

437 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
140 -> 437 [arrowhead = none , style=dashed];
437 -> 7[style=dashed];

438 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
141 -> 438 [arrowhead = none , style=dashed];
438 -> 7[style=dashed];

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

440 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 440 [arrowhead = none ];
440 -> 145;

441 [label="ONLY EVAL with clause\nright(node(X245, X246, X247), X247).\nand substitutionX230 -> X248,\nX245 -> X248,\nX231 -> X249,\nX246 -> X249,\nX232 -> X250,\nX247 -> X250,\nX198 -> X250", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 441 [arrowhead = none ];
441 -> 146;

442 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
146 -> 442 [arrowhead = none ];
442 -> 147;

443 [label="SPLIT 2\nreplacements:X248 -> T83", fontsize=14, style = filled, fillcolor = violet];
146 -> 443 [arrowhead = none ];
443 -> 148;

444 [label="INSTANCE with matching:\nX250 -> X248", fontsize=14, style = filled, fillcolor = lightgrey];
147 -> 444 [arrowhead = none , style=dashed];
444 -> 148[style=dashed];

445 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
148 -> 445 [arrowhead = none ];
445 -> 149;

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

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

448 [label="ONLY EVAL with clause\ntree(nil).\nand substitutionX250 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 448 [arrowhead = none ];
448 -> 152;

449 [label="ONLY EVAL with clause\ntree(X258) :- ','(no(empty(X258)), ','(left(X259, X260), ','(right(X259, X261), ','(tree(X260), tree(X261))))).\nand substitutionX250 -> X262,\nX258 -> X262", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 449 [arrowhead = none ];
449 -> 154;

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

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

452 [label="ONLY EVAL with clause\nno(X267) :- ','(call(X267), ','(!_41, failure(a))).\nand substitutionX262 -> X268,\nX267 -> empty(X268)", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 452 [arrowhead = none ];
452 -> 156;

453 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
156 -> 453 [arrowhead = none ];
453 -> 157;

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

455 [label="ONLY EVAL with clause\nempty(nil).\nand substitutionX268 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 455 [arrowhead = none ];
455 -> 159;

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

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

458 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
161 -> 458 [arrowhead = none ];
458 -> 162;

459 [label="ONLY EVAL with clause\ns2t(X291, node(nil, X292, X293)) :- ','(no(zero(X291)), ','(p(X291, X294), s2t(X294, X293))).\nand substitutionT3 -> T88,\nX291 -> T88,\nX292 -> X295,\nX293 -> X296,\nX12 -> node(nil, X295, X296)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 459 [arrowhead = none ];
459 -> 165;

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

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

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

463 [label="ONLY EVAL with clause\nno(X299) :- ','(call(X299), ','(!_45, failure(a))).\nand substitutionT88 -> T91,\nX299 -> zero(T91)", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 463 [arrowhead = none ];
463 -> 167;

464 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
167 -> 464 [arrowhead = none ];
464 -> 168;

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

466 [label="EVAL with clause\nzero(0).\nand substitutionT91 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 466 [arrowhead = none ];
466 -> 170;

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

468 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
170 -> 468 [arrowhead = none ];
468 -> 172;

469 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
171 -> 469 [arrowhead = none ];
469 -> 175;

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

471 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 471 [arrowhead = none ];
471 -> 174;

472 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
175 -> 472 [arrowhead = none ];
472 -> 176;

473 [label="ONLY EVAL with clause\nno(X302).\nand substitutionT91 -> T94,\nX302 -> zero(T94)", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 473 [arrowhead = none ];
473 -> 177;

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

475 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T94), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
178 -> 475 [arrowhead = none ];
475 -> 179;

476 [label="EVAL with clause\np(s(X305), X305).\nand substitutionX305 -> T97,\nT94 -> s(T97),\nX294 -> T97", fontsize=14, style = filled, fillcolor = lightblue];
179 -> 476 [arrowhead = none ];
476 -> 180;

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

478 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
180 -> 478 [arrowhead = none ];
478 -> 182;

479 [label="SPLIT 2\nnew knowledge:\nT97 is ground\nreplacements:X296 -> T98", fontsize=14, style = filled, fillcolor = violet];
180 -> 479 [arrowhead = none ];
479 -> 183;

480 [label="INSTANCE with matching:\nT17 -> T97\nX51 -> X296", fontsize=14, style = filled, fillcolor = lightgrey];
182 -> 480 [arrowhead = none , style=dashed];
480 -> 42[style=dashed];

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

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

483 [label="ONLY EVAL with clause\ntree(X313) :- ','(no(empty(X313)), ','(left(X314, X315), ','(right(X314, X316), ','(tree(X315), tree(X316))))).\nand substitutionX295 -> X317,\nT98 -> T103,\nX313 -> node(nil, X317, T103),\nT102 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 483 [arrowhead = none ];
483 -> 186;

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

485 [label="ONLY EVAL with clause\nno(X322) :- ','(call(X322), ','(!_51, failure(a))).\nand substitutionX317 -> X323,\nT103 -> T108,\nX322 -> empty(node(nil, X323, T108)),\nT107 -> T108", fontsize=14, style = filled, fillcolor = lightblue];
187 -> 485 [arrowhead = none ];
485 -> 188;

486 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
188 -> 486 [arrowhead = none ];
486 -> 189;

487 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
189 -> 487 [arrowhead = none ];
487 -> 190;

488 [label="BACKTRACK\nfor clause: empty(nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
190 -> 488 [arrowhead = none ];
488 -> 191;

489 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
191 -> 489 [arrowhead = none ];
489 -> 192;

490 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
192 -> 490 [arrowhead = none ];
490 -> 193;

491 [label="ONLY EVAL with clause\nno(X328).\nand substitutionX317 -> X329,\nT103 -> T111,\nX328 -> empty(node(nil, X329, T111))", fontsize=14, style = filled, fillcolor = lightblue];
193 -> 491 [arrowhead = none ];
491 -> 194;

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

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

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

495 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitutionX314 -> nil,\nX315 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 495 [arrowhead = none ];
495 -> 198;

496 [label="ONLY EVAL with clause\nleft(node(X345, X346, X347), X345).\nand substitutionX345 -> X348,\nX346 -> X349,\nX347 -> X350,\nX314 -> node(X348, X349, X350),\nX315 -> X348", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 496 [arrowhead = none ];
496 -> 204;

497 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
198 -> 497 [arrowhead = none ];
497 -> 199;

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

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

500 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitutionX316 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 500 [arrowhead = none ];
500 -> 202;

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

502 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
202 -> 502 [arrowhead = none , style=dashed];
502 -> 139[style=dashed];

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

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

505 [label="ONLY EVAL with clause\nright(node(X363, X364, X365), X365).\nand substitutionX348 -> X366,\nX363 -> X366,\nX349 -> X367,\nX364 -> X367,\nX350 -> X368,\nX365 -> X368,\nX316 -> X368", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 505 [arrowhead = none ];
505 -> 207;

506 [label="INSTANCE with matching:\nX248 -> X366\nX250 -> X368", fontsize=14, style = filled, fillcolor = lightgrey];
207 -> 506 [arrowhead = none , style=dashed];
506 -> 146[style=dashed];

507 [label="ONLY EVAL with clause\ns2t(X391, node(X392, X393, nil)) :- ','(no(zero(X391)), ','(p(X391, X394), s2t(X394, X392))).\nand substitutionT3 -> T116,\nX391 -> T116,\nX392 -> X395,\nX393 -> X396,\nX12 -> node(X395, X396, nil)", fontsize=14, style = filled, fillcolor = lightblue];
208 -> 507 [arrowhead = none ];
507 -> 210;

508 [label="ONLY EVAL with clause\ns2t(X475, node(nil, X476, nil)) :- no(zero(X475)).\nand substitutionT3 -> T142,\nX475 -> T142,\nX476 -> X477,\nX12 -> node(nil, X477, nil)", fontsize=14, style = filled, fillcolor = lightblue];
209 -> 508 [arrowhead = none ];
508 -> 253;

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

510 [label="ONLY EVAL with clause\nno(X399) :- ','(call(X399), ','(!_57, failure(a))).\nand substitutionT116 -> T119,\nX399 -> zero(T119)", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 510 [arrowhead = none ];
510 -> 212;

511 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
212 -> 511 [arrowhead = none ];
511 -> 213;

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

513 [label="EVAL with clause\nzero(0).\nand substitutionT119 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
214 -> 513 [arrowhead = none ];
513 -> 215;

514 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
214 -> 514 [arrowhead = none ];
514 -> 216;

515 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
215 -> 515 [arrowhead = none ];
515 -> 217;

516 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
216 -> 516 [arrowhead = none ];
516 -> 220;

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

518 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
218 -> 518 [arrowhead = none ];
518 -> 219;

519 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
220 -> 519 [arrowhead = none ];
519 -> 221;

520 [label="ONLY EVAL with clause\nno(X402).\nand substitutionT119 -> T122,\nX402 -> zero(T122)", fontsize=14, style = filled, fillcolor = lightblue];
221 -> 520 [arrowhead = none ];
520 -> 222;

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

522 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T122), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
223 -> 522 [arrowhead = none ];
522 -> 224;

523 [label="EVAL with clause\np(s(X405), X405).\nand substitutionX405 -> T125,\nT122 -> s(T125),\nX394 -> T125", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 523 [arrowhead = none ];
523 -> 225;

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

525 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
225 -> 525 [arrowhead = none ];
525 -> 227;

526 [label="SPLIT 2\nnew knowledge:\nT125 is ground\nreplacements:X395 -> T126", fontsize=14, style = filled, fillcolor = violet];
225 -> 526 [arrowhead = none ];
526 -> 228;

527 [label="INSTANCE with matching:\nT17 -> T125\nX51 -> X395", fontsize=14, style = filled, fillcolor = lightgrey];
227 -> 527 [arrowhead = none , style=dashed];
527 -> 42[style=dashed];

528 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
228 -> 528 [arrowhead = none ];
528 -> 229;

529 [label="BACKTRACK\nfor clause: tree(nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
229 -> 529 [arrowhead = none ];
529 -> 230;

530 [label="ONLY EVAL with clause\ntree(X413) :- ','(no(empty(X413)), ','(left(X414, X415), ','(right(X414, X416), ','(tree(X415), tree(X416))))).\nand substitutionT126 -> T131,\nX396 -> X417,\nX413 -> node(T131, X417, nil),\nT130 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
230 -> 530 [arrowhead = none ];
530 -> 231;

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

532 [label="ONLY EVAL with clause\nno(X422) :- ','(call(X422), ','(!_63, failure(a))).\nand substitutionT131 -> T136,\nX417 -> X423,\nX422 -> empty(node(T136, X423, nil)),\nT135 -> T136", fontsize=14, style = filled, fillcolor = lightblue];
232 -> 532 [arrowhead = none ];
532 -> 233;

533 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
233 -> 533 [arrowhead = none ];
533 -> 234;

534 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
234 -> 534 [arrowhead = none ];
534 -> 235;

535 [label="BACKTRACK\nfor clause: empty(nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
235 -> 535 [arrowhead = none ];
535 -> 236;

536 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
236 -> 536 [arrowhead = none ];
536 -> 237;

537 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
237 -> 537 [arrowhead = none ];
537 -> 238;

538 [label="ONLY EVAL with clause\nno(X428).\nand substitutionT131 -> T139,\nX417 -> X429,\nX428 -> empty(node(T139, X429, nil))", fontsize=14, style = filled, fillcolor = lightblue];
238 -> 538 [arrowhead = none ];
538 -> 239;

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

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

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

542 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitutionX414 -> nil,\nX415 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
241 -> 542 [arrowhead = none ];
542 -> 243;

543 [label="ONLY EVAL with clause\nleft(node(X445, X446, X447), X445).\nand substitutionX445 -> X448,\nX446 -> X449,\nX447 -> X450,\nX414 -> node(X448, X449, X450),\nX415 -> X448", fontsize=14, style = filled, fillcolor = lightblue];
242 -> 543 [arrowhead = none ];
543 -> 249;

544 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
243 -> 544 [arrowhead = none ];
544 -> 244;

545 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
244 -> 545 [arrowhead = none ];
545 -> 245;

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

547 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitutionX416 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
245 -> 547 [arrowhead = none ];
547 -> 247;

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

549 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
247 -> 549 [arrowhead = none , style=dashed];
549 -> 139[style=dashed];

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

551 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
250 -> 551 [arrowhead = none ];
551 -> 251;

552 [label="ONLY EVAL with clause\nright(node(X463, X464, X465), X465).\nand substitutionX448 -> X466,\nX463 -> X466,\nX449 -> X467,\nX464 -> X467,\nX450 -> X468,\nX465 -> X468,\nX416 -> X468", fontsize=14, style = filled, fillcolor = lightblue];
251 -> 552 [arrowhead = none ];
552 -> 252;

553 [label="INSTANCE with matching:\nX248 -> X466\nX250 -> X468", fontsize=14, style = filled, fillcolor = lightgrey];
252 -> 553 [arrowhead = none , style=dashed];
553 -> 146[style=dashed];

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

555 [label="ONLY EVAL with clause\nno(X480) :- ','(call(X480), ','(!_69, failure(a))).\nand substitutionT142 -> T145,\nX480 -> zero(T145)", fontsize=14, style = filled, fillcolor = lightblue];
254 -> 555 [arrowhead = none ];
555 -> 255;

556 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
255 -> 556 [arrowhead = none ];
556 -> 256;

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

558 [label="EVAL with clause\nzero(0).\nand substitutionT145 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
257 -> 558 [arrowhead = none ];
558 -> 258;

559 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
257 -> 559 [arrowhead = none ];
559 -> 259;

560 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
258 -> 560 [arrowhead = none ];
560 -> 260;

561 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
259 -> 561 [arrowhead = none ];
561 -> 263;

562 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
260 -> 562 [arrowhead = none ];
562 -> 261;

563 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
261 -> 563 [arrowhead = none ];
563 -> 262;

564 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
263 -> 564 [arrowhead = none ];
564 -> 264;

565 [label="ONLY EVAL with clause\nno(X483).\nand substitutionT145 -> T148,\nX483 -> zero(T148)", fontsize=14, style = filled, fillcolor = lightblue];
264 -> 565 [arrowhead = none ];
565 -> 265;

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

567 [label="BACKTRACK\nfor clause: tree(nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
266 -> 567 [arrowhead = none ];
567 -> 267;

568 [label="ONLY EVAL with clause\ntree(X491) :- ','(no(empty(X491)), ','(left(X492, X493), ','(right(X492, X494), ','(tree(X493), tree(X494))))).\nand substitutionX477 -> X495,\nX491 -> node(nil, X495, nil)", fontsize=14, style = filled, fillcolor = lightblue];
267 -> 568 [arrowhead = none ];
568 -> 268;

569 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
268 -> 569 [arrowhead = none ];
569 -> 269;

570 [label="ONLY EVAL with clause\nno(X500) :- ','(call(X500), ','(!_74, failure(a))).\nand substitutionX495 -> X501,\nX500 -> empty(node(nil, X501, nil))", fontsize=14, style = filled, fillcolor = lightblue];
269 -> 570 [arrowhead = none ];
570 -> 270;

571 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
270 -> 571 [arrowhead = none ];
571 -> 271;

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

573 [label="BACKTRACK\nfor clause: empty(nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
272 -> 573 [arrowhead = none ];
573 -> 273;

574 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
273 -> 574 [arrowhead = none ];
574 -> 274;

575 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
274 -> 575 [arrowhead = none ];
575 -> 275;

576 [label="ONLY EVAL with clause\nno(X506).\nand substitutionX495 -> X507,\nX506 -> empty(node(nil, X507, nil))", fontsize=14, style = filled, fillcolor = lightblue];
275 -> 576 [arrowhead = none ];
576 -> 276;

577 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
276 -> 577 [arrowhead = none ];
577 -> 277;

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

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

580 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitutionX492 -> nil,\nX493 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
278 -> 580 [arrowhead = none ];
580 -> 280;

581 [label="ONLY EVAL with clause\nleft(node(X523, X524, X525), X523).\nand substitutionX523 -> X526,\nX524 -> X527,\nX525 -> X528,\nX492 -> node(X526, X527, X528),\nX493 -> X526", fontsize=14, style = filled, fillcolor = lightblue];
279 -> 581 [arrowhead = none ];
581 -> 286;

582 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
280 -> 582 [arrowhead = none ];
582 -> 281;

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

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

585 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitutionX494 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
282 -> 585 [arrowhead = none ];
585 -> 284;

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

587 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
284 -> 587 [arrowhead = none , style=dashed];
587 -> 139[style=dashed];

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

589 [label="BACKTRACK\nfor clause: right(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
287 -> 589 [arrowhead = none ];
589 -> 288;

590 [label="ONLY EVAL with clause\nright(node(X541, X542, X543), X543).\nand substitutionX526 -> X544,\nX541 -> X544,\nX527 -> X545,\nX542 -> X545,\nX528 -> X546,\nX543 -> X546,\nX494 -> X546", fontsize=14, style = filled, fillcolor = lightblue];
288 -> 590 [arrowhead = none ];
590 -> 289;

591 [label="INSTANCE with matching:\nX248 -> X544\nX250 -> X546", fontsize=14, style = filled, fillcolor = lightgrey];
289 -> 591 [arrowhead = none , style=dashed];
591 -> 146[style=dashed];

}

(2) Obligation:

Clauses:

s2tA(0, nil).
s2tA(s(T32), node(X88, X89, X88)) :- s2tA(T32, X88).
s2tA(s(T46), node(nil, X125, X126)) :- s2tA(T46, X126).
s2tA(s(T60), node(X162, X163, nil)) :- s2tA(T60, X162).
s2tA(T69, node(nil, X181, nil)).
treeB.
treeC(nil).
pD :- treeB.
pD :- ','(treeB, treeB).
pE(X248, X250) :- treeC(X248).
pE(T83, X250) :- ','(treeC(T83), treeC(X250)).
goalF(0) :- treeB.
goalF(s(T17)) :- s2tA(T17, X51).
goalF(s(T17)) :- ','(s2tA(T17, T82), pD).
goalF(s(T17)) :- ','(s2tA(T17, T82), pE(X248, X250)).
goalF(s(T97)) :- s2tA(T97, X296).
goalF(s(T97)) :- ','(s2tA(T97, T111), pD).
goalF(s(T97)) :- ','(s2tA(T97, T111), pE(X366, X368)).
goalF(s(T125)) :- s2tA(T125, X395).
goalF(s(T125)) :- ','(s2tA(T125, T139), pD).
goalF(s(T125)) :- ','(s2tA(T125, T139), pE(X466, X468)).
goalF(T148) :- pD.
goalF(T148) :- pE(X544, X546).

Query: goalF(g)

(3) PrologToPiTRSProof (SOUND transformation)

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

goalF_in_g(0) → U9_g(treeB_in_)
treeB_in_ → treeB_out_
U9_g(treeB_out_) → goalF_out_g(0)
goalF_in_g(s(T17)) → U10_g(T17, s2tA_in_ga(T17, X51))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
s2tA_in_ga(s(T32), node(X88, X89, X88)) → U1_ga(T32, X88, X89, s2tA_in_ga(T32, X88))
s2tA_in_ga(s(T46), node(nil, X125, X126)) → U2_ga(T46, X125, X126, s2tA_in_ga(T46, X126))
s2tA_in_ga(s(T60), node(X162, X163, nil)) → U3_ga(T60, X162, X163, s2tA_in_ga(T60, X162))
s2tA_in_ga(T69, node(nil, X181, nil)) → s2tA_out_ga(T69, node(nil, X181, nil))
U3_ga(T60, X162, X163, s2tA_out_ga(T60, X162)) → s2tA_out_ga(s(T60), node(X162, X163, nil))
U2_ga(T46, X125, X126, s2tA_out_ga(T46, X126)) → s2tA_out_ga(s(T46), node(nil, X125, X126))
U1_ga(T32, X88, X89, s2tA_out_ga(T32, X88)) → s2tA_out_ga(s(T32), node(X88, X89, X88))
U10_g(T17, s2tA_out_ga(T17, X51)) → goalF_out_g(s(T17))
goalF_in_g(s(T17)) → U11_g(T17, s2tA_in_ga(T17, T82))
U11_g(T17, s2tA_out_ga(T17, T82)) → U12_g(T17, pD_in_)
pD_in_ → U4_(treeB_in_)
U4_(treeB_out_) → pD_out_
U4_(treeB_out_) → U5_(treeB_in_)
U5_(treeB_out_) → pD_out_
U12_g(T17, pD_out_) → goalF_out_g(s(T17))
U11_g(T17, s2tA_out_ga(T17, T82)) → U13_g(T17, pE_in_aa(X248, X250))
pE_in_aa(X248, X250) → U6_aa(X248, X250, treeC_in_a(X248))
treeC_in_a(nil) → treeC_out_a(nil)
U6_aa(X248, X250, treeC_out_a(X248)) → pE_out_aa(X248, X250)
pE_in_aa(T83, X250) → U7_aa(T83, X250, treeC_in_a(T83))
U7_aa(T83, X250, treeC_out_a(T83)) → U8_aa(T83, X250, treeC_in_a(X250))
U8_aa(T83, X250, treeC_out_a(X250)) → pE_out_aa(T83, X250)
U13_g(T17, pE_out_aa(X248, X250)) → goalF_out_g(s(T17))
goalF_in_g(s(T97)) → U14_g(T97, s2tA_in_ga(T97, X296))
U14_g(T97, s2tA_out_ga(T97, X296)) → goalF_out_g(s(T97))
goalF_in_g(s(T97)) → U15_g(T97, s2tA_in_ga(T97, T111))
U15_g(T97, s2tA_out_ga(T97, T111)) → U16_g(T97, pD_in_)
U16_g(T97, pD_out_) → goalF_out_g(s(T97))
U15_g(T97, s2tA_out_ga(T97, T111)) → U17_g(T97, pE_in_aa(X366, X368))
U17_g(T97, pE_out_aa(X366, X368)) → goalF_out_g(s(T97))
goalF_in_g(s(T125)) → U18_g(T125, s2tA_in_ga(T125, X395))
U18_g(T125, s2tA_out_ga(T125, X395)) → goalF_out_g(s(T125))
goalF_in_g(s(T125)) → U19_g(T125, s2tA_in_ga(T125, T139))
U19_g(T125, s2tA_out_ga(T125, T139)) → U20_g(T125, pD_in_)
U20_g(T125, pD_out_) → goalF_out_g(s(T125))
U19_g(T125, s2tA_out_ga(T125, T139)) → U21_g(T125, pE_in_aa(X466, X468))
U21_g(T125, pE_out_aa(X466, X468)) → goalF_out_g(s(T125))
goalF_in_g(T148) → U22_g(T148, pD_in_)
U22_g(T148, pD_out_) → goalF_out_g(T148)
goalF_in_g(T148) → U23_g(T148, pE_in_aa(X544, X546))
U23_g(T148, pE_out_aa(X544, X546)) → goalF_out_g(T148)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

goalF_in_g(0) → U9_g(treeB_in_)
treeB_in_ → treeB_out_
U9_g(treeB_out_) → goalF_out_g(0)
goalF_in_g(s(T17)) → U10_g(T17, s2tA_in_ga(T17, X51))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
s2tA_in_ga(s(T32), node(X88, X89, X88)) → U1_ga(T32, X88, X89, s2tA_in_ga(T32, X88))
s2tA_in_ga(s(T46), node(nil, X125, X126)) → U2_ga(T46, X125, X126, s2tA_in_ga(T46, X126))
s2tA_in_ga(s(T60), node(X162, X163, nil)) → U3_ga(T60, X162, X163, s2tA_in_ga(T60, X162))
s2tA_in_ga(T69, node(nil, X181, nil)) → s2tA_out_ga(T69, node(nil, X181, nil))
U3_ga(T60, X162, X163, s2tA_out_ga(T60, X162)) → s2tA_out_ga(s(T60), node(X162, X163, nil))
U2_ga(T46, X125, X126, s2tA_out_ga(T46, X126)) → s2tA_out_ga(s(T46), node(nil, X125, X126))
U1_ga(T32, X88, X89, s2tA_out_ga(T32, X88)) → s2tA_out_ga(s(T32), node(X88, X89, X88))
U10_g(T17, s2tA_out_ga(T17, X51)) → goalF_out_g(s(T17))
goalF_in_g(s(T17)) → U11_g(T17, s2tA_in_ga(T17, T82))
U11_g(T17, s2tA_out_ga(T17, T82)) → U12_g(T17, pD_in_)
pD_in_ → U4_(treeB_in_)
U4_(treeB_out_) → pD_out_
U4_(treeB_out_) → U5_(treeB_in_)
U5_(treeB_out_) → pD_out_
U12_g(T17, pD_out_) → goalF_out_g(s(T17))
U11_g(T17, s2tA_out_ga(T17, T82)) → U13_g(T17, pE_in_aa(X248, X250))
pE_in_aa(X248, X250) → U6_aa(X248, X250, treeC_in_a(X248))
treeC_in_a(nil) → treeC_out_a(nil)
U6_aa(X248, X250, treeC_out_a(X248)) → pE_out_aa(X248, X250)
pE_in_aa(T83, X250) → U7_aa(T83, X250, treeC_in_a(T83))
U7_aa(T83, X250, treeC_out_a(T83)) → U8_aa(T83, X250, treeC_in_a(X250))
U8_aa(T83, X250, treeC_out_a(X250)) → pE_out_aa(T83, X250)
U13_g(T17, pE_out_aa(X248, X250)) → goalF_out_g(s(T17))
goalF_in_g(s(T97)) → U14_g(T97, s2tA_in_ga(T97, X296))
U14_g(T97, s2tA_out_ga(T97, X296)) → goalF_out_g(s(T97))
goalF_in_g(s(T97)) → U15_g(T97, s2tA_in_ga(T97, T111))
U15_g(T97, s2tA_out_ga(T97, T111)) → U16_g(T97, pD_in_)
U16_g(T97, pD_out_) → goalF_out_g(s(T97))
U15_g(T97, s2tA_out_ga(T97, T111)) → U17_g(T97, pE_in_aa(X366, X368))
U17_g(T97, pE_out_aa(X366, X368)) → goalF_out_g(s(T97))
goalF_in_g(s(T125)) → U18_g(T125, s2tA_in_ga(T125, X395))
U18_g(T125, s2tA_out_ga(T125, X395)) → goalF_out_g(s(T125))
goalF_in_g(s(T125)) → U19_g(T125, s2tA_in_ga(T125, T139))
U19_g(T125, s2tA_out_ga(T125, T139)) → U20_g(T125, pD_in_)
U20_g(T125, pD_out_) → goalF_out_g(s(T125))
U19_g(T125, s2tA_out_ga(T125, T139)) → U21_g(T125, pE_in_aa(X466, X468))
U21_g(T125, pE_out_aa(X466, X468)) → goalF_out_g(s(T125))
goalF_in_g(T148) → U22_g(T148, pD_in_)
U22_g(T148, pD_out_) → goalF_out_g(T148)
goalF_in_g(T148) → U23_g(T148, pE_in_aa(X544, X546))
U23_g(T148, pE_out_aa(X544, X546)) → goalF_out_g(T148)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

GOALF_IN_G(0) → U9_G(treeB_in_)
GOALF_IN_G(0) → TREEB_IN_
GOALF_IN_G(s(T17)) → U10_G(T17, s2tA_in_ga(T17, X51))
GOALF_IN_G(s(T17)) → S2TA_IN_GA(T17, X51)
S2TA_IN_GA(s(T32), node(X88, X89, X88)) → U1_GA(T32, X88, X89, s2tA_in_ga(T32, X88))
S2TA_IN_GA(s(T32), node(X88, X89, X88)) → S2TA_IN_GA(T32, X88)
S2TA_IN_GA(s(T46), node(nil, X125, X126)) → U2_GA(T46, X125, X126, s2tA_in_ga(T46, X126))
S2TA_IN_GA(s(T46), node(nil, X125, X126)) → S2TA_IN_GA(T46, X126)
S2TA_IN_GA(s(T60), node(X162, X163, nil)) → U3_GA(T60, X162, X163, s2tA_in_ga(T60, X162))
S2TA_IN_GA(s(T60), node(X162, X163, nil)) → S2TA_IN_GA(T60, X162)
GOALF_IN_G(s(T17)) → U11_G(T17, s2tA_in_ga(T17, T82))
U11_G(T17, s2tA_out_ga(T17, T82)) → U12_G(T17, pD_in_)
U11_G(T17, s2tA_out_ga(T17, T82)) → PD_IN_
PD_IN_ → U4_¹(treeB_in_)
PD_IN_ → TREEB_IN_
U4_¹(treeB_out_) → U5_¹(treeB_in_)
U4_¹(treeB_out_) → TREEB_IN_
U11_G(T17, s2tA_out_ga(T17, T82)) → U13_G(T17, pE_in_aa(X248, X250))
U11_G(T17, s2tA_out_ga(T17, T82)) → PE_IN_AA(X248, X250)
PE_IN_AA(X248, X250) → U6_AA(X248, X250, treeC_in_a(X248))
PE_IN_AA(X248, X250) → TREEC_IN_A(X248)
PE_IN_AA(T83, X250) → U7_AA(T83, X250, treeC_in_a(T83))
U7_AA(T83, X250, treeC_out_a(T83)) → U8_AA(T83, X250, treeC_in_a(X250))
U7_AA(T83, X250, treeC_out_a(T83)) → TREEC_IN_A(X250)
GOALF_IN_G(s(T97)) → U14_G(T97, s2tA_in_ga(T97, X296))
GOALF_IN_G(s(T97)) → U15_G(T97, s2tA_in_ga(T97, T111))
U15_G(T97, s2tA_out_ga(T97, T111)) → U16_G(T97, pD_in_)
U15_G(T97, s2tA_out_ga(T97, T111)) → PD_IN_
U15_G(T97, s2tA_out_ga(T97, T111)) → U17_G(T97, pE_in_aa(X366, X368))
U15_G(T97, s2tA_out_ga(T97, T111)) → PE_IN_AA(X366, X368)
GOALF_IN_G(s(T125)) → U18_G(T125, s2tA_in_ga(T125, X395))
GOALF_IN_G(s(T125)) → U19_G(T125, s2tA_in_ga(T125, T139))
U19_G(T125, s2tA_out_ga(T125, T139)) → U20_G(T125, pD_in_)
U19_G(T125, s2tA_out_ga(T125, T139)) → PD_IN_
U19_G(T125, s2tA_out_ga(T125, T139)) → U21_G(T125, pE_in_aa(X466, X468))
U19_G(T125, s2tA_out_ga(T125, T139)) → PE_IN_AA(X466, X468)
GOALF_IN_G(T148) → U22_G(T148, pD_in_)
GOALF_IN_G(T148) → PD_IN_
GOALF_IN_G(T148) → U23_G(T148, pE_in_aa(X544, X546))
GOALF_IN_G(T148) → PE_IN_AA(X544, X546)

The TRS R consists of the following rules:

goalF_in_g(0) → U9_g(treeB_in_)
treeB_in_ → treeB_out_
U9_g(treeB_out_) → goalF_out_g(0)
goalF_in_g(s(T17)) → U10_g(T17, s2tA_in_ga(T17, X51))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
s2tA_in_ga(s(T32), node(X88, X89, X88)) → U1_ga(T32, X88, X89, s2tA_in_ga(T32, X88))
s2tA_in_ga(s(T46), node(nil, X125, X126)) → U2_ga(T46, X125, X126, s2tA_in_ga(T46, X126))
s2tA_in_ga(s(T60), node(X162, X163, nil)) → U3_ga(T60, X162, X163, s2tA_in_ga(T60, X162))
s2tA_in_ga(T69, node(nil, X181, nil)) → s2tA_out_ga(T69, node(nil, X181, nil))
U3_ga(T60, X162, X163, s2tA_out_ga(T60, X162)) → s2tA_out_ga(s(T60), node(X162, X163, nil))
U2_ga(T46, X125, X126, s2tA_out_ga(T46, X126)) → s2tA_out_ga(s(T46), node(nil, X125, X126))
U1_ga(T32, X88, X89, s2tA_out_ga(T32, X88)) → s2tA_out_ga(s(T32), node(X88, X89, X88))
U10_g(T17, s2tA_out_ga(T17, X51)) → goalF_out_g(s(T17))
goalF_in_g(s(T17)) → U11_g(T17, s2tA_in_ga(T17, T82))
U11_g(T17, s2tA_out_ga(T17, T82)) → U12_g(T17, pD_in_)
pD_in_ → U4_(treeB_in_)
U4_(treeB_out_) → pD_out_
U4_(treeB_out_) → U5_(treeB_in_)
U5_(treeB_out_) → pD_out_
U12_g(T17, pD_out_) → goalF_out_g(s(T17))
U11_g(T17, s2tA_out_ga(T17, T82)) → U13_g(T17, pE_in_aa(X248, X250))
pE_in_aa(X248, X250) → U6_aa(X248, X250, treeC_in_a(X248))
treeC_in_a(nil) → treeC_out_a(nil)
U6_aa(X248, X250, treeC_out_a(X248)) → pE_out_aa(X248, X250)
pE_in_aa(T83, X250) → U7_aa(T83, X250, treeC_in_a(T83))
U7_aa(T83, X250, treeC_out_a(T83)) → U8_aa(T83, X250, treeC_in_a(X250))
U8_aa(T83, X250, treeC_out_a(X250)) → pE_out_aa(T83, X250)
U13_g(T17, pE_out_aa(X248, X250)) → goalF_out_g(s(T17))
goalF_in_g(s(T97)) → U14_g(T97, s2tA_in_ga(T97, X296))
U14_g(T97, s2tA_out_ga(T97, X296)) → goalF_out_g(s(T97))
goalF_in_g(s(T97)) → U15_g(T97, s2tA_in_ga(T97, T111))
U15_g(T97, s2tA_out_ga(T97, T111)) → U16_g(T97, pD_in_)
U16_g(T97, pD_out_) → goalF_out_g(s(T97))
U15_g(T97, s2tA_out_ga(T97, T111)) → U17_g(T97, pE_in_aa(X366, X368))
U17_g(T97, pE_out_aa(X366, X368)) → goalF_out_g(s(T97))
goalF_in_g(s(T125)) → U18_g(T125, s2tA_in_ga(T125, X395))
U18_g(T125, s2tA_out_ga(T125, X395)) → goalF_out_g(s(T125))
goalF_in_g(s(T125)) → U19_g(T125, s2tA_in_ga(T125, T139))
U19_g(T125, s2tA_out_ga(T125, T139)) → U20_g(T125, pD_in_)
U20_g(T125, pD_out_) → goalF_out_g(s(T125))
U19_g(T125, s2tA_out_ga(T125, T139)) → U21_g(T125, pE_in_aa(X466, X468))
U21_g(T125, pE_out_aa(X466, X468)) → goalF_out_g(s(T125))
goalF_in_g(T148) → U22_g(T148, pD_in_)
U22_g(T148, pD_out_) → goalF_out_g(T148)
goalF_in_g(T148) → U23_g(T148, pE_in_aa(X544, X546))
U23_g(T148, pE_out_aa(X544, X546)) → goalF_out_g(T148)

The argument filtering Pi contains the following mapping:
goalF_in_g(x1) = goalF_in_g(x1)
0 = 0
U9_g(x1) = U9_g(x1)
treeB_in_ = treeB_in_
treeB_out_ = treeB_out_
goalF_out_g(x1) = goalF_out_g
s(x1) = s(x1)
U10_g(x1, x2) = U10_g(x2)
s2tA_in_ga(x1, x2) = s2tA_in_ga(x1)
s2tA_out_ga(x1, x2) = s2tA_out_ga(x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x4)
U2_ga(x1, x2, x3, x4) = U2_ga(x4)
U3_ga(x1, x2, x3, x4) = U3_ga(x4)
node(x1, x2, x3) = node(x1, x3)
U11_g(x1, x2) = U11_g(x2)
U12_g(x1, x2) = U12_g(x2)
pD_in_ = pD_in_
U4_(x1) = U4_(x1)
pD_out_ = pD_out_
U5_(x1) = U5_(x1)
U13_g(x1, x2) = U13_g(x2)
pE_in_aa(x1, x2) = pE_in_aa
U6_aa(x1, x2, x3) = U6_aa(x3)
treeC_in_a(x1) = treeC_in_a
treeC_out_a(x1) = treeC_out_a(x1)
pE_out_aa(x1, x2) = pE_out_aa(x1)
U7_aa(x1, x2, x3) = U7_aa(x3)
U8_aa(x1, x2, x3) = U8_aa(x1, x3)
U14_g(x1, x2) = U14_g(x2)
U15_g(x1, x2) = U15_g(x2)
U16_g(x1, x2) = U16_g(x2)
U17_g(x1, x2) = U17_g(x2)
U18_g(x1, x2) = U18_g(x2)
U19_g(x1, x2) = U19_g(x2)
U20_g(x1, x2) = U20_g(x2)
U21_g(x1, x2) = U21_g(x2)
U22_g(x1, x2) = U22_g(x2)
U23_g(x1, x2) = U23_g(x2)
nil = nil
GOALF_IN_G(x1) = GOALF_IN_G(x1)
U9_G(x1) = U9_G(x1)
TREEB_IN_ = TREEB_IN_
U10_G(x1, x2) = U10_G(x2)
S2TA_IN_GA(x1, x2) = S2TA_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x4)
U2_GA(x1, x2, x3, x4) = U2_GA(x4)
U3_GA(x1, x2, x3, x4) = U3_GA(x4)
U11_G(x1, x2) = U11_G(x2)
U12_G(x1, x2) = U12_G(x2)
PD_IN_ = PD_IN_
U4_¹(x1) = U4_¹(x1)
U5_¹(x1) = U5_¹(x1)
U13_G(x1, x2) = U13_G(x2)
PE_IN_AA(x1, x2) = PE_IN_AA
U6_AA(x1, x2, x3) = U6_AA(x3)
TREEC_IN_A(x1) = TREEC_IN_A
U7_AA(x1, x2, x3) = U7_AA(x3)
U8_AA(x1, x2, x3) = U8_AA(x1, x3)
U14_G(x1, x2) = U14_G(x2)
U15_G(x1, x2) = U15_G(x2)
U16_G(x1, x2) = U16_G(x2)
U17_G(x1, x2) = U17_G(x2)
U18_G(x1, x2) = U18_G(x2)
U19_G(x1, x2) = U19_G(x2)
U20_G(x1, x2) = U20_G(x2)
U21_G(x1, x2) = U21_G(x2)
U22_G(x1, x2) = U22_G(x2)
U23_G(x1, x2) = U23_G(x2)

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

(6) Obligation:

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

GOALF_IN_G(0) → U9_G(treeB_in_)
GOALF_IN_G(0) → TREEB_IN_
GOALF_IN_G(s(T17)) → U10_G(T17, s2tA_in_ga(T17, X51))
GOALF_IN_G(s(T17)) → S2TA_IN_GA(T17, X51)
S2TA_IN_GA(s(T32), node(X88, X89, X88)) → U1_GA(T32, X88, X89, s2tA_in_ga(T32, X88))
S2TA_IN_GA(s(T32), node(X88, X89, X88)) → S2TA_IN_GA(T32, X88)
S2TA_IN_GA(s(T46), node(nil, X125, X126)) → U2_GA(T46, X125, X126, s2tA_in_ga(T46, X126))
S2TA_IN_GA(s(T46), node(nil, X125, X126)) → S2TA_IN_GA(T46, X126)
S2TA_IN_GA(s(T60), node(X162, X163, nil)) → U3_GA(T60, X162, X163, s2tA_in_ga(T60, X162))
S2TA_IN_GA(s(T60), node(X162, X163, nil)) → S2TA_IN_GA(T60, X162)
GOALF_IN_G(s(T17)) → U11_G(T17, s2tA_in_ga(T17, T82))
U11_G(T17, s2tA_out_ga(T17, T82)) → U12_G(T17, pD_in_)
U11_G(T17, s2tA_out_ga(T17, T82)) → PD_IN_
PD_IN_ → U4_¹(treeB_in_)
PD_IN_ → TREEB_IN_
U4_¹(treeB_out_) → U5_¹(treeB_in_)
U4_¹(treeB_out_) → TREEB_IN_
U11_G(T17, s2tA_out_ga(T17, T82)) → U13_G(T17, pE_in_aa(X248, X250))
U11_G(T17, s2tA_out_ga(T17, T82)) → PE_IN_AA(X248, X250)
PE_IN_AA(X248, X250) → U6_AA(X248, X250, treeC_in_a(X248))
PE_IN_AA(X248, X250) → TREEC_IN_A(X248)
PE_IN_AA(T83, X250) → U7_AA(T83, X250, treeC_in_a(T83))
U7_AA(T83, X250, treeC_out_a(T83)) → U8_AA(T83, X250, treeC_in_a(X250))
U7_AA(T83, X250, treeC_out_a(T83)) → TREEC_IN_A(X250)
GOALF_IN_G(s(T97)) → U14_G(T97, s2tA_in_ga(T97, X296))
GOALF_IN_G(s(T97)) → U15_G(T97, s2tA_in_ga(T97, T111))
U15_G(T97, s2tA_out_ga(T97, T111)) → U16_G(T97, pD_in_)
U15_G(T97, s2tA_out_ga(T97, T111)) → PD_IN_
U15_G(T97, s2tA_out_ga(T97, T111)) → U17_G(T97, pE_in_aa(X366, X368))
U15_G(T97, s2tA_out_ga(T97, T111)) → PE_IN_AA(X366, X368)
GOALF_IN_G(s(T125)) → U18_G(T125, s2tA_in_ga(T125, X395))
GOALF_IN_G(s(T125)) → U19_G(T125, s2tA_in_ga(T125, T139))
U19_G(T125, s2tA_out_ga(T125, T139)) → U20_G(T125, pD_in_)
U19_G(T125, s2tA_out_ga(T125, T139)) → PD_IN_
U19_G(T125, s2tA_out_ga(T125, T139)) → U21_G(T125, pE_in_aa(X466, X468))
U19_G(T125, s2tA_out_ga(T125, T139)) → PE_IN_AA(X466, X468)
GOALF_IN_G(T148) → U22_G(T148, pD_in_)
GOALF_IN_G(T148) → PD_IN_
GOALF_IN_G(T148) → U23_G(T148, pE_in_aa(X544, X546))
GOALF_IN_G(T148) → PE_IN_AA(X544, X546)

The TRS R consists of the following rules:

goalF_in_g(0) → U9_g(treeB_in_)
treeB_in_ → treeB_out_
U9_g(treeB_out_) → goalF_out_g(0)
goalF_in_g(s(T17)) → U10_g(T17, s2tA_in_ga(T17, X51))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
s2tA_in_ga(s(T32), node(X88, X89, X88)) → U1_ga(T32, X88, X89, s2tA_in_ga(T32, X88))
s2tA_in_ga(s(T46), node(nil, X125, X126)) → U2_ga(T46, X125, X126, s2tA_in_ga(T46, X126))
s2tA_in_ga(s(T60), node(X162, X163, nil)) → U3_ga(T60, X162, X163, s2tA_in_ga(T60, X162))
s2tA_in_ga(T69, node(nil, X181, nil)) → s2tA_out_ga(T69, node(nil, X181, nil))
U3_ga(T60, X162, X163, s2tA_out_ga(T60, X162)) → s2tA_out_ga(s(T60), node(X162, X163, nil))
U2_ga(T46, X125, X126, s2tA_out_ga(T46, X126)) → s2tA_out_ga(s(T46), node(nil, X125, X126))
U1_ga(T32, X88, X89, s2tA_out_ga(T32, X88)) → s2tA_out_ga(s(T32), node(X88, X89, X88))
U10_g(T17, s2tA_out_ga(T17, X51)) → goalF_out_g(s(T17))
goalF_in_g(s(T17)) → U11_g(T17, s2tA_in_ga(T17, T82))
U11_g(T17, s2tA_out_ga(T17, T82)) → U12_g(T17, pD_in_)
pD_in_ → U4_(treeB_in_)
U4_(treeB_out_) → pD_out_
U4_(treeB_out_) → U5_(treeB_in_)
U5_(treeB_out_) → pD_out_
U12_g(T17, pD_out_) → goalF_out_g(s(T17))
U11_g(T17, s2tA_out_ga(T17, T82)) → U13_g(T17, pE_in_aa(X248, X250))
pE_in_aa(X248, X250) → U6_aa(X248, X250, treeC_in_a(X248))
treeC_in_a(nil) → treeC_out_a(nil)
U6_aa(X248, X250, treeC_out_a(X248)) → pE_out_aa(X248, X250)
pE_in_aa(T83, X250) → U7_aa(T83, X250, treeC_in_a(T83))
U7_aa(T83, X250, treeC_out_a(T83)) → U8_aa(T83, X250, treeC_in_a(X250))
U8_aa(T83, X250, treeC_out_a(X250)) → pE_out_aa(T83, X250)
U13_g(T17, pE_out_aa(X248, X250)) → goalF_out_g(s(T17))
goalF_in_g(s(T97)) → U14_g(T97, s2tA_in_ga(T97, X296))
U14_g(T97, s2tA_out_ga(T97, X296)) → goalF_out_g(s(T97))
goalF_in_g(s(T97)) → U15_g(T97, s2tA_in_ga(T97, T111))
U15_g(T97, s2tA_out_ga(T97, T111)) → U16_g(T97, pD_in_)
U16_g(T97, pD_out_) → goalF_out_g(s(T97))
U15_g(T97, s2tA_out_ga(T97, T111)) → U17_g(T97, pE_in_aa(X366, X368))
U17_g(T97, pE_out_aa(X366, X368)) → goalF_out_g(s(T97))
goalF_in_g(s(T125)) → U18_g(T125, s2tA_in_ga(T125, X395))
U18_g(T125, s2tA_out_ga(T125, X395)) → goalF_out_g(s(T125))
goalF_in_g(s(T125)) → U19_g(T125, s2tA_in_ga(T125, T139))
U19_g(T125, s2tA_out_ga(T125, T139)) → U20_g(T125, pD_in_)
U20_g(T125, pD_out_) → goalF_out_g(s(T125))
U19_g(T125, s2tA_out_ga(T125, T139)) → U21_g(T125, pE_in_aa(X466, X468))
U21_g(T125, pE_out_aa(X466, X468)) → goalF_out_g(s(T125))
goalF_in_g(T148) → U22_g(T148, pD_in_)
U22_g(T148, pD_out_) → goalF_out_g(T148)
goalF_in_g(T148) → U23_g(T148, pE_in_aa(X544, X546))
U23_g(T148, pE_out_aa(X544, X546)) → goalF_out_g(T148)

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

S2TA_IN_GA(s(T46), node(nil, X125, X126)) → S2TA_IN_GA(T46, X126)
S2TA_IN_GA(s(T32), node(X88, X89, X88)) → S2TA_IN_GA(T32, X88)
S2TA_IN_GA(s(T60), node(X162, X163, nil)) → S2TA_IN_GA(T60, X162)

The TRS R consists of the following rules:

goalF_in_g(0) → U9_g(treeB_in_)
treeB_in_ → treeB_out_
U9_g(treeB_out_) → goalF_out_g(0)
goalF_in_g(s(T17)) → U10_g(T17, s2tA_in_ga(T17, X51))
s2tA_in_ga(0, nil) → s2tA_out_ga(0, nil)
s2tA_in_ga(s(T32), node(X88, X89, X88)) → U1_ga(T32, X88, X89, s2tA_in_ga(T32, X88))
s2tA_in_ga(s(T46), node(nil, X125, X126)) → U2_ga(T46, X125, X126, s2tA_in_ga(T46, X126))
s2tA_in_ga(s(T60), node(X162, X163, nil)) → U3_ga(T60, X162, X163, s2tA_in_ga(T60, X162))
s2tA_in_ga(T69, node(nil, X181, nil)) → s2tA_out_ga(T69, node(nil, X181, nil))
U3_ga(T60, X162, X163, s2tA_out_ga(T60, X162)) → s2tA_out_ga(s(T60), node(X162, X163, nil))
U2_ga(T46, X125, X126, s2tA_out_ga(T46, X126)) → s2tA_out_ga(s(T46), node(nil, X125, X126))
U1_ga(T32, X88, X89, s2tA_out_ga(T32, X88)) → s2tA_out_ga(s(T32), node(X88, X89, X88))
U10_g(T17, s2tA_out_ga(T17, X51)) → goalF_out_g(s(T17))
goalF_in_g(s(T17)) → U11_g(T17, s2tA_in_ga(T17, T82))
U11_g(T17, s2tA_out_ga(T17, T82)) → U12_g(T17, pD_in_)
pD_in_ → U4_(treeB_in_)
U4_(treeB_out_) → pD_out_
U4_(treeB_out_) → U5_(treeB_in_)
U5_(treeB_out_) → pD_out_
U12_g(T17, pD_out_) → goalF_out_g(s(T17))
U11_g(T17, s2tA_out_ga(T17, T82)) → U13_g(T17, pE_in_aa(X248, X250))
pE_in_aa(X248, X250) → U6_aa(X248, X250, treeC_in_a(X248))
treeC_in_a(nil) → treeC_out_a(nil)
U6_aa(X248, X250, treeC_out_a(X248)) → pE_out_aa(X248, X250)
pE_in_aa(T83, X250) → U7_aa(T83, X250, treeC_in_a(T83))
U7_aa(T83, X250, treeC_out_a(T83)) → U8_aa(T83, X250, treeC_in_a(X250))
U8_aa(T83, X250, treeC_out_a(X250)) → pE_out_aa(T83, X250)
U13_g(T17, pE_out_aa(X248, X250)) → goalF_out_g(s(T17))
goalF_in_g(s(T97)) → U14_g(T97, s2tA_in_ga(T97, X296))
U14_g(T97, s2tA_out_ga(T97, X296)) → goalF_out_g(s(T97))
goalF_in_g(s(T97)) → U15_g(T97, s2tA_in_ga(T97, T111))
U15_g(T97, s2tA_out_ga(T97, T111)) → U16_g(T97, pD_in_)
U16_g(T97, pD_out_) → goalF_out_g(s(T97))
U15_g(T97, s2tA_out_ga(T97, T111)) → U17_g(T97, pE_in_aa(X366, X368))
U17_g(T97, pE_out_aa(X366, X368)) → goalF_out_g(s(T97))
goalF_in_g(s(T125)) → U18_g(T125, s2tA_in_ga(T125, X395))
U18_g(T125, s2tA_out_ga(T125, X395)) → goalF_out_g(s(T125))
goalF_in_g(s(T125)) → U19_g(T125, s2tA_in_ga(T125, T139))
U19_g(T125, s2tA_out_ga(T125, T139)) → U20_g(T125, pD_in_)
U20_g(T125, pD_out_) → goalF_out_g(s(T125))
U19_g(T125, s2tA_out_ga(T125, T139)) → U21_g(T125, pE_in_aa(X466, X468))
U21_g(T125, pE_out_aa(X466, X468)) → goalF_out_g(s(T125))
goalF_in_g(T148) → U22_g(T148, pD_in_)
U22_g(T148, pD_out_) → goalF_out_g(T148)
goalF_in_g(T148) → U23_g(T148, pE_in_aa(X544, X546))
U23_g(T148, pE_out_aa(X544, X546)) → goalF_out_g(T148)

(9) UsableRulesProof (EQUIVALENT transformation)

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

(10) Obligation:

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

S2TA_IN_GA(s(T46), node(nil, X125, X126)) → S2TA_IN_GA(T46, X126)
S2TA_IN_GA(s(T32), node(X88, X89, X88)) → S2TA_IN_GA(T32, X88)
S2TA_IN_GA(s(T60), node(X162, X163, nil)) → S2TA_IN_GA(T60, X162)

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

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

(11) PiDPToQDPProof (SOUND transformation)

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

(12) Obligation:

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

S2TA_IN_GA(s(T46)) → S2TA_IN_GA(T46)

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

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

S2TA_IN_GA(s(T46)) → S2TA_IN_GA(T46)
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Obligation:

(9) UsableRulesProof (EQUIVALENT transformation)

(10) Obligation:

(11) PiDPToQDPProof (SOUND transformation)

(12) Obligation:

(13) QDPSizeChangeProof (EQUIVALENT transformation)

(14) YES