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

(0) Obligation:

Clauses:

gopher(nil, L) :- ','(!, eq(L, nil)).
gopher(X, Y) :- ','(head(X, nil), ','(!, ','(tail(X, T), eq(Y, cons(nil, T))))).
gopher(X, Y) :- ','(head(X, 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).
eq(X, X).

Query: gopher(g,a)

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

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: gopher(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: 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];
6 [label="6: ','(!_1, eq(T6, nil)) | gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: gopher(T1, T2), SCOPE: 1, CLAUSE: 1 | gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX6 is free\ngopher(T1, T2) !=? gopher(nil, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: eq(T6, nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: eq(T6, nil), SCOPE: 2, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(head(T15, nil), ','(!_1, ','(tail(T15, X17), eq(T17, cons(nil, X17))))) | gopher(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX6 is free\nX17 is free\ngopher(T15, T2) !=? gopher(nil, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(head(T15, nil), ','(!_1, ','(tail(T15, X17), eq(T17, cons(nil, X17))))), SCOPE: 3, CLAUSE: 3 | ','(head(T15, nil), ','(!_1, ','(tail(T15, X17), eq(T17, cons(nil, X17))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX6 is free\nX17 is free\ngopher(T15, T2) !=? gopher(nil, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(!_1, ','(tail([], X17), eq(T17, cons(nil, X17)))) | ','(head([], nil), ','(!_1, ','(tail([], X17), eq(T17, cons(nil, X17))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(head(T15, nil), ','(!_1, ','(tail(T15, X17), eq(T17, cons(nil, X17))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX6 is free\nX17 is free\nX20 is free\ngopher(T15, T2) !=? gopher(nil, X6)\nhead(T15, nil) !=? head([], X20)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(tail([], X17), eq(T17, cons(nil, X17)))\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 5 | ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 6\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: eq(T17, cons(nil, [])) | ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 6\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: eq(T17, cons(nil, [])), SCOPE: 5, CLAUSE: 7 | ?_5 | ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 6\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: true | ?_5 | ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 6\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ?_5 | ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 6\n\nX17 is free\nX23 is free\neq(T17, cons(nil, [])) !=? eq(X23, X23)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ?_5 | ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 6\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 6\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(tail([], X17), eq(T17, cons(nil, X17))), SCOPE: 4, CLAUSE: 6\n\nX17 is free\nX23 is free\neq(T17, cons(nil, [])) !=? eq(X23, X23)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(!_1, ','(tail(.(nil, T26), X17), eq(T17, cons(nil, X17)))) | ?_3 | gopher(.(nil, T26), T2), SCOPE: 1, CLAUSE: 2\n\nT26 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ?_3 | gopher(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX6 is free\nX20 is free\nX32 is free\nX33 is free\ngopher(T15, T2) !=? gopher(nil, X6)\nhead(T15, nil) !=? head([], X20)\nhead(T15, nil) !=? head(.(X32, X33), X32)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(tail(.(nil, T26), X17), eq(T17, cons(nil, X17)))\n\nT26 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(tail(.(nil, T26), X17), eq(T17, cons(nil, X17))), SCOPE: 6, CLAUSE: 5 | ','(tail(.(nil, T26), X17), eq(T17, cons(nil, X17))), SCOPE: 6, CLAUSE: 6\n\nT26 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(tail(.(nil, T26), X17), eq(T17, cons(nil, X17))), SCOPE: 6, CLAUSE: 6\n\nT26 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: eq(T17, cons(nil, T29))\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: eq(T17, cons(nil, T29)), SCOPE: 7, CLAUSE: 7\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: gopher(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX6 is free\nX20 is free\nX32 is free\nX33 is free\ngopher(T15, T2) !=? gopher(nil, X6)\nhead(T15, nil) !=? head([], X20)\nhead(T15, nil) !=? head(.(X32, X33), X32)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(head(T41, X54), ','(head(X54, X55), ','(tail(X54, X56), ','(tail(T41, X57), gopher(cons(X55, cons(X56, X57)), T43)))))\n\nT41 is ground\nX6 is free\nX20 is free\nX32 is free\nX33 is free\nX54 is free\nX55 is free\nX56 is free\nX57 is free\ngopher(T41, T2) !=? gopher(nil, X6)\nhead(T41, nil) !=? head([], X20)\nhead(T41, nil) !=? head(.(X32, X33), X32)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(head(T41, X54), ','(head(X54, X55), ','(tail(X54, X56), ','(tail(T41, X57), gopher(cons(X55, cons(X56, X57)), T43))))), SCOPE: 8, CLAUSE: 3 | ','(head(T41, X54), ','(head(X54, X55), ','(tail(X54, X56), ','(tail(T41, X57), gopher(cons(X55, cons(X56, X57)), T43))))), SCOPE: 8, CLAUSE: 4\n\nT41 is ground\nX6 is free\nX20 is free\nX32 is free\nX33 is free\nX54 is free\nX55 is free\nX56 is free\nX57 is free\ngopher(T41, T2) !=? gopher(nil, X6)\nhead(T41, nil) !=? head([], X20)\nhead(T41, nil) !=? head(.(X32, X33), X32)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(head(T41, X54), ','(head(X54, X55), ','(tail(X54, X56), ','(tail(T41, X57), gopher(cons(X55, cons(X56, X57)), T43))))), SCOPE: 8, CLAUSE: 4\n\nT41 is ground\nX6 is free\nX20 is free\nX32 is free\nX33 is free\nX54 is free\nX55 is free\nX56 is free\nX57 is free\ngopher(T41, T2) !=? gopher(nil, X6)\nhead(T41, nil) !=? head([], X20)\nhead(T41, nil) !=? head(.(X32, X33), X32)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(head(T48, X55), ','(tail(T48, X56), ','(tail(.(T48, T49), X57), gopher(cons(X55, cons(X56, X57)), T43))))\n\nT48 is ground\nT49 is ground\nX32 is free\nX33 is free\nX55 is free\nX56 is free\nX57 is free\nhead(.(T48, T49), nil) !=? head(.(X32, X33), X32)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(head(T48, X55), ','(tail(T48, X56), ','(tail(.(T48, T49), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 3 | ','(head(T48, X55), ','(tail(T48, X56), ','(tail(.(T48, T49), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT48 is ground\nT49 is ground\nX32 is free\nX33 is free\nX55 is free\nX56 is free\nX57 is free\nhead(.(T48, T49), nil) !=? head(.(X32, X33), X32)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X73, cons(X56, X57)), T43))) | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT49 is ground\nX55 is free\nX56 is free\nX57 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(head(T48, X55), ','(tail(T48, X56), ','(tail(.(T48, T49), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT48 is ground\nT49 is ground\nX32 is free\nX33 is free\nX55 is free\nX56 is free\nX57 is free\nX72 is free\nhead(.(T48, T49), nil) !=? head(.(X32, X33), X32)\nhead(T48, X55) !=? head([], X72)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X73, cons(X56, X57)), T43))), SCOPE: 10, CLAUSE: 5 | ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X73, cons(X56, X57)), T43))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT49 is ground\nX55 is free\nX56 is free\nX57 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(tail(.([], T49), X57), gopher(cons(X73, cons([], X57)), T43)) | ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X73, cons(X56, X57)), T43))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT49 is ground\nX55 is free\nX56 is free\nX57 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(tail(.([], T49), X57), gopher(cons(X73, cons([], X57)), T43)), SCOPE: 11, CLAUSE: 5 | ','(tail(.([], T49), X57), gopher(cons(X73, cons([], X57)), T43)), SCOPE: 11, CLAUSE: 6 | ?_11 | ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X73, cons(X56, X57)), T43))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT49 is ground\nX55 is free\nX56 is free\nX57 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(tail(.([], T49), X57), gopher(cons(X73, cons([], X57)), T43)), SCOPE: 11, CLAUSE: 6 | ?_11 | ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X73, cons(X56, X57)), T43))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T49), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT49 is ground\nX55 is free\nX56 is free\nX57 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: gopher(cons(X73, cons([], T52)), T43) | ?_11 | ','(tail([], X56), ','(tail(.([], T52), X57), gopher(cons(X73, cons(X56, X57)), T43))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T52), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT52 is ground\nX55 is free\nX56 is free\nX57 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: gopher(cons(X73, cons([], T52)), T43)\n\nT52 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ?_11 | ','(tail([], X56), ','(tail(.([], T52), X57), gopher(cons(X73, cons(X56, X57)), T43))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T52), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT52 is ground\nX55 is free\nX56 is free\nX57 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: gopher(cons(X73, cons([], T52)), T43), SCOPE: 12, CLAUSE: 0 | gopher(cons(X73, cons([], T52)), T43), SCOPE: 12, CLAUSE: 1 | gopher(cons(X73, cons([], T52)), T43), SCOPE: 12, CLAUSE: 2\n\nT52 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: gopher(cons(X73, cons([], T52)), T43), SCOPE: 12, CLAUSE: 1 | gopher(cons(X73, cons([], T52)), T43), SCOPE: 12, CLAUSE: 2\n\nT52 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(head(cons(X97, cons([], T58)), nil), ','(!_12, ','(tail(cons(X97, cons([], T58)), X96), eq(T60, cons(nil, X96))))) | gopher(cons(X73, cons([], T58)), T43), SCOPE: 12, CLAUSE: 2\n\nT58 is ground\nX73 is free\nX97 is free\nX96 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(head(cons(X97, cons([], T58)), nil), ','(!_12, ','(tail(cons(X97, cons([], T58)), X96), eq(T60, cons(nil, X96))))), SCOPE: 13, CLAUSE: 3 | ','(head(cons(X97, cons([], T58)), nil), ','(!_12, ','(tail(cons(X97, cons([], T58)), X96), eq(T60, cons(nil, X96))))), SCOPE: 13, CLAUSE: 4 | ?_13 | gopher(cons(X73, cons([], T58)), T43), SCOPE: 12, CLAUSE: 2\n\nT58 is ground\nX73 is free\nX97 is free\nX96 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(head(cons(X97, cons([], T58)), nil), ','(!_12, ','(tail(cons(X97, cons([], T58)), X96), eq(T60, cons(nil, X96))))), SCOPE: 13, CLAUSE: 4 | ?_13 | gopher(cons(X73, cons([], T58)), T43), SCOPE: 12, CLAUSE: 2\n\nT58 is ground\nX73 is free\nX97 is free\nX96 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ?_13 | gopher(cons(X73, cons([], T58)), T43), SCOPE: 12, CLAUSE: 2\n\nT58 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: gopher(cons(X73, cons([], T58)), T43), SCOPE: 12, CLAUSE: 2\n\nT58 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(head(cons(X118, cons([], T66)), X114), ','(head(X114, X115), ','(tail(X114, X116), ','(tail(cons(X118, cons([], T66)), X117), gopher(cons(X115, cons(X116, X117)), T68)))))\n\nT66 is ground\nX118 is free\nX114 is free\nX115 is free\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(head(cons(X118, cons([], T66)), X114), ','(head(X114, X115), ','(tail(X114, X116), ','(tail(cons(X118, cons([], T66)), X117), gopher(cons(X115, cons(X116, X117)), T68))))), SCOPE: 14, CLAUSE: 3 | ','(head(cons(X118, cons([], T66)), X114), ','(head(X114, X115), ','(tail(X114, X116), ','(tail(cons(X118, cons([], T66)), X117), gopher(cons(X115, cons(X116, X117)), T68))))), SCOPE: 14, CLAUSE: 4\n\nT66 is ground\nX118 is free\nX114 is free\nX115 is free\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(head(cons(X118, cons([], T66)), X114), ','(head(X114, X115), ','(tail(X114, X116), ','(tail(cons(X118, cons([], T66)), X117), gopher(cons(X115, cons(X116, X117)), T68))))), SCOPE: 14, CLAUSE: 4\n\nT66 is ground\nX118 is free\nX114 is free\nX115 is free\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(tail([], X56), ','(tail(.([], T52), X57), gopher(cons(X73, cons(X56, X57)), T43))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T52), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT52 is ground\nX55 is free\nX56 is free\nX57 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ?_10 | ','(head([], X55), ','(tail([], X56), ','(tail(.([], T52), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT52 is ground\nX55 is free\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(head([], X55), ','(tail([], X56), ','(tail(.([], T52), X57), gopher(cons(X55, cons(X56, X57)), T43)))), SCOPE: 9, CLAUSE: 4\n\nT52 is ground\nX55 is free\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(tail(.(T73, T74), X56), ','(tail(.(.(T73, T74), T49), X57), gopher(cons(T73, cons(X56, X57)), T43)))\n\nT49 is ground\nT73 is ground\nT74 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(tail(.(T73, T74), X56), ','(tail(.(.(T73, T74), T49), X57), gopher(cons(T73, cons(X56, X57)), T43))), SCOPE: 15, CLAUSE: 5 | ','(tail(.(T73, T74), X56), ','(tail(.(.(T73, T74), T49), X57), gopher(cons(T73, cons(X56, X57)), T43))), SCOPE: 15, CLAUSE: 6\n\nT49 is ground\nT73 is ground\nT74 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(tail(.(T73, T74), X56), ','(tail(.(.(T73, T74), T49), X57), gopher(cons(T73, cons(X56, X57)), T43))), SCOPE: 15, CLAUSE: 6\n\nT49 is ground\nT73 is ground\nT74 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(tail(.(.(T79, T80), T49), X57), gopher(cons(T79, cons(T80, X57)), T43))\n\nT49 is ground\nT79 is ground\nT80 is ground\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(tail(.(.(T79, T80), T49), X57), gopher(cons(T79, cons(T80, X57)), T43)), SCOPE: 16, CLAUSE: 5 | ','(tail(.(.(T79, T80), T49), X57), gopher(cons(T79, cons(T80, X57)), T43)), SCOPE: 16, CLAUSE: 6\n\nT49 is ground\nT79 is ground\nT80 is ground\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(tail(.(.(T79, T80), T49), X57), gopher(cons(T79, cons(T80, X57)), T43)), SCOPE: 16, CLAUSE: 6\n\nT49 is ground\nT79 is ground\nT80 is ground\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: gopher(cons(T87, cons(T88, T89)), T43)\n\nT87 is ground\nT88 is ground\nT89 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 147 [arrowhead = none ];
147 -> 4;

148 [label="EVAL with clause\ngopher(nil, X6) :- ','(!_1, eq(X6, nil)).\nand substitutionT1 -> nil,\nT2 -> T6,\nX6 -> T6,\nT5 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 148 [arrowhead = none ];
148 -> 6;

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

150 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 150 [arrowhead = none ];
150 -> 14;

151 [label="ONLY EVAL with clause\ngopher(X15, X16) :- ','(head(X15, nil), ','(!_1, ','(tail(X15, X17), eq(X16, cons(nil, X17))))).\nand substitutionT1 -> T15,\nX15 -> T15,\nT2 -> T17,\nX16 -> T17,\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 151 [arrowhead = none ];
151 -> 25;

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

153 [label="EVAL with clause\neq(X9, X9).\nand substitutionT6 -> nil,\nX9 -> nil,\nT9 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 153 [arrowhead = none ];
153 -> 16;

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

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

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

157 [label="EVAL with clause\nhead([], X20).\nand substitutionT15 -> [],\nX20 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 157 [arrowhead = none ];
157 -> 29;

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

159 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 159 [arrowhead = none ];
159 -> 34;

160 [label="EVAL with clause\nhead(.(X32, X33), X32).\nand substitutionX32 -> nil,\nX33 -> T26,\nT15 -> .(nil, T26),\nT25 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 160 [arrowhead = none ];
160 -> 54;

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

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

163 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX17 -> []", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 163 [arrowhead = none ];
163 -> 38;

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

165 [label="EVAL with clause\neq(X23, X23).\nand substitutionT17 -> cons(nil, []),\nX23 -> cons(nil, []),\nT20 -> cons(nil, [])", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 165 [arrowhead = none ];
165 -> 42;

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

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

168 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 168 [arrowhead = none ];
168 -> 47;

169 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 169 [arrowhead = none ];
169 -> 45;

170 [label="BACKTRACK\nfor clause: tail(.(X3, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 170 [arrowhead = none ];
170 -> 46;

171 [label="BACKTRACK\nfor clause: tail(.(X3, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 171 [arrowhead = none ];
171 -> 49;

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

173 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 173 [arrowhead = none ];
173 -> 70;

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

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

176 [label="ONLY EVAL with clause\ntail(.(X38, X39), X39).\nand substitutionX38 -> nil,\nT26 -> T29,\nX39 -> T29,\nX17 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 176 [arrowhead = none ];
176 -> 64;

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

178 [label="EVAL with clause\neq(X42, X42).\nand substitutionT17 -> cons(nil, T35),\nX42 -> cons(nil, T35),\nT29 -> T35,\nT34 -> cons(nil, T35)", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 178 [arrowhead = none ];
178 -> 67;

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

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

181 [label="ONLY EVAL with clause\ngopher(X52, X53) :- ','(head(X52, X54), ','(head(X54, X55), ','(tail(X54, X56), ','(tail(X52, X57), gopher(cons(X55, cons(X56, X57)), X53))))).\nand substitutionT15 -> T41,\nX52 -> T41,\nT2 -> T43,\nX53 -> T43,\nT42 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 181 [arrowhead = none ];
181 -> 73;

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

183 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (head(T41, nil), head([], X20))", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 183 [arrowhead = none ];
183 -> 76;

184 [label="EVAL with clause\nhead(.(X65, X66), X65).\nand substitutionX65 -> T48,\nX66 -> T49,\nT41 -> .(T48, T49),\nX54 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 184 [arrowhead = none ];
184 -> 80;

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

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

187 [label="EVAL with clause\nhead([], X72).\nand substitutionT48 -> [],\nX55 -> X73,\nX72 -> X73", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 187 [arrowhead = none ];
187 -> 86;

188 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 188 [arrowhead = none ];
188 -> 88;

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

190 [label="EVAL with clause\nhead(.(X131, X132), X131).\nand substitutionX131 -> T73,\nX132 -> T74,\nT48 -> .(T73, T74),\nX55 -> T73", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 190 [arrowhead = none ];
190 -> 133;

191 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 191 [arrowhead = none ];
191 -> 135;

192 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX56 -> []", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 192 [arrowhead = none ];
192 -> 92;

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

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

195 [label="ONLY EVAL with clause\ntail(.(X82, X83), X83).\nand substitutionX82 -> [],\nT49 -> T52,\nX83 -> T52,\nX57 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 195 [arrowhead = none ];
195 -> 96;

196 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
96 -> 196 [arrowhead = none ];
196 -> 98;

197 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
96 -> 197 [arrowhead = none ];
197 -> 100;

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

199 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 199 [arrowhead = none ];
199 -> 125;

200 [label="BACKTRACK\nfor clause: gopher(nil, L) :- ','(!, eq(L, nil))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 200 [arrowhead = none ];
200 -> 104;

201 [label="ONLY EVAL with clause\ngopher(X94, X95) :- ','(head(X94, nil), ','(!_12, ','(tail(X94, X96), eq(X95, cons(nil, X96))))).\nand substitutionX73 -> X97,\nT52 -> T58,\nX94 -> cons(X97, cons([], T58)),\nT43 -> T60,\nX95 -> T60,\nT59 -> T60", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 201 [arrowhead = none ];
201 -> 106;

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

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

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

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

206 [label="ONLY EVAL with clause\ngopher(X112, X113) :- ','(head(X112, X114), ','(head(X114, X115), ','(tail(X114, X116), ','(tail(X112, X117), gopher(cons(X115, cons(X116, X117)), X113))))).\nand substitutionX73 -> X118,\nT58 -> T66,\nX112 -> cons(X118, cons([], T66)),\nT43 -> T68,\nX113 -> T68,\nT67 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 206 [arrowhead = none ];
206 -> 116;

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

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

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

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

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

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

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

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

215 [label="ONLY EVAL with clause\ntail(.(X139, X140), X140).\nand substitutionT73 -> T79,\nX139 -> T79,\nT74 -> T80,\nX140 -> T80,\nX56 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 215 [arrowhead = none ];
215 -> 142;

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

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

218 [label="ONLY EVAL with clause\ntail(.(X147, X148), X148).\nand substitutionT79 -> T87,\nT80 -> T88,\nX147 -> .(T87, T88),\nT49 -> T89,\nX148 -> T89,\nX57 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 218 [arrowhead = none ];
218 -> 146;

219 [label="INSTANCE with matching:\nT1 -> cons(T87, cons(T88, T89))\nT2 -> T43", fontsize=14, style = filled, fillcolor = lightgrey];
146 -> 219 [arrowhead = none , style=dashed];
219 -> 2[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in([]) → f2_out1
f2_in(.(nil, z0)) → f2_out1
f2_in(.([], z0)) → U1(f96_in(z0), .([], z0))
f2_in(.(.(z0, z1), z2)) → U2(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f96_out1, .([], z0)) → f2_out1
U1(f96_out3(z0, z1), .([], z2)) → f2_out1
U1(f96_out5(z0, z1), .([], z2)) → f2_out1
U2(f2_out1, .(.(z0, z1), z2)) → f2_out1
f96_in(z0) → U3(f98_in(z0), f100_in(z0), z0)
U3(f98_out1, z0, z1) → f96_out1
U3(z0, f100_out2(z1, z2), z3) → f96_out3(z1, z2)
U3(z0, f100_out4(z1, z2), z3) → f96_out5(z1, z2)

Tuples:

F2_IN(.([], z0)) → c3(U1'(f96_in(z0), .([], z0)), F96_IN(z0))
F2_IN(.(.(z0, z1), z2)) → c4(U2'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F2_IN(cons(z0, cons(z1, z2))))
F96_IN(z0) → c9(U3'(f98_in(z0), f100_in(z0), z0))

S tuples:

F2_IN(.([], z0)) → c3(U1'(f96_in(z0), .([], z0)), F96_IN(z0))
F2_IN(.(.(z0, z1), z2)) → c4(U2'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F2_IN(cons(z0, cons(z1, z2))))
F96_IN(z0) → c9(U3'(f98_in(z0), f100_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f96_in, U3

Defined Pair Symbols:

F2_IN, F96_IN

Compound Symbols:

c3, c4, c9

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in([]) → f2_out1
f2_in(.(nil, z0)) → f2_out1
f2_in(.([], z0)) → U1(f96_in(z0), .([], z0))
f2_in(.(.(z0, z1), z2)) → U2(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f96_out1, .([], z0)) → f2_out1
U1(f96_out3(z0, z1), .([], z2)) → f2_out1
U1(f96_out5(z0, z1), .([], z2)) → f2_out1
U2(f2_out1, .(.(z0, z1), z2)) → f2_out1
f96_in(z0) → U3(f98_in(z0), f100_in(z0), z0)
U3(f98_out1, z0, z1) → f96_out1
U3(z0, f100_out2(z1, z2), z3) → f96_out3(z1, z2)
U3(z0, f100_out4(z1, z2), z3) → f96_out5(z1, z2)

Tuples:

F96_IN(z0) → c9(U3'(f98_in(z0), f100_in(z0), z0))
F2_IN(.([], z0)) → c(U1'(f96_in(z0), .([], z0)))
F2_IN(.([], z0)) → c(F96_IN(z0))
F2_IN(.(.(z0, z1), z2)) → c(U2'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
F2_IN(.(.(z0, z1), z2)) → c(F2_IN(cons(z0, cons(z1, z2))))

S tuples:

F96_IN(z0) → c9(U3'(f98_in(z0), f100_in(z0), z0))
F2_IN(.([], z0)) → c(U1'(f96_in(z0), .([], z0)))
F2_IN(.([], z0)) → c(F96_IN(z0))
F2_IN(.(.(z0, z1), z2)) → c(U2'(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
F2_IN(.(.(z0, z1), z2)) → c(F2_IN(cons(z0, cons(z1, z2))))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f96_in, U3

Defined Pair Symbols:

F96_IN, F2_IN

Compound Symbols:

c9, c

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

Removed 4 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(nil) → f2_out1
f2_in([]) → f2_out1
f2_in(.(nil, z0)) → f2_out1
f2_in(.([], z0)) → U1(f96_in(z0), .([], z0))
f2_in(.(.(z0, z1), z2)) → U2(f2_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f96_out1, .([], z0)) → f2_out1
U1(f96_out3(z0, z1), .([], z2)) → f2_out1
U1(f96_out5(z0, z1), .([], z2)) → f2_out1
U2(f2_out1, .(.(z0, z1), z2)) → f2_out1
f96_in(z0) → U3(f98_in(z0), f100_in(z0), z0)
U3(f98_out1, z0, z1) → f96_out1
U3(z0, f100_out2(z1, z2), z3) → f96_out3(z1, z2)
U3(z0, f100_out4(z1, z2), z3) → f96_out5(z1, z2)

Tuples:

F2_IN(.([], z0)) → c(F96_IN(z0))
F96_IN(z0) → c9
F2_IN(.([], z0)) → c
F2_IN(.(.(z0, z1), z2)) → c

S tuples:

F2_IN(.([], z0)) → c(F96_IN(z0))
F96_IN(z0) → c9
F2_IN(.([], z0)) → c
F2_IN(.(.(z0, z1), z2)) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f96_in, U3

Defined Pair Symbols:

F2_IN, F96_IN

Compound Symbols:

c, c9, c

(7) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(.([], z0)) → c(F96_IN(z0))
F96_IN(z0) → c9
F2_IN(.([], z0)) → c
F2_IN(.(.(z0, z1), z2)) → c
F2_IN(.(.(z0, z1), z2)) → c
F96_IN(z0) → c9

Now S is empty

(8) BOUNDS(O(1), O(1))

(9) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: gopher(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: 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];
5 [label="5: ','(!_1, eq(T5, nil)) | gopher(nil, T2), SCOPE: 1, CLAUSE: 1 | gopher(nil, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: gopher(T1, T2), SCOPE: 1, CLAUSE: 1 | gopher(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX5 is free\ngopher(T1, T2) !=? gopher(nil, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: eq(T5, nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: eq(T5, nil), SCOPE: 2, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(head(T11, nil), ','(!_1, ','(tail(T11, X13), eq(T13, cons(nil, X13))))) | gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX13 is free\ngopher(T11, T2) !=? gopher(nil, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(head(T11, nil), ','(!_1, ','(tail(T11, X13), eq(T13, cons(nil, X13))))), SCOPE: 3, CLAUSE: 3 | ','(head(T11, nil), ','(!_1, ','(tail(T11, X13), eq(T13, cons(nil, X13))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX13 is free\ngopher(T11, T2) !=? gopher(nil, X5)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(!_1, ','(tail([], X13), eq(T13, cons(nil, X13)))) | ','(head([], nil), ','(!_1, ','(tail([], X13), eq(T13, cons(nil, X13))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher([], T2), SCOPE: 1, CLAUSE: 2\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(head(T11, nil), ','(!_1, ','(tail(T11, X13), eq(T13, cons(nil, X13))))), SCOPE: 3, CLAUSE: 4 | ?_3 | gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX13 is free\nX16 is free\ngopher(T11, T2) !=? gopher(nil, X5)\nhead(T11, nil) !=? head([], X16)", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(tail([], X13), eq(T13, cons(nil, X13)))\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 5 | ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: eq(T13, cons(nil, [])) | ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: eq(T13, cons(nil, [])), SCOPE: 5, CLAUSE: 7 | ?_5 | ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true | ?_5 | ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ?_5 | ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free\nX19 is free\neq(T13, cons(nil, [])) !=? eq(X19, X19)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ?_5 | ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(tail([], X13), eq(T13, cons(nil, X13))), SCOPE: 4, CLAUSE: 6\n\nX13 is free\nX19 is free\neq(T13, cons(nil, [])) !=? eq(X19, X19)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(!_1, ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13)))) | ?_3 | gopher(.(nil, T22), T2), SCOPE: 1, CLAUSE: 2\n\nT22 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ?_3 | gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX16 is free\nX28 is free\nX29 is free\ngopher(T11, T2) !=? gopher(nil, X5)\nhead(T11, nil) !=? head([], X16)\nhead(T11, nil) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13)))\n\nT22 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13))), SCOPE: 6, CLAUSE: 5 | ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13))), SCOPE: 6, CLAUSE: 6\n\nT22 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(tail(.(nil, T22), X13), eq(T13, cons(nil, X13))), SCOPE: 6, CLAUSE: 6\n\nT22 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: eq(T13, cons(nil, T25))\n\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: eq(T13, cons(nil, T25)), SCOPE: 7, CLAUSE: 7\n\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: gopher(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX5 is free\nX16 is free\nX28 is free\nX29 is free\ngopher(T11, T2) !=? gopher(nil, X5)\nhead(T11, nil) !=? head([], X16)\nhead(T11, nil) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(head(T37, X50), ','(head(X50, X51), ','(tail(X50, X52), ','(tail(T37, X53), gopher(cons(X51, cons(X52, X53)), T39)))))\n\nT37 is ground\nX5 is free\nX16 is free\nX28 is free\nX29 is free\nX50 is free\nX51 is free\nX52 is free\nX53 is free\ngopher(T37, T2) !=? gopher(nil, X5)\nhead(T37, nil) !=? head([], X16)\nhead(T37, nil) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(head(T37, X50), ','(head(X50, X51), ','(tail(X50, X52), ','(tail(T37, X53), gopher(cons(X51, cons(X52, X53)), T39))))), SCOPE: 8, CLAUSE: 3 | ','(head(T37, X50), ','(head(X50, X51), ','(tail(X50, X52), ','(tail(T37, X53), gopher(cons(X51, cons(X52, X53)), T39))))), SCOPE: 8, CLAUSE: 4\n\nT37 is ground\nX5 is free\nX16 is free\nX28 is free\nX29 is free\nX50 is free\nX51 is free\nX52 is free\nX53 is free\ngopher(T37, T2) !=? gopher(nil, X5)\nhead(T37, nil) !=? head([], X16)\nhead(T37, nil) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(head(T37, X50), ','(head(X50, X51), ','(tail(X50, X52), ','(tail(T37, X53), gopher(cons(X51, cons(X52, X53)), T39))))), SCOPE: 8, CLAUSE: 4\n\nT37 is ground\nX5 is free\nX16 is free\nX28 is free\nX29 is free\nX50 is free\nX51 is free\nX52 is free\nX53 is free\ngopher(T37, T2) !=? gopher(nil, X5)\nhead(T37, nil) !=? head([], X16)\nhead(T37, nil) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(head(T44, X51), ','(tail(T44, X52), ','(tail(.(T44, T45), X53), gopher(cons(X51, cons(X52, X53)), T39))))\n\nT44 is ground\nT45 is ground\nX28 is free\nX29 is free\nX51 is free\nX52 is free\nX53 is free\nhead(.(T44, T45), nil) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(head(T44, X51), ','(tail(T44, X52), ','(tail(.(T44, T45), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 3 | ','(head(T44, X51), ','(tail(T44, X52), ','(tail(.(T44, T45), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT44 is ground\nT45 is ground\nX28 is free\nX29 is free\nX51 is free\nX52 is free\nX53 is free\nhead(.(T44, T45), nil) !=? head(.(X28, X29), X28)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X69, cons(X52, X53)), T39))) | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT45 is ground\nX51 is free\nX52 is free\nX53 is free\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(head(T44, X51), ','(tail(T44, X52), ','(tail(.(T44, T45), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT44 is ground\nT45 is ground\nX28 is free\nX29 is free\nX51 is free\nX52 is free\nX53 is free\nX68 is free\nhead(.(T44, T45), nil) !=? head(.(X28, X29), X28)\nhead(T44, X51) !=? head([], X68)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X69, cons(X52, X53)), T39))), SCOPE: 10, CLAUSE: 5 | ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X69, cons(X52, X53)), T39))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT45 is ground\nX51 is free\nX52 is free\nX53 is free\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(tail(.([], T45), X53), gopher(cons(X69, cons([], X53)), T39)) | ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X69, cons(X52, X53)), T39))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT45 is ground\nX51 is free\nX52 is free\nX53 is free\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(tail(.([], T45), X53), gopher(cons(X69, cons([], X53)), T39)), SCOPE: 11, CLAUSE: 5 | ','(tail(.([], T45), X53), gopher(cons(X69, cons([], X53)), T39)), SCOPE: 11, CLAUSE: 6 | ?_11 | ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X69, cons(X52, X53)), T39))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT45 is ground\nX51 is free\nX52 is free\nX53 is free\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(tail(.([], T45), X53), gopher(cons(X69, cons([], X53)), T39)), SCOPE: 11, CLAUSE: 6 | ?_11 | ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X69, cons(X52, X53)), T39))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T45), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT45 is ground\nX51 is free\nX52 is free\nX53 is free\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: gopher(cons(X69, cons([], T48)), T39) | ?_11 | ','(tail([], X52), ','(tail(.([], T48), X53), gopher(cons(X69, cons(X52, X53)), T39))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T48), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT48 is ground\nX51 is free\nX52 is free\nX53 is free\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: gopher(cons(X69, cons([], T48)), T39)\n\nT48 is ground\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ?_11 | ','(tail([], X52), ','(tail(.([], T48), X53), gopher(cons(X69, cons(X52, X53)), T39))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T48), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT48 is ground\nX51 is free\nX52 is free\nX53 is free\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: gopher(cons(X69, cons([], T48)), T39), SCOPE: 12, CLAUSE: 0 | gopher(cons(X69, cons([], T48)), T39), SCOPE: 12, CLAUSE: 1 | gopher(cons(X69, cons([], T48)), T39), SCOPE: 12, CLAUSE: 2\n\nT48 is ground\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: gopher(cons(X69, cons([], T48)), T39), SCOPE: 12, CLAUSE: 1 | gopher(cons(X69, cons([], T48)), T39), SCOPE: 12, CLAUSE: 2\n\nT48 is ground\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(head(cons(X93, cons([], T54)), nil), ','(!_12, ','(tail(cons(X93, cons([], T54)), X92), eq(T56, cons(nil, X92))))) | gopher(cons(X69, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX69 is free\nX93 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(head(cons(X93, cons([], T54)), nil), ','(!_12, ','(tail(cons(X93, cons([], T54)), X92), eq(T56, cons(nil, X92))))), SCOPE: 13, CLAUSE: 3 | ','(head(cons(X93, cons([], T54)), nil), ','(!_12, ','(tail(cons(X93, cons([], T54)), X92), eq(T56, cons(nil, X92))))), SCOPE: 13, CLAUSE: 4 | ?_13 | gopher(cons(X69, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX69 is free\nX93 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(head(cons(X93, cons([], T54)), nil), ','(!_12, ','(tail(cons(X93, cons([], T54)), X92), eq(T56, cons(nil, X92))))), SCOPE: 13, CLAUSE: 4 | ?_13 | gopher(cons(X69, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX69 is free\nX93 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ?_13 | gopher(cons(X69, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: gopher(cons(X69, cons([], T54)), T39), SCOPE: 12, CLAUSE: 2\n\nT54 is ground\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(head(cons(X114, cons([], T62)), X110), ','(head(X110, X111), ','(tail(X110, X112), ','(tail(cons(X114, cons([], T62)), X113), gopher(cons(X111, cons(X112, X113)), T64)))))\n\nT62 is ground\nX114 is free\nX110 is free\nX111 is free\nX112 is free\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(head(cons(X114, cons([], T62)), X110), ','(head(X110, X111), ','(tail(X110, X112), ','(tail(cons(X114, cons([], T62)), X113), gopher(cons(X111, cons(X112, X113)), T64))))), SCOPE: 14, CLAUSE: 3 | ','(head(cons(X114, cons([], T62)), X110), ','(head(X110, X111), ','(tail(X110, X112), ','(tail(cons(X114, cons([], T62)), X113), gopher(cons(X111, cons(X112, X113)), T64))))), SCOPE: 14, CLAUSE: 4\n\nT62 is ground\nX114 is free\nX110 is free\nX111 is free\nX112 is free\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(head(cons(X114, cons([], T62)), X110), ','(head(X110, X111), ','(tail(X110, X112), ','(tail(cons(X114, cons([], T62)), X113), gopher(cons(X111, cons(X112, X113)), T64))))), SCOPE: 14, CLAUSE: 4\n\nT62 is ground\nX114 is free\nX110 is free\nX111 is free\nX112 is free\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(tail([], X52), ','(tail(.([], T48), X53), gopher(cons(X69, cons(X52, X53)), T39))), SCOPE: 10, CLAUSE: 6 | ?_10 | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T48), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT48 is ground\nX51 is free\nX52 is free\nX53 is free\nX69 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ?_10 | ','(head([], X51), ','(tail([], X52), ','(tail(.([], T48), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT48 is ground\nX51 is free\nX52 is free\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(head([], X51), ','(tail([], X52), ','(tail(.([], T48), X53), gopher(cons(X51, cons(X52, X53)), T39)))), SCOPE: 9, CLAUSE: 4\n\nT48 is ground\nX51 is free\nX52 is free\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(tail(.(T69, T70), X52), ','(tail(.(.(T69, T70), T45), X53), gopher(cons(T69, cons(X52, X53)), T39)))\n\nT45 is ground\nT69 is ground\nT70 is ground\nX52 is free\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(tail(.(T69, T70), X52), ','(tail(.(.(T69, T70), T45), X53), gopher(cons(T69, cons(X52, X53)), T39))), SCOPE: 15, CLAUSE: 5 | ','(tail(.(T69, T70), X52), ','(tail(.(.(T69, T70), T45), X53), gopher(cons(T69, cons(X52, X53)), T39))), SCOPE: 15, CLAUSE: 6\n\nT45 is ground\nT69 is ground\nT70 is ground\nX52 is free\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(tail(.(T69, T70), X52), ','(tail(.(.(T69, T70), T45), X53), gopher(cons(T69, cons(X52, X53)), T39))), SCOPE: 15, CLAUSE: 6\n\nT45 is ground\nT69 is ground\nT70 is ground\nX52 is free\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(tail(.(.(T75, T76), T45), X53), gopher(cons(T75, cons(T76, X53)), T39))\n\nT45 is ground\nT75 is ground\nT76 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(tail(.(.(T75, T76), T45), X53), gopher(cons(T75, cons(T76, X53)), T39)), SCOPE: 16, CLAUSE: 5 | ','(tail(.(.(T75, T76), T45), X53), gopher(cons(T75, cons(T76, X53)), T39)), SCOPE: 16, CLAUSE: 6\n\nT45 is ground\nT75 is ground\nT76 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(tail(.(.(T75, T76), T45), X53), gopher(cons(T75, cons(T76, X53)), T39)), SCOPE: 16, CLAUSE: 6\n\nT45 is ground\nT75 is ground\nT76 is ground\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: gopher(cons(T83, cons(T84, T85)), T39)\n\nT83 is ground\nT84 is ground\nT85 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 146 [arrowhead = none ];
146 -> 3;

147 [label="EVAL with clause\ngopher(nil, X5) :- ','(!_1, eq(X5, nil)).\nand substitutionT1 -> nil,\nT2 -> T5,\nX5 -> T5,\nT4 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 147 [arrowhead = none ];
147 -> 5;

148 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 148 [arrowhead = none ];
148 -> 7;

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

150 [label="ONLY EVAL with clause\ngopher(X11, X12) :- ','(head(X11, nil), ','(!_1, ','(tail(X11, X13), eq(X12, cons(nil, X13))))).\nand substitutionT1 -> T11,\nX11 -> T11,\nT2 -> T13,\nX12 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 150 [arrowhead = none ];
150 -> 19;

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

152 [label="EVAL with clause\neq(X8, X8).\nand substitutionT5 -> nil,\nX8 -> nil,\nT8 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 152 [arrowhead = none ];
152 -> 10;

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

154 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 154 [arrowhead = none ];
154 -> 13;

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

156 [label="EVAL with clause\nhead([], X16).\nand substitutionT11 -> [],\nX16 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 156 [arrowhead = none ];
156 -> 21;

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

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

159 [label="EVAL with clause\nhead(.(X28, X29), X28).\nand substitutionX28 -> nil,\nX29 -> T22,\nT11 -> .(nil, T22),\nT21 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 159 [arrowhead = none ];
159 -> 48;

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

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

162 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX13 -> []", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 162 [arrowhead = none ];
162 -> 26;

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

164 [label="EVAL with clause\neq(X19, X19).\nand substitutionT13 -> cons(nil, []),\nX19 -> cons(nil, []),\nT16 -> cons(nil, [])", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 164 [arrowhead = none ];
164 -> 30;

165 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 165 [arrowhead = none ];
165 -> 31;

166 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 166 [arrowhead = none ];
166 -> 33;

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

168 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 168 [arrowhead = none ];
168 -> 35;

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

170 [label="BACKTRACK\nfor clause: tail(.(X3, X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 170 [arrowhead = none ];
170 -> 41;

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

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

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

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

175 [label="ONLY EVAL with clause\ntail(.(X34, X35), X35).\nand substitutionX34 -> nil,\nT22 -> T25,\nX35 -> T25,\nX13 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 175 [arrowhead = none ];
175 -> 57;

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

177 [label="EVAL with clause\neq(X38, X38).\nand substitutionT13 -> cons(nil, T31),\nX38 -> cons(nil, T31),\nT25 -> T31,\nT30 -> cons(nil, T31)", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 177 [arrowhead = none ];
177 -> 61;

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

179 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 179 [arrowhead = none ];
179 -> 63;

180 [label="ONLY EVAL with clause\ngopher(X48, X49) :- ','(head(X48, X50), ','(head(X50, X51), ','(tail(X50, X52), ','(tail(X48, X53), gopher(cons(X51, cons(X52, X53)), X49))))).\nand substitutionT11 -> T37,\nX48 -> T37,\nT2 -> T39,\nX49 -> T39,\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 180 [arrowhead = none ];
180 -> 71;

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

182 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (head(T37, nil), head([], X16))", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 182 [arrowhead = none ];
182 -> 74;

183 [label="EVAL with clause\nhead(.(X61, X62), X61).\nand substitutionX61 -> T44,\nX62 -> T45,\nT37 -> .(T44, T45),\nX50 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 183 [arrowhead = none ];
183 -> 77;

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

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

186 [label="EVAL with clause\nhead([], X68).\nand substitutionT44 -> [],\nX51 -> X69,\nX68 -> X69", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 186 [arrowhead = none ];
186 -> 83;

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

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

189 [label="EVAL with clause\nhead(.(X127, X128), X127).\nand substitutionX127 -> T69,\nX128 -> T70,\nT44 -> .(T69, T70),\nX51 -> T69", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 189 [arrowhead = none ];
189 -> 131;

190 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 190 [arrowhead = none ];
190 -> 132;

191 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX52 -> []", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 191 [arrowhead = none ];
191 -> 87;

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

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

194 [label="ONLY EVAL with clause\ntail(.(X78, X79), X79).\nand substitutionX78 -> [],\nT45 -> T48,\nX79 -> T48,\nX53 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 194 [arrowhead = none ];
194 -> 94;

195 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
94 -> 195 [arrowhead = none ];
195 -> 97;

196 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
94 -> 196 [arrowhead = none ];
196 -> 99;

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

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

199 [label="BACKTRACK\nfor clause: gopher(nil, L) :- ','(!, eq(L, nil))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 199 [arrowhead = none ];
199 -> 103;

200 [label="ONLY EVAL with clause\ngopher(X90, X91) :- ','(head(X90, nil), ','(!_12, ','(tail(X90, X92), eq(X91, cons(nil, X92))))).\nand substitutionX69 -> X93,\nT48 -> T54,\nX90 -> cons(X93, cons([], T54)),\nT39 -> T56,\nX91 -> T56,\nT55 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 200 [arrowhead = none ];
200 -> 105;

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

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

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

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

205 [label="ONLY EVAL with clause\ngopher(X108, X109) :- ','(head(X108, X110), ','(head(X110, X111), ','(tail(X110, X112), ','(tail(X108, X113), gopher(cons(X111, cons(X112, X113)), X109))))).\nand substitutionX69 -> X114,\nT54 -> T62,\nX108 -> cons(X114, cons([], T62)),\nT39 -> T64,\nX109 -> T64,\nT63 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 205 [arrowhead = none ];
205 -> 115;

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

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

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

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

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

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

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

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

214 [label="ONLY EVAL with clause\ntail(.(X135, X136), X136).\nand substitutionT69 -> T75,\nX135 -> T75,\nT70 -> T76,\nX136 -> T76,\nX52 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 214 [arrowhead = none ];
214 -> 139;

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

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

217 [label="ONLY EVAL with clause\ntail(.(X143, X144), X144).\nand substitutionT75 -> T83,\nT76 -> T84,\nX143 -> .(T83, T84),\nT45 -> T85,\nX144 -> T85,\nX53 -> T85", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 217 [arrowhead = none ];
217 -> 145;

218 [label="INSTANCE with matching:\nT1 -> cons(T83, cons(T84, T85))\nT2 -> T39", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 218 [arrowhead = none , style=dashed];
218 -> 1[style=dashed];

}

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in([]) → f1_out1
f1_in(.(nil, z0)) → f1_out1
f1_in(.([], z0)) → U1(f94_in(z0), .([], z0))
f1_in(.(.(z0, z1), z2)) → U2(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f94_out1, .([], z0)) → f1_out1
U1(f94_out3(z0, z1), .([], z2)) → f1_out1
U1(f94_out5(z0, z1), .([], z2)) → f1_out1
U2(f1_out1, .(.(z0, z1), z2)) → f1_out1
f94_in(z0) → U3(f97_in(z0), f99_in(z0), z0)
U3(f97_out1, z0, z1) → f94_out1
U3(z0, f99_out2(z1, z2), z3) → f94_out3(z1, z2)
U3(z0, f99_out4(z1, z2), z3) → f94_out5(z1, z2)

Tuples:

F1_IN(.([], z0)) → c3(U1'(f94_in(z0), .([], z0)), F94_IN(z0))
F1_IN(.(.(z0, z1), z2)) → c4(U2'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F1_IN(cons(z0, cons(z1, z2))))
F94_IN(z0) → c9(U3'(f97_in(z0), f99_in(z0), z0))

S tuples:

F1_IN(.([], z0)) → c3(U1'(f94_in(z0), .([], z0)), F94_IN(z0))
F1_IN(.(.(z0, z1), z2)) → c4(U2'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)), F1_IN(cons(z0, cons(z1, z2))))
F94_IN(z0) → c9(U3'(f97_in(z0), f99_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f94_in, U3

Defined Pair Symbols:

F1_IN, F94_IN

Compound Symbols:

c3, c4, c9

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

Split RHS of tuples not part of any SCC

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in([]) → f1_out1
f1_in(.(nil, z0)) → f1_out1
f1_in(.([], z0)) → U1(f94_in(z0), .([], z0))
f1_in(.(.(z0, z1), z2)) → U2(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f94_out1, .([], z0)) → f1_out1
U1(f94_out3(z0, z1), .([], z2)) → f1_out1
U1(f94_out5(z0, z1), .([], z2)) → f1_out1
U2(f1_out1, .(.(z0, z1), z2)) → f1_out1
f94_in(z0) → U3(f97_in(z0), f99_in(z0), z0)
U3(f97_out1, z0, z1) → f94_out1
U3(z0, f99_out2(z1, z2), z3) → f94_out3(z1, z2)
U3(z0, f99_out4(z1, z2), z3) → f94_out5(z1, z2)

Tuples:

F94_IN(z0) → c9(U3'(f97_in(z0), f99_in(z0), z0))
F1_IN(.([], z0)) → c(U1'(f94_in(z0), .([], z0)))
F1_IN(.([], z0)) → c(F94_IN(z0))
F1_IN(.(.(z0, z1), z2)) → c(U2'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
F1_IN(.(.(z0, z1), z2)) → c(F1_IN(cons(z0, cons(z1, z2))))

S tuples:

F94_IN(z0) → c9(U3'(f97_in(z0), f99_in(z0), z0))
F1_IN(.([], z0)) → c(U1'(f94_in(z0), .([], z0)))
F1_IN(.([], z0)) → c(F94_IN(z0))
F1_IN(.(.(z0, z1), z2)) → c(U2'(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2)))
F1_IN(.(.(z0, z1), z2)) → c(F1_IN(cons(z0, cons(z1, z2))))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f94_in, U3

Defined Pair Symbols:

F94_IN, F1_IN

Compound Symbols:

c9, c

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

Removed 4 trailing tuple parts

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(nil) → f1_out1
f1_in([]) → f1_out1
f1_in(.(nil, z0)) → f1_out1
f1_in(.([], z0)) → U1(f94_in(z0), .([], z0))
f1_in(.(.(z0, z1), z2)) → U2(f1_in(cons(z0, cons(z1, z2))), .(.(z0, z1), z2))
U1(f94_out1, .([], z0)) → f1_out1
U1(f94_out3(z0, z1), .([], z2)) → f1_out1
U1(f94_out5(z0, z1), .([], z2)) → f1_out1
U2(f1_out1, .(.(z0, z1), z2)) → f1_out1
f94_in(z0) → U3(f97_in(z0), f99_in(z0), z0)
U3(f97_out1, z0, z1) → f94_out1
U3(z0, f99_out2(z1, z2), z3) → f94_out3(z1, z2)
U3(z0, f99_out4(z1, z2), z3) → f94_out5(z1, z2)

Tuples:

F1_IN(.([], z0)) → c(F94_IN(z0))
F94_IN(z0) → c9
F1_IN(.([], z0)) → c
F1_IN(.(.(z0, z1), z2)) → c

S tuples:

F1_IN(.([], z0)) → c(F94_IN(z0))
F94_IN(z0) → c9
F1_IN(.([], z0)) → c
F1_IN(.(.(z0, z1), z2)) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f94_in, U3

Defined Pair Symbols:

F1_IN, F94_IN

Compound Symbols:

c, c9, c