Runtime Complexity of the query pattern
rev(g,a)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Clauses:

rev(L, R) :- rev(L, [], R).
rev([], Y, Z) :- ','(!, eq(Y, Z)).
rev(L, S, R) :- ','(head(L, X), ','(tail(L, T), rev(T, .(X, S), R))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, Xs), Xs).
eq(X, X).

Query: rev(g,a)

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: rev(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: rev(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: rev(T9, [], T11)\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: rev(T9, [], T11), SCOPE: 2, CLAUSE: 1 | rev(T9, [], T11), SCOPE: 2, CLAUSE: 2\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(!_2, eq([], T16)) | rev([], [], T11), SCOPE: 2, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: rev(T9, [], T11), SCOPE: 2, CLAUSE: 2\n\nT9 is ground\nX18 is free\nX19 is free\nrev(T9, [], T11) !=? rev([], X18, X19)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: eq([], T16)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: eq([], T16), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(head(T23, X37), ','(tail(T23, X38), rev(X38, .(X37, []), T25)))\n\nT23 is ground\nX18 is free\nX19 is free\nX37 is free\nX38 is free\nrev(T23, [], T11) !=? rev([], X18, X19)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(head(T23, X37), ','(tail(T23, X38), rev(X38, .(X37, []), T25))), SCOPE: 4, CLAUSE: 3 | ','(head(T23, X37), ','(tail(T23, X38), rev(X38, .(X37, []), T25))), SCOPE: 4, CLAUSE: 4\n\nT23 is ground\nX18 is free\nX19 is free\nX37 is free\nX38 is free\nrev(T23, [], T11) !=? rev([], X18, X19)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(head(T23, X37), ','(tail(T23, X38), rev(X38, .(X37, []), T25))), SCOPE: 4, CLAUSE: 4\n\nT23 is ground\nX18 is free\nX19 is free\nX37 is free\nX38 is free\nrev(T23, [], T11) !=? rev([], X18, X19)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(tail(.(T31, T32), X38), rev(X38, .(T31, []), T25))\n\nT31 is ground\nT32 is ground\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(tail(.(T31, T32), X38), rev(X38, .(T31, []), T25)), SCOPE: 5, CLAUSE: 5 | ','(tail(.(T31, T32), X38), rev(X38, .(T31, []), T25)), SCOPE: 5, CLAUSE: 6\n\nT31 is ground\nT32 is ground\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(tail(.(T31, T32), X38), rev(X38, .(T31, []), T25)), SCOPE: 5, CLAUSE: 6\n\nT31 is ground\nT32 is ground\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: rev(T42, .(T41, []), T25)\n\nT41 is ground\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: rev(T42, .(T41, []), T25), SCOPE: 6, CLAUSE: 1 | rev(T42, .(T41, []), T25), SCOPE: 6, CLAUSE: 2\n\nT41 is ground\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(!_6, eq(.(T49, []), T51)) | rev([], .(T49, []), T25), SCOPE: 6, CLAUSE: 2\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: rev(T42, .(T41, []), T25), SCOPE: 6, CLAUSE: 2\n\nT41 is ground\nT42 is ground\nX66 is free\nX67 is free\nrev(T42, .(T41, []), T25) !=? rev([], X66, X67)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: eq(.(T49, []), T51)\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: eq(.(T49, []), T51), SCOPE: 7, CLAUSE: 7\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(head(T64, X85), ','(tail(T64, X86), rev(X86, .(X85, .(T65, [])), T67)))\n\nT64 is ground\nT65 is ground\nX66 is free\nX67 is free\nX85 is free\nX86 is free\nrev(T64, .(T65, []), T25) !=? rev([], X66, X67)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(head(T64, X85), ','(tail(T64, X86), rev(X86, .(X85, .(T65, [])), T67))), SCOPE: 8, CLAUSE: 3 | ','(head(T64, X85), ','(tail(T64, X86), rev(X86, .(X85, .(T65, [])), T67))), SCOPE: 8, CLAUSE: 4\n\nT64 is ground\nT65 is ground\nX66 is free\nX67 is free\nX85 is free\nX86 is free\nrev(T64, .(T65, []), T25) !=? rev([], X66, X67)", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(head(T64, X85), ','(tail(T64, X86), rev(X86, .(X85, .(T65, [])), T67))), SCOPE: 8, CLAUSE: 4\n\nT64 is ground\nT65 is ground\nX66 is free\nX67 is free\nX85 is free\nX86 is free\nrev(T64, .(T65, []), T25) !=? rev([], X66, X67)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(tail(.(T74, T75), X86), rev(X86, .(T74, .(T65, [])), T67))\n\nT65 is ground\nT74 is ground\nT75 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(tail(.(T74, T75), X86), rev(X86, .(T74, .(T65, [])), T67)), SCOPE: 9, CLAUSE: 5 | ','(tail(.(T74, T75), X86), rev(X86, .(T74, .(T65, [])), T67)), SCOPE: 9, CLAUSE: 6\n\nT65 is ground\nT74 is ground\nT75 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(tail(.(T74, T75), X86), rev(X86, .(T74, .(T65, [])), T67)), SCOPE: 9, CLAUSE: 6\n\nT65 is ground\nT74 is ground\nT75 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: rev(T87, .(T86, .(T65, [])), T67)\n\nT65 is ground\nT86 is ground\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: rev(T87, .(T86, .(T65, [])), T67), SCOPE: 10, CLAUSE: 1 | rev(T87, .(T86, .(T65, [])), T67), SCOPE: 10, CLAUSE: 2\n\nT65 is ground\nT86 is ground\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(!_10, eq(.(T97, .(T98, [])), T100)) | rev([], .(T97, .(T98, [])), T67), SCOPE: 10, CLAUSE: 2\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: rev(T87, .(T86, .(T65, [])), T67), SCOPE: 10, CLAUSE: 2\n\nT65 is ground\nT86 is ground\nT87 is ground\nX114 is free\nX115 is free\nrev(T87, .(T86, .(T65, [])), T67) !=? rev([], X114, X115)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: eq(.(T97, .(T98, [])), T100)\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: eq(.(T97, .(T98, [])), T100), SCOPE: 11, CLAUSE: 7\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(head(T119, X133), ','(tail(T119, X134), rev(X134, .(X133, .(T120, .(T121, []))), T123)))\n\nT119 is ground\nT120 is ground\nT121 is ground\nX114 is free\nX115 is free\nX133 is free\nX134 is free\nrev(T119, .(T120, .(T121, [])), T67) !=? rev([], X114, X115)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(head(T119, X133), ','(tail(T119, X134), rev(X134, .(X133, .(T120, .(T121, []))), T123))), SCOPE: 12, CLAUSE: 3 | ','(head(T119, X133), ','(tail(T119, X134), rev(X134, .(X133, .(T120, .(T121, []))), T123))), SCOPE: 12, CLAUSE: 4\n\nT119 is ground\nT120 is ground\nT121 is ground\nX114 is free\nX115 is free\nX133 is free\nX134 is free\nrev(T119, .(T120, .(T121, [])), T67) !=? rev([], X114, X115)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(head(T119, X133), ','(tail(T119, X134), rev(X134, .(X133, .(T120, .(T121, []))), T123))), SCOPE: 12, CLAUSE: 4\n\nT119 is ground\nT120 is ground\nT121 is ground\nX114 is free\nX115 is free\nX133 is free\nX134 is free\nrev(T119, .(T120, .(T121, [])), T67) !=? rev([], X114, X115)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(tail(.(T131, T132), X134), rev(X134, .(T131, .(T120, .(T121, []))), T123))\n\nT120 is ground\nT121 is ground\nT131 is ground\nT132 is ground\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(tail(.(T131, T132), X134), rev(X134, .(T131, .(T120, .(T121, []))), T123)), SCOPE: 13, CLAUSE: 5 | ','(tail(.(T131, T132), X134), rev(X134, .(T131, .(T120, .(T121, []))), T123)), SCOPE: 13, CLAUSE: 6\n\nT120 is ground\nT121 is ground\nT131 is ground\nT132 is ground\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(tail(.(T131, T132), X134), rev(X134, .(T131, .(T120, .(T121, []))), T123)), SCOPE: 13, CLAUSE: 6\n\nT120 is ground\nT121 is ground\nT131 is ground\nT132 is ground\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: rev(T146, .(T145, .(T120, .(T121, []))), T123)\n\nT120 is ground\nT121 is ground\nT145 is ground\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: rev(T146, .(T145, .(T120, .(T121, []))), T123), SCOPE: 14, CLAUSE: 1 | rev(T146, .(T145, .(T120, .(T121, []))), T123), SCOPE: 14, CLAUSE: 2\n\nT120 is ground\nT121 is ground\nT145 is ground\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(!_14, eq(.(T159, .(T160, .(T161, []))), T163)) | rev([], .(T159, .(T160, .(T161, []))), T123), SCOPE: 14, CLAUSE: 2\n\nT159 is ground\nT160 is ground\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: rev(T146, .(T145, .(T120, .(T121, []))), T123), SCOPE: 14, CLAUSE: 2\n\nT120 is ground\nT121 is ground\nT145 is ground\nT146 is ground\nX162 is free\nX163 is free\nrev(T146, .(T145, .(T120, .(T121, []))), T123) !=? rev([], X162, X163)", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: eq(.(T159, .(T160, .(T161, []))), T163)\n\nT159 is ground\nT160 is ground\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: eq(.(T159, .(T160, .(T161, []))), T163), SCOPE: 15, CLAUSE: 7\n\nT159 is ground\nT160 is ground\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(head(T188, X181), ','(tail(T188, X182), rev(X182, .(X181, .(T189, .(T190, .(T191, [])))), T193)))\n\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nX162 is free\nX163 is free\nX181 is free\nX182 is free\nrev(T188, .(T189, .(T190, .(T191, []))), T123) !=? rev([], X162, X163)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(head(T188, X181), ','(tail(T188, X182), rev(X182, .(X181, .(T189, .(T190, .(T191, [])))), T193))), SCOPE: 16, CLAUSE: 3 | ','(head(T188, X181), ','(tail(T188, X182), rev(X182, .(X181, .(T189, .(T190, .(T191, [])))), T193))), SCOPE: 16, CLAUSE: 4\n\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nX162 is free\nX163 is free\nX181 is free\nX182 is free\nrev(T188, .(T189, .(T190, .(T191, []))), T123) !=? rev([], X162, X163)", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(head(T188, X181), ','(tail(T188, X182), rev(X182, .(X181, .(T189, .(T190, .(T191, [])))), T193))), SCOPE: 16, CLAUSE: 4\n\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nX162 is free\nX163 is free\nX181 is free\nX182 is free\nrev(T188, .(T189, .(T190, .(T191, []))), T123) !=? rev([], X162, X163)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(tail(.(T202, T203), X182), rev(X182, .(T202, .(T189, .(T190, .(T191, [])))), T193))\n\nT189 is ground\nT190 is ground\nT191 is ground\nT202 is ground\nT203 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(tail(.(T202, T203), X182), rev(X182, .(T202, .(T189, .(T190, .(T191, [])))), T193)), SCOPE: 17, CLAUSE: 5 | ','(tail(.(T202, T203), X182), rev(X182, .(T202, .(T189, .(T190, .(T191, [])))), T193)), SCOPE: 17, CLAUSE: 6\n\nT189 is ground\nT190 is ground\nT191 is ground\nT202 is ground\nT203 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(tail(.(T202, T203), X182), rev(X182, .(T202, .(T189, .(T190, .(T191, [])))), T193)), SCOPE: 17, CLAUSE: 6\n\nT189 is ground\nT190 is ground\nT191 is ground\nT202 is ground\nT203 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: rev(T219, .(T218, .(T189, .(T190, .(T191, [])))), T193)\n\nT189 is ground\nT190 is ground\nT191 is ground\nT218 is ground\nT219 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: rev(T219, .(T218, .(T189, .(T190, .(T191, [])))), T193), SCOPE: 18, CLAUSE: 1 | rev(T219, .(T218, .(T189, .(T190, .(T191, [])))), T193), SCOPE: 18, CLAUSE: 2\n\nT189 is ground\nT190 is ground\nT191 is ground\nT218 is ground\nT219 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(!_18, eq(.(T235, .(T236, .(T237, .(T238, [])))), T240)) | rev([], .(T235, .(T236, .(T237, .(T238, [])))), T193), SCOPE: 18, CLAUSE: 2\n\nT235 is ground\nT236 is ground\nT237 is ground\nT238 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: rev(T219, .(T218, .(T189, .(T190, .(T191, [])))), T193), SCOPE: 18, CLAUSE: 2\n\nT189 is ground\nT190 is ground\nT191 is ground\nT218 is ground\nT219 is ground\nX210 is free\nX211 is free\nrev(T219, .(T218, .(T189, .(T190, .(T191, [])))), T193) !=? rev([], X210, X211)", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: eq(.(T235, .(T236, .(T237, .(T238, [])))), T240)\n\nT235 is ground\nT236 is ground\nT237 is ground\nT238 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: eq(.(T235, .(T236, .(T237, .(T238, [])))), T240), SCOPE: 19, CLAUSE: 7\n\nT235 is ground\nT236 is ground\nT237 is ground\nT238 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(head(T271, X229), ','(tail(T271, X230), rev(X230, .(X229, .(T272, .(T273, .(T274, .(T275, []))))), T277)))\n\nT271 is ground\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nX210 is free\nX211 is free\nX229 is free\nX230 is free\nrev(T271, .(T272, .(T273, .(T274, .(T275, [])))), T193) !=? rev([], X210, X211)", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(head(T271, X229), ','(tail(T271, X230), rev(X230, .(X229, .(T272, .(T273, .(T274, .(T275, []))))), T277))), SCOPE: 20, CLAUSE: 3 | ','(head(T271, X229), ','(tail(T271, X230), rev(X230, .(X229, .(T272, .(T273, .(T274, .(T275, []))))), T277))), SCOPE: 20, CLAUSE: 4\n\nT271 is ground\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nX210 is free\nX211 is free\nX229 is free\nX230 is free\nrev(T271, .(T272, .(T273, .(T274, .(T275, [])))), T193) !=? rev([], X210, X211)", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(head(T271, X229), ','(tail(T271, X230), rev(X230, .(X229, .(T272, .(T273, .(T274, .(T275, []))))), T277))), SCOPE: 20, CLAUSE: 4\n\nT271 is ground\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nX210 is free\nX211 is free\nX229 is free\nX230 is free\nrev(T271, .(T272, .(T273, .(T274, .(T275, [])))), T193) !=? rev([], X210, X211)", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(tail(.(T287, T288), X230), rev(X230, .(T287, .(T272, .(T273, .(T274, .(T275, []))))), T277))\n\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nT287 is ground\nT288 is ground\nX230 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(tail(.(T287, T288), X230), rev(X230, .(T287, .(T272, .(T273, .(T274, .(T275, []))))), T277)), SCOPE: 21, CLAUSE: 5 | ','(tail(.(T287, T288), X230), rev(X230, .(T287, .(T272, .(T273, .(T274, .(T275, []))))), T277)), SCOPE: 21, CLAUSE: 6\n\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nT287 is ground\nT288 is ground\nX230 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(tail(.(T287, T288), X230), rev(X230, .(T287, .(T272, .(T273, .(T274, .(T275, []))))), T277)), SCOPE: 21, CLAUSE: 6\n\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nT287 is ground\nT288 is ground\nX230 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: rev(T306, .(T305, .(T272, .(T273, .(T274, .(T275, []))))), T277)\n\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nT305 is ground\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: rev(T306, .(T305, .(T272, .(T273, .(T274, .(T275, []))))), T277), SCOPE: 22, CLAUSE: 1 | rev(T306, .(T305, .(T272, .(T273, .(T274, .(T275, []))))), T277), SCOPE: 22, CLAUSE: 2\n\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nT305 is ground\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(!_22, eq(.(T325, .(T326, .(T327, .(T328, .(T329, []))))), T331)) | rev([], .(T325, .(T326, .(T327, .(T328, .(T329, []))))), T277), SCOPE: 22, CLAUSE: 2\n\nT325 is ground\nT326 is ground\nT327 is ground\nT328 is ground\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: rev(T306, .(T305, .(T272, .(T273, .(T274, .(T275, []))))), T277), SCOPE: 22, CLAUSE: 2\n\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nT305 is ground\nT306 is ground\nX258 is free\nX259 is free\nrev(T306, .(T305, .(T272, .(T273, .(T274, .(T275, []))))), T277) !=? rev([], X258, X259)", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: eq(.(T325, .(T326, .(T327, .(T328, .(T329, []))))), T331)\n\nT325 is ground\nT326 is ground\nT327 is ground\nT328 is ground\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: eq(.(T325, .(T326, .(T327, .(T328, .(T329, []))))), T331), SCOPE: 23, CLAUSE: 7\n\nT325 is ground\nT326 is ground\nT327 is ground\nT328 is ground\nT329 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(head(T368, X277), ','(tail(T368, X278), rev(X278, .(X277, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375)))\n\nT368 is ground\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nX258 is free\nX259 is free\nX277 is free\nX278 is free\nrev(T368, .(T369, .(T370, .(T371, .(T372, .(T373, []))))), T277) !=? rev([], X258, X259)", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(head(T368, X277), ','(tail(T368, X278), rev(X278, .(X277, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375))), SCOPE: 24, CLAUSE: 3 | ','(head(T368, X277), ','(tail(T368, X278), rev(X278, .(X277, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375))), SCOPE: 24, CLAUSE: 4\n\nT368 is ground\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nX258 is free\nX259 is free\nX277 is free\nX278 is free\nrev(T368, .(T369, .(T370, .(T371, .(T372, .(T373, []))))), T277) !=? rev([], X258, X259)", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(head(T368, X277), ','(tail(T368, X278), rev(X278, .(X277, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375))), SCOPE: 24, CLAUSE: 4\n\nT368 is ground\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nX258 is free\nX259 is free\nX277 is free\nX278 is free\nrev(T368, .(T369, .(T370, .(T371, .(T372, .(T373, []))))), T277) !=? rev([], X258, X259)", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(tail(.(T386, T387), X278), rev(X278, .(T386, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375))\n\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nT386 is ground\nT387 is ground\nX278 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(tail(.(T386, T387), X278), rev(X278, .(T386, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375)), SCOPE: 25, CLAUSE: 5 | ','(tail(.(T386, T387), X278), rev(X278, .(T386, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375)), SCOPE: 25, CLAUSE: 6\n\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nT386 is ground\nT387 is ground\nX278 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(tail(.(T386, T387), X278), rev(X278, .(T386, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375)), SCOPE: 25, CLAUSE: 6\n\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nT386 is ground\nT387 is ground\nX278 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: rev(T407, .(T406, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375)\n\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nT406 is ground\nT407 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: rev(T407, .(T406, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375), SCOPE: 26, CLAUSE: 1 | rev(T407, .(T406, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375), SCOPE: 26, CLAUSE: 2\n\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nT406 is ground\nT407 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(!_26, eq(.(T429, .(T430, .(T431, .(T432, .(T433, .(T434, [])))))), T436)) | rev([], .(T429, .(T430, .(T431, .(T432, .(T433, .(T434, [])))))), T375), SCOPE: 26, CLAUSE: 2\n\nT429 is ground\nT430 is ground\nT431 is ground\nT432 is ground\nT433 is ground\nT434 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: rev(T407, .(T406, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375), SCOPE: 26, CLAUSE: 2\n\nT369 is ground\nT370 is ground\nT371 is ground\nT372 is ground\nT373 is ground\nT406 is ground\nT407 is ground\nX306 is free\nX307 is free\nrev(T407, .(T406, .(T369, .(T370, .(T371, .(T372, .(T373, [])))))), T375) !=? rev([], X306, X307)", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: eq(.(T429, .(T430, .(T431, .(T432, .(T433, .(T434, [])))))), T436)\n\nT429 is ground\nT430 is ground\nT431 is ground\nT432 is ground\nT433 is ground\nT434 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: eq(.(T429, .(T430, .(T431, .(T432, .(T433, .(T434, [])))))), T436), SCOPE: 27, CLAUSE: 7\n\nT429 is ground\nT430 is ground\nT431 is ground\nT432 is ground\nT433 is ground\nT434 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: ','(head(T479, X325), ','(tail(T479, X326), rev(X326, .(X325, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487)))\n\nT479 is ground\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nX306 is free\nX307 is free\nX325 is free\nX326 is free\nrev(T479, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, [])))))), T375) !=? rev([], X306, X307)", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: ','(head(T479, X325), ','(tail(T479, X326), rev(X326, .(X325, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487))), SCOPE: 28, CLAUSE: 3 | ','(head(T479, X325), ','(tail(T479, X326), rev(X326, .(X325, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487))), SCOPE: 28, CLAUSE: 4\n\nT479 is ground\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nX306 is free\nX307 is free\nX325 is free\nX326 is free\nrev(T479, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, [])))))), T375) !=? rev([], X306, X307)", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ','(head(T479, X325), ','(tail(T479, X326), rev(X326, .(X325, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487))), SCOPE: 28, CLAUSE: 4\n\nT479 is ground\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nX306 is free\nX307 is free\nX325 is free\nX326 is free\nrev(T479, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, [])))))), T375) !=? rev([], X306, X307)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(tail(.(T499, T500), X326), rev(X326, .(T499, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487))\n\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nT499 is ground\nT500 is ground\nX326 is free", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: ','(tail(.(T499, T500), X326), rev(X326, .(T499, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487)), SCOPE: 29, CLAUSE: 5 | ','(tail(.(T499, T500), X326), rev(X326, .(T499, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487)), SCOPE: 29, CLAUSE: 6\n\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nT499 is ground\nT500 is ground\nX326 is free", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: ','(tail(.(T499, T500), X326), rev(X326, .(T499, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487)), SCOPE: 29, CLAUSE: 6\n\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nT499 is ground\nT500 is ground\nX326 is free", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: rev(T522, .(T521, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487)\n\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nT521 is ground\nT522 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: rev(T522, .(T521, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487), SCOPE: 30, CLAUSE: 1 | rev(T522, .(T521, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487), SCOPE: 30, CLAUSE: 2\n\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nT521 is ground\nT522 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: ','(!_30, eq(.(T547, .(T548, .(T549, .(T550, .(T551, .(T552, .(T553, []))))))), T555)) | rev([], .(T547, .(T548, .(T549, .(T550, .(T551, .(T552, .(T553, []))))))), T487), SCOPE: 30, CLAUSE: 2\n\nT547 is ground\nT548 is ground\nT549 is ground\nT550 is ground\nT551 is ground\nT552 is ground\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: rev(T522, .(T521, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487), SCOPE: 30, CLAUSE: 2\n\nT480 is ground\nT481 is ground\nT482 is ground\nT483 is ground\nT484 is ground\nT485 is ground\nT521 is ground\nT522 is ground\nX354 is free\nX355 is free\nrev(T522, .(T521, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, []))))))), T487) !=? rev([], X354, X355)", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: eq(.(T547, .(T548, .(T549, .(T550, .(T551, .(T552, .(T553, []))))))), T555)\n\nT547 is ground\nT548 is ground\nT549 is ground\nT550 is ground\nT551 is ground\nT552 is ground\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: eq(.(T547, .(T548, .(T549, .(T550, .(T551, .(T552, .(T553, []))))))), T555), SCOPE: 31, CLAUSE: 7\n\nT547 is ground\nT548 is ground\nT549 is ground\nT550 is ground\nT551 is ground\nT552 is ground\nT553 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: ','(head(T604, X373), ','(tail(T604, X374), rev(X374, .(X373, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613)))\n\nT604 is ground\nT605 is ground\nT606 is ground\nT607 is ground\nT608 is ground\nT609 is ground\nT610 is ground\nT611 is ground\nX354 is free\nX355 is free\nX373 is free\nX374 is free\nrev(T604, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, []))))))), T487) !=? rev([], X354, X355)", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: ','(head(T604, X373), ','(tail(T604, X374), rev(X374, .(X373, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613))), SCOPE: 32, CLAUSE: 3 | ','(head(T604, X373), ','(tail(T604, X374), rev(X374, .(X373, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613))), SCOPE: 32, CLAUSE: 4\n\nT604 is ground\nT605 is ground\nT606 is ground\nT607 is ground\nT608 is ground\nT609 is ground\nT610 is ground\nT611 is ground\nX354 is free\nX355 is free\nX373 is free\nX374 is free\nrev(T604, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, []))))))), T487) !=? rev([], X354, X355)", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: ','(head(T604, X373), ','(tail(T604, X374), rev(X374, .(X373, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613))), SCOPE: 32, CLAUSE: 4\n\nT604 is ground\nT605 is ground\nT606 is ground\nT607 is ground\nT608 is ground\nT609 is ground\nT610 is ground\nT611 is ground\nX354 is free\nX355 is free\nX373 is free\nX374 is free\nrev(T604, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, []))))))), T487) !=? rev([], X354, X355)", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: ','(tail(.(T626, T627), X374), rev(X374, .(T626, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613))\n\nT605 is ground\nT606 is ground\nT607 is ground\nT608 is ground\nT609 is ground\nT610 is ground\nT611 is ground\nT626 is ground\nT627 is ground\nX374 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: ','(tail(.(T626, T627), X374), rev(X374, .(T626, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613)), SCOPE: 33, CLAUSE: 5 | ','(tail(.(T626, T627), X374), rev(X374, .(T626, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613)), SCOPE: 33, CLAUSE: 6\n\nT605 is ground\nT606 is ground\nT607 is ground\nT608 is ground\nT609 is ground\nT610 is ground\nT611 is ground\nT626 is ground\nT627 is ground\nX374 is free", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(tail(.(T626, T627), X374), rev(X374, .(T626, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613)), SCOPE: 33, CLAUSE: 6\n\nT605 is ground\nT606 is ground\nT607 is ground\nT608 is ground\nT609 is ground\nT610 is ground\nT611 is ground\nT626 is ground\nT627 is ground\nX374 is free", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: rev(T651, .(T650, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))), T613)\n\nT605 is ground\nT606 is ground\nT607 is ground\nT608 is ground\nT609 is ground\nT610 is ground\nT611 is ground\nT650 is ground\nT651 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: rev(T651, .(T650, T661), T613)\n\nT650 is ground\nT651 is ground\nT661 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: rev(T651, .(T650, T661), T613), SCOPE: 34, CLAUSE: 1 | rev(T651, .(T650, T661), T613), SCOPE: 34, CLAUSE: 2\n\nT650 is ground\nT651 is ground\nT661 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: ','(!_34, eq(.(T671, T672), T674)) | rev([], .(T671, T672), T613), SCOPE: 34, CLAUSE: 2\n\nT671 is ground\nT672 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: rev(T651, .(T650, T661), T613), SCOPE: 34, CLAUSE: 2\n\nT650 is ground\nT651 is ground\nT661 is ground\nX404 is free\nX405 is free\nrev(T651, .(T650, T661), T613) !=? rev([], X404, X405)", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: eq(.(T671, T672), T674)\n\nT671 is ground\nT672 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: eq(.(T671, T672), T674), SCOPE: 35, CLAUSE: 7\n\nT671 is ground\nT672 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: ','(head(T693, X423), ','(tail(T693, X424), rev(X424, .(X423, .(T694, T695)), T697)))\n\nT693 is ground\nT694 is ground\nT695 is ground\nX404 is free\nX405 is free\nX423 is free\nX424 is free\nrev(T693, .(T694, T695), T613) !=? rev([], X404, X405)", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: ','(head(T693, X423), ','(tail(T693, X424), rev(X424, .(X423, .(T694, T695)), T697))), SCOPE: 36, CLAUSE: 3 | ','(head(T693, X423), ','(tail(T693, X424), rev(X424, .(X423, .(T694, T695)), T697))), SCOPE: 36, CLAUSE: 4\n\nT693 is ground\nT694 is ground\nT695 is ground\nX404 is free\nX405 is free\nX423 is free\nX424 is free\nrev(T693, .(T694, T695), T613) !=? rev([], X404, X405)", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: ','(head(T693, X423), ','(tail(T693, X424), rev(X424, .(X423, .(T694, T695)), T697))), SCOPE: 36, CLAUSE: 4\n\nT693 is ground\nT694 is ground\nT695 is ground\nX404 is free\nX405 is free\nX423 is free\nX424 is free\nrev(T693, .(T694, T695), T613) !=? rev([], X404, X405)", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: ','(tail(.(T705, T706), X424), rev(X424, .(T705, .(T694, T695)), T697))\n\nT694 is ground\nT695 is ground\nT705 is ground\nT706 is ground\nX424 is free", fontsize=16, style=filled, fillcolor=lightyellow];
293 [label="293: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: ','(tail(.(T705, T706), X424), rev(X424, .(T705, .(T694, T695)), T697)), SCOPE: 37, CLAUSE: 5 | ','(tail(.(T705, T706), X424), rev(X424, .(T705, .(T694, T695)), T697)), SCOPE: 37, CLAUSE: 6\n\nT694 is ground\nT695 is ground\nT705 is ground\nT706 is ground\nX424 is free", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: ','(tail(.(T705, T706), X424), rev(X424, .(T705, .(T694, T695)), T697)), SCOPE: 37, CLAUSE: 6\n\nT694 is ground\nT695 is ground\nT705 is ground\nT706 is ground\nX424 is free", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: rev(T720, .(T719, .(T694, T695)), T697)\n\nT694 is ground\nT695 is ground\nT719 is ground\nT720 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 297 [arrowhead = none ];
297 -> 3;

298 [label="ONLY EVAL with clause\nrev(X10, X11) :- rev(X10, [], X11).\nand substitutionT1 -> T9,\nX10 -> T9,\nT2 -> T11,\nX11 -> T11,\nT10 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 298 [arrowhead = none ];
298 -> 7;

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

300 [label="EVAL with clause\nrev([], X18, X19) :- ','(!_2, eq(X18, X19)).\nand substitutionT9 -> [],\nX18 -> [],\nT11 -> T16,\nX19 -> T16,\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 300 [arrowhead = none ];
300 -> 16;

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

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

303 [label="ONLY EVAL with clause\nrev(X34, X35, X36) :- ','(head(X34, X37), ','(tail(X34, X38), rev(X38, .(X37, X35), X36))).\nand substitutionT9 -> T23,\nX34 -> T23,\nX35 -> [],\nT11 -> T25,\nX36 -> T25,\nT24 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 303 [arrowhead = none ];
303 -> 28;

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

305 [label="EVAL with clause\neq(X22, X22).\nand substitutionX22 -> [],\nT16 -> []", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 305 [arrowhead = none ];
305 -> 21;

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

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

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

309 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T23, [], T11), rev([], X18, X19))", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 309 [arrowhead = none ];
309 -> 32;

310 [label="EVAL with clause\nhead(.(X48, X49), X48).\nand substitutionX48 -> T31,\nX49 -> T32,\nT23 -> .(T31, T32),\nX37 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 310 [arrowhead = none ];
310 -> 34;

311 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 311 [arrowhead = none ];
311 -> 35;

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

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

314 [label="ONLY EVAL with clause\ntail(.(X58, X59), X59).\nand substitutionT31 -> T41,\nX58 -> T41,\nT32 -> T42,\nX59 -> T42,\nX38 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 314 [arrowhead = none ];
314 -> 43;

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

316 [label="EVAL with clause\nrev([], X66, X67) :- ','(!_6, eq(X66, X67)).\nand substitutionT42 -> [],\nT41 -> T49,\nX66 -> .(T49, []),\nT25 -> T51,\nX67 -> T51,\nT50 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 316 [arrowhead = none ];
316 -> 48;

317 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 317 [arrowhead = none ];
317 -> 49;

318 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 318 [arrowhead = none ];
318 -> 50;

319 [label="ONLY EVAL with clause\nrev(X82, X83, X84) :- ','(head(X82, X85), ','(tail(X82, X86), rev(X86, .(X85, X83), X84))).\nand substitutionT42 -> T64,\nX82 -> T64,\nT41 -> T65,\nX83 -> .(T65, []),\nT25 -> T67,\nX84 -> T67,\nT66 -> T67", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 319 [arrowhead = none ];
319 -> 58;

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

321 [label="EVAL with clause\neq(X70, X70).\nand substitutionT49 -> T54,\nX70 -> .(T54, []),\nT51 -> .(T54, [])", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 321 [arrowhead = none ];
321 -> 52;

322 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 322 [arrowhead = none ];
322 -> 53;

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

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

325 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T64, .(T65, []), T25), rev([], X66, X67))", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 325 [arrowhead = none ];
325 -> 64;

326 [label="EVAL with clause\nhead(.(X96, X97), X96).\nand substitutionX96 -> T74,\nX97 -> T75,\nT64 -> .(T74, T75),\nX85 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 326 [arrowhead = none ];
326 -> 65;

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

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

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

330 [label="ONLY EVAL with clause\ntail(.(X106, X107), X107).\nand substitutionT74 -> T86,\nX106 -> T86,\nT75 -> T87,\nX107 -> T87,\nX86 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 330 [arrowhead = none ];
330 -> 71;

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

332 [label="EVAL with clause\nrev([], X114, X115) :- ','(!_10, eq(X114, X115)).\nand substitutionT87 -> [],\nT86 -> T97,\nT65 -> T98,\nX114 -> .(T97, .(T98, [])),\nT67 -> T100,\nX115 -> T100,\nT99 -> T100", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 332 [arrowhead = none ];
332 -> 80;

333 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 333 [arrowhead = none ];
333 -> 81;

334 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 334 [arrowhead = none ];
334 -> 82;

335 [label="ONLY EVAL with clause\nrev(X130, X131, X132) :- ','(head(X130, X133), ','(tail(X130, X134), rev(X134, .(X133, X131), X132))).\nand substitutionT87 -> T119,\nX130 -> T119,\nT86 -> T120,\nT65 -> T121,\nX131 -> .(T120, .(T121, [])),\nT67 -> T123,\nX132 -> T123,\nT122 -> T123", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 335 [arrowhead = none ];
335 -> 90;

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

337 [label="EVAL with clause\neq(X118, X118).\nand substitutionT97 -> T105,\nT98 -> T106,\nX118 -> .(T105, .(T106, [])),\nT100 -> .(T105, .(T106, []))", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 337 [arrowhead = none ];
337 -> 84;

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

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

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

341 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T119, .(T120, .(T121, [])), T67), rev([], X114, X115))", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 341 [arrowhead = none ];
341 -> 96;

342 [label="EVAL with clause\nhead(.(X144, X145), X144).\nand substitutionX144 -> T131,\nX145 -> T132,\nT119 -> .(T131, T132),\nX133 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 342 [arrowhead = none ];
342 -> 97;

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

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

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

346 [label="ONLY EVAL with clause\ntail(.(X154, X155), X155).\nand substitutionT131 -> T145,\nX154 -> T145,\nT132 -> T146,\nX155 -> T146,\nX134 -> T146", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 346 [arrowhead = none ];
346 -> 103;

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

348 [label="EVAL with clause\nrev([], X162, X163) :- ','(!_14, eq(X162, X163)).\nand substitutionT146 -> [],\nT145 -> T159,\nT120 -> T160,\nT121 -> T161,\nX162 -> .(T159, .(T160, .(T161, []))),\nT123 -> T163,\nX163 -> T163,\nT162 -> T163", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 348 [arrowhead = none ];
348 -> 112;

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

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

351 [label="ONLY EVAL with clause\nrev(X178, X179, X180) :- ','(head(X178, X181), ','(tail(X178, X182), rev(X182, .(X181, X179), X180))).\nand substitutionT146 -> T188,\nX178 -> T188,\nT145 -> T189,\nT120 -> T190,\nT121 -> T191,\nX179 -> .(T189, .(T190, .(T191, []))),\nT123 -> T193,\nX180 -> T193,\nT192 -> T193", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 351 [arrowhead = none ];
351 -> 122;

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

353 [label="EVAL with clause\neq(X166, X166).\nand substitutionT159 -> T170,\nT160 -> T171,\nT161 -> T172,\nX166 -> .(T170, .(T171, .(T172, []))),\nT163 -> .(T170, .(T171, .(T172, [])))", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 353 [arrowhead = none ];
353 -> 116;

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

355 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 355 [arrowhead = none ];
355 -> 118;

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

357 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T188, .(T189, .(T190, .(T191, []))), T123), rev([], X162, X163))", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 357 [arrowhead = none ];
357 -> 128;

358 [label="EVAL with clause\nhead(.(X192, X193), X192).\nand substitutionX192 -> T202,\nX193 -> T203,\nT188 -> .(T202, T203),\nX181 -> T202", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 358 [arrowhead = none ];
358 -> 129;

359 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 359 [arrowhead = none ];
359 -> 130;

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

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

362 [label="ONLY EVAL with clause\ntail(.(X202, X203), X203).\nand substitutionT202 -> T218,\nX202 -> T218,\nT203 -> T219,\nX203 -> T219,\nX182 -> T219", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 362 [arrowhead = none ];
362 -> 135;

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

364 [label="EVAL with clause\nrev([], X210, X211) :- ','(!_18, eq(X210, X211)).\nand substitutionT219 -> [],\nT218 -> T235,\nT189 -> T236,\nT190 -> T237,\nT191 -> T238,\nX210 -> .(T235, .(T236, .(T237, .(T238, [])))),\nT193 -> T240,\nX211 -> T240,\nT239 -> T240", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 364 [arrowhead = none ];
364 -> 144;

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

366 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 366 [arrowhead = none ];
366 -> 146;

367 [label="ONLY EVAL with clause\nrev(X226, X227, X228) :- ','(head(X226, X229), ','(tail(X226, X230), rev(X230, .(X229, X227), X228))).\nand substitutionT219 -> T271,\nX226 -> T271,\nT218 -> T272,\nT189 -> T273,\nT190 -> T274,\nT191 -> T275,\nX227 -> .(T272, .(T273, .(T274, .(T275, [])))),\nT193 -> T277,\nX228 -> T277,\nT276 -> T277", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 367 [arrowhead = none ];
367 -> 154;

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

369 [label="EVAL with clause\neq(X214, X214).\nand substitutionT235 -> T249,\nT236 -> T250,\nT237 -> T251,\nT238 -> T252,\nX214 -> .(T249, .(T250, .(T251, .(T252, [])))),\nT240 -> .(T249, .(T250, .(T251, .(T252, []))))", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 369 [arrowhead = none ];
369 -> 148;

370 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 370 [arrowhead = none ];
370 -> 149;

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

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

373 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T271, .(T272, .(T273, .(T274, .(T275, [])))), T193), rev([], X210, X211))", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 373 [arrowhead = none ];
373 -> 160;

374 [label="EVAL with clause\nhead(.(X240, X241), X240).\nand substitutionX240 -> T287,\nX241 -> T288,\nT271 -> .(T287, T288),\nX229 -> T287", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 374 [arrowhead = none ];
374 -> 161;

375 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 375 [arrowhead = none ];
375 -> 162;

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

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

378 [label="ONLY EVAL with clause\ntail(.(X250, X251), X251).\nand substitutionT287 -> T305,\nX250 -> T305,\nT288 -> T306,\nX251 -> T306,\nX230 -> T306", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 378 [arrowhead = none ];
378 -> 167;

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

380 [label="EVAL with clause\nrev([], X258, X259) :- ','(!_22, eq(X258, X259)).\nand substitutionT306 -> [],\nT305 -> T325,\nT272 -> T326,\nT273 -> T327,\nT274 -> T328,\nT275 -> T329,\nX258 -> .(T325, .(T326, .(T327, .(T328, .(T329, []))))),\nT277 -> T331,\nX259 -> T331,\nT330 -> T331", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 380 [arrowhead = none ];
380 -> 176;

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

382 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 382 [arrowhead = none ];
382 -> 178;

383 [label="ONLY EVAL with clause\nrev(X274, X275, X276) :- ','(head(X274, X277), ','(tail(X274, X278), rev(X278, .(X277, X275), X276))).\nand substitutionT306 -> T368,\nX274 -> T368,\nT305 -> T369,\nT272 -> T370,\nT273 -> T371,\nT274 -> T372,\nT275 -> T373,\nX275 -> .(T369, .(T370, .(T371, .(T372, .(T373, []))))),\nT277 -> T375,\nX276 -> T375,\nT374 -> T375", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 383 [arrowhead = none ];
383 -> 188;

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

385 [label="EVAL with clause\neq(X262, X262).\nand substitutionT325 -> T342,\nT326 -> T343,\nT327 -> T344,\nT328 -> T345,\nT329 -> T346,\nX262 -> .(T342, .(T343, .(T344, .(T345, .(T346, []))))),\nT331 -> .(T342, .(T343, .(T344, .(T345, .(T346, [])))))", fontsize=14, style = filled, fillcolor = lightblue];
179 -> 385 [arrowhead = none ];
385 -> 180;

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

387 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
180 -> 387 [arrowhead = none ];
387 -> 182;

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

389 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T368, .(T369, .(T370, .(T371, .(T372, .(T373, []))))), T277), rev([], X258, X259))", fontsize=14, style = filled, fillcolor = lightgreen];
191 -> 389 [arrowhead = none ];
389 -> 192;

390 [label="EVAL with clause\nhead(.(X288, X289), X288).\nand substitutionX288 -> T386,\nX289 -> T387,\nT368 -> .(T386, T387),\nX277 -> T386", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 390 [arrowhead = none ];
390 -> 193;

391 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
192 -> 391 [arrowhead = none ];
391 -> 195;

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

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

394 [label="ONLY EVAL with clause\ntail(.(X298, X299), X299).\nand substitutionT386 -> T406,\nX298 -> T406,\nT387 -> T407,\nX299 -> T407,\nX278 -> T407", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 394 [arrowhead = none ];
394 -> 199;

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

396 [label="EVAL with clause\nrev([], X306, X307) :- ','(!_26, eq(X306, X307)).\nand substitutionT407 -> [],\nT406 -> T429,\nT369 -> T430,\nT370 -> T431,\nT371 -> T432,\nT372 -> T433,\nT373 -> T434,\nX306 -> .(T429, .(T430, .(T431, .(T432, .(T433, .(T434, [])))))),\nT375 -> T436,\nX307 -> T436,\nT435 -> T436", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 396 [arrowhead = none ];
396 -> 208;

397 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
204 -> 397 [arrowhead = none ];
397 -> 209;

398 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
208 -> 398 [arrowhead = none ];
398 -> 210;

399 [label="ONLY EVAL with clause\nrev(X322, X323, X324) :- ','(head(X322, X325), ','(tail(X322, X326), rev(X326, .(X325, X323), X324))).\nand substitutionT407 -> T479,\nX322 -> T479,\nT406 -> T480,\nT369 -> T481,\nT370 -> T482,\nT371 -> T483,\nT372 -> T484,\nT373 -> T485,\nX323 -> .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, [])))))),\nT375 -> T487,\nX324 -> T487,\nT486 -> T487", fontsize=14, style = filled, fillcolor = lightblue];
209 -> 399 [arrowhead = none ];
399 -> 220;

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

401 [label="EVAL with clause\neq(X310, X310).\nand substitutionT429 -> T449,\nT430 -> T450,\nT431 -> T451,\nT432 -> T452,\nT433 -> T453,\nT434 -> T454,\nX310 -> .(T449, .(T450, .(T451, .(T452, .(T453, .(T454, [])))))),\nT436 -> .(T449, .(T450, .(T451, .(T452, .(T453, .(T454, []))))))", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 401 [arrowhead = none ];
401 -> 212;

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

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

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

405 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T479, .(T480, .(T481, .(T482, .(T483, .(T484, .(T485, [])))))), T375), rev([], X306, X307))", fontsize=14, style = filled, fillcolor = lightgreen];
223 -> 405 [arrowhead = none ];
405 -> 224;

406 [label="EVAL with clause\nhead(.(X336, X337), X336).\nand substitutionX336 -> T499,\nX337 -> T500,\nT479 -> .(T499, T500),\nX325 -> T499", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 406 [arrowhead = none ];
406 -> 225;

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

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

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

410 [label="ONLY EVAL with clause\ntail(.(X346, X347), X347).\nand substitutionT499 -> T521,\nX346 -> T521,\nT500 -> T522,\nX347 -> T522,\nX326 -> T522", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 410 [arrowhead = none ];
410 -> 231;

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

412 [label="EVAL with clause\nrev([], X354, X355) :- ','(!_30, eq(X354, X355)).\nand substitutionT522 -> [],\nT521 -> T547,\nT480 -> T548,\nT481 -> T549,\nT482 -> T550,\nT483 -> T551,\nT484 -> T552,\nT485 -> T553,\nX354 -> .(T547, .(T548, .(T549, .(T550, .(T551, .(T552, .(T553, []))))))),\nT487 -> T555,\nX355 -> T555,\nT554 -> T555", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 412 [arrowhead = none ];
412 -> 240;

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

414 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
240 -> 414 [arrowhead = none ];
414 -> 242;

415 [label="ONLY EVAL with clause\nrev(X370, X371, X372) :- ','(head(X370, X373), ','(tail(X370, X374), rev(X374, .(X373, X371), X372))).\nand substitutionT522 -> T604,\nX370 -> T604,\nT521 -> T605,\nT480 -> T606,\nT481 -> T607,\nT482 -> T608,\nT483 -> T609,\nT484 -> T610,\nT485 -> T611,\nX371 -> .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, []))))))),\nT487 -> T613,\nX372 -> T613,\nT612 -> T613", fontsize=14, style = filled, fillcolor = lightblue];
241 -> 415 [arrowhead = none ];
415 -> 252;

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

417 [label="EVAL with clause\neq(X358, X358).\nand substitutionT547 -> T570,\nT548 -> T571,\nT549 -> T572,\nT550 -> T573,\nT551 -> T574,\nT552 -> T575,\nT553 -> T576,\nX358 -> .(T570, .(T571, .(T572, .(T573, .(T574, .(T575, .(T576, []))))))),\nT555 -> .(T570, .(T571, .(T572, .(T573, .(T574, .(T575, .(T576, [])))))))", fontsize=14, style = filled, fillcolor = lightblue];
243 -> 417 [arrowhead = none ];
417 -> 244;

418 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
243 -> 418 [arrowhead = none ];
418 -> 245;

419 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
244 -> 419 [arrowhead = none ];
419 -> 246;

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

421 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T604, .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, []))))))), T487), rev([], X354, X355))", fontsize=14, style = filled, fillcolor = lightgreen];
255 -> 421 [arrowhead = none ];
421 -> 256;

422 [label="EVAL with clause\nhead(.(X384, X385), X384).\nand substitutionX384 -> T626,\nX385 -> T627,\nT604 -> .(T626, T627),\nX373 -> T626", fontsize=14, style = filled, fillcolor = lightblue];
256 -> 422 [arrowhead = none ];
422 -> 258;

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

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

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

426 [label="ONLY EVAL with clause\ntail(.(X394, X395), X395).\nand substitutionT626 -> T650,\nX394 -> T650,\nT627 -> T651,\nX395 -> T651,\nX374 -> T651", fontsize=14, style = filled, fillcolor = lightblue];
261 -> 426 [arrowhead = none ];
426 -> 263;

427 [label="GENERALIZATION\nT661 <-- .(T605, .(T606, .(T607, .(T608, .(T609, .(T610, .(T611, [])))))))\n\nNew Knowledge:\nT661 is ground", fontsize=14, style = filled, fillcolor = violet];
263 -> 427 [arrowhead = none ];
427 -> 268;

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

429 [label="EVAL with clause\nrev([], X404, X405) :- ','(!_34, eq(X404, X405)).\nand substitutionT651 -> [],\nT650 -> T671,\nT661 -> T672,\nX404 -> .(T671, T672),\nT613 -> T674,\nX405 -> T674,\nT673 -> T674", fontsize=14, style = filled, fillcolor = lightblue];
273 -> 429 [arrowhead = none ];
429 -> 274;

430 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
273 -> 430 [arrowhead = none ];
430 -> 275;

431 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
274 -> 431 [arrowhead = none ];
431 -> 276;

432 [label="ONLY EVAL with clause\nrev(X420, X421, X422) :- ','(head(X420, X423), ','(tail(X420, X424), rev(X424, .(X423, X421), X422))).\nand substitutionT651 -> T693,\nX420 -> T693,\nT650 -> T694,\nT661 -> T695,\nX421 -> .(T694, T695),\nT613 -> T697,\nX422 -> T697,\nT696 -> T697", fontsize=14, style = filled, fillcolor = lightblue];
275 -> 432 [arrowhead = none ];
432 -> 288;

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

434 [label="EVAL with clause\neq(X408, X408).\nand substitutionT671 -> T679,\nT672 -> T680,\nX408 -> .(T679, T680),\nT674 -> .(T679, T680)", fontsize=14, style = filled, fillcolor = lightblue];
277 -> 434 [arrowhead = none ];
434 -> 279;

435 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
277 -> 435 [arrowhead = none ];
435 -> 280;

436 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
279 -> 436 [arrowhead = none ];
436 -> 281;

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

438 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T693, .(T694, T695), T613), rev([], X404, X405))", fontsize=14, style = filled, fillcolor = lightgreen];
289 -> 438 [arrowhead = none ];
438 -> 291;

439 [label="EVAL with clause\nhead(.(X434, X435), X434).\nand substitutionX434 -> T705,\nX435 -> T706,\nT693 -> .(T705, T706),\nX423 -> T705", fontsize=14, style = filled, fillcolor = lightblue];
291 -> 439 [arrowhead = none ];
439 -> 292;

440 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
291 -> 440 [arrowhead = none ];
440 -> 293;

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

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

443 [label="ONLY EVAL with clause\ntail(.(X444, X445), X445).\nand substitutionT705 -> T719,\nX444 -> T719,\nT706 -> T720,\nX445 -> T720,\nX424 -> T720", fontsize=14, style = filled, fillcolor = lightblue];
295 -> 443 [arrowhead = none ];
443 -> 296;

444 [label="INSTANCE with matching:\nT651 -> T720\nT650 -> T719\nT661 -> .(T694, T695)\nT613 -> T697", fontsize=14, style = filled, fillcolor = lightgrey];
296 -> 444 [arrowhead = none , style=dashed];
444 -> 268[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f268_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f268_in([], z0, z1) → f268_out1
f268_in(.(z0, z1), z2, z3) → U2(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f268_out1, .(z0, z1), z2, z3) → f268_out1

Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F268_IN(.(z0, z1), z2, z3) → c11(U2'(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F268_IN(z1, z0, .(z2, z3)))

S tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F268_IN(.(z0, z1), z2, z3) → c11(U2'(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F268_IN(z1, z0, .(z2, z3)))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f268_in, U2

Defined Pair Symbols:

F2_IN, F268_IN

Compound Symbols:

c8, c11

(3) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f268_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f268_in([], z0, z1) → f268_out1
f268_in(.(z0, z1), z2, z3) → U2(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f268_out1, .(z0, z1), z2, z3) → f268_out1

Tuples:

F268_IN(.(z0, z1), z2, z3) → c11(U2'(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F268_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))

S tuples:

F268_IN(.(z0, z1), z2, z3) → c11(U2'(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F268_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f268_in, U2

Defined Pair Symbols:

F268_IN, F2_IN

Compound Symbols:

c11, c

(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f268_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f268_in([], z0, z1) → f268_out1
f268_in(.(z0, z1), z2, z3) → U2(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f268_out1, .(z0, z1), z2, z3) → f268_out1

Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F268_IN(.(z0, z1), z2, z3) → c11(F268_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F268_IN(.(z0, z1), z2, z3) → c11(F268_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f268_in, U2

Defined Pair Symbols:

F2_IN, F268_IN

Compound Symbols:

c, c11, c

(7) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f268_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f268_in([], z0, z1) → f268_out1
f268_in(.(z0, z1), z2, z3) → U2(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f268_out1, .(z0, z1), z2, z3) → f268_out1

Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F268_IN(.(z0, z1), z2, z3) → c11(F268_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F268_IN(.(z0, z1), z2, z3) → c11(F268_IN(z1, z0, .(z2, z3)))

K tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

Defined Rule Symbols:

f2_in, U1, f268_in, U2

Defined Pair Symbols:

F2_IN, F268_IN

Compound Symbols:

c, c11, c

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F268_IN(.(z0, z1), z2, z3) → c11(F268_IN(z1, z0, .(z2, z3)))

We considered the (Usable) Rules:none
And the Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F268_IN(.(z0, z1), z2, z3) → c11(F268_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [3] + x₂   
POL(F268_IN(x₁, x₂, x₃)) = [3]x₁ + x₃   
POL(F2_IN(x₁)) = [3]x₁   
POL([]) = [2]   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c11(x₁)) = x₁   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, []))) → f2_out1
f2_in(.(z0, .(z1, .(z2, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f268_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f268_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f268_in([], z0, z1) → f268_out1
f268_in(.(z0, z1), z2, z3) → U2(f268_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f268_out1, .(z0, z1), z2, z3) → f268_out1

Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F268_IN(.(z0, z1), z2, z3) → c11(F268_IN(z1, z0, .(z2, z3)))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:none
K tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F268_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F268_IN(.(z0, z1), z2, z3) → c11(F268_IN(z1, z0, .(z2, z3)))

Defined Rule Symbols:

f2_in, U1, f268_in, U2

Defined Pair Symbols:

F2_IN, F268_IN

Compound Symbols:

c, c11, c

(11) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(12) BOUNDS(O(1), O(1))

(13) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: 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];
5 [label="5: rev(T5, [], T7)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: rev(T5, [], T7), SCOPE: 2, CLAUSE: 1 | rev(T5, [], T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(!_2, eq([], T11)) | rev([], [], T7), SCOPE: 2, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: rev(T5, [], T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX12 is free\nX13 is free\nrev(T5, [], T7) !=? rev([], X12, X13)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: eq([], T11)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: eq([], T11), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(head(T18, X31), ','(tail(T18, X32), rev(X32, .(X31, []), T20)))\n\nT18 is ground\nX12 is free\nX13 is free\nX31 is free\nX32 is free\nrev(T18, [], T7) !=? rev([], X12, X13)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(head(T18, X31), ','(tail(T18, X32), rev(X32, .(X31, []), T20))), SCOPE: 4, CLAUSE: 3 | ','(head(T18, X31), ','(tail(T18, X32), rev(X32, .(X31, []), T20))), SCOPE: 4, CLAUSE: 4\n\nT18 is ground\nX12 is free\nX13 is free\nX31 is free\nX32 is free\nrev(T18, [], T7) !=? rev([], X12, X13)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(head(T18, X31), ','(tail(T18, X32), rev(X32, .(X31, []), T20))), SCOPE: 4, CLAUSE: 4\n\nT18 is ground\nX12 is free\nX13 is free\nX31 is free\nX32 is free\nrev(T18, [], T7) !=? rev([], X12, X13)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(tail(.(T26, T27), X32), rev(X32, .(T26, []), T20))\n\nT26 is ground\nT27 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(tail(.(T26, T27), X32), rev(X32, .(T26, []), T20)), SCOPE: 5, CLAUSE: 5 | ','(tail(.(T26, T27), X32), rev(X32, .(T26, []), T20)), SCOPE: 5, CLAUSE: 6\n\nT26 is ground\nT27 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(tail(.(T26, T27), X32), rev(X32, .(T26, []), T20)), SCOPE: 5, CLAUSE: 6\n\nT26 is ground\nT27 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: rev(T37, .(T36, []), T20)\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: rev(T37, .(T36, []), T20), SCOPE: 6, CLAUSE: 1 | rev(T37, .(T36, []), T20), SCOPE: 6, CLAUSE: 2\n\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(!_6, eq(.(T44, []), T46)) | rev([], .(T44, []), T20), SCOPE: 6, CLAUSE: 2\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: rev(T37, .(T36, []), T20), SCOPE: 6, CLAUSE: 2\n\nT36 is ground\nT37 is ground\nX60 is free\nX61 is free\nrev(T37, .(T36, []), T20) !=? rev([], X60, X61)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: eq(.(T44, []), T46)\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: eq(.(T44, []), T46), SCOPE: 7, CLAUSE: 7\n\nT44 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(head(T59, X79), ','(tail(T59, X80), rev(X80, .(X79, .(T60, [])), T62)))\n\nT59 is ground\nT60 is ground\nX60 is free\nX61 is free\nX79 is free\nX80 is free\nrev(T59, .(T60, []), T20) !=? rev([], X60, X61)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(head(T59, X79), ','(tail(T59, X80), rev(X80, .(X79, .(T60, [])), T62))), SCOPE: 8, CLAUSE: 3 | ','(head(T59, X79), ','(tail(T59, X80), rev(X80, .(X79, .(T60, [])), T62))), SCOPE: 8, CLAUSE: 4\n\nT59 is ground\nT60 is ground\nX60 is free\nX61 is free\nX79 is free\nX80 is free\nrev(T59, .(T60, []), T20) !=? rev([], X60, X61)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(head(T59, X79), ','(tail(T59, X80), rev(X80, .(X79, .(T60, [])), T62))), SCOPE: 8, CLAUSE: 4\n\nT59 is ground\nT60 is ground\nX60 is free\nX61 is free\nX79 is free\nX80 is free\nrev(T59, .(T60, []), T20) !=? rev([], X60, X61)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(tail(.(T69, T70), X80), rev(X80, .(T69, .(T60, [])), T62))\n\nT60 is ground\nT69 is ground\nT70 is ground\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(tail(.(T69, T70), X80), rev(X80, .(T69, .(T60, [])), T62)), SCOPE: 9, CLAUSE: 5 | ','(tail(.(T69, T70), X80), rev(X80, .(T69, .(T60, [])), T62)), SCOPE: 9, CLAUSE: 6\n\nT60 is ground\nT69 is ground\nT70 is ground\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(tail(.(T69, T70), X80), rev(X80, .(T69, .(T60, [])), T62)), SCOPE: 9, CLAUSE: 6\n\nT60 is ground\nT69 is ground\nT70 is ground\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: rev(T82, .(T81, .(T60, [])), T62)\n\nT60 is ground\nT81 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: rev(T82, .(T81, .(T60, [])), T62), SCOPE: 10, CLAUSE: 1 | rev(T82, .(T81, .(T60, [])), T62), SCOPE: 10, CLAUSE: 2\n\nT60 is ground\nT81 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(!_10, eq(.(T92, .(T93, [])), T95)) | rev([], .(T92, .(T93, [])), T62), SCOPE: 10, CLAUSE: 2\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: rev(T82, .(T81, .(T60, [])), T62), SCOPE: 10, CLAUSE: 2\n\nT60 is ground\nT81 is ground\nT82 is ground\nX108 is free\nX109 is free\nrev(T82, .(T81, .(T60, [])), T62) !=? rev([], X108, X109)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: eq(.(T92, .(T93, [])), T95)\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: eq(.(T92, .(T93, [])), T95), SCOPE: 11, CLAUSE: 7\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(head(T114, X127), ','(tail(T114, X128), rev(X128, .(X127, .(T115, .(T116, []))), T118)))\n\nT114 is ground\nT115 is ground\nT116 is ground\nX108 is free\nX109 is free\nX127 is free\nX128 is free\nrev(T114, .(T115, .(T116, [])), T62) !=? rev([], X108, X109)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(head(T114, X127), ','(tail(T114, X128), rev(X128, .(X127, .(T115, .(T116, []))), T118))), SCOPE: 12, CLAUSE: 3 | ','(head(T114, X127), ','(tail(T114, X128), rev(X128, .(X127, .(T115, .(T116, []))), T118))), SCOPE: 12, CLAUSE: 4\n\nT114 is ground\nT115 is ground\nT116 is ground\nX108 is free\nX109 is free\nX127 is free\nX128 is free\nrev(T114, .(T115, .(T116, [])), T62) !=? rev([], X108, X109)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(head(T114, X127), ','(tail(T114, X128), rev(X128, .(X127, .(T115, .(T116, []))), T118))), SCOPE: 12, CLAUSE: 4\n\nT114 is ground\nT115 is ground\nT116 is ground\nX108 is free\nX109 is free\nX127 is free\nX128 is free\nrev(T114, .(T115, .(T116, [])), T62) !=? rev([], X108, X109)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(tail(.(T126, T127), X128), rev(X128, .(T126, .(T115, .(T116, []))), T118))\n\nT115 is ground\nT116 is ground\nT126 is ground\nT127 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(tail(.(T126, T127), X128), rev(X128, .(T126, .(T115, .(T116, []))), T118)), SCOPE: 13, CLAUSE: 5 | ','(tail(.(T126, T127), X128), rev(X128, .(T126, .(T115, .(T116, []))), T118)), SCOPE: 13, CLAUSE: 6\n\nT115 is ground\nT116 is ground\nT126 is ground\nT127 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(tail(.(T126, T127), X128), rev(X128, .(T126, .(T115, .(T116, []))), T118)), SCOPE: 13, CLAUSE: 6\n\nT115 is ground\nT116 is ground\nT126 is ground\nT127 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: rev(T141, .(T140, .(T115, .(T116, []))), T118)\n\nT115 is ground\nT116 is ground\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: rev(T141, .(T140, .(T115, .(T116, []))), T118), SCOPE: 14, CLAUSE: 1 | rev(T141, .(T140, .(T115, .(T116, []))), T118), SCOPE: 14, CLAUSE: 2\n\nT115 is ground\nT116 is ground\nT140 is ground\nT141 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(!_14, eq(.(T154, .(T155, .(T156, []))), T158)) | rev([], .(T154, .(T155, .(T156, []))), T118), SCOPE: 14, CLAUSE: 2\n\nT154 is ground\nT155 is ground\nT156 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: rev(T141, .(T140, .(T115, .(T116, []))), T118), SCOPE: 14, CLAUSE: 2\n\nT115 is ground\nT116 is ground\nT140 is ground\nT141 is ground\nX156 is free\nX157 is free\nrev(T141, .(T140, .(T115, .(T116, []))), T118) !=? rev([], X156, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: eq(.(T154, .(T155, .(T156, []))), T158)\n\nT154 is ground\nT155 is ground\nT156 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: eq(.(T154, .(T155, .(T156, []))), T158), SCOPE: 15, CLAUSE: 7\n\nT154 is ground\nT155 is ground\nT156 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(head(T183, X175), ','(tail(T183, X176), rev(X176, .(X175, .(T184, .(T185, .(T186, [])))), T188)))\n\nT183 is ground\nT184 is ground\nT185 is ground\nT186 is ground\nX156 is free\nX157 is free\nX175 is free\nX176 is free\nrev(T183, .(T184, .(T185, .(T186, []))), T118) !=? rev([], X156, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(head(T183, X175), ','(tail(T183, X176), rev(X176, .(X175, .(T184, .(T185, .(T186, [])))), T188))), SCOPE: 16, CLAUSE: 3 | ','(head(T183, X175), ','(tail(T183, X176), rev(X176, .(X175, .(T184, .(T185, .(T186, [])))), T188))), SCOPE: 16, CLAUSE: 4\n\nT183 is ground\nT184 is ground\nT185 is ground\nT186 is ground\nX156 is free\nX157 is free\nX175 is free\nX176 is free\nrev(T183, .(T184, .(T185, .(T186, []))), T118) !=? rev([], X156, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(head(T183, X175), ','(tail(T183, X176), rev(X176, .(X175, .(T184, .(T185, .(T186, [])))), T188))), SCOPE: 16, CLAUSE: 4\n\nT183 is ground\nT184 is ground\nT185 is ground\nT186 is ground\nX156 is free\nX157 is free\nX175 is free\nX176 is free\nrev(T183, .(T184, .(T185, .(T186, []))), T118) !=? rev([], X156, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(tail(.(T197, T198), X176), rev(X176, .(T197, .(T184, .(T185, .(T186, [])))), T188))\n\nT184 is ground\nT185 is ground\nT186 is ground\nT197 is ground\nT198 is ground\nX176 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(tail(.(T197, T198), X176), rev(X176, .(T197, .(T184, .(T185, .(T186, [])))), T188)), SCOPE: 17, CLAUSE: 5 | ','(tail(.(T197, T198), X176), rev(X176, .(T197, .(T184, .(T185, .(T186, [])))), T188)), SCOPE: 17, CLAUSE: 6\n\nT184 is ground\nT185 is ground\nT186 is ground\nT197 is ground\nT198 is ground\nX176 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(tail(.(T197, T198), X176), rev(X176, .(T197, .(T184, .(T185, .(T186, [])))), T188)), SCOPE: 17, CLAUSE: 6\n\nT184 is ground\nT185 is ground\nT186 is ground\nT197 is ground\nT198 is ground\nX176 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: rev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188)\n\nT184 is ground\nT185 is ground\nT186 is ground\nT213 is ground\nT214 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: rev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188), SCOPE: 18, CLAUSE: 1 | rev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188), SCOPE: 18, CLAUSE: 2\n\nT184 is ground\nT185 is ground\nT186 is ground\nT213 is ground\nT214 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(!_18, eq(.(T230, .(T231, .(T232, .(T233, [])))), T235)) | rev([], .(T230, .(T231, .(T232, .(T233, [])))), T188), SCOPE: 18, CLAUSE: 2\n\nT230 is ground\nT231 is ground\nT232 is ground\nT233 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: rev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188), SCOPE: 18, CLAUSE: 2\n\nT184 is ground\nT185 is ground\nT186 is ground\nT213 is ground\nT214 is ground\nX204 is free\nX205 is free\nrev(T214, .(T213, .(T184, .(T185, .(T186, [])))), T188) !=? rev([], X204, X205)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: eq(.(T230, .(T231, .(T232, .(T233, [])))), T235)\n\nT230 is ground\nT231 is ground\nT232 is ground\nT233 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: eq(.(T230, .(T231, .(T232, .(T233, [])))), T235), SCOPE: 19, CLAUSE: 7\n\nT230 is ground\nT231 is ground\nT232 is ground\nT233 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(head(T266, X223), ','(tail(T266, X224), rev(X224, .(X223, .(T267, .(T268, .(T269, .(T270, []))))), T272)))\n\nT266 is ground\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nX204 is free\nX205 is free\nX223 is free\nX224 is free\nrev(T266, .(T267, .(T268, .(T269, .(T270, [])))), T188) !=? rev([], X204, X205)", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(head(T266, X223), ','(tail(T266, X224), rev(X224, .(X223, .(T267, .(T268, .(T269, .(T270, []))))), T272))), SCOPE: 20, CLAUSE: 3 | ','(head(T266, X223), ','(tail(T266, X224), rev(X224, .(X223, .(T267, .(T268, .(T269, .(T270, []))))), T272))), SCOPE: 20, CLAUSE: 4\n\nT266 is ground\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nX204 is free\nX205 is free\nX223 is free\nX224 is free\nrev(T266, .(T267, .(T268, .(T269, .(T270, [])))), T188) !=? rev([], X204, X205)", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(head(T266, X223), ','(tail(T266, X224), rev(X224, .(X223, .(T267, .(T268, .(T269, .(T270, []))))), T272))), SCOPE: 20, CLAUSE: 4\n\nT266 is ground\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nX204 is free\nX205 is free\nX223 is free\nX224 is free\nrev(T266, .(T267, .(T268, .(T269, .(T270, [])))), T188) !=? rev([], X204, X205)", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(tail(.(T282, T283), X224), rev(X224, .(T282, .(T267, .(T268, .(T269, .(T270, []))))), T272))\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT282 is ground\nT283 is ground\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: ','(tail(.(T282, T283), X224), rev(X224, .(T282, .(T267, .(T268, .(T269, .(T270, []))))), T272)), SCOPE: 21, CLAUSE: 5 | ','(tail(.(T282, T283), X224), rev(X224, .(T282, .(T267, .(T268, .(T269, .(T270, []))))), T272)), SCOPE: 21, CLAUSE: 6\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT282 is ground\nT283 is ground\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(tail(.(T282, T283), X224), rev(X224, .(T282, .(T267, .(T268, .(T269, .(T270, []))))), T272)), SCOPE: 21, CLAUSE: 6\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT282 is ground\nT283 is ground\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: rev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272)\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT300 is ground\nT301 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: rev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272), SCOPE: 22, CLAUSE: 1 | rev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272), SCOPE: 22, CLAUSE: 2\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT300 is ground\nT301 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(!_22, eq(.(T320, .(T321, .(T322, .(T323, .(T324, []))))), T326)) | rev([], .(T320, .(T321, .(T322, .(T323, .(T324, []))))), T272), SCOPE: 22, CLAUSE: 2\n\nT320 is ground\nT321 is ground\nT322 is ground\nT323 is ground\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: rev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272), SCOPE: 22, CLAUSE: 2\n\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT300 is ground\nT301 is ground\nX252 is free\nX253 is free\nrev(T301, .(T300, .(T267, .(T268, .(T269, .(T270, []))))), T272) !=? rev([], X252, X253)", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: eq(.(T320, .(T321, .(T322, .(T323, .(T324, []))))), T326)\n\nT320 is ground\nT321 is ground\nT322 is ground\nT323 is ground\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: eq(.(T320, .(T321, .(T322, .(T323, .(T324, []))))), T326), SCOPE: 23, CLAUSE: 7\n\nT320 is ground\nT321 is ground\nT322 is ground\nT323 is ground\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ','(head(T363, X271), ','(tail(T363, X272), rev(X272, .(X271, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)))\n\nT363 is ground\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nX252 is free\nX253 is free\nX271 is free\nX272 is free\nrev(T363, .(T364, .(T365, .(T366, .(T367, .(T368, []))))), T272) !=? rev([], X252, X253)", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ','(head(T363, X271), ','(tail(T363, X272), rev(X272, .(X271, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370))), SCOPE: 24, CLAUSE: 3 | ','(head(T363, X271), ','(tail(T363, X272), rev(X272, .(X271, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370))), SCOPE: 24, CLAUSE: 4\n\nT363 is ground\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nX252 is free\nX253 is free\nX271 is free\nX272 is free\nrev(T363, .(T364, .(T365, .(T366, .(T367, .(T368, []))))), T272) !=? rev([], X252, X253)", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(head(T363, X271), ','(tail(T363, X272), rev(X272, .(X271, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370))), SCOPE: 24, CLAUSE: 4\n\nT363 is ground\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nX252 is free\nX253 is free\nX271 is free\nX272 is free\nrev(T363, .(T364, .(T365, .(T366, .(T367, .(T368, []))))), T272) !=? rev([], X252, X253)", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(tail(.(T381, T382), X272), rev(X272, .(T381, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370))\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT381 is ground\nT382 is ground\nX272 is free", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(tail(.(T381, T382), X272), rev(X272, .(T381, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)), SCOPE: 25, CLAUSE: 5 | ','(tail(.(T381, T382), X272), rev(X272, .(T381, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)), SCOPE: 25, CLAUSE: 6\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT381 is ground\nT382 is ground\nX272 is free", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(tail(.(T381, T382), X272), rev(X272, .(T381, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)), SCOPE: 25, CLAUSE: 6\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT381 is ground\nT382 is ground\nX272 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: rev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370)\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT401 is ground\nT402 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: rev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370), SCOPE: 26, CLAUSE: 1 | rev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370), SCOPE: 26, CLAUSE: 2\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT401 is ground\nT402 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ','(!_26, eq(.(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))), T431)) | rev([], .(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))), T370), SCOPE: 26, CLAUSE: 2\n\nT424 is ground\nT425 is ground\nT426 is ground\nT427 is ground\nT428 is ground\nT429 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: rev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370), SCOPE: 26, CLAUSE: 2\n\nT364 is ground\nT365 is ground\nT366 is ground\nT367 is ground\nT368 is ground\nT401 is ground\nT402 is ground\nX300 is free\nX301 is free\nrev(T402, .(T401, .(T364, .(T365, .(T366, .(T367, .(T368, [])))))), T370) !=? rev([], X300, X301)", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: eq(.(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))), T431)\n\nT424 is ground\nT425 is ground\nT426 is ground\nT427 is ground\nT428 is ground\nT429 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: eq(.(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))), T431), SCOPE: 27, CLAUSE: 7\n\nT424 is ground\nT425 is ground\nT426 is ground\nT427 is ground\nT428 is ground\nT429 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(head(T474, X319), ','(tail(T474, X320), rev(X320, .(X319, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)))\n\nT474 is ground\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nX300 is free\nX301 is free\nX319 is free\nX320 is free\nrev(T474, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))), T370) !=? rev([], X300, X301)", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(head(T474, X319), ','(tail(T474, X320), rev(X320, .(X319, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482))), SCOPE: 28, CLAUSE: 3 | ','(head(T474, X319), ','(tail(T474, X320), rev(X320, .(X319, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482))), SCOPE: 28, CLAUSE: 4\n\nT474 is ground\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nX300 is free\nX301 is free\nX319 is free\nX320 is free\nrev(T474, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))), T370) !=? rev([], X300, X301)", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(head(T474, X319), ','(tail(T474, X320), rev(X320, .(X319, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482))), SCOPE: 28, CLAUSE: 4\n\nT474 is ground\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nX300 is free\nX301 is free\nX319 is free\nX320 is free\nrev(T474, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))), T370) !=? rev([], X300, X301)", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(tail(.(T494, T495), X320), rev(X320, .(T494, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482))\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT494 is ground\nT495 is ground\nX320 is free", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(tail(.(T494, T495), X320), rev(X320, .(T494, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)), SCOPE: 29, CLAUSE: 5 | ','(tail(.(T494, T495), X320), rev(X320, .(T494, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)), SCOPE: 29, CLAUSE: 6\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT494 is ground\nT495 is ground\nX320 is free", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: ','(tail(.(T494, T495), X320), rev(X320, .(T494, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)), SCOPE: 29, CLAUSE: 6\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT494 is ground\nT495 is ground\nX320 is free", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: rev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482)\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT516 is ground\nT517 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: rev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482), SCOPE: 30, CLAUSE: 1 | rev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482), SCOPE: 30, CLAUSE: 2\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT516 is ground\nT517 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(!_30, eq(.(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))), T550)) | rev([], .(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))), T482), SCOPE: 30, CLAUSE: 2\n\nT542 is ground\nT543 is ground\nT544 is ground\nT545 is ground\nT546 is ground\nT547 is ground\nT548 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: rev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482), SCOPE: 30, CLAUSE: 2\n\nT475 is ground\nT476 is ground\nT477 is ground\nT478 is ground\nT479 is ground\nT480 is ground\nT516 is ground\nT517 is ground\nX348 is free\nX349 is free\nrev(T517, .(T516, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, []))))))), T482) !=? rev([], X348, X349)", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: eq(.(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))), T550)\n\nT542 is ground\nT543 is ground\nT544 is ground\nT545 is ground\nT546 is ground\nT547 is ground\nT548 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: eq(.(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))), T550), SCOPE: 31, CLAUSE: 7\n\nT542 is ground\nT543 is ground\nT544 is ground\nT545 is ground\nT546 is ground\nT547 is ground\nT548 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: ','(head(T599, X367), ','(tail(T599, X368), rev(X368, .(X367, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)))\n\nT599 is ground\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nX348 is free\nX349 is free\nX367 is free\nX368 is free\nrev(T599, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T482) !=? rev([], X348, X349)", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: ','(head(T599, X367), ','(tail(T599, X368), rev(X368, .(X367, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608))), SCOPE: 32, CLAUSE: 3 | ','(head(T599, X367), ','(tail(T599, X368), rev(X368, .(X367, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608))), SCOPE: 32, CLAUSE: 4\n\nT599 is ground\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nX348 is free\nX349 is free\nX367 is free\nX368 is free\nrev(T599, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T482) !=? rev([], X348, X349)", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(head(T599, X367), ','(tail(T599, X368), rev(X368, .(X367, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608))), SCOPE: 32, CLAUSE: 4\n\nT599 is ground\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nX348 is free\nX349 is free\nX367 is free\nX368 is free\nrev(T599, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T482) !=? rev([], X348, X349)", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ','(tail(.(T621, T622), X368), rev(X368, .(T621, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608))\n\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nT621 is ground\nT622 is ground\nX368 is free", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: ','(tail(.(T621, T622), X368), rev(X368, .(T621, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)), SCOPE: 33, CLAUSE: 5 | ','(tail(.(T621, T622), X368), rev(X368, .(T621, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)), SCOPE: 33, CLAUSE: 6\n\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nT621 is ground\nT622 is ground\nX368 is free", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: ','(tail(.(T621, T622), X368), rev(X368, .(T621, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)), SCOPE: 33, CLAUSE: 6\n\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nT621 is ground\nT622 is ground\nX368 is free", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: rev(T646, .(T645, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))), T608)\n\nT600 is ground\nT601 is ground\nT602 is ground\nT603 is ground\nT604 is ground\nT605 is ground\nT606 is ground\nT645 is ground\nT646 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: rev(T646, .(T645, T656), T608)\n\nT645 is ground\nT646 is ground\nT656 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: rev(T646, .(T645, T656), T608), SCOPE: 34, CLAUSE: 1 | rev(T646, .(T645, T656), T608), SCOPE: 34, CLAUSE: 2\n\nT645 is ground\nT646 is ground\nT656 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: ','(!_34, eq(.(T666, T667), T669)) | rev([], .(T666, T667), T608), SCOPE: 34, CLAUSE: 2\n\nT666 is ground\nT667 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: rev(T646, .(T645, T656), T608), SCOPE: 34, CLAUSE: 2\n\nT645 is ground\nT646 is ground\nT656 is ground\nX398 is free\nX399 is free\nrev(T646, .(T645, T656), T608) !=? rev([], X398, X399)", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: eq(.(T666, T667), T669)\n\nT666 is ground\nT667 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: eq(.(T666, T667), T669), SCOPE: 35, CLAUSE: 7\n\nT666 is ground\nT667 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: ','(head(T688, X417), ','(tail(T688, X418), rev(X418, .(X417, .(T689, T690)), T692)))\n\nT688 is ground\nT689 is ground\nT690 is ground\nX398 is free\nX399 is free\nX417 is free\nX418 is free\nrev(T688, .(T689, T690), T608) !=? rev([], X398, X399)", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: ','(head(T688, X417), ','(tail(T688, X418), rev(X418, .(X417, .(T689, T690)), T692))), SCOPE: 36, CLAUSE: 3 | ','(head(T688, X417), ','(tail(T688, X418), rev(X418, .(X417, .(T689, T690)), T692))), SCOPE: 36, CLAUSE: 4\n\nT688 is ground\nT689 is ground\nT690 is ground\nX398 is free\nX399 is free\nX417 is free\nX418 is free\nrev(T688, .(T689, T690), T608) !=? rev([], X398, X399)", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: ','(head(T688, X417), ','(tail(T688, X418), rev(X418, .(X417, .(T689, T690)), T692))), SCOPE: 36, CLAUSE: 4\n\nT688 is ground\nT689 is ground\nT690 is ground\nX398 is free\nX399 is free\nX417 is free\nX418 is free\nrev(T688, .(T689, T690), T608) !=? rev([], X398, X399)", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: ','(tail(.(T700, T701), X418), rev(X418, .(T700, .(T689, T690)), T692))\n\nT689 is ground\nT690 is ground\nT700 is ground\nT701 is ground\nX418 is free", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: ','(tail(.(T700, T701), X418), rev(X418, .(T700, .(T689, T690)), T692)), SCOPE: 37, CLAUSE: 5 | ','(tail(.(T700, T701), X418), rev(X418, .(T700, .(T689, T690)), T692)), SCOPE: 37, CLAUSE: 6\n\nT689 is ground\nT690 is ground\nT700 is ground\nT701 is ground\nX418 is free", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: ','(tail(.(T700, T701), X418), rev(X418, .(T700, .(T689, T690)), T692)), SCOPE: 37, CLAUSE: 6\n\nT689 is ground\nT690 is ground\nT700 is ground\nT701 is ground\nX418 is free", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: rev(T715, .(T714, .(T689, T690)), T692)\n\nT689 is ground\nT690 is ground\nT714 is ground\nT715 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 291 [arrowhead = none ];
291 -> 4;

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

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

294 [label="EVAL with clause\nrev([], X12, X13) :- ','(!_2, eq(X12, X13)).\nand substitutionT5 -> [],\nX12 -> [],\nT7 -> T11,\nX13 -> T11,\nT10 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 294 [arrowhead = none ];
294 -> 8;

295 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 295 [arrowhead = none ];
295 -> 9;

296 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 296 [arrowhead = none ];
296 -> 10;

297 [label="ONLY EVAL with clause\nrev(X28, X29, X30) :- ','(head(X28, X31), ','(tail(X28, X32), rev(X32, .(X31, X29), X30))).\nand substitutionT5 -> T18,\nX28 -> T18,\nX29 -> [],\nT7 -> T20,\nX30 -> T20,\nT19 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 297 [arrowhead = none ];
297 -> 17;

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

299 [label="EVAL with clause\neq(X16, X16).\nand substitutionX16 -> [],\nT11 -> []", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 299 [arrowhead = none ];
299 -> 12;

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

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

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

303 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T18, [], T7), rev([], X12, X13))", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 303 [arrowhead = none ];
303 -> 25;

304 [label="EVAL with clause\nhead(.(X42, X43), X42).\nand substitutionX42 -> T26,\nX43 -> T27,\nT18 -> .(T26, T27),\nX31 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 304 [arrowhead = none ];
304 -> 26;

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

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

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

308 [label="ONLY EVAL with clause\ntail(.(X52, X53), X53).\nand substitutionT26 -> T36,\nX52 -> T36,\nT27 -> T37,\nX53 -> T37,\nX32 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 308 [arrowhead = none ];
308 -> 33;

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

310 [label="EVAL with clause\nrev([], X60, X61) :- ','(!_6, eq(X60, X61)).\nand substitutionT37 -> [],\nT36 -> T44,\nX60 -> .(T44, []),\nT20 -> T46,\nX61 -> T46,\nT45 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 310 [arrowhead = none ];
310 -> 39;

311 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 311 [arrowhead = none ];
311 -> 40;

312 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 312 [arrowhead = none ];
312 -> 41;

313 [label="ONLY EVAL with clause\nrev(X76, X77, X78) :- ','(head(X76, X79), ','(tail(X76, X80), rev(X80, .(X79, X77), X78))).\nand substitutionT37 -> T59,\nX76 -> T59,\nT36 -> T60,\nX77 -> .(T60, []),\nT20 -> T62,\nX78 -> T62,\nT61 -> T62", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 313 [arrowhead = none ];
313 -> 55;

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

315 [label="EVAL with clause\neq(X64, X64).\nand substitutionT44 -> T49,\nX64 -> .(T49, []),\nT46 -> .(T49, [])", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 315 [arrowhead = none ];
315 -> 44;

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

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

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

319 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T59, .(T60, []), T20), rev([], X60, X61))", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 319 [arrowhead = none ];
319 -> 57;

320 [label="EVAL with clause\nhead(.(X90, X91), X90).\nand substitutionX90 -> T69,\nX91 -> T70,\nT59 -> .(T69, T70),\nX79 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 320 [arrowhead = none ];
320 -> 59;

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

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

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

324 [label="ONLY EVAL with clause\ntail(.(X100, X101), X101).\nand substitutionT69 -> T81,\nX100 -> T81,\nT70 -> T82,\nX101 -> T82,\nX80 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 324 [arrowhead = none ];
324 -> 67;

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

326 [label="EVAL with clause\nrev([], X108, X109) :- ','(!_10, eq(X108, X109)).\nand substitutionT82 -> [],\nT81 -> T92,\nT60 -> T93,\nX108 -> .(T92, .(T93, [])),\nT62 -> T95,\nX109 -> T95,\nT94 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 326 [arrowhead = none ];
326 -> 72;

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

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

329 [label="ONLY EVAL with clause\nrev(X124, X125, X126) :- ','(head(X124, X127), ','(tail(X124, X128), rev(X128, .(X127, X125), X126))).\nand substitutionT82 -> T114,\nX124 -> T114,\nT81 -> T115,\nT60 -> T116,\nX125 -> .(T115, .(T116, [])),\nT62 -> T118,\nX126 -> T118,\nT117 -> T118", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 329 [arrowhead = none ];
329 -> 87;

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

331 [label="EVAL with clause\neq(X112, X112).\nand substitutionT92 -> T100,\nT93 -> T101,\nX112 -> .(T100, .(T101, [])),\nT95 -> .(T100, .(T101, []))", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 331 [arrowhead = none ];
331 -> 77;

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

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

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

335 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T114, .(T115, .(T116, [])), T62), rev([], X108, X109))", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 335 [arrowhead = none ];
335 -> 89;

336 [label="EVAL with clause\nhead(.(X138, X139), X138).\nand substitutionX138 -> T126,\nX139 -> T127,\nT114 -> .(T126, T127),\nX127 -> T126", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 336 [arrowhead = none ];
336 -> 91;

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

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

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

340 [label="ONLY EVAL with clause\ntail(.(X148, X149), X149).\nand substitutionT126 -> T140,\nX148 -> T140,\nT127 -> T141,\nX149 -> T141,\nX128 -> T141", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 340 [arrowhead = none ];
340 -> 99;

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

342 [label="EVAL with clause\nrev([], X156, X157) :- ','(!_14, eq(X156, X157)).\nand substitutionT141 -> [],\nT140 -> T154,\nT115 -> T155,\nT116 -> T156,\nX156 -> .(T154, .(T155, .(T156, []))),\nT118 -> T158,\nX157 -> T158,\nT157 -> T158", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 342 [arrowhead = none ];
342 -> 104;

343 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 343 [arrowhead = none ];
343 -> 105;

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

345 [label="ONLY EVAL with clause\nrev(X172, X173, X174) :- ','(head(X172, X175), ','(tail(X172, X176), rev(X176, .(X175, X173), X174))).\nand substitutionT141 -> T183,\nX172 -> T183,\nT140 -> T184,\nT115 -> T185,\nT116 -> T186,\nX173 -> .(T184, .(T185, .(T186, []))),\nT118 -> T188,\nX174 -> T188,\nT187 -> T188", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 345 [arrowhead = none ];
345 -> 119;

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

347 [label="EVAL with clause\neq(X160, X160).\nand substitutionT154 -> T165,\nT155 -> T166,\nT156 -> T167,\nX160 -> .(T165, .(T166, .(T167, []))),\nT158 -> .(T165, .(T166, .(T167, [])))", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 347 [arrowhead = none ];
347 -> 109;

348 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 348 [arrowhead = none ];
348 -> 110;

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

350 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
119 -> 350 [arrowhead = none ];
350 -> 120;

351 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T183, .(T184, .(T185, .(T186, []))), T118), rev([], X156, X157))", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 351 [arrowhead = none ];
351 -> 121;

352 [label="EVAL with clause\nhead(.(X186, X187), X186).\nand substitutionX186 -> T197,\nX187 -> T198,\nT183 -> .(T197, T198),\nX175 -> T197", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 352 [arrowhead = none ];
352 -> 123;

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

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

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

356 [label="ONLY EVAL with clause\ntail(.(X196, X197), X197).\nand substitutionT197 -> T213,\nX196 -> T213,\nT198 -> T214,\nX197 -> T214,\nX176 -> T214", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 356 [arrowhead = none ];
356 -> 131;

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

358 [label="EVAL with clause\nrev([], X204, X205) :- ','(!_18, eq(X204, X205)).\nand substitutionT214 -> [],\nT213 -> T230,\nT184 -> T231,\nT185 -> T232,\nT186 -> T233,\nX204 -> .(T230, .(T231, .(T232, .(T233, [])))),\nT188 -> T235,\nX205 -> T235,\nT234 -> T235", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 358 [arrowhead = none ];
358 -> 136;

359 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 359 [arrowhead = none ];
359 -> 138;

360 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 360 [arrowhead = none ];
360 -> 139;

361 [label="ONLY EVAL with clause\nrev(X220, X221, X222) :- ','(head(X220, X223), ','(tail(X220, X224), rev(X224, .(X223, X221), X222))).\nand substitutionT214 -> T266,\nX220 -> T266,\nT213 -> T267,\nT184 -> T268,\nT185 -> T269,\nT186 -> T270,\nX221 -> .(T267, .(T268, .(T269, .(T270, [])))),\nT188 -> T272,\nX222 -> T272,\nT271 -> T272", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 361 [arrowhead = none ];
361 -> 151;

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

363 [label="EVAL with clause\neq(X208, X208).\nand substitutionT230 -> T244,\nT231 -> T245,\nT232 -> T246,\nT233 -> T247,\nX208 -> .(T244, .(T245, .(T246, .(T247, [])))),\nT235 -> .(T244, .(T245, .(T246, .(T247, []))))", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 363 [arrowhead = none ];
363 -> 141;

364 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 364 [arrowhead = none ];
364 -> 142;

365 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 365 [arrowhead = none ];
365 -> 143;

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

367 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T266, .(T267, .(T268, .(T269, .(T270, [])))), T188), rev([], X204, X205))", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 367 [arrowhead = none ];
367 -> 153;

368 [label="EVAL with clause\nhead(.(X234, X235), X234).\nand substitutionX234 -> T282,\nX235 -> T283,\nT266 -> .(T282, T283),\nX223 -> T282", fontsize=14, style = filled, fillcolor = lightblue];
153 -> 368 [arrowhead = none ];
368 -> 155;

369 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
153 -> 369 [arrowhead = none ];
369 -> 156;

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

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

372 [label="ONLY EVAL with clause\ntail(.(X244, X245), X245).\nand substitutionT282 -> T300,\nX244 -> T300,\nT283 -> T301,\nX245 -> T301,\nX224 -> T301", fontsize=14, style = filled, fillcolor = lightblue];
159 -> 372 [arrowhead = none ];
372 -> 163;

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

374 [label="EVAL with clause\nrev([], X252, X253) :- ','(!_22, eq(X252, X253)).\nand substitutionT301 -> [],\nT300 -> T320,\nT267 -> T321,\nT268 -> T322,\nT269 -> T323,\nT270 -> T324,\nX252 -> .(T320, .(T321, .(T322, .(T323, .(T324, []))))),\nT272 -> T326,\nX253 -> T326,\nT325 -> T326", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 374 [arrowhead = none ];
374 -> 168;

375 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
166 -> 375 [arrowhead = none ];
375 -> 170;

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

377 [label="ONLY EVAL with clause\nrev(X268, X269, X270) :- ','(head(X268, X271), ','(tail(X268, X272), rev(X272, .(X271, X269), X270))).\nand substitutionT301 -> T363,\nX268 -> T363,\nT300 -> T364,\nT267 -> T365,\nT268 -> T366,\nT269 -> T367,\nT270 -> T368,\nX269 -> .(T364, .(T365, .(T366, .(T367, .(T368, []))))),\nT272 -> T370,\nX270 -> T370,\nT369 -> T370", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 377 [arrowhead = none ];
377 -> 183;

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

379 [label="EVAL with clause\neq(X256, X256).\nand substitutionT320 -> T337,\nT321 -> T338,\nT322 -> T339,\nT323 -> T340,\nT324 -> T341,\nX256 -> .(T337, .(T338, .(T339, .(T340, .(T341, []))))),\nT326 -> .(T337, .(T338, .(T339, .(T340, .(T341, [])))))", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 379 [arrowhead = none ];
379 -> 173;

380 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 380 [arrowhead = none ];
380 -> 174;

381 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 381 [arrowhead = none ];
381 -> 175;

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

383 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T363, .(T364, .(T365, .(T366, .(T367, .(T368, []))))), T272), rev([], X252, X253))", fontsize=14, style = filled, fillcolor = lightgreen];
184 -> 383 [arrowhead = none ];
383 -> 185;

384 [label="EVAL with clause\nhead(.(X282, X283), X282).\nand substitutionX282 -> T381,\nX283 -> T382,\nT363 -> .(T381, T382),\nX271 -> T381", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 384 [arrowhead = none ];
384 -> 186;

385 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
185 -> 385 [arrowhead = none ];
385 -> 187;

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

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

388 [label="ONLY EVAL with clause\ntail(.(X292, X293), X293).\nand substitutionT381 -> T401,\nX292 -> T401,\nT382 -> T402,\nX293 -> T402,\nX272 -> T402", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 388 [arrowhead = none ];
388 -> 194;

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

390 [label="EVAL with clause\nrev([], X300, X301) :- ','(!_26, eq(X300, X301)).\nand substitutionT402 -> [],\nT401 -> T424,\nT364 -> T425,\nT365 -> T426,\nT366 -> T427,\nT367 -> T428,\nT368 -> T429,\nX300 -> .(T424, .(T425, .(T426, .(T427, .(T428, .(T429, [])))))),\nT370 -> T431,\nX301 -> T431,\nT430 -> T431", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 390 [arrowhead = none ];
390 -> 200;

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

392 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 392 [arrowhead = none ];
392 -> 202;

393 [label="ONLY EVAL with clause\nrev(X316, X317, X318) :- ','(head(X316, X319), ','(tail(X316, X320), rev(X320, .(X319, X317), X318))).\nand substitutionT402 -> T474,\nX316 -> T474,\nT401 -> T475,\nT364 -> T476,\nT365 -> T477,\nT366 -> T478,\nT367 -> T479,\nT368 -> T480,\nX317 -> .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))),\nT370 -> T482,\nX318 -> T482,\nT481 -> T482", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 393 [arrowhead = none ];
393 -> 215;

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

395 [label="EVAL with clause\neq(X304, X304).\nand substitutionT424 -> T444,\nT425 -> T445,\nT426 -> T446,\nT427 -> T447,\nT428 -> T448,\nT429 -> T449,\nX304 -> .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, [])))))),\nT431 -> .(T444, .(T445, .(T446, .(T447, .(T448, .(T449, []))))))", fontsize=14, style = filled, fillcolor = lightblue];
203 -> 395 [arrowhead = none ];
395 -> 205;

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

397 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 397 [arrowhead = none ];
397 -> 207;

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

399 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T474, .(T475, .(T476, .(T477, .(T478, .(T479, .(T480, [])))))), T370), rev([], X300, X301))", fontsize=14, style = filled, fillcolor = lightgreen];
216 -> 399 [arrowhead = none ];
399 -> 217;

400 [label="EVAL with clause\nhead(.(X330, X331), X330).\nand substitutionX330 -> T494,\nX331 -> T495,\nT474 -> .(T494, T495),\nX319 -> T494", fontsize=14, style = filled, fillcolor = lightblue];
217 -> 400 [arrowhead = none ];
400 -> 218;

401 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 401 [arrowhead = none ];
401 -> 219;

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

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

404 [label="ONLY EVAL with clause\ntail(.(X340, X341), X341).\nand substitutionT494 -> T516,\nX340 -> T516,\nT495 -> T517,\nX341 -> T517,\nX320 -> T517", fontsize=14, style = filled, fillcolor = lightblue];
222 -> 404 [arrowhead = none ];
404 -> 227;

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

406 [label="EVAL with clause\nrev([], X348, X349) :- ','(!_30, eq(X348, X349)).\nand substitutionT517 -> [],\nT516 -> T542,\nT475 -> T543,\nT476 -> T544,\nT477 -> T545,\nT478 -> T546,\nT479 -> T547,\nT480 -> T548,\nX348 -> .(T542, .(T543, .(T544, .(T545, .(T546, .(T547, .(T548, []))))))),\nT482 -> T550,\nX349 -> T550,\nT549 -> T550", fontsize=14, style = filled, fillcolor = lightblue];
230 -> 406 [arrowhead = none ];
406 -> 232;

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

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

409 [label="ONLY EVAL with clause\nrev(X364, X365, X366) :- ','(head(X364, X367), ','(tail(X364, X368), rev(X368, .(X367, X365), X366))).\nand substitutionT517 -> T599,\nX364 -> T599,\nT516 -> T600,\nT475 -> T601,\nT476 -> T602,\nT477 -> T603,\nT478 -> T604,\nT479 -> T605,\nT480 -> T606,\nX365 -> .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))),\nT482 -> T608,\nX366 -> T608,\nT607 -> T608", fontsize=14, style = filled, fillcolor = lightblue];
233 -> 409 [arrowhead = none ];
409 -> 247;

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

411 [label="EVAL with clause\neq(X352, X352).\nand substitutionT542 -> T565,\nT543 -> T566,\nT544 -> T567,\nT545 -> T568,\nT546 -> T569,\nT547 -> T570,\nT548 -> T571,\nX352 -> .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, []))))))),\nT550 -> .(T565, .(T566, .(T567, .(T568, .(T569, .(T570, .(T571, [])))))))", fontsize=14, style = filled, fillcolor = lightblue];
236 -> 411 [arrowhead = none ];
411 -> 237;

412 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
236 -> 412 [arrowhead = none ];
412 -> 238;

413 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
237 -> 413 [arrowhead = none ];
413 -> 239;

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

415 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T599, .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, []))))))), T482), rev([], X348, X349))", fontsize=14, style = filled, fillcolor = lightgreen];
248 -> 415 [arrowhead = none ];
415 -> 249;

416 [label="EVAL with clause\nhead(.(X378, X379), X378).\nand substitutionX378 -> T621,\nX379 -> T622,\nT599 -> .(T621, T622),\nX367 -> T621", fontsize=14, style = filled, fillcolor = lightblue];
249 -> 416 [arrowhead = none ];
416 -> 250;

417 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
249 -> 417 [arrowhead = none ];
417 -> 251;

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

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

420 [label="ONLY EVAL with clause\ntail(.(X388, X389), X389).\nand substitutionT621 -> T645,\nX388 -> T645,\nT622 -> T646,\nX389 -> T646,\nX368 -> T646", fontsize=14, style = filled, fillcolor = lightblue];
254 -> 420 [arrowhead = none ];
420 -> 257;

421 [label="GENERALIZATION\nT656 <-- .(T600, .(T601, .(T602, .(T603, .(T604, .(T605, .(T606, [])))))))\n\nNew Knowledge:\nT656 is ground", fontsize=14, style = filled, fillcolor = violet];
257 -> 421 [arrowhead = none ];
421 -> 262;

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

423 [label="EVAL with clause\nrev([], X398, X399) :- ','(!_34, eq(X398, X399)).\nand substitutionT646 -> [],\nT645 -> T666,\nT656 -> T667,\nX398 -> .(T666, T667),\nT608 -> T669,\nX399 -> T669,\nT668 -> T669", fontsize=14, style = filled, fillcolor = lightblue];
264 -> 423 [arrowhead = none ];
423 -> 265;

424 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
264 -> 424 [arrowhead = none ];
424 -> 266;

425 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
265 -> 425 [arrowhead = none ];
425 -> 267;

426 [label="ONLY EVAL with clause\nrev(X414, X415, X416) :- ','(head(X414, X417), ','(tail(X414, X418), rev(X418, .(X417, X415), X416))).\nand substitutionT646 -> T688,\nX414 -> T688,\nT645 -> T689,\nT656 -> T690,\nX415 -> .(T689, T690),\nT608 -> T692,\nX416 -> T692,\nT691 -> T692", fontsize=14, style = filled, fillcolor = lightblue];
266 -> 426 [arrowhead = none ];
426 -> 278;

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

428 [label="EVAL with clause\neq(X402, X402).\nand substitutionT666 -> T674,\nT667 -> T675,\nX402 -> .(T674, T675),\nT669 -> .(T674, T675)", fontsize=14, style = filled, fillcolor = lightblue];
269 -> 428 [arrowhead = none ];
428 -> 270;

429 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
269 -> 429 [arrowhead = none ];
429 -> 271;

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

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

432 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (rev(T688, .(T689, T690), T608), rev([], X398, X399))", fontsize=14, style = filled, fillcolor = lightgreen];
282 -> 432 [arrowhead = none ];
432 -> 283;

433 [label="EVAL with clause\nhead(.(X428, X429), X428).\nand substitutionX428 -> T700,\nX429 -> T701,\nT688 -> .(T700, T701),\nX417 -> T700", fontsize=14, style = filled, fillcolor = lightblue];
283 -> 433 [arrowhead = none ];
433 -> 284;

434 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
283 -> 434 [arrowhead = none ];
434 -> 285;

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

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

437 [label="ONLY EVAL with clause\ntail(.(X438, X439), X439).\nand substitutionT700 -> T714,\nX438 -> T714,\nT701 -> T715,\nX439 -> T715,\nX418 -> T715", fontsize=14, style = filled, fillcolor = lightblue];
287 -> 437 [arrowhead = none ];
437 -> 290;

438 [label="INSTANCE with matching:\nT646 -> T715\nT645 -> T714\nT656 -> .(T689, T690)\nT608 -> T692", fontsize=14, style = filled, fillcolor = lightgrey];
290 -> 438 [arrowhead = none , style=dashed];
438 -> 262[style=dashed];

}

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f262_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f262_in([], z0, z1) → f262_out1
f262_in(.(z0, z1), z2, z3) → U2(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f262_out1, .(z0, z1), z2, z3) → f262_out1

Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F262_IN(.(z0, z1), z2, z3) → c11(U2'(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F262_IN(z1, z0, .(z2, z3)))

S tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F262_IN(.(z0, z1), z2, z3) → c11(U2'(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F262_IN(z1, z0, .(z2, z3)))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f262_in, U2

Defined Pair Symbols:

F1_IN, F262_IN

Compound Symbols:

c8, c11

(15) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f262_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f262_in([], z0, z1) → f262_out1
f262_in(.(z0, z1), z2, z3) → U2(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f262_out1, .(z0, z1), z2, z3) → f262_out1

Tuples:

F262_IN(.(z0, z1), z2, z3) → c11(U2'(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F262_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))

S tuples:

F262_IN(.(z0, z1), z2, z3) → c11(U2'(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3), F262_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f262_in, U2

Defined Pair Symbols:

F262_IN, F1_IN

Compound Symbols:

c11, c

(17) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f262_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f262_in([], z0, z1) → f262_out1
f262_in(.(z0, z1), z2, z3) → U2(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f262_out1, .(z0, z1), z2, z3) → f262_out1

Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F262_IN(.(z0, z1), z2, z3) → c11(F262_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F262_IN(.(z0, z1), z2, z3) → c11(F262_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f262_in, U2

Defined Pair Symbols:

F1_IN, F262_IN

Compound Symbols:

c, c11, c

(19) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f262_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f262_in([], z0, z1) → f262_out1
f262_in(.(z0, z1), z2, z3) → U2(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f262_out1, .(z0, z1), z2, z3) → f262_out1

Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F262_IN(.(z0, z1), z2, z3) → c11(F262_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F262_IN(.(z0, z1), z2, z3) → c11(F262_IN(z1, z0, .(z2, z3)))

K tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

Defined Rule Symbols:

f1_in, U1, f262_in, U2

Defined Pair Symbols:

F1_IN, F262_IN

Compound Symbols:

c, c11, c

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F262_IN(.(z0, z1), z2, z3) → c11(F262_IN(z1, z0, .(z2, z3)))

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F262_IN(.(z0, z1), z2, z3) → c11(F262_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [3] + x₂   
POL(F1_IN(x₁)) = [3]x₁   
POL(F262_IN(x₁, x₂, x₃)) = [3]x₁ + x₃   
POL([]) = [2]   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c11(x₁)) = x₁   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, []))) → f1_out1
f1_in(.(z0, .(z1, .(z2, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f262_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f262_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f262_in([], z0, z1) → f262_out1
f262_in(.(z0, z1), z2, z3) → U2(f262_in(z1, z0, .(z2, z3)), .(z0, z1), z2, z3)
U2(f262_out1, .(z0, z1), z2, z3) → f262_out1

Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F262_IN(.(z0, z1), z2, z3) → c11(F262_IN(z1, z0, .(z2, z3)))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:none
K tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F262_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, [])))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F262_IN(.(z0, z1), z2, z3) → c11(F262_IN(z1, z0, .(z2, z3)))

Defined Rule Symbols:

f1_in, U1, f262_in, U2

Defined Pair Symbols:

F1_IN, F262_IN

Compound Symbols:

c, c11, c