Left Termination proof of /tmp/tmp0MBiOz/rev2.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 730 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 16 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 PiDP

↳7 UsableRulesProof (⇔, 0 ms)

↳8 PiDP

↳9 PiDPToQDPProof (⇒, 20 ms)

↳10 QDP

↳11 QDPSizeChangeProof (⇔, 0 ms)

↳12 YES

(0) Obligation:

Clauses:

rev(L, R) :- rev(L, [], R).
rev([], Y, Y).
rev(L, S, R) :- ','(no(empty(L)), ','(head(L, X), ','(tail(L, T), rev(T, .(X, S), R)))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, Xs), Xs).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: rev(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: rev(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: rev(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: rev(T5, [], T7)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: rev(T5, [], T7), SCOPE: 2, CLAUSE: 1 | rev(T5, [], T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: rev(T5, [], T7), SCOPE: 2, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: rev(T5, [], T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(no(empty(T15)), ','(head(T15, X29), ','(tail(T15, X30), rev(X30, .(X29, []), T17))))\n\nT15 is ground\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(no(empty(T15)), ','(head(T15, X29), ','(tail(T15, X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 8 | ','(no(empty(T15)), ','(head(T15, X29), ','(tail(T15, X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 9\n\nT15 is ground\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(','(call(empty(T22)), ','(!_3, failure(a))), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17)))) | ','(no(empty(T22)), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 9\n\nT22 is ground\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(empty(T22), ','(','(!_3, failure(a)), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17))))) | ?_4 | ','(no(empty(T22)), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 9\n\nT22 is ground\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(empty(T22), ','(','(!_3, failure(a)), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17))))), SCOPE: 5, CLAUSE: 7 | ?_5 | ?_4 | ','(no(empty(T22)), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 9\n\nT22 is ground\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(','(!_3, failure(a)), ','(head([], X29), ','(tail([], X30), rev(X30, .(X29, []), T17)))) | ?_5 | ?_4 | ','(no(empty([])), ','(head([], X29), ','(tail([], X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 9\n\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ?_5 | ?_4 | ','(no(empty(T22)), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 9\n\nT22 is ground\nX29 is free\nX30 is free\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(failure(a), ','(head([], X29), ','(tail([], X30), rev(X30, .(X29, []), T17))))\n\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(failure(a), ','(head([], X29), ','(tail([], X30), rev(X30, .(X29, []), T17)))), SCOPE: 6, CLAUSE: 10\n\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ?_4 | ','(no(empty(T22)), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 9\n\nT22 is ground\nX29 is free\nX30 is free\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(no(empty(T22)), ','(head(T22, X29), ','(tail(T22, X30), rev(X30, .(X29, []), T17)))), SCOPE: 3, CLAUSE: 9\n\nT22 is ground\nX29 is free\nX30 is free\nempty(T22) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(head(T29, X29), ','(tail(T29, X30), rev(X30, .(X29, []), T17)))\n\nT29 is ground\nX29 is free\nX30 is free\nempty(T29) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(head(T29, X29), ','(tail(T29, X30), rev(X30, .(X29, []), T17))), SCOPE: 7, CLAUSE: 3 | ','(head(T29, X29), ','(tail(T29, X30), rev(X30, .(X29, []), T17))), SCOPE: 7, CLAUSE: 4\n\nT29 is ground\nX29 is free\nX30 is free\nempty(T29) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(head(T29, X29), ','(tail(T29, X30), rev(X30, .(X29, []), T17))), SCOPE: 7, CLAUSE: 4\n\nT29 is ground\nX29 is free\nX30 is free\nempty(T29) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(tail(.(T36, T37), X30), rev(X30, .(T36, []), T17))\n\nT36 is ground\nT37 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(tail(.(T36, T37), X30), rev(X30, .(T36, []), T17)), SCOPE: 8, CLAUSE: 5 | ','(tail(.(T36, T37), X30), rev(X30, .(T36, []), T17)), SCOPE: 8, CLAUSE: 6\n\nT36 is ground\nT37 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(tail(.(T36, T37), X30), rev(X30, .(T36, []), T17)), SCOPE: 8, CLAUSE: 6\n\nT36 is ground\nT37 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: rev(T47, .(T46, []), T17)\n\nT46 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: rev(T47, .(T46, []), T17), SCOPE: 9, CLAUSE: 1 | rev(T47, .(T46, []), T17), SCOPE: 9, CLAUSE: 2\n\nT46 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: rev(T47, .(T46, []), T17), SCOPE: 9, CLAUSE: 1\n\nT46 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: rev(T47, .(T46, []), T17), SCOPE: 9, CLAUSE: 2\n\nT46 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(no(empty(T66)), ','(head(T66, X93), ','(tail(T66, X94), rev(X94, .(X93, .(T67, [])), T69))))\n\nT66 is ground\nT67 is ground\nX93 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(no(empty(T66)), ','(head(T66, X93), ','(tail(T66, X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 8 | ','(no(empty(T66)), ','(head(T66, X93), ','(tail(T66, X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 9\n\nT66 is ground\nT67 is ground\nX93 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(','(call(empty(T76)), ','(!_10, failure(a))), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69)))) | ','(no(empty(T76)), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 9\n\nT67 is ground\nT76 is ground\nX93 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(empty(T76), ','(','(!_10, failure(a)), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69))))) | ?_11 | ','(no(empty(T76)), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 9\n\nT67 is ground\nT76 is ground\nX93 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(empty(T76), ','(','(!_10, failure(a)), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69))))), SCOPE: 12, CLAUSE: 7 | ?_12 | ?_11 | ','(no(empty(T76)), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 9\n\nT67 is ground\nT76 is ground\nX93 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(','(!_10, failure(a)), ','(head([], X93), ','(tail([], X94), rev(X94, .(X93, .(T67, [])), T69)))) | ?_12 | ?_11 | ','(no(empty([])), ','(head([], X93), ','(tail([], X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 9\n\nT67 is ground\nX93 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ?_12 | ?_11 | ','(no(empty(T76)), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 9\n\nT67 is ground\nT76 is ground\nX93 is free\nX94 is free\nempty(T76) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(failure(a), ','(head([], X93), ','(tail([], X94), rev(X94, .(X93, .(T67, [])), T69))))\n\nT67 is ground\nX93 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(failure(a), ','(head([], X93), ','(tail([], X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 13, CLAUSE: 10\n\nT67 is ground\nX93 is free\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ?_11 | ','(no(empty(T76)), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 9\n\nT67 is ground\nT76 is ground\nX93 is free\nX94 is free\nempty(T76) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(no(empty(T76)), ','(head(T76, X93), ','(tail(T76, X94), rev(X94, .(X93, .(T67, [])), T69)))), SCOPE: 10, CLAUSE: 9\n\nT67 is ground\nT76 is ground\nX93 is free\nX94 is free\nempty(T76) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ','(head(T87, X93), ','(tail(T87, X94), rev(X94, .(X93, .(T67, [])), T69)))\n\nT67 is ground\nT87 is ground\nX93 is free\nX94 is free\nempty(T87) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(head(T87, X93), ','(tail(T87, X94), rev(X94, .(X93, .(T67, [])), T69))), SCOPE: 14, CLAUSE: 3 | ','(head(T87, X93), ','(tail(T87, X94), rev(X94, .(X93, .(T67, [])), T69))), SCOPE: 14, CLAUSE: 4\n\nT67 is ground\nT87 is ground\nX93 is free\nX94 is free\nempty(T87) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(head(T87, X93), ','(tail(T87, X94), rev(X94, .(X93, .(T67, [])), T69))), SCOPE: 14, CLAUSE: 4\n\nT67 is ground\nT87 is ground\nX93 is free\nX94 is free\nempty(T87) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(tail(.(T96, T97), X94), rev(X94, .(T96, .(T67, [])), T69))\n\nT67 is ground\nT96 is ground\nT97 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ','(tail(.(T96, T97), X94), rev(X94, .(T96, .(T67, [])), T69)), SCOPE: 15, CLAUSE: 5 | ','(tail(.(T96, T97), X94), rev(X94, .(T96, .(T67, [])), T69)), SCOPE: 15, CLAUSE: 6\n\nT67 is ground\nT96 is ground\nT97 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ','(tail(.(T96, T97), X94), rev(X94, .(T96, .(T67, [])), T69)), SCOPE: 15, CLAUSE: 6\n\nT67 is ground\nT96 is ground\nT97 is ground\nX94 is free", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: rev(T111, .(T110, .(T67, [])), T69)\n\nT67 is ground\nT110 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: rev(T111, .(T110, .(T67, [])), T69), SCOPE: 16, CLAUSE: 1 | rev(T111, .(T110, .(T67, [])), T69), SCOPE: 16, CLAUSE: 2\n\nT67 is ground\nT110 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: rev(T111, .(T110, .(T67, [])), T69), SCOPE: 16, CLAUSE: 1\n\nT67 is ground\nT110 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: rev(T111, .(T110, .(T67, [])), T69), SCOPE: 16, CLAUSE: 2\n\nT67 is ground\nT110 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(no(empty(T141)), ','(head(T141, X157), ','(tail(T141, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145))))\n\nT141 is ground\nT142 is ground\nT143 is ground\nX157 is free\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: ','(no(empty(T141)), ','(head(T141, X157), ','(tail(T141, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 8 | ','(no(empty(T141)), ','(head(T141, X157), ','(tail(T141, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 9\n\nT141 is ground\nT142 is ground\nT143 is ground\nX157 is free\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: ','(','(call(empty(T154)), ','(!_17, failure(a))), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))) | ','(no(empty(T154)), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 9\n\nT142 is ground\nT143 is ground\nT154 is ground\nX157 is free\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: ','(empty(T154), ','(','(!_17, failure(a)), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145))))) | ?_18 | ','(no(empty(T154)), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 9\n\nT142 is ground\nT143 is ground\nT154 is ground\nX157 is free\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: ','(empty(T154), ','(','(!_17, failure(a)), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145))))), SCOPE: 19, CLAUSE: 7 | ?_19 | ?_18 | ','(no(empty(T154)), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 9\n\nT142 is ground\nT143 is ground\nT154 is ground\nX157 is free\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: ','(','(!_17, failure(a)), ','(head([], X157), ','(tail([], X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))) | ?_19 | ?_18 | ','(no(empty([])), ','(head([], X157), ','(tail([], X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 9\n\nT142 is ground\nT143 is ground\nX157 is free\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: ?_19 | ?_18 | ','(no(empty(T154)), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 9\n\nT142 is ground\nT143 is ground\nT154 is ground\nX157 is free\nX158 is free\nempty(T154) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: ','(failure(a), ','(head([], X157), ','(tail([], X158), rev(X158, .(X157, .(T142, .(T143, []))), T145))))\n\nT142 is ground\nT143 is ground\nX157 is free\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: ','(failure(a), ','(head([], X157), ','(tail([], X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 20, CLAUSE: 10\n\nT142 is ground\nT143 is ground\nX157 is free\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: ?_18 | ','(no(empty(T154)), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 9\n\nT142 is ground\nT143 is ground\nT154 is ground\nX157 is free\nX158 is free\nempty(T154) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: ','(no(empty(T154)), ','(head(T154, X157), ','(tail(T154, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))), SCOPE: 17, CLAUSE: 9\n\nT142 is ground\nT143 is ground\nT154 is ground\nX157 is free\nX158 is free\nempty(T154) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: ','(head(T169, X157), ','(tail(T169, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145)))\n\nT142 is ground\nT143 is ground\nT169 is ground\nX157 is free\nX158 is free\nempty(T169) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: ','(head(T169, X157), ','(tail(T169, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145))), SCOPE: 21, CLAUSE: 3 | ','(head(T169, X157), ','(tail(T169, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145))), SCOPE: 21, CLAUSE: 4\n\nT142 is ground\nT143 is ground\nT169 is ground\nX157 is free\nX158 is free\nempty(T169) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: ','(head(T169, X157), ','(tail(T169, X158), rev(X158, .(X157, .(T142, .(T143, []))), T145))), SCOPE: 21, CLAUSE: 4\n\nT142 is ground\nT143 is ground\nT169 is ground\nX157 is free\nX158 is free\nempty(T169) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: ','(tail(.(T180, T181), X158), rev(X158, .(T180, .(T142, .(T143, []))), T145))\n\nT142 is ground\nT143 is ground\nT180 is ground\nT181 is ground\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: ','(tail(.(T180, T181), X158), rev(X158, .(T180, .(T142, .(T143, []))), T145)), SCOPE: 22, CLAUSE: 5 | ','(tail(.(T180, T181), X158), rev(X158, .(T180, .(T142, .(T143, []))), T145)), SCOPE: 22, CLAUSE: 6\n\nT142 is ground\nT143 is ground\nT180 is ground\nT181 is ground\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: ','(tail(.(T180, T181), X158), rev(X158, .(T180, .(T142, .(T143, []))), T145)), SCOPE: 22, CLAUSE: 6\n\nT142 is ground\nT143 is ground\nT180 is ground\nT181 is ground\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: rev(T199, .(T198, .(T142, .(T143, []))), T145)\n\nT142 is ground\nT143 is ground\nT198 is ground\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: rev(T199, .(T198, .(T142, .(T143, []))), T145), SCOPE: 23, CLAUSE: 1 | rev(T199, .(T198, .(T142, .(T143, []))), T145), SCOPE: 23, CLAUSE: 2\n\nT142 is ground\nT143 is ground\nT198 is ground\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: rev(T199, .(T198, .(T142, .(T143, []))), T145), SCOPE: 23, CLAUSE: 1\n\nT142 is ground\nT143 is ground\nT198 is ground\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: rev(T199, .(T198, .(T142, .(T143, []))), T145), SCOPE: 23, CLAUSE: 2\n\nT142 is ground\nT143 is ground\nT198 is ground\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
337 [label="337: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
353 [label="353: ','(no(empty(T240)), ','(head(T240, X221), ','(tail(T240, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245))))\n\nT240 is ground\nT241 is ground\nT242 is ground\nT243 is ground\nX221 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: ','(no(empty(T240)), ','(head(T240, X221), ','(tail(T240, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 8 | ','(no(empty(T240)), ','(head(T240, X221), ','(tail(T240, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 9\n\nT240 is ground\nT241 is ground\nT242 is ground\nT243 is ground\nX221 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
357 [label="357: ','(','(call(empty(T256)), ','(!_24, failure(a))), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))) | ','(no(empty(T256)), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 9\n\nT241 is ground\nT242 is ground\nT243 is ground\nT256 is ground\nX221 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
360 [label="360: ','(empty(T256), ','(','(!_24, failure(a)), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245))))) | ?_25 | ','(no(empty(T256)), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 9\n\nT241 is ground\nT242 is ground\nT243 is ground\nT256 is ground\nX221 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
361 [label="361: ','(empty(T256), ','(','(!_24, failure(a)), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245))))), SCOPE: 26, CLAUSE: 7 | ?_26 | ?_25 | ','(no(empty(T256)), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 9\n\nT241 is ground\nT242 is ground\nT243 is ground\nT256 is ground\nX221 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
362 [label="362: ','(','(!_24, failure(a)), ','(head([], X221), ','(tail([], X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))) | ?_26 | ?_25 | ','(no(empty([])), ','(head([], X221), ','(tail([], X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 9\n\nT241 is ground\nT242 is ground\nT243 is ground\nX221 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
363 [label="363: ?_26 | ?_25 | ','(no(empty(T256)), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 9\n\nT241 is ground\nT242 is ground\nT243 is ground\nT256 is ground\nX221 is free\nX222 is free\nempty(T256) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
364 [label="364: ','(failure(a), ','(head([], X221), ','(tail([], X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245))))\n\nT241 is ground\nT242 is ground\nT243 is ground\nX221 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
374 [label="374: ','(failure(a), ','(head([], X221), ','(tail([], X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 27, CLAUSE: 10\n\nT241 is ground\nT242 is ground\nT243 is ground\nX221 is free\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: ?_25 | ','(no(empty(T256)), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 9\n\nT241 is ground\nT242 is ground\nT243 is ground\nT256 is ground\nX221 is free\nX222 is free\nempty(T256) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
377 [label="377: ','(no(empty(T256)), ','(head(T256, X221), ','(tail(T256, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))), SCOPE: 24, CLAUSE: 9\n\nT241 is ground\nT242 is ground\nT243 is ground\nT256 is ground\nX221 is free\nX222 is free\nempty(T256) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: ','(head(T275, X221), ','(tail(T275, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245)))\n\nT241 is ground\nT242 is ground\nT243 is ground\nT275 is ground\nX221 is free\nX222 is free\nempty(T275) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
380 [label="380: ','(head(T275, X221), ','(tail(T275, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245))), SCOPE: 28, CLAUSE: 3 | ','(head(T275, X221), ','(tail(T275, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245))), SCOPE: 28, CLAUSE: 4\n\nT241 is ground\nT242 is ground\nT243 is ground\nT275 is ground\nX221 is free\nX222 is free\nempty(T275) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
381 [label="381: ','(head(T275, X221), ','(tail(T275, X222), rev(X222, .(X221, .(T241, .(T242, .(T243, [])))), T245))), SCOPE: 28, CLAUSE: 4\n\nT241 is ground\nT242 is ground\nT243 is ground\nT275 is ground\nX221 is free\nX222 is free\nempty(T275) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
401 [label="401: ','(tail(.(T288, T289), X222), rev(X222, .(T288, .(T241, .(T242, .(T243, [])))), T245))\n\nT241 is ground\nT242 is ground\nT243 is ground\nT288 is ground\nT289 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
402 [label="402: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
408 [label="408: ','(tail(.(T288, T289), X222), rev(X222, .(T288, .(T241, .(T242, .(T243, [])))), T245)), SCOPE: 29, CLAUSE: 5 | ','(tail(.(T288, T289), X222), rev(X222, .(T288, .(T241, .(T242, .(T243, [])))), T245)), SCOPE: 29, CLAUSE: 6\n\nT241 is ground\nT242 is ground\nT243 is ground\nT288 is ground\nT289 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
409 [label="409: ','(tail(.(T288, T289), X222), rev(X222, .(T288, .(T241, .(T242, .(T243, [])))), T245)), SCOPE: 29, CLAUSE: 6\n\nT241 is ground\nT242 is ground\nT243 is ground\nT288 is ground\nT289 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
412 [label="412: rev(T311, .(T310, .(T241, .(T242, .(T243, [])))), T245)\n\nT241 is ground\nT242 is ground\nT243 is ground\nT310 is ground\nT311 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
416 [label="416: rev(T311, .(T310, .(T241, .(T242, .(T243, [])))), T245), SCOPE: 30, CLAUSE: 1 | rev(T311, .(T310, .(T241, .(T242, .(T243, [])))), T245), SCOPE: 30, CLAUSE: 2\n\nT241 is ground\nT242 is ground\nT243 is ground\nT310 is ground\nT311 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
426 [label="426: rev(T311, .(T310, .(T241, .(T242, .(T243, [])))), T245), SCOPE: 30, CLAUSE: 1\n\nT241 is ground\nT242 is ground\nT243 is ground\nT310 is ground\nT311 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
427 [label="427: rev(T311, .(T310, .(T241, .(T242, .(T243, [])))), T245), SCOPE: 30, CLAUSE: 2\n\nT241 is ground\nT242 is ground\nT243 is ground\nT310 is ground\nT311 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
430 [label="430: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
431 [label="431: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
432 [label="432: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
444 [label="444: ','(no(empty(T363)), ','(head(T363, X285), ','(tail(T363, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369))))\n\nT363 is ground\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nX285 is free\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
445 [label="445: ','(no(empty(T363)), ','(head(T363, X285), ','(tail(T363, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 8 | ','(no(empty(T363)), ','(head(T363, X285), ','(tail(T363, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 9\n\nT363 is ground\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nX285 is free\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
446 [label="446: ','(','(call(empty(T382)), ','(!_31, failure(a))), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))) | ','(no(empty(T382)), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 9\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT382 is ground\nX285 is free\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
447 [label="447: ','(empty(T382), ','(','(!_31, failure(a)), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369))))) | ?_32 | ','(no(empty(T382)), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 9\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT382 is ground\nX285 is free\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
448 [label="448: ','(empty(T382), ','(','(!_31, failure(a)), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369))))), SCOPE: 33, CLAUSE: 7 | ?_33 | ?_32 | ','(no(empty(T382)), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 9\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT382 is ground\nX285 is free\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
449 [label="449: ','(','(!_31, failure(a)), ','(head([], X285), ','(tail([], X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))) | ?_33 | ?_32 | ','(no(empty([])), ','(head([], X285), ','(tail([], X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 9\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nX285 is free\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
450 [label="450: ?_33 | ?_32 | ','(no(empty(T382)), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 9\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT382 is ground\nX285 is free\nX286 is free\nempty(T382) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: ','(failure(a), ','(head([], X285), ','(tail([], X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369))))\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nX285 is free\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
453 [label="453: ','(failure(a), ','(head([], X285), ','(tail([], X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 34, CLAUSE: 10\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nX285 is free\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
454 [label="454: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
455 [label="455: ?_32 | ','(no(empty(T382)), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 9\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT382 is ground\nX285 is free\nX286 is free\nempty(T382) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
456 [label="456: ','(no(empty(T382)), ','(head(T382, X285), ','(tail(T382, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))), SCOPE: 31, CLAUSE: 9\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT382 is ground\nX285 is free\nX286 is free\nempty(T382) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
474 [label="474: ','(head(T405, X285), ','(tail(T405, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369)))\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT405 is ground\nX285 is free\nX286 is free\nempty(T405) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
477 [label="477: ','(head(T405, X285), ','(tail(T405, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369))), SCOPE: 35, CLAUSE: 3 | ','(head(T405, X285), ','(tail(T405, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369))), SCOPE: 35, CLAUSE: 4\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT405 is ground\nX285 is free\nX286 is free\nempty(T405) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
478 [label="478: ','(head(T405, X285), ','(tail(T405, X286), rev(X286, .(X285, .(T364, .(T365, .(T366, .(T367, []))))), T369))), SCOPE: 35, CLAUSE: 4\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT405 is ground\nX285 is free\nX286 is free\nempty(T405) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
482 [label="482: ','(tail(.(T420, T421), X286), rev(X286, .(T420, .(T364, .(T365, .(T366, .(T367, []))))), T369))\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT420 is ground\nT421 is ground\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
484 [label="484: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
486 [label="486: ','(tail(.(T420, T421), X286), rev(X286, .(T420, .(T364, .(T365, .(T366, .(T367, []))))), T369)), SCOPE: 36, CLAUSE: 5 | ','(tail(.(T420, T421), X286), rev(X286, .(T420, .(T364, .(T365, .(T366, .(T367, []))))), T369)), SCOPE: 36, CLAUSE: 6\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT420 is ground\nT421 is ground\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
487 [label="487: ','(tail(.(T420, T421), X286), rev(X286, .(T420, .(T364, .(T365, .(T366, .(T367, []))))), T369)), SCOPE: 36, CLAUSE: 6\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT420 is ground\nT421 is ground\nX286 is free", fontsize=16, style=filled, fillcolor=lightyellow];
491 [label="491: rev(T447, .(T446, .(T364, .(T365, .(T366, .(T367, []))))), T369)\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT446 is ground\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
494 [label="494: rev(T447, .(T446, .(T364, .(T365, .(T366, .(T367, []))))), T369), SCOPE: 37, CLAUSE: 1 | rev(T447, .(T446, .(T364, .(T365, .(T366, .(T367, []))))), T369), SCOPE: 37, CLAUSE: 2\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT446 is ground\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
499 [label="499: rev(T447, .(T446, .(T364, .(T365, .(T366, .(T367, []))))), T369), SCOPE: 37, CLAUSE: 1\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT446 is ground\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
500 [label="500: rev(T447, .(T446, .(T364, .(T365, .(T366, .(T367, []))))), T369), SCOPE: 37, CLAUSE: 2\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT446 is ground\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
503 [label="503: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
504 [label="504: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
505 [label="505: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
509 [label="509: ','(no(empty(T510)), ','(head(T510, X349), ','(tail(T510, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517))))\n\nT510 is ground\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
512 [label="512: ','(no(empty(T510)), ','(head(T510, X349), ','(tail(T510, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 8 | ','(no(empty(T510)), ','(head(T510, X349), ','(tail(T510, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 9\n\nT510 is ground\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
515 [label="515: ','(','(call(empty(T532)), ','(!_38, failure(a))), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))) | ','(no(empty(T532)), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 9\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT532 is ground\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
516 [label="516: ','(empty(T532), ','(','(!_38, failure(a)), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517))))) | ?_39 | ','(no(empty(T532)), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 9\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT532 is ground\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
517 [label="517: ','(empty(T532), ','(','(!_38, failure(a)), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517))))), SCOPE: 40, CLAUSE: 7 | ?_40 | ?_39 | ','(no(empty(T532)), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 9\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT532 is ground\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
518 [label="518: ','(','(!_38, failure(a)), ','(head([], X349), ','(tail([], X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))) | ?_40 | ?_39 | ','(no(empty([])), ','(head([], X349), ','(tail([], X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 9\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
519 [label="519: ?_40 | ?_39 | ','(no(empty(T532)), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 9\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT532 is ground\nX349 is free\nX350 is free\nempty(T532) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
520 [label="520: ','(failure(a), ','(head([], X349), ','(tail([], X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517))))\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
527 [label="527: ','(failure(a), ','(head([], X349), ','(tail([], X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 41, CLAUSE: 10\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nX349 is free\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
528 [label="528: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
529 [label="529: ?_39 | ','(no(empty(T532)), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 9\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT532 is ground\nX349 is free\nX350 is free\nempty(T532) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
530 [label="530: ','(no(empty(T532)), ','(head(T532, X349), ','(tail(T532, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))), SCOPE: 38, CLAUSE: 9\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT532 is ground\nX349 is free\nX350 is free\nempty(T532) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
531 [label="531: ','(head(T559, X349), ','(tail(T559, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)))\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT559 is ground\nX349 is free\nX350 is free\nempty(T559) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
535 [label="535: ','(head(T559, X349), ','(tail(T559, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517))), SCOPE: 42, CLAUSE: 3 | ','(head(T559, X349), ','(tail(T559, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517))), SCOPE: 42, CLAUSE: 4\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT559 is ground\nX349 is free\nX350 is free\nempty(T559) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
536 [label="536: ','(head(T559, X349), ','(tail(T559, X350), rev(X350, .(X349, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517))), SCOPE: 42, CLAUSE: 4\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT559 is ground\nX349 is free\nX350 is free\nempty(T559) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
537 [label="537: ','(tail(.(T576, T577), X350), rev(X350, .(T576, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517))\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT576 is ground\nT577 is ground\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
538 [label="538: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
539 [label="539: ','(tail(.(T576, T577), X350), rev(X350, .(T576, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)), SCOPE: 43, CLAUSE: 5 | ','(tail(.(T576, T577), X350), rev(X350, .(T576, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)), SCOPE: 43, CLAUSE: 6\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT576 is ground\nT577 is ground\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
540 [label="540: ','(tail(.(T576, T577), X350), rev(X350, .(T576, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)), SCOPE: 43, CLAUSE: 6\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT576 is ground\nT577 is ground\nX350 is free", fontsize=16, style=filled, fillcolor=lightyellow];
542 [label="542: rev(T607, .(T606, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517)\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT606 is ground\nT607 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
546 [label="546: rev(T607, .(T606, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517), SCOPE: 44, CLAUSE: 1 | rev(T607, .(T606, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517), SCOPE: 44, CLAUSE: 2\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT606 is ground\nT607 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
552 [label="552: rev(T607, .(T606, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517), SCOPE: 44, CLAUSE: 1\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT606 is ground\nT607 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
553 [label="553: rev(T607, .(T606, .(T511, .(T512, .(T513, .(T514, .(T515, [])))))), T517), SCOPE: 44, CLAUSE: 2\n\nT511 is ground\nT512 is ground\nT513 is ground\nT514 is ground\nT515 is ground\nT606 is ground\nT607 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
559 [label="559: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
560 [label="560: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
562 [label="562: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
573 [label="573: ','(no(empty(T681)), ','(head(T681, X413), ','(tail(T681, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689))))\n\nT681 is ground\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nX413 is free\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
579 [label="579: ','(no(empty(T681)), ','(head(T681, X413), ','(tail(T681, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 8 | ','(no(empty(T681)), ','(head(T681, X413), ','(tail(T681, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 9\n\nT681 is ground\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nX413 is free\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
580 [label="580: ','(','(call(empty(T706)), ','(!_45, failure(a))), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))) | ','(no(empty(T706)), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 9\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT706 is ground\nX413 is free\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
581 [label="581: ','(empty(T706), ','(','(!_45, failure(a)), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689))))) | ?_46 | ','(no(empty(T706)), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 9\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT706 is ground\nX413 is free\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
582 [label="582: ','(empty(T706), ','(','(!_45, failure(a)), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689))))), SCOPE: 47, CLAUSE: 7 | ?_47 | ?_46 | ','(no(empty(T706)), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 9\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT706 is ground\nX413 is free\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
583 [label="583: ','(','(!_45, failure(a)), ','(head([], X413), ','(tail([], X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))) | ?_47 | ?_46 | ','(no(empty([])), ','(head([], X413), ','(tail([], X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 9\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nX413 is free\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
584 [label="584: ?_47 | ?_46 | ','(no(empty(T706)), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 9\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT706 is ground\nX413 is free\nX414 is free\nempty(T706) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
585 [label="585: ','(failure(a), ','(head([], X413), ','(tail([], X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689))))\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nX413 is free\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
590 [label="590: ','(failure(a), ','(head([], X413), ','(tail([], X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 48, CLAUSE: 10\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nX413 is free\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
591 [label="591: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
592 [label="592: ?_46 | ','(no(empty(T706)), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 9\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT706 is ground\nX413 is free\nX414 is free\nempty(T706) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
593 [label="593: ','(no(empty(T706)), ','(head(T706, X413), ','(tail(T706, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))), SCOPE: 45, CLAUSE: 9\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT706 is ground\nX413 is free\nX414 is free\nempty(T706) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
596 [label="596: ','(head(T737, X413), ','(tail(T737, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)))\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT737 is ground\nX413 is free\nX414 is free\nempty(T737) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
600 [label="600: ','(head(T737, X413), ','(tail(T737, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689))), SCOPE: 49, CLAUSE: 3 | ','(head(T737, X413), ','(tail(T737, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689))), SCOPE: 49, CLAUSE: 4\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT737 is ground\nX413 is free\nX414 is free\nempty(T737) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
601 [label="601: ','(head(T737, X413), ','(tail(T737, X414), rev(X414, .(X413, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689))), SCOPE: 49, CLAUSE: 4\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT737 is ground\nX413 is free\nX414 is free\nempty(T737) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
602 [label="602: ','(tail(.(T756, T757), X414), rev(X414, .(T756, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689))\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT756 is ground\nT757 is ground\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
603 [label="603: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
605 [label="605: ','(tail(.(T756, T757), X414), rev(X414, .(T756, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)), SCOPE: 50, CLAUSE: 5 | ','(tail(.(T756, T757), X414), rev(X414, .(T756, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)), SCOPE: 50, CLAUSE: 6\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT756 is ground\nT757 is ground\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
606 [label="606: ','(tail(.(T756, T757), X414), rev(X414, .(T756, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)), SCOPE: 50, CLAUSE: 6\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT756 is ground\nT757 is ground\nX414 is free", fontsize=16, style=filled, fillcolor=lightyellow];
615 [label="615: rev(T791, .(T790, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689)\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT790 is ground\nT791 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
620 [label="620: rev(T791, .(T790, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689), SCOPE: 51, CLAUSE: 1 | rev(T791, .(T790, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689), SCOPE: 51, CLAUSE: 2\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT790 is ground\nT791 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
646 [label="646: rev(T791, .(T790, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689), SCOPE: 51, CLAUSE: 1\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT790 is ground\nT791 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
647 [label="647: rev(T791, .(T790, .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, []))))))), T689), SCOPE: 51, CLAUSE: 2\n\nT682 is ground\nT683 is ground\nT684 is ground\nT685 is ground\nT686 is ground\nT687 is ground\nT790 is ground\nT791 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
657 [label="657: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
658 [label="658: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
659 [label="659: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
668 [label="668: ','(no(empty(T876)), ','(head(T876, X477), ','(tail(T876, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885))))\n\nT876 is ground\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nX477 is free\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
669 [label="669: ','(no(empty(T876)), ','(head(T876, X477), ','(tail(T876, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 8 | ','(no(empty(T876)), ','(head(T876, X477), ','(tail(T876, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 9\n\nT876 is ground\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nX477 is free\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
670 [label="670: ','(','(call(empty(T904)), ','(!_52, failure(a))), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))) | ','(no(empty(T904)), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 9\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT904 is ground\nX477 is free\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
671 [label="671: ','(empty(T904), ','(','(!_52, failure(a)), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885))))) | ?_53 | ','(no(empty(T904)), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 9\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT904 is ground\nX477 is free\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
672 [label="672: ','(empty(T904), ','(','(!_52, failure(a)), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885))))), SCOPE: 54, CLAUSE: 7 | ?_54 | ?_53 | ','(no(empty(T904)), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 9\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT904 is ground\nX477 is free\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
673 [label="673: ','(','(!_52, failure(a)), ','(head([], X477), ','(tail([], X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))) | ?_54 | ?_53 | ','(no(empty([])), ','(head([], X477), ','(tail([], X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 9\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nX477 is free\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
674 [label="674: ?_54 | ?_53 | ','(no(empty(T904)), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 9\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT904 is ground\nX477 is free\nX478 is free\nempty(T904) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
675 [label="675: ','(failure(a), ','(head([], X477), ','(tail([], X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885))))\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nX477 is free\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
676 [label="676: ','(failure(a), ','(head([], X477), ','(tail([], X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 55, CLAUSE: 10\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nX477 is free\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
677 [label="677: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
678 [label="678: ?_53 | ','(no(empty(T904)), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 9\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT904 is ground\nX477 is free\nX478 is free\nempty(T904) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
679 [label="679: ','(no(empty(T904)), ','(head(T904, X477), ','(tail(T904, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))), SCOPE: 52, CLAUSE: 9\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT904 is ground\nX477 is free\nX478 is free\nempty(T904) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
680 [label="680: ','(head(T939, X477), ','(tail(T939, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)))\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT939 is ground\nX477 is free\nX478 is free\nempty(T939) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
681 [label="681: ','(head(T939, X477), ','(tail(T939, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885))), SCOPE: 56, CLAUSE: 3 | ','(head(T939, X477), ','(tail(T939, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885))), SCOPE: 56, CLAUSE: 4\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT939 is ground\nX477 is free\nX478 is free\nempty(T939) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
682 [label="682: ','(head(T939, X477), ','(tail(T939, X478), rev(X478, .(X477, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885))), SCOPE: 56, CLAUSE: 4\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT939 is ground\nX477 is free\nX478 is free\nempty(T939) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
683 [label="683: ','(tail(.(T960, T961), X478), rev(X478, .(T960, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885))\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT960 is ground\nT961 is ground\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
684 [label="684: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
685 [label="685: ','(tail(.(T960, T961), X478), rev(X478, .(T960, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)), SCOPE: 57, CLAUSE: 5 | ','(tail(.(T960, T961), X478), rev(X478, .(T960, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)), SCOPE: 57, CLAUSE: 6\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT960 is ground\nT961 is ground\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
686 [label="686: ','(tail(.(T960, T961), X478), rev(X478, .(T960, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)), SCOPE: 57, CLAUSE: 6\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT960 is ground\nT961 is ground\nX478 is free", fontsize=16, style=filled, fillcolor=lightyellow];
687 [label="687: rev(T999, .(T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))), T885)\n\nT877 is ground\nT878 is ground\nT879 is ground\nT880 is ground\nT881 is ground\nT882 is ground\nT883 is ground\nT998 is ground\nT999 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
688 [label="B: rev(T999, .(T998, T1016), T885)\n\nT998 is ground\nT999 is ground\nT1016 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
689 [label="689: rev(T999, .(T998, T1016), T885), SCOPE: 58, CLAUSE: 1 | rev(T999, .(T998, T1016), T885), SCOPE: 58, CLAUSE: 2\n\nT998 is ground\nT999 is ground\nT1016 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
690 [label="690: rev(T999, .(T998, T1016), T885), SCOPE: 58, CLAUSE: 1\n\nT998 is ground\nT999 is ground\nT1016 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
691 [label="691: rev(T999, .(T998, T1016), T885), SCOPE: 58, CLAUSE: 2\n\nT998 is ground\nT999 is ground\nT1016 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
692 [label="692: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
693 [label="693: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
694 [label="694: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
695 [label="695: ','(no(empty(T1046)), ','(head(T1046, X543), ','(tail(T1046, X544), rev(X544, .(X543, .(T1047, T1048)), T1050))))\n\nT1046 is ground\nT1047 is ground\nT1048 is ground\nX543 is free\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
696 [label="696: ','(no(empty(T1046)), ','(head(T1046, X543), ','(tail(T1046, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 8 | ','(no(empty(T1046)), ','(head(T1046, X543), ','(tail(T1046, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 9\n\nT1046 is ground\nT1047 is ground\nT1048 is ground\nX543 is free\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
697 [label="697: ','(','(call(empty(T1059)), ','(!_59, failure(a))), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))) | ','(no(empty(T1059)), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 9\n\nT1047 is ground\nT1048 is ground\nT1059 is ground\nX543 is free\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
698 [label="698: ','(empty(T1059), ','(','(!_59, failure(a)), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050))))) | ?_60 | ','(no(empty(T1059)), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 9\n\nT1047 is ground\nT1048 is ground\nT1059 is ground\nX543 is free\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
699 [label="699: ','(empty(T1059), ','(','(!_59, failure(a)), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050))))), SCOPE: 61, CLAUSE: 7 | ?_61 | ?_60 | ','(no(empty(T1059)), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 9\n\nT1047 is ground\nT1048 is ground\nT1059 is ground\nX543 is free\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
700 [label="700: ','(','(!_59, failure(a)), ','(head([], X543), ','(tail([], X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))) | ?_61 | ?_60 | ','(no(empty([])), ','(head([], X543), ','(tail([], X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 9\n\nT1047 is ground\nT1048 is ground\nX543 is free\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
701 [label="701: ?_61 | ?_60 | ','(no(empty(T1059)), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 9\n\nT1047 is ground\nT1048 is ground\nT1059 is ground\nX543 is free\nX544 is free\nempty(T1059) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
702 [label="702: ','(failure(a), ','(head([], X543), ','(tail([], X544), rev(X544, .(X543, .(T1047, T1048)), T1050))))\n\nT1047 is ground\nT1048 is ground\nX543 is free\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
703 [label="703: ','(failure(a), ','(head([], X543), ','(tail([], X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 62, CLAUSE: 10\n\nT1047 is ground\nT1048 is ground\nX543 is free\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
704 [label="704: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
705 [label="705: ?_60 | ','(no(empty(T1059)), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 9\n\nT1047 is ground\nT1048 is ground\nT1059 is ground\nX543 is free\nX544 is free\nempty(T1059) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
706 [label="706: ','(no(empty(T1059)), ','(head(T1059, X543), ','(tail(T1059, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))), SCOPE: 59, CLAUSE: 9\n\nT1047 is ground\nT1048 is ground\nT1059 is ground\nX543 is free\nX544 is free\nempty(T1059) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
707 [label="707: ','(head(T1074, X543), ','(tail(T1074, X544), rev(X544, .(X543, .(T1047, T1048)), T1050)))\n\nT1047 is ground\nT1048 is ground\nT1074 is ground\nX543 is free\nX544 is free\nempty(T1074) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
708 [label="708: ','(head(T1074, X543), ','(tail(T1074, X544), rev(X544, .(X543, .(T1047, T1048)), T1050))), SCOPE: 63, CLAUSE: 3 | ','(head(T1074, X543), ','(tail(T1074, X544), rev(X544, .(X543, .(T1047, T1048)), T1050))), SCOPE: 63, CLAUSE: 4\n\nT1047 is ground\nT1048 is ground\nT1074 is ground\nX543 is free\nX544 is free\nempty(T1074) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
709 [label="709: ','(head(T1074, X543), ','(tail(T1074, X544), rev(X544, .(X543, .(T1047, T1048)), T1050))), SCOPE: 63, CLAUSE: 4\n\nT1047 is ground\nT1048 is ground\nT1074 is ground\nX543 is free\nX544 is free\nempty(T1074) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
710 [label="710: ','(tail(.(T1085, T1086), X544), rev(X544, .(T1085, .(T1047, T1048)), T1050))\n\nT1047 is ground\nT1048 is ground\nT1085 is ground\nT1086 is ground\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
711 [label="711: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
712 [label="712: ','(tail(.(T1085, T1086), X544), rev(X544, .(T1085, .(T1047, T1048)), T1050)), SCOPE: 64, CLAUSE: 5 | ','(tail(.(T1085, T1086), X544), rev(X544, .(T1085, .(T1047, T1048)), T1050)), SCOPE: 64, CLAUSE: 6\n\nT1047 is ground\nT1048 is ground\nT1085 is ground\nT1086 is ground\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
713 [label="713: ','(tail(.(T1085, T1086), X544), rev(X544, .(T1085, .(T1047, T1048)), T1050)), SCOPE: 64, CLAUSE: 6\n\nT1047 is ground\nT1048 is ground\nT1085 is ground\nT1086 is ground\nX544 is free", fontsize=16, style=filled, fillcolor=lightyellow];
714 [label="714: rev(T1104, .(T1103, .(T1047, T1048)), T1050)\n\nT1047 is ground\nT1048 is ground\nT1103 is ground\nT1104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
715 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 715 [arrowhead = none ];
715 -> 4;

716 [label="ONLY EVAL with clause\nrev(X7, X8) :- rev(X7, [], X8).\nand substitutionT1 -> T5,\nX7 -> T5,\nT2 -> T7,\nX8 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 716 [arrowhead = none ];
716 -> 8;

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

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

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

720 [label="EVAL with clause\nrev([], X13, X13).\nand substitutionT5 -> [],\nX13 -> [],\nT7 -> []", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 720 [arrowhead = none ];
720 -> 16;

721 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 721 [arrowhead = none ];
721 -> 18;

722 [label="ONLY EVAL with clause\nrev(X26, X27, X28) :- ','(no(empty(X26)), ','(head(X26, X29), ','(tail(X26, X30), rev(X30, .(X29, X27), X28)))).\nand substitutionT5 -> T15,\nX26 -> T15,\nX27 -> [],\nT7 -> T17,\nX28 -> T17,\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 722 [arrowhead = none ];
722 -> 29;

723 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 723 [arrowhead = none ];
723 -> 21;

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

725 [label="ONLY EVAL with clause\nno(X37) :- ','(call(X37), ','(!_3, failure(a))).\nand substitutionT15 -> T22,\nX37 -> empty(T22)", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 725 [arrowhead = none ];
725 -> 44;

726 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
44 -> 726 [arrowhead = none ];
726 -> 47;

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

728 [label="EVAL with clause\nempty([]).\nand substitutionT22 -> []", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 728 [arrowhead = none ];
728 -> 49;

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

730 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 730 [arrowhead = none ];
730 -> 51;

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

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

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

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

735 [label="ONLY EVAL with clause\nno(X48).\nand substitutionT22 -> T29,\nX48 -> empty(T29)", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 735 [arrowhead = none ];
735 -> 65;

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

737 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T29), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 737 [arrowhead = none ];
737 -> 72;

738 [label="EVAL with clause\nhead(.(X59, X60), X59).\nand substitutionX59 -> T36,\nX60 -> T37,\nT29 -> .(T36, T37),\nX29 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 738 [arrowhead = none ];
738 -> 92;

739 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 739 [arrowhead = none ];
739 -> 93;

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

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

742 [label="ONLY EVAL with clause\ntail(.(X69, X70), X70).\nand substitutionT36 -> T46,\nX69 -> T46,\nT37 -> T47,\nX70 -> T47,\nX30 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 742 [arrowhead = none ];
742 -> 106;

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

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

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

746 [label="EVAL with clause\nrev([], X77, X77).\nand substitutionT47 -> [],\nT46 -> T54,\nX77 -> .(T54, []),\nT17 -> .(T54, [])", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 746 [arrowhead = none ];
746 -> 123;

747 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 747 [arrowhead = none ];
747 -> 124;

748 [label="ONLY EVAL with clause\nrev(X90, X91, X92) :- ','(no(empty(X90)), ','(head(X90, X93), ','(tail(X90, X94), rev(X94, .(X93, X91), X92)))).\nand substitutionT47 -> T66,\nX90 -> T66,\nT46 -> T67,\nX91 -> .(T67, []),\nT17 -> T69,\nX92 -> T69,\nT68 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 748 [arrowhead = none ];
748 -> 146;

749 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 749 [arrowhead = none ];
749 -> 125;

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

751 [label="ONLY EVAL with clause\nno(X101) :- ','(call(X101), ','(!_10, failure(a))).\nand substitutionT66 -> T76,\nX101 -> empty(T76)", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 751 [arrowhead = none ];
751 -> 153;

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

753 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
156 -> 753 [arrowhead = none ];
753 -> 159;

754 [label="EVAL with clause\nempty([]).\nand substitutionT76 -> []", fontsize=14, style = filled, fillcolor = lightblue];
159 -> 754 [arrowhead = none ];
754 -> 166;

755 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
159 -> 755 [arrowhead = none ];
755 -> 167;

756 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
166 -> 756 [arrowhead = none ];
756 -> 168;

757 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
167 -> 757 [arrowhead = none ];
757 -> 174;

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

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

760 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
174 -> 760 [arrowhead = none ];
760 -> 177;

761 [label="ONLY EVAL with clause\nno(X112).\nand substitutionT76 -> T87,\nX112 -> empty(T87)", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 761 [arrowhead = none ];
761 -> 184;

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

763 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T87), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
199 -> 763 [arrowhead = none ];
763 -> 201;

764 [label="EVAL with clause\nhead(.(X123, X124), X123).\nand substitutionX123 -> T96,\nX124 -> T97,\nT87 -> .(T96, T97),\nX93 -> T96", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 764 [arrowhead = none ];
764 -> 205;

765 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 765 [arrowhead = none ];
765 -> 206;

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

767 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
211 -> 767 [arrowhead = none ];
767 -> 212;

768 [label="ONLY EVAL with clause\ntail(.(X133, X134), X134).\nand substitutionT96 -> T110,\nX133 -> T110,\nT97 -> T111,\nX134 -> T111,\nX94 -> T111", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 768 [arrowhead = none ];
768 -> 223;

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

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

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

772 [label="EVAL with clause\nrev([], X141, X141).\nand substitutionT111 -> [],\nT110 -> T124,\nT67 -> T125,\nX141 -> .(T124, .(T125, [])),\nT69 -> .(T124, .(T125, []))", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 772 [arrowhead = none ];
772 -> 233;

773 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
229 -> 773 [arrowhead = none ];
773 -> 234;

774 [label="ONLY EVAL with clause\nrev(X154, X155, X156) :- ','(no(empty(X154)), ','(head(X154, X157), ','(tail(X154, X158), rev(X158, .(X157, X155), X156)))).\nand substitutionT111 -> T141,\nX154 -> T141,\nT110 -> T142,\nT67 -> T143,\nX155 -> .(T142, .(T143, [])),\nT69 -> T145,\nX156 -> T145,\nT144 -> T145", fontsize=14, style = filled, fillcolor = lightblue];
230 -> 774 [arrowhead = none ];
774 -> 261;

775 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
233 -> 775 [arrowhead = none ];
775 -> 235;

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

777 [label="ONLY EVAL with clause\nno(X165) :- ','(call(X165), ','(!_17, failure(a))).\nand substitutionT141 -> T154,\nX165 -> empty(T154)", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 777 [arrowhead = none ];
777 -> 266;

778 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
266 -> 778 [arrowhead = none ];
778 -> 267;

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

780 [label="EVAL with clause\nempty([]).\nand substitutionT154 -> []", fontsize=14, style = filled, fillcolor = lightblue];
268 -> 780 [arrowhead = none ];
780 -> 269;

781 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
268 -> 781 [arrowhead = none ];
781 -> 270;

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

783 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
270 -> 783 [arrowhead = none ];
783 -> 289;

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

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

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

787 [label="ONLY EVAL with clause\nno(X176).\nand substitutionT154 -> T169,\nX176 -> empty(T169)", fontsize=14, style = filled, fillcolor = lightblue];
290 -> 787 [arrowhead = none ];
787 -> 296;

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

789 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T169), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
298 -> 789 [arrowhead = none ];
789 -> 299;

790 [label="EVAL with clause\nhead(.(X187, X188), X187).\nand substitutionX187 -> T180,\nX188 -> T181,\nT169 -> .(T180, T181),\nX157 -> T180", fontsize=14, style = filled, fillcolor = lightblue];
299 -> 790 [arrowhead = none ];
790 -> 302;

791 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
299 -> 791 [arrowhead = none ];
791 -> 304;

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

793 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
305 -> 793 [arrowhead = none ];
793 -> 306;

794 [label="ONLY EVAL with clause\ntail(.(X197, X198), X198).\nand substitutionT180 -> T198,\nX197 -> T198,\nT181 -> T199,\nX198 -> T199,\nX158 -> T199", fontsize=14, style = filled, fillcolor = lightblue];
306 -> 794 [arrowhead = none ];
794 -> 322;

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

796 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
328 -> 796 [arrowhead = none ];
796 -> 329;

797 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
328 -> 797 [arrowhead = none ];
797 -> 330;

798 [label="EVAL with clause\nrev([], X205, X205).\nand substitutionT199 -> [],\nT198 -> T218,\nT142 -> T219,\nT143 -> T220,\nX205 -> .(T218, .(T219, .(T220, []))),\nT145 -> .(T218, .(T219, .(T220, [])))", fontsize=14, style = filled, fillcolor = lightblue];
329 -> 798 [arrowhead = none ];
798 -> 336;

799 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
329 -> 799 [arrowhead = none ];
799 -> 337;

800 [label="ONLY EVAL with clause\nrev(X218, X219, X220) :- ','(no(empty(X218)), ','(head(X218, X221), ','(tail(X218, X222), rev(X222, .(X221, X219), X220)))).\nand substitutionT199 -> T240,\nX218 -> T240,\nT198 -> T241,\nT142 -> T242,\nT143 -> T243,\nX219 -> .(T241, .(T242, .(T243, []))),\nT145 -> T245,\nX220 -> T245,\nT244 -> T245", fontsize=14, style = filled, fillcolor = lightblue];
330 -> 800 [arrowhead = none ];
800 -> 353;

801 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
336 -> 801 [arrowhead = none ];
801 -> 338;

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

803 [label="ONLY EVAL with clause\nno(X229) :- ','(call(X229), ','(!_24, failure(a))).\nand substitutionT240 -> T256,\nX229 -> empty(T256)", fontsize=14, style = filled, fillcolor = lightblue];
356 -> 803 [arrowhead = none ];
803 -> 357;

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

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

806 [label="EVAL with clause\nempty([]).\nand substitutionT256 -> []", fontsize=14, style = filled, fillcolor = lightblue];
361 -> 806 [arrowhead = none ];
806 -> 362;

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

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

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

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

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

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

813 [label="ONLY EVAL with clause\nno(X240).\nand substitutionT256 -> T275,\nX240 -> empty(T275)", fontsize=14, style = filled, fillcolor = lightblue];
377 -> 813 [arrowhead = none ];
813 -> 379;

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

815 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T275), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
380 -> 815 [arrowhead = none ];
815 -> 381;

816 [label="EVAL with clause\nhead(.(X251, X252), X251).\nand substitutionX251 -> T288,\nX252 -> T289,\nT275 -> .(T288, T289),\nX221 -> T288", fontsize=14, style = filled, fillcolor = lightblue];
381 -> 816 [arrowhead = none ];
816 -> 401;

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

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

819 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
408 -> 819 [arrowhead = none ];
819 -> 409;

820 [label="ONLY EVAL with clause\ntail(.(X261, X262), X262).\nand substitutionT288 -> T310,\nX261 -> T310,\nT289 -> T311,\nX262 -> T311,\nX222 -> T311", fontsize=14, style = filled, fillcolor = lightblue];
409 -> 820 [arrowhead = none ];
820 -> 412;

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

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

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

824 [label="EVAL with clause\nrev([], X269, X269).\nand substitutionT311 -> [],\nT310 -> T336,\nT241 -> T337,\nT242 -> T338,\nT243 -> T339,\nX269 -> .(T336, .(T337, .(T338, .(T339, [])))),\nT245 -> .(T336, .(T337, .(T338, .(T339, []))))", fontsize=14, style = filled, fillcolor = lightblue];
426 -> 824 [arrowhead = none ];
824 -> 430;

825 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
426 -> 825 [arrowhead = none ];
825 -> 431;

826 [label="ONLY EVAL with clause\nrev(X282, X283, X284) :- ','(no(empty(X282)), ','(head(X282, X285), ','(tail(X282, X286), rev(X286, .(X285, X283), X284)))).\nand substitutionT311 -> T363,\nX282 -> T363,\nT310 -> T364,\nT241 -> T365,\nT242 -> T366,\nT243 -> T367,\nX283 -> .(T364, .(T365, .(T366, .(T367, [])))),\nT245 -> T369,\nX284 -> T369,\nT368 -> T369", fontsize=14, style = filled, fillcolor = lightblue];
427 -> 826 [arrowhead = none ];
826 -> 444;

827 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
430 -> 827 [arrowhead = none ];
827 -> 432;

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

829 [label="ONLY EVAL with clause\nno(X293) :- ','(call(X293), ','(!_31, failure(a))).\nand substitutionT363 -> T382,\nX293 -> empty(T382)", fontsize=14, style = filled, fillcolor = lightblue];
445 -> 829 [arrowhead = none ];
829 -> 446;

830 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
446 -> 830 [arrowhead = none ];
830 -> 447;

831 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
447 -> 831 [arrowhead = none ];
831 -> 448;

832 [label="EVAL with clause\nempty([]).\nand substitutionT382 -> []", fontsize=14, style = filled, fillcolor = lightblue];
448 -> 832 [arrowhead = none ];
832 -> 449;

833 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
448 -> 833 [arrowhead = none ];
833 -> 450;

834 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
449 -> 834 [arrowhead = none ];
834 -> 451;

835 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
450 -> 835 [arrowhead = none ];
835 -> 455;

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

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

838 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
455 -> 838 [arrowhead = none ];
838 -> 456;

839 [label="ONLY EVAL with clause\nno(X304).\nand substitutionT382 -> T405,\nX304 -> empty(T405)", fontsize=14, style = filled, fillcolor = lightblue];
456 -> 839 [arrowhead = none ];
839 -> 474;

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

841 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T405), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
477 -> 841 [arrowhead = none ];
841 -> 478;

842 [label="EVAL with clause\nhead(.(X315, X316), X315).\nand substitutionX315 -> T420,\nX316 -> T421,\nT405 -> .(T420, T421),\nX285 -> T420", fontsize=14, style = filled, fillcolor = lightblue];
478 -> 842 [arrowhead = none ];
842 -> 482;

843 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
478 -> 843 [arrowhead = none ];
843 -> 484;

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

845 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
486 -> 845 [arrowhead = none ];
845 -> 487;

846 [label="ONLY EVAL with clause\ntail(.(X325, X326), X326).\nand substitutionT420 -> T446,\nX325 -> T446,\nT421 -> T447,\nX326 -> T447,\nX286 -> T447", fontsize=14, style = filled, fillcolor = lightblue];
487 -> 846 [arrowhead = none ];
846 -> 491;

847 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
491 -> 847 [arrowhead = none ];
847 -> 494;

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

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

850 [label="EVAL with clause\nrev([], X333, X333).\nand substitutionT447 -> [],\nT446 -> T478,\nT364 -> T479,\nT365 -> T480,\nT366 -> T481,\nT367 -> T482,\nX333 -> .(T478, .(T479, .(T480, .(T481, .(T482, []))))),\nT369 -> .(T478, .(T479, .(T480, .(T481, .(T482, [])))))", fontsize=14, style = filled, fillcolor = lightblue];
499 -> 850 [arrowhead = none ];
850 -> 503;

851 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
499 -> 851 [arrowhead = none ];
851 -> 504;

852 [label="ONLY EVAL with clause\nrev(X346, X347, X348) :- ','(no(empty(X346)), ','(head(X346, X349), ','(tail(X346, X350), rev(X350, .(X349, X347), X348)))).\nand substitutionT447 -> T510,\nX346 -> T510,\nT446 -> T511,\nT364 -> T512,\nT365 -> T513,\nT366 -> T514,\nT367 -> T515,\nX347 -> .(T511, .(T512, .(T513, .(T514, .(T515, []))))),\nT369 -> T517,\nX348 -> T517,\nT516 -> T517", fontsize=14, style = filled, fillcolor = lightblue];
500 -> 852 [arrowhead = none ];
852 -> 509;

853 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
503 -> 853 [arrowhead = none ];
853 -> 505;

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

855 [label="ONLY EVAL with clause\nno(X357) :- ','(call(X357), ','(!_38, failure(a))).\nand substitutionT510 -> T532,\nX357 -> empty(T532)", fontsize=14, style = filled, fillcolor = lightblue];
512 -> 855 [arrowhead = none ];
855 -> 515;

856 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
515 -> 856 [arrowhead = none ];
856 -> 516;

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

858 [label="EVAL with clause\nempty([]).\nand substitutionT532 -> []", fontsize=14, style = filled, fillcolor = lightblue];
517 -> 858 [arrowhead = none ];
858 -> 518;

859 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
517 -> 859 [arrowhead = none ];
859 -> 519;

860 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
518 -> 860 [arrowhead = none ];
860 -> 520;

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

862 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
520 -> 862 [arrowhead = none ];
862 -> 527;

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

864 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
529 -> 864 [arrowhead = none ];
864 -> 530;

865 [label="ONLY EVAL with clause\nno(X368).\nand substitutionT532 -> T559,\nX368 -> empty(T559)", fontsize=14, style = filled, fillcolor = lightblue];
530 -> 865 [arrowhead = none ];
865 -> 531;

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

867 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T559), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
535 -> 867 [arrowhead = none ];
867 -> 536;

868 [label="EVAL with clause\nhead(.(X379, X380), X379).\nand substitutionX379 -> T576,\nX380 -> T577,\nT559 -> .(T576, T577),\nX349 -> T576", fontsize=14, style = filled, fillcolor = lightblue];
536 -> 868 [arrowhead = none ];
868 -> 537;

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

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

871 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
539 -> 871 [arrowhead = none ];
871 -> 540;

872 [label="ONLY EVAL with clause\ntail(.(X389, X390), X390).\nand substitutionT576 -> T606,\nX389 -> T606,\nT577 -> T607,\nX390 -> T607,\nX350 -> T607", fontsize=14, style = filled, fillcolor = lightblue];
540 -> 872 [arrowhead = none ];
872 -> 542;

873 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
542 -> 873 [arrowhead = none ];
873 -> 546;

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

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

876 [label="EVAL with clause\nrev([], X397, X397).\nand substitutionT607 -> [],\nT606 -> T644,\nT511 -> T645,\nT512 -> T646,\nT513 -> T647,\nT514 -> T648,\nT515 -> T649,\nX397 -> .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, [])))))),\nT517 -> .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, []))))))", fontsize=14, style = filled, fillcolor = lightblue];
552 -> 876 [arrowhead = none ];
876 -> 559;

877 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
552 -> 877 [arrowhead = none ];
877 -> 560;

878 [label="ONLY EVAL with clause\nrev(X410, X411, X412) :- ','(no(empty(X410)), ','(head(X410, X413), ','(tail(X410, X414), rev(X414, .(X413, X411), X412)))).\nand substitutionT607 -> T681,\nX410 -> T681,\nT606 -> T682,\nT511 -> T683,\nT512 -> T684,\nT513 -> T685,\nT514 -> T686,\nT515 -> T687,\nX411 -> .(T682, .(T683, .(T684, .(T685, .(T686, .(T687, [])))))),\nT517 -> T689,\nX412 -> T689,\nT688 -> T689", fontsize=14, style = filled, fillcolor = lightblue];
553 -> 878 [arrowhead = none ];
878 -> 573;

879 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
559 -> 879 [arrowhead = none ];
879 -> 562;

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

881 [label="ONLY EVAL with clause\nno(X421) :- ','(call(X421), ','(!_45, failure(a))).\nand substitutionT681 -> T706,\nX421 -> empty(T706)", fontsize=14, style = filled, fillcolor = lightblue];
579 -> 881 [arrowhead = none ];
881 -> 580;

882 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
580 -> 882 [arrowhead = none ];
882 -> 581;

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

884 [label="EVAL with clause\nempty([]).\nand substitutionT706 -> []", fontsize=14, style = filled, fillcolor = lightblue];
582 -> 884 [arrowhead = none ];
884 -> 583;

885 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
582 -> 885 [arrowhead = none ];
885 -> 584;

886 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
583 -> 886 [arrowhead = none ];
886 -> 585;

887 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
584 -> 887 [arrowhead = none ];
887 -> 592;

888 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
585 -> 888 [arrowhead = none ];
888 -> 590;

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

890 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
592 -> 890 [arrowhead = none ];
890 -> 593;

891 [label="ONLY EVAL with clause\nno(X432).\nand substitutionT706 -> T737,\nX432 -> empty(T737)", fontsize=14, style = filled, fillcolor = lightblue];
593 -> 891 [arrowhead = none ];
891 -> 596;

892 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
596 -> 892 [arrowhead = none ];
892 -> 600;

893 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T737), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
600 -> 893 [arrowhead = none ];
893 -> 601;

894 [label="EVAL with clause\nhead(.(X443, X444), X443).\nand substitutionX443 -> T756,\nX444 -> T757,\nT737 -> .(T756, T757),\nX413 -> T756", fontsize=14, style = filled, fillcolor = lightblue];
601 -> 894 [arrowhead = none ];
894 -> 602;

895 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
601 -> 895 [arrowhead = none ];
895 -> 603;

896 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
602 -> 896 [arrowhead = none ];
896 -> 605;

897 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
605 -> 897 [arrowhead = none ];
897 -> 606;

898 [label="ONLY EVAL with clause\ntail(.(X453, X454), X454).\nand substitutionT756 -> T790,\nX453 -> T790,\nT757 -> T791,\nX454 -> T791,\nX414 -> T791", fontsize=14, style = filled, fillcolor = lightblue];
606 -> 898 [arrowhead = none ];
898 -> 615;

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

900 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
620 -> 900 [arrowhead = none ];
900 -> 646;

901 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
620 -> 901 [arrowhead = none ];
901 -> 647;

902 [label="EVAL with clause\nrev([], X461, X461).\nand substitutionT791 -> [],\nT790 -> T834,\nT682 -> T835,\nT683 -> T836,\nT684 -> T837,\nT685 -> T838,\nT686 -> T839,\nT687 -> T840,\nX461 -> .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, []))))))),\nT689 -> .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, [])))))))", fontsize=14, style = filled, fillcolor = lightblue];
646 -> 902 [arrowhead = none ];
902 -> 657;

903 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
646 -> 903 [arrowhead = none ];
903 -> 658;

904 [label="ONLY EVAL with clause\nrev(X474, X475, X476) :- ','(no(empty(X474)), ','(head(X474, X477), ','(tail(X474, X478), rev(X478, .(X477, X475), X476)))).\nand substitutionT791 -> T876,\nX474 -> T876,\nT790 -> T877,\nT682 -> T878,\nT683 -> T879,\nT684 -> T880,\nT685 -> T881,\nT686 -> T882,\nT687 -> T883,\nX475 -> .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))),\nT689 -> T885,\nX476 -> T885,\nT884 -> T885", fontsize=14, style = filled, fillcolor = lightblue];
647 -> 904 [arrowhead = none ];
904 -> 668;

905 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
657 -> 905 [arrowhead = none ];
905 -> 659;

906 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
668 -> 906 [arrowhead = none ];
906 -> 669;

907 [label="ONLY EVAL with clause\nno(X485) :- ','(call(X485), ','(!_52, failure(a))).\nand substitutionT876 -> T904,\nX485 -> empty(T904)", fontsize=14, style = filled, fillcolor = lightblue];
669 -> 907 [arrowhead = none ];
907 -> 670;

908 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
670 -> 908 [arrowhead = none ];
908 -> 671;

909 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
671 -> 909 [arrowhead = none ];
909 -> 672;

910 [label="EVAL with clause\nempty([]).\nand substitutionT904 -> []", fontsize=14, style = filled, fillcolor = lightblue];
672 -> 910 [arrowhead = none ];
910 -> 673;

911 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
672 -> 911 [arrowhead = none ];
911 -> 674;

912 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
673 -> 912 [arrowhead = none ];
912 -> 675;

913 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
674 -> 913 [arrowhead = none ];
913 -> 678;

914 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
675 -> 914 [arrowhead = none ];
914 -> 676;

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

916 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
678 -> 916 [arrowhead = none ];
916 -> 679;

917 [label="ONLY EVAL with clause\nno(X496).\nand substitutionT904 -> T939,\nX496 -> empty(T939)", fontsize=14, style = filled, fillcolor = lightblue];
679 -> 917 [arrowhead = none ];
917 -> 680;

918 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
680 -> 918 [arrowhead = none ];
918 -> 681;

919 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T939), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
681 -> 919 [arrowhead = none ];
919 -> 682;

920 [label="EVAL with clause\nhead(.(X507, X508), X507).\nand substitutionX507 -> T960,\nX508 -> T961,\nT939 -> .(T960, T961),\nX477 -> T960", fontsize=14, style = filled, fillcolor = lightblue];
682 -> 920 [arrowhead = none ];
920 -> 683;

921 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
682 -> 921 [arrowhead = none ];
921 -> 684;

922 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
683 -> 922 [arrowhead = none ];
922 -> 685;

923 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
685 -> 923 [arrowhead = none ];
923 -> 686;

924 [label="ONLY EVAL with clause\ntail(.(X517, X518), X518).\nand substitutionT960 -> T998,\nX517 -> T998,\nT961 -> T999,\nX518 -> T999,\nX478 -> T999", fontsize=14, style = filled, fillcolor = lightblue];
686 -> 924 [arrowhead = none ];
924 -> 687;

925 [label="GENERALIZATION\nT1016 <-- .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, [])))))))\n\nNew Knowledge:\nT1016 is ground", fontsize=14, style = filled, fillcolor = violet];
687 -> 925 [arrowhead = none ];
925 -> 688;

926 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
688 -> 926 [arrowhead = none ];
926 -> 689;

927 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
689 -> 927 [arrowhead = none ];
927 -> 690;

928 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
689 -> 928 [arrowhead = none ];
928 -> 691;

929 [label="EVAL with clause\nrev([], X527, X527).\nand substitutionT999 -> [],\nT998 -> T1029,\nT1016 -> T1030,\nX527 -> .(T1029, T1030),\nT885 -> .(T1029, T1030)", fontsize=14, style = filled, fillcolor = lightblue];
690 -> 929 [arrowhead = none ];
929 -> 692;

930 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
690 -> 930 [arrowhead = none ];
930 -> 693;

931 [label="ONLY EVAL with clause\nrev(X540, X541, X542) :- ','(no(empty(X540)), ','(head(X540, X543), ','(tail(X540, X544), rev(X544, .(X543, X541), X542)))).\nand substitutionT999 -> T1046,\nX540 -> T1046,\nT998 -> T1047,\nT1016 -> T1048,\nX541 -> .(T1047, T1048),\nT885 -> T1050,\nX542 -> T1050,\nT1049 -> T1050", fontsize=14, style = filled, fillcolor = lightblue];
691 -> 931 [arrowhead = none ];
931 -> 695;

932 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
692 -> 932 [arrowhead = none ];
932 -> 694;

933 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
695 -> 933 [arrowhead = none ];
933 -> 696;

934 [label="ONLY EVAL with clause\nno(X551) :- ','(call(X551), ','(!_59, failure(a))).\nand substitutionT1046 -> T1059,\nX551 -> empty(T1059)", fontsize=14, style = filled, fillcolor = lightblue];
696 -> 934 [arrowhead = none ];
934 -> 697;

935 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
697 -> 935 [arrowhead = none ];
935 -> 698;

936 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
698 -> 936 [arrowhead = none ];
936 -> 699;

937 [label="EVAL with clause\nempty([]).\nand substitutionT1059 -> []", fontsize=14, style = filled, fillcolor = lightblue];
699 -> 937 [arrowhead = none ];
937 -> 700;

938 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
699 -> 938 [arrowhead = none ];
938 -> 701;

939 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
700 -> 939 [arrowhead = none ];
939 -> 702;

940 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
701 -> 940 [arrowhead = none ];
940 -> 705;

941 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
702 -> 941 [arrowhead = none ];
941 -> 703;

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

943 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
705 -> 943 [arrowhead = none ];
943 -> 706;

944 [label="ONLY EVAL with clause\nno(X562).\nand substitutionT1059 -> T1074,\nX562 -> empty(T1074)", fontsize=14, style = filled, fillcolor = lightblue];
706 -> 944 [arrowhead = none ];
944 -> 707;

945 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
707 -> 945 [arrowhead = none ];
945 -> 708;

946 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T1074), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
708 -> 946 [arrowhead = none ];
946 -> 709;

947 [label="EVAL with clause\nhead(.(X573, X574), X573).\nand substitutionX573 -> T1085,\nX574 -> T1086,\nT1074 -> .(T1085, T1086),\nX543 -> T1085", fontsize=14, style = filled, fillcolor = lightblue];
709 -> 947 [arrowhead = none ];
947 -> 710;

948 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
709 -> 948 [arrowhead = none ];
948 -> 711;

949 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
710 -> 949 [arrowhead = none ];
949 -> 712;

950 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
712 -> 950 [arrowhead = none ];
950 -> 713;

951 [label="ONLY EVAL with clause\ntail(.(X583, X584), X584).\nand substitutionT1085 -> T1103,\nX583 -> T1103,\nT1086 -> T1104,\nX584 -> T1104,\nX544 -> T1104", fontsize=14, style = filled, fillcolor = lightblue];
713 -> 951 [arrowhead = none ];
951 -> 714;

952 [label="INSTANCE with matching:\nT999 -> T1104\nT998 -> T1103\nT1016 -> .(T1047, T1048)\nT885 -> T1050", fontsize=14, style = filled, fillcolor = lightgrey];
714 -> 952 [arrowhead = none , style=dashed];
952 -> 688[style=dashed];

}

(2) Obligation:

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

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T54, []), .(T54, [])) → revA_out_ga(.(T54, []), .(T54, []))
revA_in_ga(.(T125, .(T124, [])), .(T124, .(T125, []))) → revA_out_ga(.(T125, .(T124, [])), .(T124, .(T125, [])))
revA_in_ga(.(T220, .(T219, .(T218, []))), .(T218, .(T219, .(T220, [])))) → revA_out_ga(.(T220, .(T219, .(T218, []))), .(T218, .(T219, .(T220, []))))
revA_in_ga(.(T339, .(T338, .(T337, .(T336, [])))), .(T336, .(T337, .(T338, .(T339, []))))) → revA_out_ga(.(T339, .(T338, .(T337, .(T336, [])))), .(T336, .(T337, .(T338, .(T339, [])))))
revA_in_ga(.(T482, .(T481, .(T480, .(T479, .(T478, []))))), .(T478, .(T479, .(T480, .(T481, .(T482, [])))))) → revA_out_ga(.(T482, .(T481, .(T480, .(T479, .(T478, []))))), .(T478, .(T479, .(T480, .(T481, .(T482, []))))))
revA_in_ga(.(T649, .(T648, .(T647, .(T646, .(T645, .(T644, [])))))), .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, []))))))) → revA_out_ga(.(T649, .(T648, .(T647, .(T646, .(T645, .(T644, [])))))), .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, [])))))))
revA_in_ga(.(T840, .(T839, .(T838, .(T837, .(T836, .(T835, .(T834, []))))))), .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, [])))))))) → revA_out_ga(.(T840, .(T839, .(T838, .(T837, .(T836, .(T835, .(T834, []))))))), .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, []))))))))
revA_in_ga(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885) → U1_ga(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_in_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885))
revB_in_ggga([], T1029, T1030, .(T1029, T1030)) → revB_out_ggga([], T1029, T1030, .(T1029, T1030))
revB_in_ggga(.(T1103, T1104), T1047, T1048, T1050) → U2_ggga(T1103, T1104, T1047, T1048, T1050, revB_in_ggga(T1104, T1103, .(T1047, T1048), T1050))
U2_ggga(T1103, T1104, T1047, T1048, T1050, revB_out_ggga(T1104, T1103, .(T1047, T1048), T1050)) → revB_out_ggga(.(T1103, T1104), T1047, T1048, T1050)
U1_ga(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_out_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885)) → revA_out_ga(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885)

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

REVA_IN_GA(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885) → U1_GA(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_in_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885))
REVA_IN_GA(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885) → REVB_IN_GGGA(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885)
REVB_IN_GGGA(.(T1103, T1104), T1047, T1048, T1050) → U2_GGGA(T1103, T1104, T1047, T1048, T1050, revB_in_ggga(T1104, T1103, .(T1047, T1048), T1050))
REVB_IN_GGGA(.(T1103, T1104), T1047, T1048, T1050) → REVB_IN_GGGA(T1104, T1103, .(T1047, T1048), T1050)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T54, []), .(T54, [])) → revA_out_ga(.(T54, []), .(T54, []))
revA_in_ga(.(T125, .(T124, [])), .(T124, .(T125, []))) → revA_out_ga(.(T125, .(T124, [])), .(T124, .(T125, [])))
revA_in_ga(.(T220, .(T219, .(T218, []))), .(T218, .(T219, .(T220, [])))) → revA_out_ga(.(T220, .(T219, .(T218, []))), .(T218, .(T219, .(T220, []))))
revA_in_ga(.(T339, .(T338, .(T337, .(T336, [])))), .(T336, .(T337, .(T338, .(T339, []))))) → revA_out_ga(.(T339, .(T338, .(T337, .(T336, [])))), .(T336, .(T337, .(T338, .(T339, [])))))
revA_in_ga(.(T482, .(T481, .(T480, .(T479, .(T478, []))))), .(T478, .(T479, .(T480, .(T481, .(T482, [])))))) → revA_out_ga(.(T482, .(T481, .(T480, .(T479, .(T478, []))))), .(T478, .(T479, .(T480, .(T481, .(T482, []))))))
revA_in_ga(.(T649, .(T648, .(T647, .(T646, .(T645, .(T644, [])))))), .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, []))))))) → revA_out_ga(.(T649, .(T648, .(T647, .(T646, .(T645, .(T644, [])))))), .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, [])))))))
revA_in_ga(.(T840, .(T839, .(T838, .(T837, .(T836, .(T835, .(T834, []))))))), .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, [])))))))) → revA_out_ga(.(T840, .(T839, .(T838, .(T837, .(T836, .(T835, .(T834, []))))))), .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, []))))))))
revA_in_ga(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885) → U1_ga(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_in_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885))
revB_in_ggga([], T1029, T1030, .(T1029, T1030)) → revB_out_ggga([], T1029, T1030, .(T1029, T1030))
revB_in_ggga(.(T1103, T1104), T1047, T1048, T1050) → U2_ggga(T1103, T1104, T1047, T1048, T1050, revB_in_ggga(T1104, T1103, .(T1047, T1048), T1050))
U2_ggga(T1103, T1104, T1047, T1048, T1050, revB_out_ggga(T1104, T1103, .(T1047, T1048), T1050)) → revB_out_ggga(.(T1103, T1104), T1047, T1048, T1050)
U1_ga(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_out_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885)) → revA_out_ga(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2) = revA_in_ga(x1)
[] = []
revA_out_ga(x1, x2) = revA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = U1_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11)
revB_in_ggga(x1, x2, x3, x4) = revB_in_ggga(x1, x2, x3)
revB_out_ggga(x1, x2, x3, x4) = revB_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x2, x3, x4, x6)
REVA_IN_GA(x1, x2) = REVA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = U1_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11)
REVB_IN_GGGA(x1, x2, x3, x4) = REVB_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5, x6) = U2_GGGA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

REVA_IN_GA(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885) → U1_GA(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_in_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885))
REVA_IN_GA(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885) → REVB_IN_GGGA(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885)
REVB_IN_GGGA(.(T1103, T1104), T1047, T1048, T1050) → U2_GGGA(T1103, T1104, T1047, T1048, T1050, revB_in_ggga(T1104, T1103, .(T1047, T1048), T1050))
REVB_IN_GGGA(.(T1103, T1104), T1047, T1048, T1050) → REVB_IN_GGGA(T1104, T1103, .(T1047, T1048), T1050)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T54, []), .(T54, [])) → revA_out_ga(.(T54, []), .(T54, []))
revA_in_ga(.(T125, .(T124, [])), .(T124, .(T125, []))) → revA_out_ga(.(T125, .(T124, [])), .(T124, .(T125, [])))
revA_in_ga(.(T220, .(T219, .(T218, []))), .(T218, .(T219, .(T220, [])))) → revA_out_ga(.(T220, .(T219, .(T218, []))), .(T218, .(T219, .(T220, []))))
revA_in_ga(.(T339, .(T338, .(T337, .(T336, [])))), .(T336, .(T337, .(T338, .(T339, []))))) → revA_out_ga(.(T339, .(T338, .(T337, .(T336, [])))), .(T336, .(T337, .(T338, .(T339, [])))))
revA_in_ga(.(T482, .(T481, .(T480, .(T479, .(T478, []))))), .(T478, .(T479, .(T480, .(T481, .(T482, [])))))) → revA_out_ga(.(T482, .(T481, .(T480, .(T479, .(T478, []))))), .(T478, .(T479, .(T480, .(T481, .(T482, []))))))
revA_in_ga(.(T649, .(T648, .(T647, .(T646, .(T645, .(T644, [])))))), .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, []))))))) → revA_out_ga(.(T649, .(T648, .(T647, .(T646, .(T645, .(T644, [])))))), .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, [])))))))
revA_in_ga(.(T840, .(T839, .(T838, .(T837, .(T836, .(T835, .(T834, []))))))), .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, [])))))))) → revA_out_ga(.(T840, .(T839, .(T838, .(T837, .(T836, .(T835, .(T834, []))))))), .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, []))))))))
revA_in_ga(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885) → U1_ga(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_in_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885))
revB_in_ggga([], T1029, T1030, .(T1029, T1030)) → revB_out_ggga([], T1029, T1030, .(T1029, T1030))
revB_in_ggga(.(T1103, T1104), T1047, T1048, T1050) → U2_ggga(T1103, T1104, T1047, T1048, T1050, revB_in_ggga(T1104, T1103, .(T1047, T1048), T1050))
U2_ggga(T1103, T1104, T1047, T1048, T1050, revB_out_ggga(T1104, T1103, .(T1047, T1048), T1050)) → revB_out_ggga(.(T1103, T1104), T1047, T1048, T1050)
U1_ga(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_out_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885)) → revA_out_ga(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

REVB_IN_GGGA(.(T1103, T1104), T1047, T1048, T1050) → REVB_IN_GGGA(T1104, T1103, .(T1047, T1048), T1050)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T54, []), .(T54, [])) → revA_out_ga(.(T54, []), .(T54, []))
revA_in_ga(.(T125, .(T124, [])), .(T124, .(T125, []))) → revA_out_ga(.(T125, .(T124, [])), .(T124, .(T125, [])))
revA_in_ga(.(T220, .(T219, .(T218, []))), .(T218, .(T219, .(T220, [])))) → revA_out_ga(.(T220, .(T219, .(T218, []))), .(T218, .(T219, .(T220, []))))
revA_in_ga(.(T339, .(T338, .(T337, .(T336, [])))), .(T336, .(T337, .(T338, .(T339, []))))) → revA_out_ga(.(T339, .(T338, .(T337, .(T336, [])))), .(T336, .(T337, .(T338, .(T339, [])))))
revA_in_ga(.(T482, .(T481, .(T480, .(T479, .(T478, []))))), .(T478, .(T479, .(T480, .(T481, .(T482, [])))))) → revA_out_ga(.(T482, .(T481, .(T480, .(T479, .(T478, []))))), .(T478, .(T479, .(T480, .(T481, .(T482, []))))))
revA_in_ga(.(T649, .(T648, .(T647, .(T646, .(T645, .(T644, [])))))), .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, []))))))) → revA_out_ga(.(T649, .(T648, .(T647, .(T646, .(T645, .(T644, [])))))), .(T644, .(T645, .(T646, .(T647, .(T648, .(T649, [])))))))
revA_in_ga(.(T840, .(T839, .(T838, .(T837, .(T836, .(T835, .(T834, []))))))), .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, [])))))))) → revA_out_ga(.(T840, .(T839, .(T838, .(T837, .(T836, .(T835, .(T834, []))))))), .(T834, .(T835, .(T836, .(T837, .(T838, .(T839, .(T840, []))))))))
revA_in_ga(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885) → U1_ga(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_in_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885))
revB_in_ggga([], T1029, T1030, .(T1029, T1030)) → revB_out_ggga([], T1029, T1030, .(T1029, T1030))
revB_in_ggga(.(T1103, T1104), T1047, T1048, T1050) → U2_ggga(T1103, T1104, T1047, T1048, T1050, revB_in_ggga(T1104, T1103, .(T1047, T1048), T1050))
U2_ggga(T1103, T1104, T1047, T1048, T1050, revB_out_ggga(T1104, T1103, .(T1047, T1048), T1050)) → revB_out_ggga(.(T1103, T1104), T1047, T1048, T1050)
U1_ga(T883, T882, T881, T880, T879, T878, T877, T998, T999, T885, revB_out_ggga(T999, T998, .(T877, .(T878, .(T879, .(T880, .(T881, .(T882, .(T883, []))))))), T885)) → revA_out_ga(.(T883, .(T882, .(T881, .(T880, .(T879, .(T878, .(T877, .(T998, T999)))))))), T885)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2) = revA_in_ga(x1)
[] = []
revA_out_ga(x1, x2) = revA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) = U1_ga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x11)
revB_in_ggga(x1, x2, x3, x4) = revB_in_ggga(x1, x2, x3)
revB_out_ggga(x1, x2, x3, x4) = revB_out_ggga(x1, x2, x3, x4)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x2, x3, x4, x6)
REVB_IN_GGGA(x1, x2, x3, x4) = REVB_IN_GGGA(x1, x2, x3)

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

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

REVB_IN_GGGA(.(T1103, T1104), T1047, T1048, T1050) → REVB_IN_GGGA(T1104, T1103, .(T1047, T1048), T1050)

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

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

(9) PiDPToQDPProof (SOUND transformation)

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

(10) Obligation:

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

REVB_IN_GGGA(.(T1103, T1104), T1047, T1048) → REVB_IN_GGGA(T1104, T1103, .(T1047, T1048))

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

(11) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

REVB_IN_GGGA(.(T1103, T1104), T1047, T1048) → REVB_IN_GGGA(T1104, T1103, .(T1047, T1048))
The graph contains the following edges 1 > 1, 1 > 2

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Obligation:

(7) UsableRulesProof (EQUIVALENT transformation)

(8) Obligation:

(9) PiDPToQDPProof (SOUND transformation)

(10) Obligation:

(11) QDPSizeChangeProof (EQUIVALENT transformation)

(12) YES