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

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳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).

Queries:

gopher(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: gopher(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: 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];
3 [label="3: true | gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: 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];
5 [label="5: gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))) | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\ngopher(nil, T2) !=? gopher(X7, cons(nil, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(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];
9 [label="9: ','(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];
10 [label="10: ','(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];
11 [label="11: ','(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];
12 [label="12: ?_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];
13 [label="13: ?_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];
14 [label="14: ','(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];
15 [label="15: ','(no(empty(nil)), ','(head(nil, nil), tail(nil, T5))), SCOPE: 2, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ?_2 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(head(nil, nil), tail(nil, T5))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(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];
19 [label="19: ','(head(nil, nil), tail(nil, T5)), SCOPE: 5, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11)))))))\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))), SCOPE: 6, CLAUSE: 8 | ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))), SCOPE: 6, CLAUSE: 9\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(call(empty(nil)), ','(!_6, ','(failure(a), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))))) | ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))), SCOPE: 6, CLAUSE: 9\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(empty(nil), ','(!_6, ','(failure(a), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))))) | ?_7 | ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))), SCOPE: 6, CLAUSE: 9\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(empty(nil), ','(!_6, ','(failure(a), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))))), SCOPE: 8, CLAUSE: 7 | ?_8 | ?_7 | ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))), SCOPE: 6, CLAUSE: 9\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ?_8 | ?_7 | ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))), SCOPE: 6, CLAUSE: 9\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ?_7 | ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))), SCOPE: 6, CLAUSE: 9\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(no(empty(nil)), ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))), SCOPE: 6, CLAUSE: 9\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11))))))\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11)))))), SCOPE: 9, CLAUSE: 3 | ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11)))))), SCOPE: 9, CLAUSE: 4\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(head(nil, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(nil, X40), gopher(cons(X38, cons(X39, X40)), T11)))))), SCOPE: 9, CLAUSE: 4\n\nX37 is free\nX38 is free; \nX39 is free; \nX40 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17)))))))\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))), SCOPE: 10, CLAUSE: 8 | ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))), SCOPE: 10, CLAUSE: 9\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(call(empty(nil)), ','(!_10, ','(failure(a), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))))) | ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))), SCOPE: 10, CLAUSE: 9\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(empty(nil), ','(!_10, ','(failure(a), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))))) | ?_11 | ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))), SCOPE: 10, CLAUSE: 9\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(empty(nil), ','(!_10, ','(failure(a), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))))), SCOPE: 12, CLAUSE: 7 | ?_12 | ?_11 | ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))), SCOPE: 10, CLAUSE: 9\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ?_12 | ?_11 | ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))), SCOPE: 10, CLAUSE: 9\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ?_11 | ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))), SCOPE: 10, CLAUSE: 9\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(no(empty(nil)), ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))), SCOPE: 10, CLAUSE: 9\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17))))))\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17)))))), SCOPE: 13, CLAUSE: 3 | ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17)))))), SCOPE: 13, CLAUSE: 4\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(head(nil, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(nil, X72), gopher(cons(X70, cons(X71, X72)), T17)))))), SCOPE: 13, CLAUSE: 4\n\nX69 is free\nX70 is free; \nX71 is free; \nX72 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(no(empty(T22)), ','(head(T22, nil), tail(T22, T24))) | gopher(T22, T2), SCOPE: 1, CLAUSE: 2\n\nT22 is ground\ngopher(T22, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ngopher(T1, T2) !=? gopher(nil, nil)\ngopher(T1, T2) !=? gopher(X94, cons(nil, X95))", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(no(empty(T22)), ','(head(T22, nil), tail(T22, T24))), SCOPE: 14, CLAUSE: 8 | ','(no(empty(T22)), ','(head(T22, nil), tail(T22, T24))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T22, T2), SCOPE: 1, CLAUSE: 2\n\nT22 is ground\ngopher(T22, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(call(empty(T27)), ','(!_14, ','(failure(a), ','(head(T27, nil), tail(T27, T24))))) | ','(no(empty(T27)), ','(head(T27, nil), tail(T27, T24))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T27, T2), SCOPE: 1, CLAUSE: 2\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(empty(T27), ','(!_14, ','(failure(a), ','(head(T27, nil), tail(T27, T24))))) | ?_15 | ','(no(empty(T27)), ','(head(T27, nil), tail(T27, T24))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T27, T2), SCOPE: 1, CLAUSE: 2\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(empty(T27), ','(!_14, ','(failure(a), ','(head(T27, nil), tail(T27, T24))))), SCOPE: 16, CLAUSE: 7 | ?_16 | ?_15 | ','(no(empty(T27)), ','(head(T27, nil), tail(T27, T24))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T27, T2), SCOPE: 1, CLAUSE: 2\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(!_14, ','(failure(a), ','(head([], nil), tail([], T24)))) | ?_16 | ?_15 | ','(no(empty([])), ','(head([], nil), tail([], T24))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ?_16 | ?_15 | ','(no(empty(T27)), ','(head(T27, nil), tail(T27, T24))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T27, T2), SCOPE: 1, CLAUSE: 2\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)\nempty(T27) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(failure(a), ','(head([], nil), tail([], T24))) | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(failure(a), ','(head([], nil), tail([], T24)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: gopher([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(failure(a), ','(head([], nil), tail([], T24))), SCOPE: 17, CLAUSE: 10\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(no(empty([])), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33)))))))\n\nX116 is free\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(no(empty([])), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))), SCOPE: 18, CLAUSE: 8 | ','(no(empty([])), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))), SCOPE: 18, CLAUSE: 9\n\nX116 is free\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(call(empty([])), ','(!_18, ','(failure(a), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))))) | ','(no(empty([])), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))), SCOPE: 18, CLAUSE: 9\n\nX116 is free\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(empty([]), ','(!_18, ','(failure(a), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))))) | ?_19 | ','(no(empty([])), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))), SCOPE: 18, CLAUSE: 9\n\nX116 is free\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(empty([]), ','(!_18, ','(failure(a), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))))), SCOPE: 20, CLAUSE: 7 | ?_20 | ?_19 | ','(no(empty([])), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))), SCOPE: 18, CLAUSE: 9\n\nX116 is free\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(!_18, ','(failure(a), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33)))))))) | ?_20 | ?_19 | ','(no(empty([])), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))), SCOPE: 18, CLAUSE: 9\n\nX116 is free\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(failure(a), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33)))))))\n\nX116 is free\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(failure(a), ','(head([], X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail([], X119), gopher(cons(X117, cons(X118, X119)), T33))))))), SCOPE: 21, CLAUSE: 10\n\nX116 is free\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ?_15 | ','(no(empty(T27)), ','(head(T27, nil), tail(T27, T24))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T27, T2), SCOPE: 1, CLAUSE: 2\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)\nempty(T27) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(no(empty(T27)), ','(head(T27, nil), tail(T27, T24))), SCOPE: 14, CLAUSE: 9 | ?_14 | gopher(T27, T2), SCOPE: 1, CLAUSE: 2\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)\nempty(T27) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(no(empty(T27)), ','(head(T27, nil), tail(T27, T24))), SCOPE: 14, CLAUSE: 9\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)\nempty(T27) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ?_14 | gopher(T27, T2), SCOPE: 1, CLAUSE: 2\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)\nempty(T27) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(head(T40, nil), tail(T40, T24))\n\nT40 is ground\ngopher(T40, T2) !=? gopher(nil, nil)\nempty(T40) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(head(T40, nil), tail(T40, T24)), SCOPE: 22, CLAUSE: 3 | ','(head(T40, nil), tail(T40, T24)), SCOPE: 22, CLAUSE: 4\n\nT40 is ground\ngopher(T40, T2) !=? gopher(nil, nil)\nempty(T40) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(head(T40, nil), tail(T40, T24)), SCOPE: 22, CLAUSE: 4\n\nT40 is ground\ngopher(T40, T2) !=? gopher(nil, nil)\nempty(T40) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: tail(.(nil, T46), T24)\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: tail(.(nil, T46), T24), SCOPE: 23, CLAUSE: 5 | tail(.(nil, T46), T24), SCOPE: 23, CLAUSE: 6\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: tail(.(nil, T46), T24), SCOPE: 23, CLAUSE: 6\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: gopher(T27, T2), SCOPE: 1, CLAUSE: 2\n\nT27 is ground\ngopher(T27, T2) !=? gopher(nil, nil)\nempty(T27) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(no(empty(T56)), ','(head(T56, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T56, X173), gopher(cons(X171, cons(X172, X173)), T58)))))))\n\nT56 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T56, T2) !=? gopher(nil, nil)\nempty(T56) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(no(empty(T56)), ','(head(T56, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T56, X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 24, CLAUSE: 8 | ','(no(empty(T56)), ','(head(T56, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T56, X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 24, CLAUSE: 9\n\nT56 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T56, T2) !=? gopher(nil, nil)\nempty(T56) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(call(empty(T62)), ','(!_24, ','(failure(a), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))))) | ','(no(empty(T62)), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 24, CLAUSE: 9\n\nT62 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T62, T2) !=? gopher(nil, nil)\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(empty(T62), ','(!_24, ','(failure(a), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))))) | ?_25 | ','(no(empty(T62)), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 24, CLAUSE: 9\n\nT62 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T62, T2) !=? gopher(nil, nil)\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(empty(T62), ','(!_24, ','(failure(a), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))))), SCOPE: 26, CLAUSE: 7 | ?_26 | ?_25 | ','(no(empty(T62)), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 24, CLAUSE: 9\n\nT62 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T62, T2) !=? gopher(nil, nil)\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ?_26 | ?_25 | ','(no(empty(T62)), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 24, CLAUSE: 9\n\nT62 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T62, T2) !=? gopher(nil, nil)\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ?_25 | ','(no(empty(T62)), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 24, CLAUSE: 9\n\nT62 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T62, T2) !=? gopher(nil, nil)\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(no(empty(T62)), ','(head(T62, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T62, X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 24, CLAUSE: 9\n\nT62 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T62, T2) !=? gopher(nil, nil)\nempty(T62) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(head(T66, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T66, X173), gopher(cons(X171, cons(X172, X173)), T58))))))\n\nT66 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T66, T2) !=? gopher(nil, nil)\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(head(T66, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T66, X173), gopher(cons(X171, cons(X172, X173)), T58)))))), SCOPE: 27, CLAUSE: 3 | ','(head(T66, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T66, X173), gopher(cons(X171, cons(X172, X173)), T58)))))), SCOPE: 27, CLAUSE: 4\n\nT66 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T66, T2) !=? gopher(nil, nil)\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(head(T66, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(T66, X173), gopher(cons(X171, cons(X172, X173)), T58)))))), SCOPE: 27, CLAUSE: 4\n\nT66 is ground\nX170 is free; \nX171 is free; \nX172 is free; \nX173 is free; \ngopher(T66, T2) !=? gopher(nil, nil)\nempty(T66) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(no(empty(T72)), ','(head(T72, X171), ','(tail(T72, X172), ','(tail(.(T72, T73), X173), gopher(cons(X171, cons(X172, X173)), T58)))))\n\nT72 is ground\nT73 is ground\nX171 is free; \nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(no(empty(T72)), ','(head(T72, X171), ','(tail(T72, X172), ','(tail(.(T72, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 8 | ','(no(empty(T72)), ','(head(T72, X171), ','(tail(T72, X172), ','(tail(.(T72, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 9\n\nT72 is ground\nT73 is ground\nX171 is free; \nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(call(empty(T77)), ','(!_28, ','(failure(a), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))))) | ','(no(empty(T77)), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 9\n\nT73 is ground\nT77 is ground\nX171 is free; \nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(empty(T77), ','(!_28, ','(failure(a), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))))) | ?_29 | ','(no(empty(T77)), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 9\n\nT73 is ground\nT77 is ground\nX171 is free; \nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(empty(T77), ','(!_28, ','(failure(a), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))))), SCOPE: 30, CLAUSE: 7 | ?_30 | ?_29 | ','(no(empty(T77)), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 9\n\nT73 is ground\nT77 is ground\nX171 is free; \nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(!_28, ','(failure(a), ','(head([], X171), ','(tail([], X172), ','(tail(.([], T73), X173), gopher(cons(X171, cons(X172, X173)), T58)))))) | ?_30 | ?_29 | ','(no(empty([])), ','(head([], X171), ','(tail([], X172), ','(tail(.([], T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 9\n\nT73 is ground\nX171 is free; \nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ?_30 | ?_29 | ','(no(empty(T77)), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 9\n\nT73 is ground\nT77 is ground\nX171 is free; \nX172 is free; \nX173 is free; \nempty(T77) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(failure(a), ','(head([], X171), ','(tail([], X172), ','(tail(.([], T73), X173), gopher(cons(X171, cons(X172, X173)), T58)))))\n\nT73 is ground\nX171 is free; \nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(failure(a), ','(head([], X171), ','(tail([], X172), ','(tail(.([], T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 31, CLAUSE: 10\n\nT73 is ground\nX171 is free; \nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ?_29 | ','(no(empty(T77)), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 9\n\nT73 is ground\nT77 is ground\nX171 is free; \nX172 is free; \nX173 is free; \nempty(T77) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(no(empty(T77)), ','(head(T77, X171), ','(tail(T77, X172), ','(tail(.(T77, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))), SCOPE: 28, CLAUSE: 9\n\nT73 is ground\nT77 is ground\nX171 is free; \nX172 is free; \nX173 is free; \nempty(T77) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(head(T82, X171), ','(tail(T82, X172), ','(tail(.(T82, T73), X173), gopher(cons(X171, cons(X172, X173)), T58))))\n\nT73 is ground\nT82 is ground\nX171 is free; \nX172 is free; \nX173 is free; \nempty(T82) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(head(T82, X171), ','(tail(T82, X172), ','(tail(.(T82, T73), X173), gopher(cons(X171, cons(X172, X173)), T58)))), SCOPE: 32, CLAUSE: 3 | ','(head(T82, X171), ','(tail(T82, X172), ','(tail(.(T82, T73), X173), gopher(cons(X171, cons(X172, X173)), T58)))), SCOPE: 32, CLAUSE: 4\n\nT73 is ground\nT82 is ground\nX171 is free; \nX172 is free; \nX173 is free; \nempty(T82) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(head(T82, X171), ','(tail(T82, X172), ','(tail(.(T82, T73), X173), gopher(cons(X171, cons(X172, X173)), T58)))), SCOPE: 32, CLAUSE: 4\n\nT73 is ground\nT82 is ground\nX171 is free; \nX172 is free; \nX173 is free; \nempty(T82) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(tail(.(T88, T89), X172), ','(tail(.(.(T88, T89), T73), X173), gopher(cons(T88, cons(X172, X173)), T58)))\n\nT73 is ground\nT88 is ground\nT89 is ground\nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(tail(.(T88, T89), X172), ','(tail(.(.(T88, T89), T73), X173), gopher(cons(T88, cons(X172, X173)), T58))), SCOPE: 33, CLAUSE: 5 | ','(tail(.(T88, T89), X172), ','(tail(.(.(T88, T89), T73), X173), gopher(cons(T88, cons(X172, X173)), T58))), SCOPE: 33, CLAUSE: 6\n\nT73 is ground\nT88 is ground\nT89 is ground\nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(tail(.(T88, T89), X172), ','(tail(.(.(T88, T89), T73), X173), gopher(cons(T88, cons(X172, X173)), T58))), SCOPE: 33, CLAUSE: 6\n\nT73 is ground\nT88 is ground\nT89 is ground\nX172 is free; \nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(tail(.(.(T99, T100), T73), X173), gopher(cons(T99, cons(T100, X173)), T58))\n\nT73 is ground\nT99 is ground\nT100 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(tail(.(.(T99, T100), T73), X173), gopher(cons(T99, cons(T100, X173)), T58)), SCOPE: 34, CLAUSE: 5 | ','(tail(.(.(T99, T100), T73), X173), gopher(cons(T99, cons(T100, X173)), T58)), SCOPE: 34, CLAUSE: 6\n\nT73 is ground\nT99 is ground\nT100 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(tail(.(.(T99, T100), T73), X173), gopher(cons(T99, cons(T100, X173)), T58)), SCOPE: 34, CLAUSE: 6\n\nT73 is ground\nT99 is ground\nT100 is ground\nX173 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: gopher(cons(T114, cons(T115, T116)), T58)\n\nT114 is ground\nT115 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(no(empty(T123)), ','(head(T123, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T123, X274), gopher(cons(X272, cons(X273, X274)), T125)))))))\n\nT123 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T123, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(no(empty(T123)), ','(head(T123, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T123, X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 8 | ','(no(empty(T123)), ','(head(T123, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T123, X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 9\n\nT123 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T123, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(call(empty(T128)), ','(!_35, ','(failure(a), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))))) | ','(no(empty(T128)), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 9\n\nT128 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T128, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(empty(T128), ','(!_35, ','(failure(a), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))))) | ?_36 | ','(no(empty(T128)), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 9\n\nT128 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T128, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(empty(T128), ','(!_35, ','(failure(a), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))))), SCOPE: 37, CLAUSE: 7 | ?_37 | ?_36 | ','(no(empty(T128)), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 9\n\nT128 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T128, T2) !=? gopher(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(!_35, ','(failure(a), ','(head([], X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail([], X274), gopher(cons(X272, cons(X273, X274)), T125)))))))) | ?_37 | ?_36 | ','(no(empty([])), ','(head([], X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail([], X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 9\n\nX271 is free\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ?_37 | ?_36 | ','(no(empty(T128)), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 9\n\nT128 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T128, T2) !=? gopher(nil, nil)\nempty(T128) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(failure(a), ','(head([], X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail([], X274), gopher(cons(X272, cons(X273, X274)), T125)))))))\n\nX271 is free\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(failure(a), ','(head([], X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail([], X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 38, CLAUSE: 10\n\nX271 is free\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ?_36 | ','(no(empty(T128)), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 9\n\nT128 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T128, T2) !=? gopher(nil, nil)\nempty(T128) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(no(empty(T128)), ','(head(T128, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T128, X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 35, CLAUSE: 9\n\nT128 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T128, T2) !=? gopher(nil, nil)\nempty(T128) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(head(T133, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T133, X274), gopher(cons(X272, cons(X273, X274)), T125))))))\n\nT133 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T133, T2) !=? gopher(nil, nil)\nempty(T133) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(head(T133, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T133, X274), gopher(cons(X272, cons(X273, X274)), T125)))))), SCOPE: 39, CLAUSE: 3 | ','(head(T133, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T133, X274), gopher(cons(X272, cons(X273, X274)), T125)))))), SCOPE: 39, CLAUSE: 4\n\nT133 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T133, T2) !=? gopher(nil, nil)\nempty(T133) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(head(T133, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(T133, X274), gopher(cons(X272, cons(X273, X274)), T125)))))), SCOPE: 39, CLAUSE: 4\n\nT133 is ground\nX271 is free; \nX272 is free; \nX273 is free; \nX274 is free; \ngopher(T133, T2) !=? gopher(nil, nil)\nempty(T133) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(no(empty(T139)), ','(head(T139, X272), ','(tail(T139, X273), ','(tail(.(T139, T140), X274), gopher(cons(X272, cons(X273, X274)), T125)))))\n\nT139 is ground\nT140 is ground\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(no(empty(T139)), ','(head(T139, X272), ','(tail(T139, X273), ','(tail(.(T139, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 8 | ','(no(empty(T139)), ','(head(T139, X272), ','(tail(T139, X273), ','(tail(.(T139, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 9\n\nT139 is ground\nT140 is ground\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(call(empty(T144)), ','(!_40, ','(failure(a), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))))) | ','(no(empty(T144)), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 9\n\nT140 is ground\nT144 is ground\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(empty(T144), ','(!_40, ','(failure(a), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))))) | ?_41 | ','(no(empty(T144)), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 9\n\nT140 is ground\nT144 is ground\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(empty(T144), ','(!_40, ','(failure(a), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))))), SCOPE: 42, CLAUSE: 7 | ?_42 | ?_41 | ','(no(empty(T144)), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 9\n\nT140 is ground\nT144 is ground\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(!_40, ','(failure(a), ','(head([], X272), ','(tail([], X273), ','(tail(.([], T140), X274), gopher(cons(X272, cons(X273, X274)), T125)))))) | ?_42 | ?_41 | ','(no(empty([])), ','(head([], X272), ','(tail([], X273), ','(tail(.([], T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 9\n\nT140 is ground\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ?_42 | ?_41 | ','(no(empty(T144)), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 9\n\nT140 is ground\nT144 is ground\nX272 is free; \nX273 is free; \nX274 is free; \nempty(T144) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(failure(a), ','(head([], X272), ','(tail([], X273), ','(tail(.([], T140), X274), gopher(cons(X272, cons(X273, X274)), T125)))))\n\nT140 is ground\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(failure(a), ','(head([], X272), ','(tail([], X273), ','(tail(.([], T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 43, CLAUSE: 10\n\nT140 is ground\nX272 is free; \nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ?_41 | ','(no(empty(T144)), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 9\n\nT140 is ground\nT144 is ground\nX272 is free; \nX273 is free; \nX274 is free; \nempty(T144) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(no(empty(T144)), ','(head(T144, X272), ','(tail(T144, X273), ','(tail(.(T144, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))), SCOPE: 40, CLAUSE: 9\n\nT140 is ground\nT144 is ground\nX272 is free; \nX273 is free; \nX274 is free; \nempty(T144) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(head(T149, X272), ','(tail(T149, X273), ','(tail(.(T149, T140), X274), gopher(cons(X272, cons(X273, X274)), T125))))\n\nT140 is ground\nT149 is ground\nX272 is free; \nX273 is free; \nX274 is free; \nempty(T149) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(head(T149, X272), ','(tail(T149, X273), ','(tail(.(T149, T140), X274), gopher(cons(X272, cons(X273, X274)), T125)))), SCOPE: 44, CLAUSE: 3 | ','(head(T149, X272), ','(tail(T149, X273), ','(tail(.(T149, T140), X274), gopher(cons(X272, cons(X273, X274)), T125)))), SCOPE: 44, CLAUSE: 4\n\nT140 is ground\nT149 is ground\nX272 is free; \nX273 is free; \nX274 is free; \nempty(T149) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(head(T149, X272), ','(tail(T149, X273), ','(tail(.(T149, T140), X274), gopher(cons(X272, cons(X273, X274)), T125)))), SCOPE: 44, CLAUSE: 4\n\nT140 is ground\nT149 is ground\nX272 is free; \nX273 is free; \nX274 is free; \nempty(T149) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(tail(.(T155, T156), X273), ','(tail(.(.(T155, T156), T140), X274), gopher(cons(T155, cons(X273, X274)), T125)))\n\nT140 is ground\nT155 is ground\nT156 is ground\nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(tail(.(T155, T156), X273), ','(tail(.(.(T155, T156), T140), X274), gopher(cons(T155, cons(X273, X274)), T125))), SCOPE: 45, CLAUSE: 5 | ','(tail(.(T155, T156), X273), ','(tail(.(.(T155, T156), T140), X274), gopher(cons(T155, cons(X273, X274)), T125))), SCOPE: 45, CLAUSE: 6\n\nT140 is ground\nT155 is ground\nT156 is ground\nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(tail(.(T155, T156), X273), ','(tail(.(.(T155, T156), T140), X274), gopher(cons(T155, cons(X273, X274)), T125))), SCOPE: 45, CLAUSE: 6\n\nT140 is ground\nT155 is ground\nT156 is ground\nX273 is free; \nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(tail(.(.(T166, T167), T140), X274), gopher(cons(T166, cons(T167, X274)), T125))\n\nT140 is ground\nT166 is ground\nT167 is ground\nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(tail(.(.(T166, T167), T140), X274), gopher(cons(T166, cons(T167, X274)), T125)), SCOPE: 46, CLAUSE: 5 | ','(tail(.(.(T166, T167), T140), X274), gopher(cons(T166, cons(T167, X274)), T125)), SCOPE: 46, CLAUSE: 6\n\nT140 is ground\nT166 is ground\nT167 is ground\nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(tail(.(.(T166, T167), T140), X274), gopher(cons(T166, cons(T167, X274)), T125)), SCOPE: 46, CLAUSE: 6\n\nT140 is ground\nT166 is ground\nT167 is ground\nX274 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: gopher(cons(T181, cons(T182, T183)), T125)\n\nT181 is ground\nT182 is ground\nT183 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 157 [arrowhead = none ];
157 -> 2;

158 [label="EVAL with clause\ngopher(nil, nil).\nand substitution\nT1 -> nil\nT2 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 158 [arrowhead = none ];
158 -> 3;

159 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 159 [arrowhead = none ];
159 -> 4;

160 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 160 [arrowhead = none ];
160 -> 5;

161 [label="EVAL with clause\ngopher(X94, cons(nil, X95)) :- ','(no(empty(X94)), ','(head(X94, nil), tail(X94, X95))).\nand substitution\nT1 -> T22\nX94 -> T22\nX95 -> T24\nT2 -> cons(nil, T24)\nT23 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 161 [arrowhead = none ];
161 -> 46;

162 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 162 [arrowhead = none ];
162 -> 47;

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

164 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 164 [arrowhead = none ];
164 -> 7;

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

166 [label="ONLY EVAL with clause\ngopher(X67, X68) :- ','(no(empty(X67)), ','(head(X67, X69), ','(no(empty(X69)), ','(head(X69, X70), ','(tail(X69, X71), ','(tail(X67, X72), gopher(cons(X70, cons(X71, X72)), X68))))))).\nand substitution\nX67 -> nil\nT2 -> T17\nX68 -> T17\nT16 -> T17", fontsize=14, style = filled, fillcolor = white];
7 -> 166 [arrowhead = none ];
166 -> 34;

167 [label="ONLY EVAL with clause\nno(X13) :- ','(call(X13), ','(!_2, failure(a))).\nand substitution\nX13 -> empty(nil)", fontsize=14, style = filled, fillcolor = white];
8 -> 167 [arrowhead = none ];
167 -> 9;

168 [label="CALL", fontsize=14, style = filled, fillcolor = white];
9 -> 168 [arrowhead = none ];
168 -> 10;

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

170 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = white];
11 -> 170 [arrowhead = none ];
170 -> 12;

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

172 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 172 [arrowhead = none ];
172 -> 14;

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

174 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 174 [arrowhead = none ];
174 -> 16;

175 [label="ONLY EVAL with clause\nno(X18).\nand substitution\nX18 -> empty(nil)", fontsize=14, style = filled, fillcolor = white];
15 -> 175 [arrowhead = none ];
175 -> 17;

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

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

178 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = white];
18 -> 178 [arrowhead = none ];
178 -> 19;

179 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
19 -> 179 [arrowhead = none ];
179 -> 20;

180 [label="ONLY EVAL with clause\ngopher(X35, X36) :- ','(no(empty(X35)), ','(head(X35, X37), ','(no(empty(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(tail(X35, X40), gopher(cons(X38, cons(X39, X40)), X36))))))).\nand substitution\nX35 -> nil\nT2 -> T11\nX36 -> T11\nT10 -> T11", fontsize=14, style = filled, fillcolor = white];
21 -> 180 [arrowhead = none ];
180 -> 22;

181 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 181 [arrowhead = none ];
181 -> 23;

182 [label="ONLY EVAL with clause\nno(X48) :- ','(call(X48), ','(!_6, failure(a))).\nand substitution\nX48 -> empty(nil)", fontsize=14, style = filled, fillcolor = white];
23 -> 182 [arrowhead = none ];
182 -> 24;

183 [label="CALL", fontsize=14, style = filled, fillcolor = white];
24 -> 183 [arrowhead = none ];
183 -> 25;

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

185 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = white];
26 -> 185 [arrowhead = none ];
185 -> 27;

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

187 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 187 [arrowhead = none ];
187 -> 29;

188 [label="ONLY EVAL with clause\nno(X56).\nand substitution\nX56 -> empty(nil)", fontsize=14, style = filled, fillcolor = white];
29 -> 188 [arrowhead = none ];
188 -> 30;

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

190 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = white];
31 -> 190 [arrowhead = none ];
190 -> 32;

191 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
32 -> 191 [arrowhead = none ];
191 -> 33;

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

193 [label="ONLY EVAL with clause\nno(X75) :- ','(call(X75), ','(!_10, failure(a))).\nand substitution\nX75 -> empty(nil)", fontsize=14, style = filled, fillcolor = white];
35 -> 193 [arrowhead = none ];
193 -> 36;

194 [label="CALL", fontsize=14, style = filled, fillcolor = white];
36 -> 194 [arrowhead = none ];
194 -> 37;

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

196 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = white];
38 -> 196 [arrowhead = none ];
196 -> 39;

197 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 197 [arrowhead = none ];
197 -> 40;

198 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 198 [arrowhead = none ];
198 -> 41;

199 [label="ONLY EVAL with clause\nno(X83).\nand substitution\nX83 -> empty(nil)", fontsize=14, style = filled, fillcolor = white];
41 -> 199 [arrowhead = none ];
199 -> 42;

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

201 [label="BACKTRACK\nfor clause: head([], X1)because of non-unification", fontsize=14, style = filled, fillcolor = white];
43 -> 201 [arrowhead = none ];
201 -> 44;

202 [label="BACKTRACK\nfor clause: head(.(X, X2), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
44 -> 202 [arrowhead = none ];
202 -> 45;

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

204 [label="ONLY EVAL with clause\ngopher(X269, X270) :- ','(no(empty(X269)), ','(head(X269, X271), ','(no(empty(X271)), ','(head(X271, X272), ','(tail(X271, X273), ','(tail(X269, X274), gopher(cons(X272, cons(X273, X274)), X270))))))).\nand substitution\nT1 -> T123\nX269 -> T123\nT2 -> T125\nX270 -> T125\nT124 -> T125", fontsize=14, style = filled, fillcolor = white];
47 -> 204 [arrowhead = none ];
204 -> 118;

205 [label="ONLY EVAL with clause\nno(X100) :- ','(call(X100), ','(!_14, failure(a))).\nand substitution\nT22 -> T27\nX100 -> empty(T27)", fontsize=14, style = filled, fillcolor = white];
48 -> 205 [arrowhead = none ];
205 -> 49;

206 [label="CALL", fontsize=14, style = filled, fillcolor = white];
49 -> 206 [arrowhead = none ];
206 -> 50;

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

208 [label="EVAL with clause\nempty([]).\nand substitution\nT27 -> []", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 208 [arrowhead = none ];
208 -> 52;

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

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

211 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 211 [arrowhead = none ];
211 -> 68;

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

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

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

215 [label="ONLY EVAL with clause\ngopher(X114, X115) :- ','(no(empty(X114)), ','(head(X114, X116), ','(no(empty(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(tail(X114, X119), gopher(cons(X117, cons(X118, X119)), X115))))))).\nand substitution\nX114 -> []\nT2 -> T33\nX115 -> T33\nT32 -> T33", fontsize=14, style = filled, fillcolor = white];
56 -> 215 [arrowhead = none ];
215 -> 59;

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

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

218 [label="ONLY EVAL with clause\nno(X127) :- ','(call(X127), ','(!_18, failure(a))).\nand substitution\nX127 -> empty([])", fontsize=14, style = filled, fillcolor = white];
60 -> 218 [arrowhead = none ];
218 -> 61;

219 [label="CALL", fontsize=14, style = filled, fillcolor = white];
61 -> 219 [arrowhead = none ];
219 -> 62;

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

221 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = white];
63 -> 221 [arrowhead = none ];
221 -> 64;

222 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 222 [arrowhead = none ];
222 -> 65;

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

224 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = white];
66 -> 224 [arrowhead = none ];
224 -> 67;

225 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 225 [arrowhead = none ];
225 -> 69;

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

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

228 [label="ONLY EVAL with clause\nno(X137).\nand substitution\nT27 -> T40\nX137 -> empty(T40)", fontsize=14, style = filled, fillcolor = white];
70 -> 228 [arrowhead = none ];
228 -> 72;

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

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

231 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T40), empty([]))", fontsize=14, style = filled, fillcolor = white];
73 -> 231 [arrowhead = none ];
231 -> 74;

232 [label="EVAL with clause\nhead(.(X143, X144), X143).\nand substitution\nX143 -> nil\nX144 -> T46\nT40 -> .(nil, T46)\nT45 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 232 [arrowhead = none ];
232 -> 75;

233 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 233 [arrowhead = none ];
233 -> 76;

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

235 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
77 -> 235 [arrowhead = none ];
235 -> 78;

236 [label="EVAL with clause\ntail(.(X151, X152), X152).\nand substitution\nX151 -> nil\nT46 -> T49\nX152 -> T49\nT24 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 236 [arrowhead = none ];
236 -> 79;

237 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 237 [arrowhead = none ];
237 -> 80;

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

239 [label="ONLY EVAL with clause\ngopher(X168, X169) :- ','(no(empty(X168)), ','(head(X168, X170), ','(no(empty(X170)), ','(head(X170, X171), ','(tail(X170, X172), ','(tail(X168, X173), gopher(cons(X171, cons(X172, X173)), X169))))))).\nand substitution\nT27 -> T56\nX168 -> T56\nT2 -> T58\nX169 -> T58\nT57 -> T58", fontsize=14, style = filled, fillcolor = white];
82 -> 239 [arrowhead = none ];
239 -> 83;

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

241 [label="ONLY EVAL with clause\nno(X181) :- ','(call(X181), ','(!_24, failure(a))).\nand substitution\nT56 -> T62\nX181 -> empty(T62)", fontsize=14, style = filled, fillcolor = white];
84 -> 241 [arrowhead = none ];
241 -> 85;

242 [label="CALL", fontsize=14, style = filled, fillcolor = white];
85 -> 242 [arrowhead = none ];
242 -> 86;

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

244 [label="BACKTRACK\nfor clause: empty([])\nwith clash: (empty(T62), empty([]))", fontsize=14, style = filled, fillcolor = white];
87 -> 244 [arrowhead = none ];
244 -> 88;

245 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 245 [arrowhead = none ];
245 -> 89;

246 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 246 [arrowhead = none ];
246 -> 90;

247 [label="ONLY EVAL with clause\nno(X189).\nand substitution\nT62 -> T66\nX189 -> empty(T66)", fontsize=14, style = filled, fillcolor = white];
90 -> 247 [arrowhead = none ];
247 -> 91;

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

249 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T66), empty([]))", fontsize=14, style = filled, fillcolor = white];
92 -> 249 [arrowhead = none ];
249 -> 93;

250 [label="EVAL with clause\nhead(.(X201, X202), X201).\nand substitution\nX201 -> T72\nX202 -> T73\nT66 -> .(T72, T73)\nX170 -> T72", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 250 [arrowhead = none ];
250 -> 94;

251 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 251 [arrowhead = none ];
251 -> 95;

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

253 [label="ONLY EVAL with clause\nno(X212) :- ','(call(X212), ','(!_28, failure(a))).\nand substitution\nT72 -> T77\nX212 -> empty(T77)", fontsize=14, style = filled, fillcolor = white];
96 -> 253 [arrowhead = none ];
253 -> 97;

254 [label="CALL", fontsize=14, style = filled, fillcolor = white];
97 -> 254 [arrowhead = none ];
254 -> 98;

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

256 [label="EVAL with clause\nempty([]).\nand substitution\nT77 -> []", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 256 [arrowhead = none ];
256 -> 100;

257 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 257 [arrowhead = none ];
257 -> 101;

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

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

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

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

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

263 [label="ONLY EVAL with clause\nno(X225).\nand substitution\nT77 -> T82\nX225 -> empty(T82)", fontsize=14, style = filled, fillcolor = white];
106 -> 263 [arrowhead = none ];
263 -> 107;

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

265 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T82), empty([]))", fontsize=14, style = filled, fillcolor = white];
108 -> 265 [arrowhead = none ];
265 -> 109;

266 [label="EVAL with clause\nhead(.(X237, X238), X237).\nand substitution\nX237 -> T88\nX238 -> T89\nT82 -> .(T88, T89)\nX171 -> T88", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 266 [arrowhead = none ];
266 -> 110;

267 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 267 [arrowhead = none ];
267 -> 111;

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

269 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
112 -> 269 [arrowhead = none ];
269 -> 113;

270 [label="ONLY EVAL with clause\ntail(.(X252, X253), X253).\nand substitution\nT88 -> T99\nX252 -> T99\nT89 -> T100\nX253 -> T100\nX172 -> T100", fontsize=14, style = filled, fillcolor = white];
113 -> 270 [arrowhead = none ];
270 -> 114;

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

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

273 [label="ONLY EVAL with clause\ntail(.(X263, X264), X264).\nand substitution\nT99 -> T114\nT100 -> T115\nX263 -> .(T114, T115)\nT73 -> T116\nX264 -> T116\nX173 -> T116", fontsize=14, style = filled, fillcolor = white];
116 -> 273 [arrowhead = none ];
273 -> 117;

274 [label="INSTANCE with matching:\nT1 -> cons(T114, cons(T115, T116))\nT2 -> T58", fontsize=14, style = filled, fillcolor = lightgrey];
117 -> 274 [arrowhead = none , style=dashed];
274 -> 1[style=dashed];

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

276 [label="ONLY EVAL with clause\nno(X277) :- ','(call(X277), ','(!_35, failure(a))).\nand substitution\nT123 -> T128\nX277 -> empty(T128)", fontsize=14, style = filled, fillcolor = white];
119 -> 276 [arrowhead = none ];
276 -> 120;

277 [label="CALL", fontsize=14, style = filled, fillcolor = white];
120 -> 277 [arrowhead = none ];
277 -> 121;

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

279 [label="EVAL with clause\nempty([]).\nand substitution\nT128 -> []", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 279 [arrowhead = none ];
279 -> 123;

280 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 280 [arrowhead = none ];
280 -> 124;

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

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

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

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

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

286 [label="ONLY EVAL with clause\nno(X290).\nand substitution\nT128 -> T133\nX290 -> empty(T133)", fontsize=14, style = filled, fillcolor = white];
129 -> 286 [arrowhead = none ];
286 -> 130;

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

288 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T133), empty([]))", fontsize=14, style = filled, fillcolor = white];
131 -> 288 [arrowhead = none ];
288 -> 132;

289 [label="EVAL with clause\nhead(.(X302, X303), X302).\nand substitution\nX302 -> T139\nX303 -> T140\nT133 -> .(T139, T140)\nX271 -> T139", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 289 [arrowhead = none ];
289 -> 133;

290 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 290 [arrowhead = none ];
290 -> 134;

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

292 [label="ONLY EVAL with clause\nno(X313) :- ','(call(X313), ','(!_40, failure(a))).\nand substitution\nT139 -> T144\nX313 -> empty(T144)", fontsize=14, style = filled, fillcolor = white];
135 -> 292 [arrowhead = none ];
292 -> 136;

293 [label="CALL", fontsize=14, style = filled, fillcolor = white];
136 -> 293 [arrowhead = none ];
293 -> 137;

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

295 [label="EVAL with clause\nempty([]).\nand substitution\nT144 -> []", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 295 [arrowhead = none ];
295 -> 139;

296 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 296 [arrowhead = none ];
296 -> 140;

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

298 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 298 [arrowhead = none ];
298 -> 144;

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

300 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = white];
142 -> 300 [arrowhead = none ];
300 -> 143;

301 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 301 [arrowhead = none ];
301 -> 145;

302 [label="ONLY EVAL with clause\nno(X326).\nand substitution\nT144 -> T149\nX326 -> empty(T149)", fontsize=14, style = filled, fillcolor = white];
145 -> 302 [arrowhead = none ];
302 -> 146;

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

304 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T149), empty([]))", fontsize=14, style = filled, fillcolor = white];
147 -> 304 [arrowhead = none ];
304 -> 148;

305 [label="EVAL with clause\nhead(.(X338, X339), X338).\nand substitution\nX338 -> T155\nX339 -> T156\nT149 -> .(T155, T156)\nX272 -> T155", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 305 [arrowhead = none ];
305 -> 149;

306 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 306 [arrowhead = none ];
306 -> 150;

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

308 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
151 -> 308 [arrowhead = none ];
308 -> 152;

309 [label="ONLY EVAL with clause\ntail(.(X353, X354), X354).\nand substitution\nT155 -> T166\nX353 -> T166\nT156 -> T167\nX354 -> T167\nX273 -> T167", fontsize=14, style = filled, fillcolor = white];
152 -> 309 [arrowhead = none ];
309 -> 153;

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

311 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
154 -> 311 [arrowhead = none ];
311 -> 155;

312 [label="ONLY EVAL with clause\ntail(.(X364, X365), X365).\nand substitution\nT166 -> T181\nT167 -> T182\nX364 -> .(T181, T182)\nT140 -> T183\nX365 -> T183\nX274 -> T183", fontsize=14, style = filled, fillcolor = white];
155 -> 312 [arrowhead = none ];
312 -> 156;

313 [label="INSTANCE with matching:\nT1 -> cons(T181, cons(T182, T183))\nT2 -> T125", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 313 [arrowhead = none , style=dashed];
313 -> 1[style=dashed];

}

(2) Obligation:

Triples:

gopher1(.(.(T114, T115), T116), T58) :- gopher1(cons(T114, cons(T115, T116)), T58).
gopher1(.(.(T181, T182), T183), T125) :- gopher1(cons(T181, cons(T182, T183)), T125).

Clauses:

gopherc1(nil, nil).
gopherc1(.(nil, T49), cons(nil, T49)).
gopherc1(.(.(T114, T115), T116), T58) :- gopherc1(cons(T114, cons(T115, T116)), T58).
gopherc1(.(.(T181, T182), T183), T125) :- gopherc1(cons(T181, cons(T182, T183)), T125).

Afs:

gopher1(x1, x2) = gopher1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
gopher1_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOPHER1_IN_GA(.(.(T114, T115), T116), T58) → U1_GA(T114, T115, T116, T58, gopher1_in_ga(cons(T114, cons(T115, T116)), T58))
GOPHER1_IN_GA(.(.(T114, T115), T116), T58) → GOPHER1_IN_GA(cons(T114, cons(T115, T116)), T58)
GOPHER1_IN_GA(.(.(T181, T182), T183), T125) → U2_GA(T181, T182, T183, T125, gopher1_in_ga(cons(T181, cons(T182, T183)), T125))

R is empty.
The argument filtering Pi contains the following mapping:
gopher1_in_ga(x1, x2) = gopher1_in_ga(x1)
.(x1, x2) = .(x1, x2)
cons(x1, x2) = cons(x1, x2)
GOPHER1_IN_GA(x1, x2) = GOPHER1_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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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