Left Termination proof of /tmp/tmpThtBzd/gopher2.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 275 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 0 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 TRUE

(0) Obligation:

Clauses:

gopher(nil, nil).
gopher(X, cons(nil, T)) :- ','(no(empty(X)), ','(head(X, nil), tail(X, T))).
gopher(X, Y) :- ','(no(empty(X)), ','(head(X, H), ','(no(empty(H)), ','(head(H, U), ','(tail(H, V), ','(tail(X, W), gopher(cons(U, cons(V, W)), Y))))))).
head([], X1).
head(.(X, X2), X).
tail([], []).
tail(.(X3, X), X).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: gopher(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: gopher(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: gopher(T1, T2), SCOPE: 1, CLAUSE: 0 | gopher(T1, T2), SCOPE: 1, CLAUSE: 1 | gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true | gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: gopher(T1, T2), SCOPE: 1, CLAUSE: 1 | gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ngopher(T1, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))) | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\nX7 is free\nX8 is free\ngopher(nil, T2) !=? gopher(X7, cons(nil, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 8 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(','(call(empty(nil)), ','(!_2, failure(a))), ','(head(nil, nil), tail(nil, T5))) | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(empty(nil), ','(','(!_2, failure(a)), ','(head(nil, nil), tail(nil, T5)))) | ?_3 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(empty(nil), ','(','(!_2, failure(a)), ','(head(nil, nil), tail(nil, T5)))), SCOPE: 4, CLAUSE: 7 | ?_4 | ?_3 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ?_4 | ?_3 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ?_3 | ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9 | ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(head(nil, nil), tail(nil, T5))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(head(nil, nil), tail(nil, T5)), SCOPE: 5, CLAUSE: 3 | ','(head(nil, nil), tail(nil, T5)), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(head(nil, nil), tail(nil, T5)), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))))\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 8 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(','(call(empty(nil)), ','(!_6, failure(a))), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))) | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(empty(nil), ','(','(!_6, failure(a)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))))) | ?_7 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(empty(nil), ','(','(!_6, failure(a)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))))), SCOPE: 8, CLAUSE: 7 | ?_8 | ?_7 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ?_8 | ?_7 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ?_7 | ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(no(empty(nil)), ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))), SCOPE: 6, CLAUSE: 9\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10))))))\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))), SCOPE: 9, CLAUSE: 3 | ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))), SCOPE: 9, CLAUSE: 4\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(head(nil, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(nil, X33), gopher(cons(X31, cons(X32, X33)), T10)))))), SCOPE: 9, CLAUSE: 4\n\nX30 is free\nX31 is free\nX32 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))))\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 8 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(','(call(empty(nil)), ','(!_10, failure(a))), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))) | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(empty(nil), ','(','(!_10, failure(a)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))))) | ?_11 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(empty(nil), ','(','(!_10, failure(a)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))))), SCOPE: 12, CLAUSE: 7 | ?_12 | ?_11 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ?_12 | ?_11 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ?_11 | ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(no(empty(nil)), ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))), SCOPE: 10, CLAUSE: 9\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13))))))\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))), SCOPE: 13, CLAUSE: 3 | ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))), SCOPE: 13, CLAUSE: 4\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: ','(head(nil, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(nil, X50), gopher(cons(X48, cons(X49, X50)), T13)))))), SCOPE: 13, CLAUSE: 4\n\nX47 is free\nX48 is free\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(no(empty(T16)), ','(head(T16, nil), tail(T16, T18))) | gopher(T16, T2), SCOPE: 1, CLAUSE: 2\n\nT16 is ground\ngopher(T16, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX62 is free\nX63 is free\ngopher(T1, T2) !=? gopher(nil, nil)\ngopher(T1, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ','(no(empty(T16)), ','(head(T16, nil), tail(T16, T18))), SCOPE: 14, CLAUSE: 8 | ','(no(empty(T16)), ','(head(T16, nil), tail(T16, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T16, T2), SCOPE: 1, CLAUSE: 2\n\nT16 is ground\ngopher(T16, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ','(','(call(empty(T21)), ','(!_14, failure(a))), ','(head(T21, nil), tail(T21, T18))) | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(empty(T21), ','(','(!_14, failure(a)), ','(head(T21, nil), tail(T21, T18)))) | ?_15 | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(empty(T21), ','(','(!_14, failure(a)), ','(head(T21, nil), tail(T21, T18)))), SCOPE: 16, CLAUSE: 7 | ?_16 | ?_15 | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ','(','(!_14, failure(a)), ','(head([], nil), tail([], T18))) | ?_16 | ?_15 | ','(no(empty([])), ','(head([], nil), tail([], T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ?_16 | ?_15 | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(failure(a), ','(head([], nil), tail([], T18))) | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(failure(a), ','(head([], nil), tail([], T18)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(failure(a), ','(head([], nil), tail([], T18))), SCOPE: 17, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26)))))))\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 8 | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(','(call(empty([])), ','(!_18, failure(a))), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))) | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(empty([]), ','(','(!_18, failure(a)), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26)))))))) | ?_19 | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ','(empty([]), ','(','(!_18, failure(a)), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26)))))))), SCOPE: 20, CLAUSE: 7 | ?_20 | ?_19 | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ','(','(!_18, failure(a)), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))) | ?_20 | ?_19 | ','(no(empty([])), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 18, CLAUSE: 9\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(failure(a), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26)))))))\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(failure(a), ','(head([], X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail([], X80), gopher(cons(X78, cons(X79, X80)), T26))))))), SCOPE: 21, CLAUSE: 10\n\nX77 is free\nX78 is free\nX79 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ?_15 | ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: ','(no(empty(T21)), ','(head(T21, nil), tail(T21, T18))), SCOPE: 14, CLAUSE: 9\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: ?_14 | gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(head(T31, nil), tail(T31, T18))\n\nT31 is ground\ngopher(T31, T2) !=? gopher(nil, nil)\nempty(T31) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: ','(head(T31, nil), tail(T31, T18)), SCOPE: 22, CLAUSE: 3 | ','(head(T31, nil), tail(T31, T18)), SCOPE: 22, CLAUSE: 4\n\nT31 is ground\ngopher(T31, T2) !=? gopher(nil, nil)\nempty(T31) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: ','(head(T31, nil), tail(T31, T18)), SCOPE: 22, CLAUSE: 4\n\nT31 is ground\ngopher(T31, T2) !=? gopher(nil, nil)\nempty(T31) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: tail(.(nil, T37), T18)\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: tail(.(nil, T37), T18), SCOPE: 23, CLAUSE: 5 | tail(.(nil, T37), T18), SCOPE: 23, CLAUSE: 6\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: tail(.(nil, T37), T18), SCOPE: 23, CLAUSE: 6\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: gopher(T21, T2), SCOPE: 1, CLAUSE: 2\n\nT21 is ground\ngopher(T21, T2) !=? gopher(nil, nil)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: ','(no(empty(T46)), ','(head(T46, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T46, X115), gopher(cons(X113, cons(X114, X115)), T48)))))))\n\nT46 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T46, T2) !=? gopher(nil, nil)\nempty(T46) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: ','(no(empty(T46)), ','(head(T46, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T46, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 8 | ','(no(empty(T46)), ','(head(T46, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T46, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT46 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T46, T2) !=? gopher(nil, nil)\nempty(T46) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(','(call(empty(T51)), ','(!_24, failure(a))), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))) | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ','(empty(T51), ','(','(!_24, failure(a)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48)))))))) | ?_25 | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: ','(empty(T51), ','(','(!_24, failure(a)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48)))))))), SCOPE: 26, CLAUSE: 7 | ?_26 | ?_25 | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: ?_26 | ?_25 | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: ?_25 | ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: ','(no(empty(T51)), ','(head(T51, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T51, X115), gopher(cons(X113, cons(X114, X115)), T48))))))), SCOPE: 24, CLAUSE: 9\n\nT51 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T51, T2) !=? gopher(nil, nil)\nempty(T51) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: ','(head(T54, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T54, X115), gopher(cons(X113, cons(X114, X115)), T48))))))\n\nT54 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T54, T2) !=? gopher(nil, nil)\nempty(T54) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(head(T54, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T54, X115), gopher(cons(X113, cons(X114, X115)), T48)))))), SCOPE: 27, CLAUSE: 3 | ','(head(T54, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T54, X115), gopher(cons(X113, cons(X114, X115)), T48)))))), SCOPE: 27, CLAUSE: 4\n\nT54 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T54, T2) !=? gopher(nil, nil)\nempty(T54) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: ','(head(T54, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(T54, X115), gopher(cons(X113, cons(X114, X115)), T48)))))), SCOPE: 27, CLAUSE: 4\n\nT54 is ground\nX112 is free\nX113 is free\nX114 is free\nX115 is free\ngopher(T54, T2) !=? gopher(nil, nil)\nempty(T54) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: ','(no(empty(T59)), ','(head(T59, X113), ','(tail(T59, X114), ','(tail(.(T59, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))))\n\nT59 is ground\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: ','(no(empty(T59)), ','(head(T59, X113), ','(tail(T59, X114), ','(tail(.(T59, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 8 | ','(no(empty(T59)), ','(head(T59, X113), ','(tail(T59, X114), ','(tail(.(T59, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT59 is ground\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: ','(','(call(empty(T63)), ','(!_28, failure(a))), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))) | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: ','(empty(T63), ','(','(!_28, failure(a)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))))) | ?_29 | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: ','(empty(T63), ','(','(!_28, failure(a)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))))), SCOPE: 30, CLAUSE: 7 | ?_30 | ?_29 | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: ','(','(!_28, failure(a)), ','(head([], X113), ','(tail([], X114), ','(tail(.([], T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))) | ?_30 | ?_29 | ','(no(empty([])), ','(head([], X113), ','(tail([], X114), ','(tail(.([], T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: ?_30 | ?_29 | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T63) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: ','(failure(a), ','(head([], X113), ','(tail([], X114), ','(tail(.([], T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))))\n\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: ','(failure(a), ','(head([], X113), ','(tail([], X114), ','(tail(.([], T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 31, CLAUSE: 10\n\nT60 is ground\nX113 is free\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: ?_29 | ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T63) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: ','(no(empty(T63)), ','(head(T63, X113), ','(tail(T63, X114), ','(tail(.(T63, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))), SCOPE: 28, CLAUSE: 9\n\nT60 is ground\nT63 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T63) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: ','(head(T66, X113), ','(tail(T66, X114), ','(tail(.(T66, T60), X115), gopher(cons(X113, cons(X114, X115)), T48))))\n\nT60 is ground\nT66 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: ','(head(T66, X113), ','(tail(T66, X114), ','(tail(.(T66, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))), SCOPE: 32, CLAUSE: 3 | ','(head(T66, X113), ','(tail(T66, X114), ','(tail(.(T66, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))), SCOPE: 32, CLAUSE: 4\n\nT60 is ground\nT66 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: ','(head(T66, X113), ','(tail(T66, X114), ','(tail(.(T66, T60), X115), gopher(cons(X113, cons(X114, X115)), T48)))), SCOPE: 32, CLAUSE: 4\n\nT60 is ground\nT66 is ground\nX113 is free\nX114 is free\nX115 is free\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: ','(tail(.(T71, T72), X114), ','(tail(.(.(T71, T72), T60), X115), gopher(cons(T71, cons(X114, X115)), T48)))\n\nT60 is ground\nT71 is ground\nT72 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: ','(tail(.(T71, T72), X114), ','(tail(.(.(T71, T72), T60), X115), gopher(cons(T71, cons(X114, X115)), T48))), SCOPE: 33, CLAUSE: 5 | ','(tail(.(T71, T72), X114), ','(tail(.(.(T71, T72), T60), X115), gopher(cons(T71, cons(X114, X115)), T48))), SCOPE: 33, CLAUSE: 6\n\nT60 is ground\nT71 is ground\nT72 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: ','(tail(.(T71, T72), X114), ','(tail(.(.(T71, T72), T60), X115), gopher(cons(T71, cons(X114, X115)), T48))), SCOPE: 33, CLAUSE: 6\n\nT60 is ground\nT71 is ground\nT72 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: ','(tail(.(.(T77, T78), T60), X115), gopher(cons(T77, cons(T78, X115)), T48))\n\nT60 is ground\nT77 is ground\nT78 is ground\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: ','(tail(.(.(T77, T78), T60), X115), gopher(cons(T77, cons(T78, X115)), T48)), SCOPE: 34, CLAUSE: 5 | ','(tail(.(.(T77, T78), T60), X115), gopher(cons(T77, cons(T78, X115)), T48)), SCOPE: 34, CLAUSE: 6\n\nT60 is ground\nT77 is ground\nT78 is ground\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: ','(tail(.(.(T77, T78), T60), X115), gopher(cons(T77, cons(T78, X115)), T48)), SCOPE: 34, CLAUSE: 6\n\nT60 is ground\nT77 is ground\nT78 is ground\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: gopher(cons(T85, cons(T86, T87)), T48)\n\nT85 is ground\nT86 is ground\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: ','(no(empty(T90)), ','(head(T90, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T90, X163), gopher(cons(X161, cons(X162, X163)), T92)))))))\n\nT90 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T90, T2) !=? gopher(nil, nil)\ngopher(T90, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: ','(no(empty(T90)), ','(head(T90, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T90, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 8 | ','(no(empty(T90)), ','(head(T90, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T90, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT90 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T90, T2) !=? gopher(nil, nil)\ngopher(T90, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: ','(','(call(empty(T95)), ','(!_35, failure(a))), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))) | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: ','(empty(T95), ','(','(!_35, failure(a)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92)))))))) | ?_36 | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: ','(empty(T95), ','(','(!_35, failure(a)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92)))))))), SCOPE: 37, CLAUSE: 7 | ?_37 | ?_36 | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: ','(','(!_35, failure(a)), ','(head([], X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail([], X163), gopher(cons(X161, cons(X162, X163)), T92))))))) | ?_37 | ?_36 | ','(no(empty([])), ','(head([], X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail([], X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nX160 is free\nX161 is free\nX162 is free\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="327: ?_37 | ?_36 | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))\nempty(T95) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: ','(failure(a), ','(head([], X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail([], X163), gopher(cons(X161, cons(X162, X163)), T92)))))))\n\nX160 is free\nX161 is free\nX162 is free\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: ','(failure(a), ','(head([], X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail([], X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 38, CLAUSE: 10\n\nX160 is free\nX161 is free\nX162 is free\nX163 is free", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: ?_36 | ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))\nempty(T95) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: ','(no(empty(T95)), ','(head(T95, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T95, X163), gopher(cons(X161, cons(X162, X163)), T92))))))), SCOPE: 35, CLAUSE: 9\n\nT95 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T95, T2) !=? gopher(nil, nil)\ngopher(T95, T2) !=? gopher(X62, cons(nil, X63))\nempty(T95) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
337 [label="337: ','(head(T98, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T98, X163), gopher(cons(X161, cons(X162, X163)), T92))))))\n\nT98 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T98, T2) !=? gopher(nil, nil)\ngopher(T98, T2) !=? gopher(X62, cons(nil, X63))\nempty(T98) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: ','(head(T98, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T98, X163), gopher(cons(X161, cons(X162, X163)), T92)))))), SCOPE: 39, CLAUSE: 3 | ','(head(T98, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T98, X163), gopher(cons(X161, cons(X162, X163)), T92)))))), SCOPE: 39, CLAUSE: 4\n\nT98 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T98, T2) !=? gopher(nil, nil)\ngopher(T98, T2) !=? gopher(X62, cons(nil, X63))\nempty(T98) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: ','(head(T98, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(T98, X163), gopher(cons(X161, cons(X162, X163)), T92)))))), SCOPE: 39, CLAUSE: 4\n\nT98 is ground\nX62 is free\nX63 is free\nX160 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(T98, T2) !=? gopher(nil, nil)\ngopher(T98, T2) !=? gopher(X62, cons(nil, X63))\nempty(T98) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: ','(no(empty(T103)), ','(head(T103, X161), ','(tail(T103, X162), ','(tail(.(T103, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))))\n\nT103 is ground\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T103, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
358 [label="358: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
361 [label="361: ','(no(empty(T103)), ','(head(T103, X161), ','(tail(T103, X162), ','(tail(.(T103, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 8 | ','(no(empty(T103)), ','(head(T103, X161), ','(tail(T103, X162), ','(tail(.(T103, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT103 is ground\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T103, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
362 [label="362: ','(','(call(empty(T107)), ','(!_40, failure(a))), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))) | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
364 [label="364: ','(empty(T107), ','(','(!_40, failure(a)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))))) | ?_41 | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: ','(empty(T107), ','(','(!_40, failure(a)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))))), SCOPE: 42, CLAUSE: 7 | ?_42 | ?_41 | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: ','(','(!_40, failure(a)), ','(head([], X161), ','(tail([], X162), ','(tail(.([], T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))) | ?_42 | ?_41 | ','(no(empty([])), ','(head([], X161), ','(tail([], X162), ','(tail(.([], T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.([], T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
367 [label="367: ?_42 | ?_41 | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T107) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
368 [label="368: ','(failure(a), ','(head([], X161), ','(tail([], X162), ','(tail(.([], T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))))\n\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.([], T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
369 [label="369: ','(failure(a), ','(head([], X161), ','(tail([], X162), ','(tail(.([], T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 43, CLAUSE: 10\n\nT104 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.([], T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: ?_41 | ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T107) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
372 [label="372: ','(no(empty(T107)), ','(head(T107, X161), ','(tail(T107, X162), ','(tail(.(T107, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))), SCOPE: 40, CLAUSE: 9\n\nT104 is ground\nT107 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T107, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T107) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="373: ','(head(T110, X161), ','(tail(T110, X162), ','(tail(.(T110, T104), X163), gopher(cons(X161, cons(X162, X163)), T92))))\n\nT104 is ground\nT110 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T110, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T110) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
374 [label="374: ','(head(T110, X161), ','(tail(T110, X162), ','(tail(.(T110, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))), SCOPE: 44, CLAUSE: 3 | ','(head(T110, X161), ','(tail(T110, X162), ','(tail(.(T110, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))), SCOPE: 44, CLAUSE: 4\n\nT104 is ground\nT110 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T110, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T110) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: ','(head(T110, X161), ','(tail(T110, X162), ','(tail(.(T110, T104), X163), gopher(cons(X161, cons(X162, X163)), T92)))), SCOPE: 44, CLAUSE: 4\n\nT104 is ground\nT110 is ground\nX62 is free\nX63 is free\nX161 is free\nX162 is free\nX163 is free\ngopher(.(T110, T104), T2) !=? gopher(X62, cons(nil, X63))\nempty(T110) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: ','(tail(.(T115, T116), X162), ','(tail(.(.(T115, T116), T104), X163), gopher(cons(T115, cons(X162, X163)), T92)))\n\nT104 is ground\nT115 is ground\nT116 is ground\nX62 is free\nX63 is free\nX162 is free\nX163 is free\ngopher(.(.(T115, T116), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
377 [label="377: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
378 [label="378: ','(tail(.(T115, T116), X162), ','(tail(.(.(T115, T116), T104), X163), gopher(cons(T115, cons(X162, X163)), T92))), SCOPE: 45, CLAUSE: 5 | ','(tail(.(T115, T116), X162), ','(tail(.(.(T115, T116), T104), X163), gopher(cons(T115, cons(X162, X163)), T92))), SCOPE: 45, CLAUSE: 6\n\nT104 is ground\nT115 is ground\nT116 is ground\nX62 is free\nX63 is free\nX162 is free\nX163 is free\ngopher(.(.(T115, T116), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: ','(tail(.(T115, T116), X162), ','(tail(.(.(T115, T116), T104), X163), gopher(cons(T115, cons(X162, X163)), T92))), SCOPE: 45, CLAUSE: 6\n\nT104 is ground\nT115 is ground\nT116 is ground\nX62 is free\nX63 is free\nX162 is free\nX163 is free\ngopher(.(.(T115, T116), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
380 [label="380: ','(tail(.(.(T121, T122), T104), X163), gopher(cons(T121, cons(T122, X163)), T92))\n\nT104 is ground\nT121 is ground\nT122 is ground\nX62 is free\nX63 is free\nX163 is free\ngopher(.(.(T121, T122), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
381 [label="381: ','(tail(.(.(T121, T122), T104), X163), gopher(cons(T121, cons(T122, X163)), T92)), SCOPE: 46, CLAUSE: 5 | ','(tail(.(.(T121, T122), T104), X163), gopher(cons(T121, cons(T122, X163)), T92)), SCOPE: 46, CLAUSE: 6\n\nT104 is ground\nT121 is ground\nT122 is ground\nX62 is free\nX63 is free\nX163 is free\ngopher(.(.(T121, T122), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: ','(tail(.(.(T121, T122), T104), X163), gopher(cons(T121, cons(T122, X163)), T92)), SCOPE: 46, CLAUSE: 6\n\nT104 is ground\nT121 is ground\nT122 is ground\nX62 is free\nX63 is free\nX163 is free\ngopher(.(.(T121, T122), T104), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
383 [label="383: gopher(cons(T129, cons(T130, T131)), T92)\n\nT129 is ground\nT130 is ground\nT131 is ground\nX62 is free\nX63 is free\ngopher(.(.(T129, T130), T131), T2) !=? gopher(X62, cons(nil, X63))", fontsize=16, style=filled, fillcolor=lightyellow];
384 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 384 [arrowhead = none ];
384 -> 6;

385 [label="EVAL with clause\ngopher(nil, nil).\nand substitutionT1 -> nil,\nT2 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 385 [arrowhead = none ];
385 -> 26;

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

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

388 [label="EVAL with clause\ngopher(X62, cons(nil, X63)) :- ','(no(empty(X62)), ','(head(X62, nil), tail(X62, X63))).\nand substitutionT1 -> T16,\nX62 -> T16,\nX63 -> T18,\nT2 -> cons(nil, T18),\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 388 [arrowhead = none ];
388 -> 167;

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

390 [label="EVAL with clause\ngopher(X7, cons(nil, X8)) :- ','(no(empty(X7)), ','(head(X7, nil), tail(X7, X8))).\nand substitutionX7 -> nil,\nX8 -> T5,\nT2 -> cons(nil, T5),\nT4 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 390 [arrowhead = none ];
390 -> 38;

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

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

393 [label="ONLY EVAL with clause\ngopher(X45, X46) :- ','(no(empty(X45)), ','(head(X45, X47), ','(no(empty(X47)), ','(head(X47, X48), ','(tail(X47, X49), ','(tail(X45, X50), gopher(cons(X48, cons(X49, X50)), X46))))))).\nand substitutionX45 -> nil,\nT2 -> T13,\nX46 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 393 [arrowhead = none ];
393 -> 129;

394 [label="ONLY EVAL with clause\nno(X11) :- ','(call(X11), ','(!_2, failure(a))).\nand substitutionX11 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 394 [arrowhead = none ];
394 -> 53;

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

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

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

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

399 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 399 [arrowhead = none ];
399 -> 60;

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

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

402 [label="ONLY EVAL with clause\nno(X16).\nand substitutionX16 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 402 [arrowhead = none ];
402 -> 66;

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

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

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

406 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 406 [arrowhead = none ];
406 -> 79;

407 [label="ONLY EVAL with clause\ngopher(X28, X29) :- ','(no(empty(X28)), ','(head(X28, X30), ','(no(empty(X30)), ','(head(X30, X31), ','(tail(X30, X32), ','(tail(X28, X33), gopher(cons(X31, cons(X32, X33)), X29))))))).\nand substitutionX28 -> nil,\nT2 -> T10,\nX29 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 407 [arrowhead = none ];
407 -> 90;

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

409 [label="ONLY EVAL with clause\nno(X36) :- ','(call(X36), ','(!_6, failure(a))).\nand substitutionX36 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 409 [arrowhead = none ];
409 -> 97;

410 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
97 -> 410 [arrowhead = none ];
410 -> 101;

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

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

413 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 413 [arrowhead = none ];
413 -> 112;

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

415 [label="ONLY EVAL with clause\nno(X39).\nand substitutionX39 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 415 [arrowhead = none ];
415 -> 117;

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

417 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 417 [arrowhead = none ];
417 -> 122;

418 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 418 [arrowhead = none ];
418 -> 124;

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

420 [label="ONLY EVAL with clause\nno(X53) :- ','(call(X53), ','(!_10, failure(a))).\nand substitutionX53 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 420 [arrowhead = none ];
420 -> 137;

421 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
137 -> 421 [arrowhead = none ];
421 -> 140;

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

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

424 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 424 [arrowhead = none ];
424 -> 149;

425 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 425 [arrowhead = none ];
425 -> 151;

426 [label="ONLY EVAL with clause\nno(X56).\nand substitutionX56 -> empty(nil)", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 426 [arrowhead = none ];
426 -> 156;

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

428 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 428 [arrowhead = none ];
428 -> 162;

429 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
162 -> 429 [arrowhead = none ];
429 -> 163;

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

431 [label="ONLY EVAL with clause\ngopher(X158, X159) :- ','(no(empty(X158)), ','(head(X158, X160), ','(no(empty(X160)), ','(head(X160, X161), ','(tail(X160, X162), ','(tail(X158, X163), gopher(cons(X161, cons(X162, X163)), X159))))))).\nand substitutionT1 -> T90,\nX158 -> T90,\nT2 -> T92,\nX159 -> T92,\nT91 -> T92", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 431 [arrowhead = none ];
431 -> 316;

432 [label="ONLY EVAL with clause\nno(X66) :- ','(call(X66), ','(!_14, failure(a))).\nand substitutionT16 -> T21,\nX66 -> empty(T21)", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 432 [arrowhead = none ];
432 -> 174;

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

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

435 [label="EVAL with clause\nempty([]).\nand substitutionT21 -> []", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 435 [arrowhead = none ];
435 -> 182;

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

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

438 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
186 -> 438 [arrowhead = none ];
438 -> 217;

439 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
189 -> 439 [arrowhead = none ];
439 -> 190;

440 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
189 -> 440 [arrowhead = none ];
440 -> 192;

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

442 [label="ONLY EVAL with clause\ngopher(X75, X76) :- ','(no(empty(X75)), ','(head(X75, X77), ','(no(empty(X77)), ','(head(X77, X78), ','(tail(X77, X79), ','(tail(X75, X80), gopher(cons(X78, cons(X79, X80)), X76))))))).\nand substitutionX75 -> [],\nT2 -> T26,\nX76 -> T26,\nT25 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 442 [arrowhead = none ];
442 -> 203;

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

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

445 [label="ONLY EVAL with clause\nno(X83) :- ','(call(X83), ','(!_18, failure(a))).\nand substitutionX83 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 445 [arrowhead = none ];
445 -> 205;

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

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

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

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

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

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

452 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 452 [arrowhead = none ];
452 -> 218;

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

454 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
218 -> 454 [arrowhead = none ];
454 -> 220;

455 [label="ONLY EVAL with clause\nno(X88).\nand substitutionT21 -> T31,\nX88 -> empty(T31)", fontsize=14, style = filled, fillcolor = lightblue];
219 -> 455 [arrowhead = none ];
455 -> 225;

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

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

458 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T31), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
226 -> 458 [arrowhead = none ];
458 -> 227;

459 [label="EVAL with clause\nhead(.(X94, X95), X94).\nand substitutionX94 -> nil,\nX95 -> T37,\nT31 -> .(nil, T37),\nT36 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
227 -> 459 [arrowhead = none ];
459 -> 228;

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

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

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

463 [label="EVAL with clause\ntail(.(X100, X101), X101).\nand substitutionX100 -> nil,\nT37 -> T40,\nX101 -> T40,\nT18 -> T40", fontsize=14, style = filled, fillcolor = lightblue];
231 -> 463 [arrowhead = none ];
463 -> 233;

464 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
231 -> 464 [arrowhead = none ];
464 -> 235;

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

466 [label="ONLY EVAL with clause\ngopher(X110, X111) :- ','(no(empty(X110)), ','(head(X110, X112), ','(no(empty(X112)), ','(head(X112, X113), ','(tail(X112, X114), ','(tail(X110, X115), gopher(cons(X113, cons(X114, X115)), X111))))))).\nand substitutionT21 -> T46,\nX110 -> T46,\nT2 -> T48,\nX111 -> T48,\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 466 [arrowhead = none ];
466 -> 244;

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

468 [label="ONLY EVAL with clause\nno(X118) :- ','(call(X118), ','(!_24, failure(a))).\nand substitutionT46 -> T51,\nX118 -> empty(T51)", fontsize=14, style = filled, fillcolor = lightblue];
245 -> 468 [arrowhead = none ];
468 -> 249;

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

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

471 [label="BACKTRACK\nfor clause: empty([])\nwith clash: (empty(T51), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
251 -> 471 [arrowhead = none ];
471 -> 252;

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

473 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
254 -> 473 [arrowhead = none ];
473 -> 256;

474 [label="ONLY EVAL with clause\nno(X121).\nand substitutionT51 -> T54,\nX121 -> empty(T54)", fontsize=14, style = filled, fillcolor = lightblue];
256 -> 474 [arrowhead = none ];
474 -> 258;

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

476 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T54), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
261 -> 476 [arrowhead = none ];
476 -> 263;

477 [label="EVAL with clause\nhead(.(X128, X129), X128).\nand substitutionX128 -> T59,\nX129 -> T60,\nT54 -> .(T59, T60),\nX112 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
263 -> 477 [arrowhead = none ];
477 -> 271;

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

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

480 [label="ONLY EVAL with clause\nno(X132) :- ','(call(X132), ','(!_28, failure(a))).\nand substitutionT59 -> T63,\nX132 -> empty(T63)", fontsize=14, style = filled, fillcolor = lightblue];
273 -> 480 [arrowhead = none ];
480 -> 277;

481 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
277 -> 481 [arrowhead = none ];
481 -> 278;

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

483 [label="EVAL with clause\nempty([]).\nand substitutionT63 -> []", fontsize=14, style = filled, fillcolor = lightblue];
280 -> 483 [arrowhead = none ];
483 -> 284;

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

485 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
284 -> 485 [arrowhead = none ];
485 -> 286;

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

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

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

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

490 [label="ONLY EVAL with clause\nno(X135).\nand substitutionT63 -> T66,\nX135 -> empty(T66)", fontsize=14, style = filled, fillcolor = lightblue];
290 -> 490 [arrowhead = none ];
490 -> 294;

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

492 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T66), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
295 -> 492 [arrowhead = none ];
492 -> 296;

493 [label="EVAL with clause\nhead(.(X142, X143), X142).\nand substitutionX142 -> T71,\nX143 -> T72,\nT66 -> .(T71, T72),\nX113 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
296 -> 493 [arrowhead = none ];
493 -> 298;

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

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

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

497 [label="ONLY EVAL with clause\ntail(.(X148, X149), X149).\nand substitutionT71 -> T77,\nX148 -> T77,\nT72 -> T78,\nX149 -> T78,\nX114 -> T78", fontsize=14, style = filled, fillcolor = lightblue];
301 -> 497 [arrowhead = none ];
497 -> 302;

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

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

500 [label="ONLY EVAL with clause\ntail(.(X154, X155), X155).\nand substitutionT77 -> T85,\nT78 -> T86,\nX154 -> .(T85, T86),\nT60 -> T87,\nX155 -> T87,\nX115 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
304 -> 500 [arrowhead = none ];
500 -> 307;

501 [label="INSTANCE with matching:\nT1 -> cons(T85, cons(T86, T87))\nT2 -> T48", fontsize=14, style = filled, fillcolor = lightgrey];
307 -> 501 [arrowhead = none , style=dashed];
501 -> 1[style=dashed];

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

503 [label="ONLY EVAL with clause\nno(X166) :- ','(call(X166), ','(!_35, failure(a))).\nand substitutionT90 -> T95,\nX166 -> empty(T95)", fontsize=14, style = filled, fillcolor = lightblue];
318 -> 503 [arrowhead = none ];
503 -> 321;

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

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

506 [label="EVAL with clause\nempty([]).\nand substitutionT95 -> []", fontsize=14, style = filled, fillcolor = lightblue];
324 -> 506 [arrowhead = none ];
506 -> 326;

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

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

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

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

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

512 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
333 -> 512 [arrowhead = none ];
512 -> 335;

513 [label="ONLY EVAL with clause\nno(X169).\nand substitutionT95 -> T98,\nX169 -> empty(T98)", fontsize=14, style = filled, fillcolor = lightblue];
335 -> 513 [arrowhead = none ];
513 -> 337;

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

515 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T98), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
340 -> 515 [arrowhead = none ];
515 -> 341;

516 [label="EVAL with clause\nhead(.(X176, X177), X176).\nand substitutionX176 -> T103,\nX177 -> T104,\nT98 -> .(T103, T104),\nX160 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
341 -> 516 [arrowhead = none ];
516 -> 356;

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

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

519 [label="ONLY EVAL with clause\nno(X180) :- ','(call(X180), ','(!_40, failure(a))).\nand substitutionT103 -> T107,\nX180 -> empty(T107)", fontsize=14, style = filled, fillcolor = lightblue];
361 -> 519 [arrowhead = none ];
519 -> 362;

520 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
362 -> 520 [arrowhead = none ];
520 -> 364;

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

522 [label="EVAL with clause\nempty([]).\nand substitutionT107 -> []", fontsize=14, style = filled, fillcolor = lightblue];
365 -> 522 [arrowhead = none ];
522 -> 366;

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

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

525 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
367 -> 525 [arrowhead = none ];
525 -> 371;

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

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

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

529 [label="ONLY EVAL with clause\nno(X183).\nand substitutionT107 -> T110,\nX183 -> empty(T110)", fontsize=14, style = filled, fillcolor = lightblue];
372 -> 529 [arrowhead = none ];
529 -> 373;

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

531 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T110), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
374 -> 531 [arrowhead = none ];
531 -> 375;

532 [label="EVAL with clause\nhead(.(X190, X191), X190).\nand substitutionX190 -> T115,\nX191 -> T116,\nT110 -> .(T115, T116),\nX161 -> T115", fontsize=14, style = filled, fillcolor = lightblue];
375 -> 532 [arrowhead = none ];
532 -> 376;

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

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

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

536 [label="ONLY EVAL with clause\ntail(.(X196, X197), X197).\nand substitutionT115 -> T121,\nX196 -> T121,\nT116 -> T122,\nX197 -> T122,\nX162 -> T122", fontsize=14, style = filled, fillcolor = lightblue];
379 -> 536 [arrowhead = none ];
536 -> 380;

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

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

539 [label="ONLY EVAL with clause\ntail(.(X202, X203), X203).\nand substitutionT121 -> T129,\nT122 -> T130,\nX202 -> .(T129, T130),\nT104 -> T131,\nX203 -> T131,\nX163 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
382 -> 539 [arrowhead = none ];
539 -> 383;

540 [label="INSTANCE with matching:\nT1 -> cons(T129, cons(T130, T131))\nT2 -> T92", fontsize=14, style = filled, fillcolor = lightgrey];
383 -> 540 [arrowhead = none , style=dashed];
540 -> 1[style=dashed];

}

(2) Obligation:

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

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(.(nil, T40), cons(nil, T40)) → gopherA_out_ga(.(nil, T40), cons(nil, T40))
gopherA_in_ga(.(.(T85, T86), T87), T48) → U1_ga(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
gopherA_in_ga(.(.(T129, T130), T131), T92) → U2_ga(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))
U2_ga(T129, T130, T131, T92, gopherA_out_ga(cons(T129, cons(T130, T131)), T92)) → gopherA_out_ga(.(.(T129, T130), T131), T92)
U1_ga(T85, T86, T87, T48, gopherA_out_ga(cons(T85, cons(T86, T87)), T48)) → gopherA_out_ga(.(.(T85, T86), T87), T48)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

GOPHERA_IN_GA(.(.(T85, T86), T87), T48) → U1_GA(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
GOPHERA_IN_GA(.(.(T85, T86), T87), T48) → GOPHERA_IN_GA(cons(T85, cons(T86, T87)), T48)
GOPHERA_IN_GA(.(.(T129, T130), T131), T92) → U2_GA(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))

The TRS R consists of the following rules:

gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(.(nil, T40), cons(nil, T40)) → gopherA_out_ga(.(nil, T40), cons(nil, T40))
gopherA_in_ga(.(.(T85, T86), T87), T48) → U1_ga(T85, T86, T87, T48, gopherA_in_ga(cons(T85, cons(T86, T87)), T48))
gopherA_in_ga(.(.(T129, T130), T131), T92) → U2_ga(T129, T130, T131, T92, gopherA_in_ga(cons(T129, cons(T130, T131)), T92))
U2_ga(T129, T130, T131, T92, gopherA_out_ga(cons(T129, cons(T130, T131)), T92)) → gopherA_out_ga(.(.(T129, T130), T131), T92)
U1_ga(T85, T86, T87, T48, gopherA_out_ga(cons(T85, cons(T86, T87)), T48)) → gopherA_out_ga(.(.(T85, T86), T87), T48)

The argument filtering Pi contains the following mapping:
gopherA_in_ga(x1, x2) = gopherA_in_ga(x1)
nil = nil
gopherA_out_ga(x1, x2) = gopherA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x1, x2, x3, x5)
cons(x1, x2) = cons(x1, x2)
GOPHERA_IN_GA(x1, x2) = GOPHERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x3, x5)

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

(4) Obligation:

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