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

(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) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

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];
5 [label="5: goal(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(s2t(T4, X14), tree(X14))\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: s2t(T4, X14)\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: tree(T5)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: s2t(T4, X14), SCOPE: 2, CLAUSE: 3 | s2t(T4, X14), SCOPE: 2, CLAUSE: 4 | s2t(T4, X14), SCOPE: 2, CLAUSE: 5 | s2t(T4, X14), SCOPE: 2, CLAUSE: 6 | s2t(T4, X14), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: s2t(T4, X14), SCOPE: 2, CLAUSE: 3\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: s2t(T4, X14), SCOPE: 2, CLAUSE: 4 | s2t(T4, X14), SCOPE: 2, CLAUSE: 5 | s2t(T4, X14), SCOPE: 2, CLAUSE: 6 | s2t(T4, X14), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: s2t(T4, X14), SCOPE: 2, CLAUSE: 4\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: s2t(T4, X14), SCOPE: 2, CLAUSE: 5 | s2t(T4, X14), SCOPE: 2, CLAUSE: 6 | s2t(T4, X14), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(no(zero(T10)), ','(p(T10, X40), s2t(X40, X41)))\n\nT10 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(no(zero(T10)), ','(p(T10, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 16 | ','(no(zero(T10)), ','(p(T10, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 17\n\nT10 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(','(call(zero(T13)), ','(!_3, failure(a))), ','(p(T13, X40), s2t(X40, X41))) | ','(no(zero(T13)), ','(p(T13, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 17\n\nT13 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(zero(T13), ','(','(!_3, failure(a)), ','(p(T13, X40), s2t(X40, X41)))) | ?_4 | ','(no(zero(T13)), ','(p(T13, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 17\n\nT13 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(zero(T13), ','(','(!_3, failure(a)), ','(p(T13, X40), s2t(X40, X41)))), SCOPE: 5, CLAUSE: 15 | ?_5 | ?_4 | ','(no(zero(T13)), ','(p(T13, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 17\n\nT13 is ground\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(','(!_3, failure(a)), ','(p(0, X40), s2t(X40, X41))) | ?_5 | ?_4 | ','(no(zero(0)), ','(p(0, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 17\n\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ?_5 | ?_4 | ','(no(zero(T13)), ','(p(T13, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 17\n\nT13 is ground\nX41 is free\nX40 is free\nzero(T13) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(failure(a), ','(p(0, X40), s2t(X40, X41)))\n\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(failure(a), ','(p(0, X40), s2t(X40, X41))), SCOPE: 6, CLAUSE: 18\n\nX41 is free\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ?_4 | ','(no(zero(T13)), ','(p(T13, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 17\n\nT13 is ground\nX41 is free\nX40 is free\nzero(T13) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(no(zero(T13)), ','(p(T13, X40), s2t(X40, X41))), SCOPE: 3, CLAUSE: 17\n\nT13 is ground\nX41 is free\nX40 is free\nzero(T13) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(p(T16, X40), s2t(X40, X41))\n\nT16 is ground\nX41 is free\nX40 is free\nzero(T16) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(p(T16, X40), s2t(X40, X41)), SCOPE: 7, CLAUSE: 12 | ','(p(T16, X40), s2t(X40, X41)), SCOPE: 7, CLAUSE: 13\n\nT16 is ground\nX41 is free\nX40 is free\nzero(T16) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(p(T16, X40), s2t(X40, X41)), SCOPE: 7, CLAUSE: 13\n\nT16 is ground\nX41 is free\nX40 is free\nzero(T16) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: s2t(T19, X41)\n\nT19 is ground\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: s2t(T4, X14), SCOPE: 2, CLAUSE: 5\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: s2t(T4, X14), SCOPE: 2, CLAUSE: 6 | s2t(T4, X14), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(no(zero(T24)), ','(p(T24, X77), s2t(X77, X79)))\n\nT24 is ground\nX79 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(no(zero(T24)), ','(p(T24, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 16 | ','(no(zero(T24)), ','(p(T24, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 17\n\nT24 is ground\nX79 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ','(','(call(zero(T27)), ','(!_8, failure(a))), ','(p(T27, X77), s2t(X77, X79))) | ','(no(zero(T27)), ','(p(T27, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 17\n\nT27 is ground\nX79 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(zero(T27), ','(','(!_8, failure(a)), ','(p(T27, X77), s2t(X77, X79)))) | ?_9 | ','(no(zero(T27)), ','(p(T27, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 17\n\nT27 is ground\nX79 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ','(zero(T27), ','(','(!_8, failure(a)), ','(p(T27, X77), s2t(X77, X79)))), SCOPE: 10, CLAUSE: 15 | ?_10 | ?_9 | ','(no(zero(T27)), ','(p(T27, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 17\n\nT27 is ground\nX79 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: ','(','(!_8, failure(a)), ','(p(0, X77), s2t(X77, X79))) | ?_10 | ?_9 | ','(no(zero(0)), ','(p(0, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 17\n\nX79 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ?_10 | ?_9 | ','(no(zero(T27)), ','(p(T27, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 17\n\nT27 is ground\nX79 is free\nX77 is free\nzero(T27) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ','(failure(a), ','(p(0, X77), s2t(X77, X79)))\n\nX79 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(failure(a), ','(p(0, X77), s2t(X77, X79))), SCOPE: 11, CLAUSE: 18\n\nX79 is free\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ?_9 | ','(no(zero(T27)), ','(p(T27, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 17\n\nT27 is ground\nX79 is free\nX77 is free\nzero(T27) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(no(zero(T27)), ','(p(T27, X77), s2t(X77, X79))), SCOPE: 8, CLAUSE: 17\n\nT27 is ground\nX79 is free\nX77 is free\nzero(T27) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(p(T30, X77), s2t(X77, X79))\n\nT30 is ground\nX79 is free\nX77 is free\nzero(T30) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(p(T30, X77), s2t(X77, X79)), SCOPE: 12, CLAUSE: 12 | ','(p(T30, X77), s2t(X77, X79)), SCOPE: 12, CLAUSE: 13\n\nT30 is ground\nX79 is free\nX77 is free\nzero(T30) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(p(T30, X77), s2t(X77, X79)), SCOPE: 12, CLAUSE: 13\n\nT30 is ground\nX79 is free\nX77 is free\nzero(T30) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: s2t(T33, X79)\n\nT33 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: s2t(T4, X14), SCOPE: 2, CLAUSE: 6\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: s2t(T4, X14), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: ','(no(zero(T38)), ','(p(T38, X114), s2t(X114, X115)))\n\nT38 is ground\nX115 is free\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: ','(no(zero(T38)), ','(p(T38, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 16 | ','(no(zero(T38)), ','(p(T38, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 17\n\nT38 is ground\nX115 is free\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: ','(','(call(zero(T41)), ','(!_13, failure(a))), ','(p(T41, X114), s2t(X114, X115))) | ','(no(zero(T41)), ','(p(T41, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 17\n\nT41 is ground\nX115 is free\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: ','(zero(T41), ','(','(!_13, failure(a)), ','(p(T41, X114), s2t(X114, X115)))) | ?_14 | ','(no(zero(T41)), ','(p(T41, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 17\n\nT41 is ground\nX115 is free\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: ','(zero(T41), ','(','(!_13, failure(a)), ','(p(T41, X114), s2t(X114, X115)))), SCOPE: 15, CLAUSE: 15 | ?_15 | ?_14 | ','(no(zero(T41)), ','(p(T41, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 17\n\nT41 is ground\nX115 is free\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: ','(','(!_13, failure(a)), ','(p(0, X114), s2t(X114, X115))) | ?_15 | ?_14 | ','(no(zero(0)), ','(p(0, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 17\n\nX115 is free\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: ?_15 | ?_14 | ','(no(zero(T41)), ','(p(T41, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 17\n\nT41 is ground\nX115 is free\nX114 is free\nzero(T41) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: ','(failure(a), ','(p(0, X114), s2t(X114, X115)))\n\nX115 is free\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: ','(failure(a), ','(p(0, X114), s2t(X114, X115))), SCOPE: 16, CLAUSE: 18\n\nX115 is free\nX114 is free", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: ?_14 | ','(no(zero(T41)), ','(p(T41, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 17\n\nT41 is ground\nX115 is free\nX114 is free\nzero(T41) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: ','(no(zero(T41)), ','(p(T41, X114), s2t(X114, X115))), SCOPE: 13, CLAUSE: 17\n\nT41 is ground\nX115 is free\nX114 is free\nzero(T41) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: ','(p(T44, X114), s2t(X114, X115))\n\nT44 is ground\nX115 is free\nX114 is free\nzero(T44) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: ','(p(T44, X114), s2t(X114, X115)), SCOPE: 17, CLAUSE: 12 | ','(p(T44, X114), s2t(X114, X115)), SCOPE: 17, CLAUSE: 13\n\nT44 is ground\nX115 is free\nX114 is free\nzero(T44) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: ','(p(T44, X114), s2t(X114, X115)), SCOPE: 17, CLAUSE: 13\n\nT44 is ground\nX115 is free\nX114 is free\nzero(T44) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: s2t(T47, X115)\n\nT47 is ground\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: no(zero(T50))\n\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: no(zero(T50)), SCOPE: 18, CLAUSE: 16 | no(zero(T50)), SCOPE: 18, CLAUSE: 17\n\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: ','(call(zero(T53)), ','(!_18, failure(a))) | no(zero(T53)), SCOPE: 18, CLAUSE: 17\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: ','(zero(T53), ','(!_18, failure(a))) | ?_19 | no(zero(T53)), SCOPE: 18, CLAUSE: 17\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: ','(zero(T53), ','(!_18, failure(a))), SCOPE: 20, CLAUSE: 15 | ?_20 | ?_19 | no(zero(T53)), SCOPE: 18, CLAUSE: 17\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: ','(!_18, failure(a)) | ?_20 | ?_19 | no(zero(0)), SCOPE: 18, CLAUSE: 17\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="327: ?_20 | ?_19 | no(zero(T53)), SCOPE: 18, CLAUSE: 17\n\nT53 is ground\nzero(T53) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: failure(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: failure(a), SCOPE: 21, CLAUSE: 18\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: ?_19 | no(zero(T53)), SCOPE: 18, CLAUSE: 17\n\nT53 is ground\nzero(T53) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
332 [label="332: no(zero(T53)), SCOPE: 18, CLAUSE: 17\n\nT53 is ground\nzero(T53) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: tree(T5), SCOPE: 22, CLAUSE: 1 | tree(T5), SCOPE: 22, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: tree(T5), SCOPE: 22, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: tree(T5), SCOPE: 22, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
343 [label="343: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
345 [label="345: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
346 [label="346: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
353 [label="353: ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149)))))\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
355 [label="355: ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 16 | ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 17\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
360 [label="360: ','(','(call(empty(T66)), ','(!_23, failure(a))), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))) | ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 17\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
361 [label="361: ','(empty(T66), ','(','(!_23, failure(a)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149)))))) | ?_24 | ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 17\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
362 [label="362: ','(empty(T66), ','(','(!_23, failure(a)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149)))))), SCOPE: 25, CLAUSE: 14 | ?_25 | ?_24 | ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 17\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
364 [label="364: ','(','(!_23, failure(a)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))) | ?_25 | ?_24 | ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 17\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: ?_25 | ?_24 | ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 17\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
368 [label="368: ','(failure(a), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149)))))\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: ','(failure(a), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 26, CLAUSE: 18\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
374 [label="374: ?_24 | ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 17\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: ','(no(empty(T61)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))), SCOPE: 23, CLAUSE: 17\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
377 [label="377: ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149)))), SCOPE: 27, CLAUSE: 8 | ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149)))), SCOPE: 27, CLAUSE: 9\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
383 [label="383: ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149)))), SCOPE: 27, CLAUSE: 8\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
385 [label="385: ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149)))), SCOPE: 27, CLAUSE: 9\n\nX147 is free\nX148 is free\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
386 [label="386: ','(right(nil, X149), ','(tree(nil), tree(X149)))\n\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: ','(right(nil, X149), ','(tree(nil), tree(X149))), SCOPE: 28, CLAUSE: 10 | ','(right(nil, X149), ','(tree(nil), tree(X149))), SCOPE: 28, CLAUSE: 11\n\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
388 [label="388: ','(right(nil, X149), ','(tree(nil), tree(X149))), SCOPE: 28, CLAUSE: 10\n\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: ','(right(nil, X149), ','(tree(nil), tree(X149))), SCOPE: 28, CLAUSE: 11\n\nX149 is free", fontsize=16, style=filled, fillcolor=lightyellow];
391 [label="391: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
397 [label="397: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
398 [label="398: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
400 [label="400: tree(nil), SCOPE: 29, CLAUSE: 1 | tree(nil), SCOPE: 29, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
401 [label="401: tree(nil), SCOPE: 29, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
402 [label="402: tree(nil), SCOPE: 29, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
403 [label="403: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
404 [label="404: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
408 [label="408: ','(no(empty(nil)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164)))))\n\nX162 is free\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
411 [label="411: ','(no(empty(nil)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))), SCOPE: 30, CLAUSE: 16 | ','(no(empty(nil)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))), SCOPE: 30, CLAUSE: 17\n\nX162 is free\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
412 [label="412: ','(','(call(empty(nil)), ','(!_30, failure(a))), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))) | ','(no(empty(nil)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))), SCOPE: 30, CLAUSE: 17\n\nX162 is free\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
415 [label="415: ','(empty(nil), ','(','(!_30, failure(a)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164)))))) | ?_31 | ','(no(empty(nil)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))), SCOPE: 30, CLAUSE: 17\n\nX162 is free\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
418 [label="418: ','(empty(nil), ','(','(!_30, failure(a)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164)))))), SCOPE: 32, CLAUSE: 14 | ?_32 | ?_31 | ','(no(empty(nil)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))), SCOPE: 30, CLAUSE: 17\n\nX162 is free\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
420 [label="420: ','(','(!_30, failure(a)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))) | ?_32 | ?_31 | ','(no(empty(nil)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))), SCOPE: 30, CLAUSE: 17\n\nX162 is free\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
421 [label="421: ','(failure(a), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164)))))\n\nX162 is free\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
422 [label="422: ','(failure(a), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))), SCOPE: 33, CLAUSE: 18\n\nX162 is free\nX163 is free\nX164 is free", fontsize=16, style=filled, fillcolor=lightyellow];
423 [label="423: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
424 [label="424: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
428 [label="428: ','(right(node(X186, X187, X188), X149), ','(tree(X186), tree(X149)))\n\nX149 is free\nX186 is free\nX187 is free\nX188 is free", fontsize=16, style=filled, fillcolor=lightyellow];
429 [label="429: ','(right(node(X186, X187, X188), X149), ','(tree(X186), tree(X149))), SCOPE: 34, CLAUSE: 10 | ','(right(node(X186, X187, X188), X149), ','(tree(X186), tree(X149))), SCOPE: 34, CLAUSE: 11\n\nX149 is free\nX186 is free\nX187 is free\nX188 is free", fontsize=16, style=filled, fillcolor=lightyellow];
430 [label="430: ','(right(node(X186, X187, X188), X149), ','(tree(X186), tree(X149))), SCOPE: 34, CLAUSE: 11\n\nX149 is free\nX186 is free\nX187 is free\nX188 is free", fontsize=16, style=filled, fillcolor=lightyellow];
438 [label="438: ','(tree(X204), tree(X206))\n\nX204 is free\nX206 is free", fontsize=16, style=filled, fillcolor=lightyellow];
444 [label="444: tree(X204)\n\nX204 is free", fontsize=16, style=filled, fillcolor=lightyellow];
446 [label="446: tree(X206)\n\nX206 is free", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: tree(X206), SCOPE: 35, CLAUSE: 1 | tree(X206), SCOPE: 35, CLAUSE: 2\n\nX206 is free", fontsize=16, style=filled, fillcolor=lightyellow];
452 [label="452: tree(X206), SCOPE: 35, CLAUSE: 1\n\nX206 is free", fontsize=16, style=filled, fillcolor=lightyellow];
453 [label="453: tree(X206), SCOPE: 35, CLAUSE: 2\n\nX206 is free", fontsize=16, style=filled, fillcolor=lightyellow];
455 [label="455: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
466 [label="466: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
469 [label="469: ','(no(empty(X218)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217)))))\n\nX218 is free\nX215 is free\nX216 is free\nX217 is free", fontsize=16, style=filled, fillcolor=lightyellow];
471 [label="471: ','(no(empty(X218)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))), SCOPE: 36, CLAUSE: 16 | ','(no(empty(X218)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))), SCOPE: 36, CLAUSE: 17\n\nX218 is free\nX215 is free\nX216 is free\nX217 is free", fontsize=16, style=filled, fillcolor=lightyellow];
476 [label="476: ','(','(call(empty(X224)), ','(!_36, failure(a))), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))) | ','(no(empty(X218)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))), SCOPE: 36, CLAUSE: 17\n\nX218 is free\nX215 is free\nX216 is free\nX217 is free\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
478 [label="478: ','(empty(X224), ','(','(!_36, failure(a)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217)))))) | ?_37 | ','(no(empty(X218)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))), SCOPE: 36, CLAUSE: 17\n\nX218 is free\nX215 is free\nX216 is free\nX217 is free\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
480 [label="480: ','(empty(X224), ','(','(!_36, failure(a)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217)))))), SCOPE: 38, CLAUSE: 14 | ?_38 | ?_37 | ','(no(empty(X218)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))), SCOPE: 36, CLAUSE: 17\n\nX218 is free\nX215 is free\nX216 is free\nX217 is free\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
481 [label="481: ','(','(!_36, failure(a)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))) | ?_38 | ?_37 | ','(no(empty(X218)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))), SCOPE: 36, CLAUSE: 17\n\nX218 is free\nX215 is free\nX216 is free\nX217 is free", fontsize=16, style=filled, fillcolor=lightyellow];
482 [label="482: ','(failure(a), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217)))))\n\nX215 is free\nX216 is free\nX217 is free", fontsize=16, style=filled, fillcolor=lightyellow];
483 [label="483: ','(failure(a), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))), SCOPE: 39, CLAUSE: 18\n\nX215 is free\nX216 is free\nX217 is free", fontsize=16, style=filled, fillcolor=lightyellow];
484 [label="484: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
485 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 485 [arrowhead = none ];
485 -> 5;

486 [label="ONLY EVAL with clause\ngoal(X13) :- ','(s2t(X13, X14), tree(X14)).\nand substitutionT1 -> T4,\nX13 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 486 [arrowhead = none ];
486 -> 9;

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

488 [label="SPLIT 2\nnew knowledge:\nT4 is ground\nreplacements:X14 -> T5", fontsize=14, style = filled, fillcolor = violet];
9 -> 488 [arrowhead = none ];
488 -> 29;

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

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

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

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

493 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT4 -> 0,\nX14 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 493 [arrowhead = none ];
493 -> 44;

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

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

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

497 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 497 [arrowhead = none ];
497 -> 46;

498 [label="ONLY EVAL with clause\ns2t(X37, node(X38, X39, X38)) :- ','(no(zero(X37)), ','(p(X37, X40), s2t(X40, X38))).\nand substitutionT4 -> T10,\nX37 -> T10,\nX38 -> X41,\nX39 -> X42,\nX14 -> node(X41, X42, X41)", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 498 [arrowhead = none ];
498 -> 76;

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

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

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

502 [label="ONLY EVAL with clause\nno(X45) :- ','(call(X45), ','(!_3, failure(a))).\nand substitutionT10 -> T13,\nX45 -> zero(T13)", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 502 [arrowhead = none ];
502 -> 91;

503 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 503 [arrowhead = none ];
503 -> 94;

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

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

506 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 506 [arrowhead = none ];
506 -> 97;

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

508 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 508 [arrowhead = none ];
508 -> 104;

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

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

511 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 511 [arrowhead = none ];
511 -> 106;

512 [label="ONLY EVAL with clause\nno(X48).\nand substitutionT13 -> T16,\nX48 -> zero(T16)", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 512 [arrowhead = none ];
512 -> 113;

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

514 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T16), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 514 [arrowhead = none ];
514 -> 118;

515 [label="EVAL with clause\np(s(X51), X51).\nand substitutionX51 -> T19,\nT16 -> s(T19),\nX40 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 515 [arrowhead = none ];
515 -> 119;

516 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 516 [arrowhead = none ];
516 -> 120;

517 [label="INSTANCE with matching:\nT4 -> T19\nX14 -> X41", fontsize=14, style = filled, fillcolor = lightgrey];
119 -> 517 [arrowhead = none , style=dashed];
517 -> 28[style=dashed];

518 [label="ONLY EVAL with clause\ns2t(X74, node(nil, X75, X76)) :- ','(no(zero(X74)), ','(p(X74, X77), s2t(X77, X76))).\nand substitutionT4 -> T24,\nX74 -> T24,\nX75 -> X78,\nX76 -> X79,\nX14 -> node(nil, X78, X79)", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 518 [arrowhead = none ];
518 -> 168;

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

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

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

522 [label="ONLY EVAL with clause\nno(X82) :- ','(call(X82), ','(!_8, failure(a))).\nand substitutionT24 -> T27,\nX82 -> zero(T27)", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 522 [arrowhead = none ];
522 -> 175;

523 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
175 -> 523 [arrowhead = none ];
523 -> 176;

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

525 [label="EVAL with clause\nzero(0).\nand substitutionT27 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 525 [arrowhead = none ];
525 -> 180;

526 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
178 -> 526 [arrowhead = none ];
526 -> 182;

527 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
180 -> 527 [arrowhead = none ];
527 -> 183;

528 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 528 [arrowhead = none ];
528 -> 189;

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

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

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

532 [label="ONLY EVAL with clause\nno(X85).\nand substitutionT27 -> T30,\nX85 -> zero(T30)", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 532 [arrowhead = none ];
532 -> 197;

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

534 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T30), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 534 [arrowhead = none ];
534 -> 218;

535 [label="EVAL with clause\np(s(X88), X88).\nand substitutionX88 -> T33,\nT30 -> s(T33),\nX77 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
218 -> 535 [arrowhead = none ];
535 -> 222;

536 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
218 -> 536 [arrowhead = none ];
536 -> 223;

537 [label="INSTANCE with matching:\nT4 -> T33\nX14 -> X79", fontsize=14, style = filled, fillcolor = lightgrey];
222 -> 537 [arrowhead = none , style=dashed];
537 -> 28[style=dashed];

538 [label="ONLY EVAL with clause\ns2t(X111, node(X112, X113, nil)) :- ','(no(zero(X111)), ','(p(X111, X114), s2t(X114, X112))).\nand substitutionT4 -> T38,\nX111 -> T38,\nX112 -> X115,\nX113 -> X116,\nX14 -> node(X115, X116, nil)", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 538 [arrowhead = none ];
538 -> 274;

539 [label="ONLY EVAL with clause\ns2t(X132, node(nil, X133, nil)) :- no(zero(X132)).\nand substitutionT4 -> T50,\nX132 -> T50,\nX133 -> X134,\nX14 -> node(nil, X134, nil)", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 539 [arrowhead = none ];
539 -> 314;

540 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
274 -> 540 [arrowhead = none ];
540 -> 275;

541 [label="ONLY EVAL with clause\nno(X119) :- ','(call(X119), ','(!_13, failure(a))).\nand substitutionT38 -> T41,\nX119 -> zero(T41)", fontsize=14, style = filled, fillcolor = lightblue];
275 -> 541 [arrowhead = none ];
541 -> 280;

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

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

544 [label="EVAL with clause\nzero(0).\nand substitutionT41 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
282 -> 544 [arrowhead = none ];
544 -> 283;

545 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
282 -> 545 [arrowhead = none ];
545 -> 286;

546 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
283 -> 546 [arrowhead = none ];
546 -> 287;

547 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
286 -> 547 [arrowhead = none ];
547 -> 290;

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

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

550 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
290 -> 550 [arrowhead = none ];
550 -> 291;

551 [label="ONLY EVAL with clause\nno(X122).\nand substitutionT41 -> T44,\nX122 -> zero(T44)", fontsize=14, style = filled, fillcolor = lightblue];
291 -> 551 [arrowhead = none ];
551 -> 292;

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

553 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T44), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
295 -> 553 [arrowhead = none ];
553 -> 296;

554 [label="EVAL with clause\np(s(X125), X125).\nand substitutionX125 -> T47,\nT44 -> s(T47),\nX114 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
296 -> 554 [arrowhead = none ];
554 -> 297;

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

556 [label="INSTANCE with matching:\nT4 -> T47\nX14 -> X115", fontsize=14, style = filled, fillcolor = lightgrey];
297 -> 556 [arrowhead = none , style=dashed];
556 -> 28[style=dashed];

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

558 [label="ONLY EVAL with clause\nno(X137) :- ','(call(X137), ','(!_18, failure(a))).\nand substitutionT50 -> T53,\nX137 -> zero(T53)", fontsize=14, style = filled, fillcolor = lightblue];
315 -> 558 [arrowhead = none ];
558 -> 318;

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

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

561 [label="EVAL with clause\nzero(0).\nand substitutionT53 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
324 -> 561 [arrowhead = none ];
561 -> 326;

562 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
324 -> 562 [arrowhead = none ];
562 -> 327;

563 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
326 -> 563 [arrowhead = none ];
563 -> 328;

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

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

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

567 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
331 -> 567 [arrowhead = none ];
567 -> 332;

568 [label="ONLY EVAL with clause\nno(X140).\nand substitutionT53 -> T56,\nX140 -> zero(T56)", fontsize=14, style = filled, fillcolor = lightblue];
332 -> 568 [arrowhead = none ];
568 -> 333;

569 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
333 -> 569 [arrowhead = none ];
569 -> 334;

570 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
338 -> 570 [arrowhead = none ];
570 -> 339;

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

572 [label="EVAL with clause\ntree(nil).\nand substitutionT5 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
339 -> 572 [arrowhead = none ];
572 -> 343;

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

574 [label="ONLY EVAL with clause\ntree(X146) :- ','(no(empty(X146)), ','(left(X147, X148), ','(right(X147, X149), ','(tree(X148), tree(X149))))).\nand substitutionT5 -> T61,\nX146 -> T61,\nT60 -> T61", fontsize=14, style = filled, fillcolor = lightblue];
341 -> 574 [arrowhead = none ];
574 -> 353;

575 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
343 -> 575 [arrowhead = none ];
575 -> 346;

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

577 [label="ONLY EVAL with clause\nno(X152) :- ','(call(X152), ','(!_23, failure(a))).\nand substitutionT61 -> T66,\nX152 -> empty(T66),\nT65 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
355 -> 577 [arrowhead = none ];
577 -> 360;

578 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
360 -> 578 [arrowhead = none ];
578 -> 361;

579 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
361 -> 579 [arrowhead = none ];
579 -> 362;

580 [label="EVAL with clause\nempty(nil).\nand substitutionT66 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
362 -> 580 [arrowhead = none ];
580 -> 364;

581 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
362 -> 581 [arrowhead = none ];
581 -> 365;

582 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
364 -> 582 [arrowhead = none ];
582 -> 368;

583 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
365 -> 583 [arrowhead = none ];
583 -> 374;

584 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
368 -> 584 [arrowhead = none ];
584 -> 370;

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

586 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
374 -> 586 [arrowhead = none ];
586 -> 375;

587 [label="ONLY EVAL with clause\nno(X155).\nand substitutionT61 -> T69,\nX155 -> empty(T69)", fontsize=14, style = filled, fillcolor = lightblue];
375 -> 587 [arrowhead = none ];
587 -> 377;

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

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

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

591 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitutionX147 -> nil,\nX148 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
383 -> 591 [arrowhead = none ];
591 -> 386;

592 [label="ONLY EVAL with clause\nleft(node(X183, X184, X185), X183).\nand substitutionX183 -> X186,\nX184 -> X187,\nX185 -> X188,\nX147 -> node(X186, X187, X188),\nX148 -> X186", fontsize=14, style = filled, fillcolor = lightblue];
385 -> 592 [arrowhead = none ];
592 -> 428;

593 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
386 -> 593 [arrowhead = none ];
593 -> 387;

594 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
387 -> 594 [arrowhead = none ];
594 -> 388;

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

596 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitutionX149 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
388 -> 596 [arrowhead = none ];
596 -> 391;

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

598 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
391 -> 598 [arrowhead = none ];
598 -> 397;

599 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
391 -> 599 [arrowhead = none ];
599 -> 398;

600 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
397 -> 600 [arrowhead = none , style=dashed];
600 -> 398[style=dashed];

601 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
398 -> 601 [arrowhead = none ];
601 -> 400;

602 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
400 -> 602 [arrowhead = none ];
602 -> 401;

603 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
400 -> 603 [arrowhead = none ];
603 -> 402;

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

605 [label="ONLY EVAL with clause\ntree(X161) :- ','(no(empty(X161)), ','(left(X162, X163), ','(right(X162, X164), ','(tree(X163), tree(X164))))).\nand substitutionX161 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
402 -> 605 [arrowhead = none ];
605 -> 408;

606 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
403 -> 606 [arrowhead = none ];
606 -> 404;

607 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
408 -> 607 [arrowhead = none ];
607 -> 411;

608 [label="ONLY EVAL with clause\nno(X167) :- ','(call(X167), ','(!_30, failure(a))).\nand substitutionX167 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
411 -> 608 [arrowhead = none ];
608 -> 412;

609 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
412 -> 609 [arrowhead = none ];
609 -> 415;

610 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
415 -> 610 [arrowhead = none ];
610 -> 418;

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

612 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
420 -> 612 [arrowhead = none ];
612 -> 421;

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

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

615 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
428 -> 615 [arrowhead = none ];
615 -> 429;

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

617 [label="ONLY EVAL with clause\nright(node(X201, X202, X203), X203).\nand substitutionX186 -> X204,\nX201 -> X204,\nX187 -> X205,\nX202 -> X205,\nX188 -> X206,\nX203 -> X206,\nX149 -> X206", fontsize=14, style = filled, fillcolor = lightblue];
430 -> 617 [arrowhead = none ];
617 -> 438;

618 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
438 -> 618 [arrowhead = none ];
618 -> 444;

619 [label="SPLIT 2\nreplacements:X204 -> T70", fontsize=14, style = filled, fillcolor = violet];
438 -> 619 [arrowhead = none ];
619 -> 446;

620 [label="INSTANCE with matching:\nX206 -> X204", fontsize=14, style = filled, fillcolor = lightgrey];
444 -> 620 [arrowhead = none , style=dashed];
620 -> 446[style=dashed];

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

622 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
451 -> 622 [arrowhead = none ];
622 -> 452;

623 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
451 -> 623 [arrowhead = none ];
623 -> 453;

624 [label="ONLY EVAL with clause\ntree(nil).\nand substitutionX206 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
452 -> 624 [arrowhead = none ];
624 -> 455;

625 [label="ONLY EVAL with clause\ntree(X214) :- ','(no(empty(X214)), ','(left(X215, X216), ','(right(X215, X217), ','(tree(X216), tree(X217))))).\nand substitutionX206 -> X218,\nX214 -> X218", fontsize=14, style = filled, fillcolor = lightblue];
453 -> 625 [arrowhead = none ];
625 -> 469;

626 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
455 -> 626 [arrowhead = none ];
626 -> 466;

627 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
469 -> 627 [arrowhead = none ];
627 -> 471;

628 [label="ONLY EVAL with clause\nno(X223) :- ','(call(X223), ','(!_36, failure(a))).\nand substitutionX218 -> X224,\nX223 -> empty(X224)", fontsize=14, style = filled, fillcolor = lightblue];
471 -> 628 [arrowhead = none ];
628 -> 476;

629 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
476 -> 629 [arrowhead = none ];
629 -> 478;

630 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
478 -> 630 [arrowhead = none ];
630 -> 480;

631 [label="ONLY EVAL with clause\nempty(nil).\nand substitutionX224 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
480 -> 631 [arrowhead = none ];
631 -> 481;

632 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
481 -> 632 [arrowhead = none ];
632 -> 482;

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

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

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1_in(T4) → U1(f9_in(T4), T4)
U1(f9_out1, T4) → f1_out1
f28_in(0) → f28_out1
f28_in(s(T19)) → U2(f28_in(T19), s(T19))
U2(f28_out1, s(T19)) → f28_out1
f28_in(s(T33)) → U3(f28_in(T33), s(T33))
U3(f28_out1, s(T33)) → f28_out1
f28_in(s(T47)) → U4(f28_in(T47), s(T47))
U4(f28_out1, s(T47)) → f28_out1
f28_in(T56) → f28_out1
f398_in → f398_out1
f446_in → f446_out1
f29_in → f29_out1
f29_in → U5(f391_in)
U5(f391_out1) → f29_out1
f29_in → U6(f438_in)
U6(f438_out1) → f29_out1
f9_in(T4) → U7(f28_in(T4), T4)
U7(f28_out1, T4) → U8(f29_in, T4)
U8(f29_out1, T4) → f9_out1
f391_in → U9(f398_in)
U9(f398_out1) → U10(f398_in)
U10(f398_out1) → f391_out1
f438_in → U11(f446_in)
U11(f446_out1) → U12(f446_in)
U12(f446_out1) → f438_out1

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
f1_in(x1)  =  f1_in(x1)
U1(x1, x2)  =  U1(x1, x2)
f9_in(x1)  =  f9_in(x1)
f9_out1  =  f9_out1
f1_out1  =  f1_out1
f28_in(x1)  =  f28_in(x1)
0  =  0
f28_out1  =  f28_out1
s(x1)  =  s(x1)
U2(x1, x2)  =  U2(x1, x2)
U3(x1, x2)  =  U3(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
f398_in  =  f398_in
f398_out1  =  f398_out1
f446_in  =  f446_in
f446_out1  =  f446_out1
f29_in  =  f29_in
f29_out1  =  f29_out1
U5(x1)  =  U5(x1)
f391_in  =  f391_in
f391_out1  =  f391_out1
U6(x1)  =  x1
f438_in  =  f438_in
f438_out1  =  f438_out1
U7(x1, x2)  =  U7(x1, x2)
U8(x1, x2)  =  U8(x1, x2)
U9(x1)  =  U9(x1)
U10(x1)  =  x1
U11(x1)  =  U11(x1)
U12(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:

f1_in1 > U1₂ > f1_out1
f1_in1 > f9_in1 > [f28_in1, s₁] > U2₂ > f28_out1
f1_in1 > f9_in1 > [f28_in1, s₁] > U3₂
f1_in1 > f9_in1 > [f28_in1, s₁] > U4₂ > f28_out1
f1_in1 > f9_in1 > [f29_in, U7₂] > U5₁ > [f29_out1, f391_out1, f438_out1]
f1_in1 > f9_in1 > [f29_in, U7₂] > f391_in > [f398_in, U9₁] > f398_out1 > [f29_out1, f391_out1, f438_out1]
f1_in1 > f9_in1 > [f29_in, U7₂] > f438_in > U11₁ > f446_in > f446_out1 > [f29_out1, f391_out1, f438_out1]
f1_in1 > f9_in1 > [f29_in, U7₂] > U8₂ > f9_out1 > f1_out1
0 > f28_out1

Status:

f1_in1: multiset
U1₂: [2,1]
f9_in1: [1]
f9_out1: multiset
f1_out1: multiset
f28_in1: multiset
0: multiset
f28_out1: multiset
s₁: multiset
U2₂: multiset
U3₂: multiset
U4₂: multiset
f398_in: multiset
f398_out1: multiset
f446_in: multiset
f446_out1: multiset
f29_in: multiset
f29_out1: multiset
U5₁: multiset
f391_in: multiset
f391_out1: multiset
f438_in: multiset
f438_out1: multiset
U7₂: [1,2]
U8₂: multiset
U9₁: multiset
U11₁: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f1_in(T4) → U1(f9_in(T4), T4)
U1(f9_out1, T4) → f1_out1
f28_in(0) → f28_out1
f28_in(s(T19)) → U2(f28_in(T19), s(T19))
U2(f28_out1, s(T19)) → f28_out1
f28_in(s(T33)) → U3(f28_in(T33), s(T33))
U3(f28_out1, s(T33)) → f28_out1
f28_in(s(T47)) → U4(f28_in(T47), s(T47))
U4(f28_out1, s(T47)) → f28_out1
f28_in(T56) → f28_out1
f398_in → f398_out1
f446_in → f446_out1
f29_in → f29_out1
f29_in → U5(f391_in)
U5(f391_out1) → f29_out1
f29_in → U6(f438_in)
f9_in(T4) → U7(f28_in(T4), T4)
U7(f28_out1, T4) → U8(f29_in, T4)
U8(f29_out1, T4) → f9_out1
f391_in → U9(f398_in)
U9(f398_out1) → U10(f398_in)
U10(f398_out1) → f391_out1
f438_in → U11(f446_in)
U11(f446_out1) → U12(f446_in)
U12(f446_out1) → f438_out1

(4) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

U6(f438_out1) → f29_out1

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
U6(x1)  =  x1
f438_out1  =  f438_out1
f29_out1  =  f29_out1

Recursive path order with status [RPO].
Quasi-Precedence:

f438_out1 > f29_out1

Status:

f438_out1: multiset
f29_out1: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U6(f438_out1) → f29_out1

(6) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(7) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(8) YES