Left Termination proof of /tmp/tmpJbrWkx/countstack2.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 157 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 17 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 PiDP

↳7 UsableRulesProof (⇔, 0 ms)

↳8 PiDP

↳9 PiDPToQDPProof (⇒, 0 ms)

↳10 QDP

↳11 UsableRulesReductionPairsProof (⇔, 4 ms)

↳12 QDP

↳13 PisEmptyProof (⇔, 0 ms)

↳14 YES

(0) Obligation:

Clauses:

countstack(empty, 0).
countstack(S, X) :- ','(no(empty_stack(S)), ','(pop(S, nil), ','(popped(S, Pd), countstack(Pd, X)))).
countstack(S, s(X)) :- ','(no(empty_stack(S)), ','(pop(S, P), ','(no(empty_list(P)), ','(head(P, H), ','(tail(P, T), ','(popped(S, Pd), countstack(push(H, push(T, Pd)), X))))))).
pop(empty, X1).
pop(push(P, X2), P).
popped(empty, empty).
popped(push(X3, Pd), Pd).
head(nil, X4).
head(cons(H, X5), H).
tail(nil, nil).
tail(cons(X6, T), T).
empty_stack(empty).
empty_list(nil).
no(X) :- ','(X, ','(!, failure(a))).
no(X7).
failure(b).

Query: countstack(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: countstack(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: countstack(T1, T2), SCOPE: 1, CLAUSE: 0 | countstack(T1, T2), SCOPE: 1, CLAUSE: 1 | countstack(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | countstack(empty, T2), SCOPE: 1, CLAUSE: 1 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: countstack(T1, T2), SCOPE: 1, CLAUSE: 1 | countstack(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ncountstack(T1, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: countstack(empty, T2), SCOPE: 1, CLAUSE: 1 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))) | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))), SCOPE: 2, CLAUSE: 13 | ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))), SCOPE: 2, CLAUSE: 14 | ?_2 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(','(call(empty_stack(empty)), ','(!_2, failure(a))), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))) | ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))), SCOPE: 2, CLAUSE: 14 | ?_2 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(empty_stack(empty), ','(','(!_2, failure(a)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5))))) | ?_3 | ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))), SCOPE: 2, CLAUSE: 14 | ?_2 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(empty_stack(empty), ','(','(!_2, failure(a)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5))))), SCOPE: 4, CLAUSE: 11 | ?_4 | ?_3 | ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))), SCOPE: 2, CLAUSE: 14 | ?_2 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(','(!_2, failure(a)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))) | ?_4 | ?_3 | ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))), SCOPE: 2, CLAUSE: 14 | ?_2 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))) | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5))))\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5)))), SCOPE: 5, CLAUSE: 15\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(no(empty_stack(empty)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9)))))))\n\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(no(empty_stack(empty)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))), SCOPE: 6, CLAUSE: 13 | ','(no(empty_stack(empty)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))), SCOPE: 6, CLAUSE: 14\n\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(','(call(empty_stack(empty)), ','(!_6, failure(a))), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))) | ','(no(empty_stack(empty)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))), SCOPE: 6, CLAUSE: 14\n\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(empty_stack(empty), ','(','(!_6, failure(a)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9)))))))) | ?_7 | ','(no(empty_stack(empty)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))), SCOPE: 6, CLAUSE: 14\n\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(empty_stack(empty), ','(','(!_6, failure(a)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9)))))))), SCOPE: 8, CLAUSE: 11 | ?_8 | ?_7 | ','(no(empty_stack(empty)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))), SCOPE: 6, CLAUSE: 14\n\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(','(!_6, failure(a)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))) | ?_8 | ?_7 | ','(no(empty_stack(empty)), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))), SCOPE: 6, CLAUSE: 14\n\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(failure(a), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9)))))))\n\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(failure(a), ','(pop(empty, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(empty, X29), countstack(push(X27, push(X28, X29)), T9))))))), SCOPE: 9, CLAUSE: 15\n\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(no(empty_stack(T12)), ','(pop(T12, nil), ','(popped(T12, X37), countstack(X37, T14)))) | countstack(T12, T2), SCOPE: 1, CLAUSE: 2\n\nT12 is ground\nX37 is free\ncountstack(T12, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(no(empty_stack(T12)), ','(pop(T12, nil), ','(popped(T12, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 13 | ','(no(empty_stack(T12)), ','(pop(T12, nil), ','(popped(T12, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T12, T2), SCOPE: 1, CLAUSE: 2\n\nT12 is ground\nX37 is free\ncountstack(T12, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(','(call(empty_stack(T17)), ','(!_10, failure(a))), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14)))) | ','(no(empty_stack(T17)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T17, T2), SCOPE: 1, CLAUSE: 2\n\nT17 is ground\nX37 is free\ncountstack(T17, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(empty_stack(T17), ','(','(!_10, failure(a)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14))))) | ?_11 | ','(no(empty_stack(T17)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T17, T2), SCOPE: 1, CLAUSE: 2\n\nT17 is ground\nX37 is free\ncountstack(T17, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(empty_stack(T17), ','(','(!_10, failure(a)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14))))), SCOPE: 12, CLAUSE: 11 | ?_12 | ?_11 | ','(no(empty_stack(T17)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T17, T2), SCOPE: 1, CLAUSE: 2\n\nT17 is ground\nX37 is free\ncountstack(T17, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(','(!_10, failure(a)), ','(pop(empty, nil), ','(popped(empty, X37), countstack(X37, T14)))) | ?_12 | ?_11 | ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX37 is free\ncountstack(empty, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ?_12 | ?_11 | ','(no(empty_stack(T17)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T17, T2), SCOPE: 1, CLAUSE: 2\n\nT17 is ground\nX37 is free\ncountstack(T17, T2) !=? countstack(empty, 0)\nempty_stack(T17) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X37), countstack(X37, T14)))) | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX37 is free\ncountstack(empty, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X37), countstack(X37, T14))))\n\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\ncountstack(empty, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X37), countstack(X37, T14)))), SCOPE: 13, CLAUSE: 15\n\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(no(empty_stack(empty)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21)))))))\n\nX51 is free\nX52 is free\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(no(empty_stack(empty)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))), SCOPE: 14, CLAUSE: 13 | ','(no(empty_stack(empty)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))), SCOPE: 14, CLAUSE: 14\n\nX51 is free\nX52 is free\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(','(call(empty_stack(empty)), ','(!_14, failure(a))), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))) | ','(no(empty_stack(empty)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))), SCOPE: 14, CLAUSE: 14\n\nX51 is free\nX52 is free\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ','(empty_stack(empty), ','(','(!_14, failure(a)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21)))))))) | ?_15 | ','(no(empty_stack(empty)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))), SCOPE: 14, CLAUSE: 14\n\nX51 is free\nX52 is free\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: ','(empty_stack(empty), ','(','(!_14, failure(a)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21)))))))), SCOPE: 16, CLAUSE: 11 | ?_16 | ?_15 | ','(no(empty_stack(empty)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))), SCOPE: 14, CLAUSE: 14\n\nX51 is free\nX52 is free\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(','(!_14, failure(a)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))) | ?_16 | ?_15 | ','(no(empty_stack(empty)), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))), SCOPE: 14, CLAUSE: 14\n\nX51 is free\nX52 is free\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ','(failure(a), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21)))))))\n\nX51 is free\nX52 is free\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ','(failure(a), ','(pop(empty, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(empty, X54), countstack(push(X52, push(X53, X54)), T21))))))), SCOPE: 17, CLAUSE: 15\n\nX51 is free\nX52 is free\nX53 is free\nX54 is free", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ?_11 | ','(no(empty_stack(T17)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T17, T2), SCOPE: 1, CLAUSE: 2\n\nT17 is ground\nX37 is free\ncountstack(T17, T2) !=? countstack(empty, 0)\nempty_stack(T17) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(no(empty_stack(T17)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T17, T2), SCOPE: 1, CLAUSE: 2\n\nT17 is ground\nX37 is free\ncountstack(T17, T2) !=? countstack(empty, 0)\nempty_stack(T17) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(no(empty_stack(T17)), ','(pop(T17, nil), ','(popped(T17, X37), countstack(X37, T14)))), SCOPE: 10, CLAUSE: 14\n\nT17 is ground\nX37 is free\ncountstack(T17, T2) !=? countstack(empty, 0)\nempty_stack(T17) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ?_10 | countstack(T17, T2), SCOPE: 1, CLAUSE: 2\n\nT17 is ground\ncountstack(T17, T2) !=? countstack(empty, 0)\nempty_stack(T17) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(pop(T26, nil), ','(popped(T26, X37), countstack(X37, T14)))\n\nT26 is ground\nX37 is free\ncountstack(T26, T2) !=? countstack(empty, 0)\nempty_stack(T26) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: ','(pop(T26, nil), ','(popped(T26, X37), countstack(X37, T14))), SCOPE: 18, CLAUSE: 3 | ','(pop(T26, nil), ','(popped(T26, X37), countstack(X37, T14))), SCOPE: 18, CLAUSE: 4\n\nT26 is ground\nX37 is free\ncountstack(T26, T2) !=? countstack(empty, 0)\nempty_stack(T26) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: ','(pop(T26, nil), ','(popped(T26, X37), countstack(X37, T14))), SCOPE: 18, CLAUSE: 4\n\nT26 is ground\nX37 is free\ncountstack(T26, T2) !=? countstack(empty, 0)\nempty_stack(T26) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ','(popped(push(nil, T32), X37), countstack(X37, T14))\n\nT32 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(popped(push(nil, T32), X37), countstack(X37, T14)), SCOPE: 19, CLAUSE: 5 | ','(popped(push(nil, T32), X37), countstack(X37, T14)), SCOPE: 19, CLAUSE: 6\n\nT32 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(popped(push(nil, T32), X37), countstack(X37, T14)), SCOPE: 19, CLAUSE: 6\n\nT32 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: countstack(T35, T14)\n\nT35 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: countstack(T17, T2), SCOPE: 1, CLAUSE: 2\n\nT17 is ground\ncountstack(T17, T2) !=? countstack(empty, 0)\nempty_stack(T17) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: ','(no(empty_stack(T40)), ','(pop(T40, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T40, X89), countstack(push(X87, push(X88, X89)), T42)))))))\n\nT40 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T40, T2) !=? countstack(empty, 0)\nempty_stack(T40) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: ','(no(empty_stack(T40)), ','(pop(T40, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T40, X89), countstack(push(X87, push(X88, X89)), T42))))))), SCOPE: 20, CLAUSE: 13 | ','(no(empty_stack(T40)), ','(pop(T40, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T40, X89), countstack(push(X87, push(X88, X89)), T42))))))), SCOPE: 20, CLAUSE: 14\n\nT40 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T40, T2) !=? countstack(empty, 0)\nempty_stack(T40) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: ','(','(call(empty_stack(T45)), ','(!_20, failure(a))), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42))))))) | ','(no(empty_stack(T45)), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42))))))), SCOPE: 20, CLAUSE: 14\n\nT45 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T45, T2) !=? countstack(empty, 0)\nempty_stack(T45) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(empty_stack(T45), ','(','(!_20, failure(a)), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42)))))))) | ?_21 | ','(no(empty_stack(T45)), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42))))))), SCOPE: 20, CLAUSE: 14\n\nT45 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T45, T2) !=? countstack(empty, 0)\nempty_stack(T45) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: ','(empty_stack(T45), ','(','(!_20, failure(a)), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42)))))))), SCOPE: 22, CLAUSE: 11 | ?_22 | ?_21 | ','(no(empty_stack(T45)), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42))))))), SCOPE: 20, CLAUSE: 14\n\nT45 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T45, T2) !=? countstack(empty, 0)\nempty_stack(T45) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ?_22 | ?_21 | ','(no(empty_stack(T45)), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42))))))), SCOPE: 20, CLAUSE: 14\n\nT45 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T45, T2) !=? countstack(empty, 0)\nempty_stack(T45) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: ?_21 | ','(no(empty_stack(T45)), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42))))))), SCOPE: 20, CLAUSE: 14\n\nT45 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T45, T2) !=? countstack(empty, 0)\nempty_stack(T45) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: ','(no(empty_stack(T45)), ','(pop(T45, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T45, X89), countstack(push(X87, push(X88, X89)), T42))))))), SCOPE: 20, CLAUSE: 14\n\nT45 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T45, T2) !=? countstack(empty, 0)\nempty_stack(T45) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: ','(pop(T48, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T48, X89), countstack(push(X87, push(X88, X89)), T42))))))\n\nT48 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T48, T2) !=? countstack(empty, 0)\nempty_stack(T48) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ','(pop(T48, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T48, X89), countstack(push(X87, push(X88, X89)), T42)))))), SCOPE: 23, CLAUSE: 3 | ','(pop(T48, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T48, X89), countstack(push(X87, push(X88, X89)), T42)))))), SCOPE: 23, CLAUSE: 4\n\nT48 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T48, T2) !=? countstack(empty, 0)\nempty_stack(T48) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: ','(pop(T48, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(T48, X89), countstack(push(X87, push(X88, X89)), T42)))))), SCOPE: 23, CLAUSE: 4\n\nT48 is ground\nX86 is free\nX87 is free\nX88 is free\nX89 is free\ncountstack(T48, T2) !=? countstack(empty, 0)\nempty_stack(T48) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: ','(no(empty_list(T53)), ','(head(T53, X87), ','(tail(T53, X88), ','(popped(push(T53, T54), X89), countstack(push(X87, push(X88, X89)), T42)))))\n\nT53 is ground\nT54 is ground\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: ','(no(empty_list(T53)), ','(head(T53, X87), ','(tail(T53, X88), ','(popped(push(T53, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 13 | ','(no(empty_list(T53)), ','(head(T53, X87), ','(tail(T53, X88), ','(popped(push(T53, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 14\n\nT53 is ground\nT54 is ground\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: ','(','(call(empty_list(T57)), ','(!_24, failure(a))), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42))))) | ','(no(empty_list(T57)), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 14\n\nT54 is ground\nT57 is ground\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: ','(empty_list(T57), ','(','(!_24, failure(a)), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42)))))) | ?_25 | ','(no(empty_list(T57)), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 14\n\nT54 is ground\nT57 is ground\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: ','(empty_list(T57), ','(','(!_24, failure(a)), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42)))))), SCOPE: 26, CLAUSE: 12 | ?_26 | ?_25 | ','(no(empty_list(T57)), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 14\n\nT54 is ground\nT57 is ground\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: ','(','(!_24, failure(a)), ','(head(nil, X87), ','(tail(nil, X88), ','(popped(push(nil, T54), X89), countstack(push(X87, push(X88, X89)), T42))))) | ?_26 | ?_25 | ','(no(empty_list(nil)), ','(head(nil, X87), ','(tail(nil, X88), ','(popped(push(nil, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 14\n\nT54 is ground\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: ?_26 | ?_25 | ','(no(empty_list(T57)), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 14\n\nT54 is ground\nT57 is ground\nX87 is free\nX88 is free\nX89 is free\nempty_list(T57) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: ','(failure(a), ','(head(nil, X87), ','(tail(nil, X88), ','(popped(push(nil, T54), X89), countstack(push(X87, push(X88, X89)), T42)))))\n\nT54 is ground\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(failure(a), ','(head(nil, X87), ','(tail(nil, X88), ','(popped(push(nil, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 27, CLAUSE: 15\n\nT54 is ground\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: ?_25 | ','(no(empty_list(T57)), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 14\n\nT54 is ground\nT57 is ground\nX87 is free\nX88 is free\nX89 is free\nempty_list(T57) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: ','(no(empty_list(T57)), ','(head(T57, X87), ','(tail(T57, X88), ','(popped(push(T57, T54), X89), countstack(push(X87, push(X88, X89)), T42))))), SCOPE: 24, CLAUSE: 14\n\nT54 is ground\nT57 is ground\nX87 is free\nX88 is free\nX89 is free\nempty_list(T57) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: ','(head(T60, X87), ','(tail(T60, X88), ','(popped(push(T60, T54), X89), countstack(push(X87, push(X88, X89)), T42))))\n\nT54 is ground\nT60 is ground\nX87 is free\nX88 is free\nX89 is free\nempty_list(T60) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: ','(head(T60, X87), ','(tail(T60, X88), ','(popped(push(T60, T54), X89), countstack(push(X87, push(X88, X89)), T42)))), SCOPE: 28, CLAUSE: 7 | ','(head(T60, X87), ','(tail(T60, X88), ','(popped(push(T60, T54), X89), countstack(push(X87, push(X88, X89)), T42)))), SCOPE: 28, CLAUSE: 8\n\nT54 is ground\nT60 is ground\nX87 is free\nX88 is free\nX89 is free\nempty_list(T60) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: ','(head(T60, X87), ','(tail(T60, X88), ','(popped(push(T60, T54), X89), countstack(push(X87, push(X88, X89)), T42)))), SCOPE: 28, CLAUSE: 8\n\nT54 is ground\nT60 is ground\nX87 is free\nX88 is free\nX89 is free\nempty_list(T60) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: ','(tail(cons(T65, T66), X88), ','(popped(push(cons(T65, T66), T54), X89), countstack(push(T65, push(X88, X89)), T42)))\n\nT54 is ground\nT65 is ground\nT66 is ground\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: ','(tail(cons(T65, T66), X88), ','(popped(push(cons(T65, T66), T54), X89), countstack(push(T65, push(X88, X89)), T42))), SCOPE: 29, CLAUSE: 9 | ','(tail(cons(T65, T66), X88), ','(popped(push(cons(T65, T66), T54), X89), countstack(push(T65, push(X88, X89)), T42))), SCOPE: 29, CLAUSE: 10\n\nT54 is ground\nT65 is ground\nT66 is ground\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: ','(tail(cons(T65, T66), X88), ','(popped(push(cons(T65, T66), T54), X89), countstack(push(T65, push(X88, X89)), T42))), SCOPE: 29, CLAUSE: 10\n\nT54 is ground\nT65 is ground\nT66 is ground\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: ','(popped(push(cons(T71, T72), T54), X89), countstack(push(T71, push(T72, X89)), T42))\n\nT54 is ground\nT71 is ground\nT72 is ground\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(popped(push(cons(T71, T72), T54), X89), countstack(push(T71, push(T72, X89)), T42)), SCOPE: 30, CLAUSE: 5 | ','(popped(push(cons(T71, T72), T54), X89), countstack(push(T71, push(T72, X89)), T42)), SCOPE: 30, CLAUSE: 6\n\nT54 is ground\nT71 is ground\nT72 is ground\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: ','(popped(push(cons(T71, T72), T54), X89), countstack(push(T71, push(T72, X89)), T42)), SCOPE: 30, CLAUSE: 6\n\nT54 is ground\nT71 is ground\nT72 is ground\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: countstack(push(T79, push(T80, T81)), T42)\n\nT79 is ground\nT80 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 264 [arrowhead = none ];
264 -> 6;

265 [label="EVAL with clause\ncountstack(empty, 0).\nand substitutionT1 -> empty,\nT2 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 265 [arrowhead = none ];
265 -> 11;

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

267 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 267 [arrowhead = none ];
267 -> 17;

268 [label="ONLY EVAL with clause\ncountstack(X35, X36) :- ','(no(empty_stack(X35)), ','(pop(X35, nil), ','(popped(X35, X37), countstack(X37, X36)))).\nand substitutionT1 -> T12,\nX35 -> T12,\nT2 -> T14,\nX36 -> T14,\nT13 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 268 [arrowhead = none ];
268 -> 98;

269 [label="ONLY EVAL with clause\ncountstack(X10, X11) :- ','(no(empty_stack(X10)), ','(pop(X10, nil), ','(popped(X10, X12), countstack(X12, X11)))).\nand substitutionX10 -> empty,\nT2 -> T5,\nX11 -> T5,\nT4 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 269 [arrowhead = none ];
269 -> 19;

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

271 [label="ONLY EVAL with clause\nno(X15) :- ','(call(X15), ','(!_2, failure(a))).\nand substitutionX15 -> empty_stack(empty)", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 271 [arrowhead = none ];
271 -> 26;

272 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
26 -> 272 [arrowhead = none ];
272 -> 27;

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

274 [label="ONLY EVAL with clause\nempty_stack(empty).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 274 [arrowhead = none ];
274 -> 37;

275 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 275 [arrowhead = none ];
275 -> 40;

276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 276 [arrowhead = none ];
276 -> 41;

277 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 277 [arrowhead = none ];
277 -> 42;

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

279 [label="EVAL with clause\ncountstack(X24, s(X25)) :- ','(no(empty_stack(X24)), ','(pop(X24, X26), ','(no(empty_list(X26)), ','(head(X26, X27), ','(tail(X26, X28), ','(popped(X24, X29), countstack(push(X27, push(X28, X29)), X25))))))).\nand substitutionX24 -> empty,\nX25 -> T9,\nT2 -> s(T9),\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 279 [arrowhead = none ];
279 -> 50;

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

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

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

283 [label="ONLY EVAL with clause\nno(X32) :- ','(call(X32), ','(!_6, failure(a))).\nand substitutionX32 -> empty_stack(empty)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 283 [arrowhead = none ];
283 -> 59;

284 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
59 -> 284 [arrowhead = none ];
284 -> 64;

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

286 [label="ONLY EVAL with clause\nempty_stack(empty).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 286 [arrowhead = none ];
286 -> 70;

287 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 287 [arrowhead = none ];
287 -> 71;

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

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

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

291 [label="ONLY EVAL with clause\nno(X40) :- ','(call(X40), ','(!_10, failure(a))).\nand substitutionT12 -> T17,\nX40 -> empty_stack(T17)", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 291 [arrowhead = none ];
291 -> 104;

292 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
104 -> 292 [arrowhead = none ];
292 -> 107;

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

294 [label="EVAL with clause\nempty_stack(empty).\nand substitutionT17 -> empty", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 294 [arrowhead = none ];
294 -> 114;

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

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

297 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 297 [arrowhead = none ];
297 -> 184;

298 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 298 [arrowhead = none ];
298 -> 139;

299 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 299 [arrowhead = none ];
299 -> 141;

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

301 [label="EVAL with clause\ncountstack(X49, s(X50)) :- ','(no(empty_stack(X49)), ','(pop(X49, X51), ','(no(empty_list(X51)), ','(head(X51, X52), ','(tail(X51, X53), ','(popped(X49, X54), countstack(push(X52, push(X53, X54)), X50))))))).\nand substitutionX49 -> empty,\nX50 -> T21,\nT2 -> s(T21),\nT20 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 301 [arrowhead = none ];
301 -> 161;

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

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

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

305 [label="ONLY EVAL with clause\nno(X57) :- ','(call(X57), ','(!_14, failure(a))).\nand substitutionX57 -> empty_stack(empty)", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 305 [arrowhead = none ];
305 -> 169;

306 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
169 -> 306 [arrowhead = none ];
306 -> 171;

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

308 [label="ONLY EVAL with clause\nempty_stack(empty).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 308 [arrowhead = none ];
308 -> 179;

309 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
179 -> 309 [arrowhead = none ];
309 -> 181;

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

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

312 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
184 -> 312 [arrowhead = none ];
312 -> 185;

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

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

315 [label="ONLY EVAL with clause\nno(X62).\nand substitutionT17 -> T26,\nX62 -> empty_stack(T26)", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 315 [arrowhead = none ];
315 -> 199;

316 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 316 [arrowhead = none ];
316 -> 226;

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

318 [label="BACKTRACK\nfor clause: pop(empty, X1)\nwith clash: (empty_stack(T26), empty_stack(empty))", fontsize=14, style = filled, fillcolor = lightgreen];
202 -> 318 [arrowhead = none ];
318 -> 204;

319 [label="EVAL with clause\npop(push(X68, X69), X68).\nand substitutionX68 -> nil,\nX69 -> T32,\nT26 -> push(nil, T32),\nT31 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 319 [arrowhead = none ];
319 -> 211;

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

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

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

323 [label="ONLY EVAL with clause\npopped(push(X74, X75), X75).\nand substitutionX74 -> nil,\nT32 -> T35,\nX75 -> T35,\nX37 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
214 -> 323 [arrowhead = none ];
323 -> 225;

324 [label="INSTANCE with matching:\nT1 -> T35\nT2 -> T14", fontsize=14, style = filled, fillcolor = lightgrey];
225 -> 324 [arrowhead = none , style=dashed];
324 -> 3[style=dashed];

325 [label="EVAL with clause\ncountstack(X84, s(X85)) :- ','(no(empty_stack(X84)), ','(pop(X84, X86), ','(no(empty_list(X86)), ','(head(X86, X87), ','(tail(X86, X88), ','(popped(X84, X89), countstack(push(X87, push(X88, X89)), X85))))))).\nand substitutionT17 -> T40,\nX84 -> T40,\nX85 -> T42,\nT2 -> s(T42),\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
226 -> 325 [arrowhead = none ];
325 -> 228;

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

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

328 [label="ONLY EVAL with clause\nno(X92) :- ','(call(X92), ','(!_20, failure(a))).\nand substitutionT40 -> T45,\nX92 -> empty_stack(T45)", fontsize=14, style = filled, fillcolor = lightblue];
230 -> 328 [arrowhead = none ];
328 -> 231;

329 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
231 -> 329 [arrowhead = none ];
329 -> 232;

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

331 [label="BACKTRACK\nfor clause: empty_stack(empty)\nwith clash: (empty_stack(T45), empty_stack(empty))", fontsize=14, style = filled, fillcolor = lightgreen];
233 -> 331 [arrowhead = none ];
331 -> 234;

332 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
234 -> 332 [arrowhead = none ];
332 -> 235;

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

334 [label="ONLY EVAL with clause\nno(X95).\nand substitutionT45 -> T48,\nX95 -> empty_stack(T48)", fontsize=14, style = filled, fillcolor = lightblue];
236 -> 334 [arrowhead = none ];
334 -> 237;

335 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
237 -> 335 [arrowhead = none ];
335 -> 238;

336 [label="BACKTRACK\nfor clause: pop(empty, X1)\nwith clash: (empty_stack(T48), empty_stack(empty))", fontsize=14, style = filled, fillcolor = lightgreen];
238 -> 336 [arrowhead = none ];
336 -> 239;

337 [label="EVAL with clause\npop(push(X102, X103), X102).\nand substitutionX102 -> T53,\nX103 -> T54,\nT48 -> push(T53, T54),\nX86 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
239 -> 337 [arrowhead = none ];
337 -> 240;

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

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

340 [label="ONLY EVAL with clause\nno(X106) :- ','(call(X106), ','(!_24, failure(a))).\nand substitutionT53 -> T57,\nX106 -> empty_list(T57)", fontsize=14, style = filled, fillcolor = lightblue];
242 -> 340 [arrowhead = none ];
340 -> 243;

341 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
243 -> 341 [arrowhead = none ];
341 -> 244;

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

343 [label="EVAL with clause\nempty_list(nil).\nand substitutionT57 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
245 -> 343 [arrowhead = none ];
343 -> 246;

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

345 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
246 -> 345 [arrowhead = none ];
345 -> 248;

346 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
247 -> 346 [arrowhead = none ];
346 -> 251;

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

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

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

350 [label="ONLY EVAL with clause\nno(X109).\nand substitutionT57 -> T60,\nX109 -> empty_list(T60)", fontsize=14, style = filled, fillcolor = lightblue];
252 -> 350 [arrowhead = none ];
350 -> 253;

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

352 [label="BACKTRACK\nfor clause: head(nil, X4)\nwith clash: (empty_list(T60), empty_list(nil))", fontsize=14, style = filled, fillcolor = lightgreen];
254 -> 352 [arrowhead = none ];
352 -> 255;

353 [label="EVAL with clause\nhead(cons(X116, X117), X116).\nand substitutionX116 -> T65,\nX117 -> T66,\nT60 -> cons(T65, T66),\nX87 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
255 -> 353 [arrowhead = none ];
353 -> 256;

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

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

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

357 [label="ONLY EVAL with clause\ntail(cons(X122, X123), X123).\nand substitutionT65 -> T71,\nX122 -> T71,\nT66 -> T72,\nX123 -> T72,\nX88 -> T72", fontsize=14, style = filled, fillcolor = lightblue];
259 -> 357 [arrowhead = none ];
357 -> 260;

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

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

360 [label="ONLY EVAL with clause\npopped(push(X128, X129), X129).\nand substitutionT71 -> T79,\nT72 -> T80,\nX128 -> cons(T79, T80),\nT54 -> T81,\nX129 -> T81,\nX89 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 360 [arrowhead = none ];
360 -> 263;

361 [label="INSTANCE with matching:\nT1 -> push(T79, push(T80, T81))\nT2 -> T42", fontsize=14, style = filled, fillcolor = lightgrey];
263 -> 361 [arrowhead = none , style=dashed];
361 -> 3[style=dashed];

}

(2) Obligation:

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

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, T35), T14) → U1_ga(T35, T14, countstackA_in_ga(T35, T14))
countstackA_in_ga(push(cons(T79, T80), T81), s(T42)) → U2_ga(T79, T80, T81, T42, countstackA_in_ga(push(T79, push(T80, T81)), T42))
U2_ga(T79, T80, T81, T42, countstackA_out_ga(push(T79, push(T80, T81)), T42)) → countstackA_out_ga(push(cons(T79, T80), T81), s(T42))
U1_ga(T35, T14, countstackA_out_ga(T35, T14)) → countstackA_out_ga(push(nil, T35), T14)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

COUNTSTACKA_IN_GA(push(nil, T35), T14) → U1_GA(T35, T14, countstackA_in_ga(T35, T14))
COUNTSTACKA_IN_GA(push(nil, T35), T14) → COUNTSTACKA_IN_GA(T35, T14)
COUNTSTACKA_IN_GA(push(cons(T79, T80), T81), s(T42)) → U2_GA(T79, T80, T81, T42, countstackA_in_ga(push(T79, push(T80, T81)), T42))
COUNTSTACKA_IN_GA(push(cons(T79, T80), T81), s(T42)) → COUNTSTACKA_IN_GA(push(T79, push(T80, T81)), T42)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, T35), T14) → U1_ga(T35, T14, countstackA_in_ga(T35, T14))
countstackA_in_ga(push(cons(T79, T80), T81), s(T42)) → U2_ga(T79, T80, T81, T42, countstackA_in_ga(push(T79, push(T80, T81)), T42))
U2_ga(T79, T80, T81, T42, countstackA_out_ga(push(T79, push(T80, T81)), T42)) → countstackA_out_ga(push(cons(T79, T80), T81), s(T42))
U1_ga(T35, T14, countstackA_out_ga(T35, T14)) → countstackA_out_ga(push(nil, T35), T14)

The argument filtering Pi contains the following mapping:
countstackA_in_ga(x1, x2) = countstackA_in_ga(x1)
empty = empty
countstackA_out_ga(x1, x2) = countstackA_out_ga(x1, x2)
push(x1, x2) = push(x1, x2)
nil = nil
U1_ga(x1, x2, x3) = U1_ga(x1, x3)
cons(x1, x2) = cons(x1, x2)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x1, x2, x3, x5)
s(x1) = s(x1)
COUNTSTACKA_IN_GA(x1, x2) = COUNTSTACKA_IN_GA(x1)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x3, x5)

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

(4) Obligation:

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

COUNTSTACKA_IN_GA(push(nil, T35), T14) → U1_GA(T35, T14, countstackA_in_ga(T35, T14))
COUNTSTACKA_IN_GA(push(nil, T35), T14) → COUNTSTACKA_IN_GA(T35, T14)
COUNTSTACKA_IN_GA(push(cons(T79, T80), T81), s(T42)) → U2_GA(T79, T80, T81, T42, countstackA_in_ga(push(T79, push(T80, T81)), T42))
COUNTSTACKA_IN_GA(push(cons(T79, T80), T81), s(T42)) → COUNTSTACKA_IN_GA(push(T79, push(T80, T81)), T42)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, T35), T14) → U1_ga(T35, T14, countstackA_in_ga(T35, T14))
countstackA_in_ga(push(cons(T79, T80), T81), s(T42)) → U2_ga(T79, T80, T81, T42, countstackA_in_ga(push(T79, push(T80, T81)), T42))
U2_ga(T79, T80, T81, T42, countstackA_out_ga(push(T79, push(T80, T81)), T42)) → countstackA_out_ga(push(cons(T79, T80), T81), s(T42))
U1_ga(T35, T14, countstackA_out_ga(T35, T14)) → countstackA_out_ga(push(nil, T35), T14)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

COUNTSTACKA_IN_GA(push(cons(T79, T80), T81), s(T42)) → COUNTSTACKA_IN_GA(push(T79, push(T80, T81)), T42)
COUNTSTACKA_IN_GA(push(nil, T35), T14) → COUNTSTACKA_IN_GA(T35, T14)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, T35), T14) → U1_ga(T35, T14, countstackA_in_ga(T35, T14))
countstackA_in_ga(push(cons(T79, T80), T81), s(T42)) → U2_ga(T79, T80, T81, T42, countstackA_in_ga(push(T79, push(T80, T81)), T42))
U2_ga(T79, T80, T81, T42, countstackA_out_ga(push(T79, push(T80, T81)), T42)) → countstackA_out_ga(push(cons(T79, T80), T81), s(T42))
U1_ga(T35, T14, countstackA_out_ga(T35, T14)) → countstackA_out_ga(push(nil, T35), T14)

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

COUNTSTACKA_IN_GA(push(cons(T79, T80), T81), s(T42)) → COUNTSTACKA_IN_GA(push(T79, push(T80, T81)), T42)
COUNTSTACKA_IN_GA(push(nil, T35), T14) → COUNTSTACKA_IN_GA(T35, T14)

R is empty.
The argument filtering Pi contains the following mapping:
push(x1, x2) = push(x1, x2)
nil = nil
cons(x1, x2) = cons(x1, x2)
s(x1) = s(x1)
COUNTSTACKA_IN_GA(x1, x2) = COUNTSTACKA_IN_GA(x1)

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

(9) PiDPToQDPProof (SOUND transformation)

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

(10) Obligation:

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

COUNTSTACKA_IN_GA(push(cons(T79, T80), T81)) → COUNTSTACKA_IN_GA(push(T79, push(T80, T81)))
COUNTSTACKA_IN_GA(push(nil, T35)) → COUNTSTACKA_IN_GA(T35)

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

(11) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

COUNTSTACKA_IN_GA(push(cons(T79, T80), T81)) → COUNTSTACKA_IN_GA(push(T79, push(T80, T81)))
COUNTSTACKA_IN_GA(push(nil, T35)) → COUNTSTACKA_IN_GA(T35)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(COUNTSTACKA_IN_GA(x₁)) = 2·x₁
POL(cons(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(nil) = 0
POL(push(x₁, x₂)) = 1 + 2·x₁ + x₂

(12) Obligation:

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

(13) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Obligation:

(7) UsableRulesProof (EQUIVALENT transformation)

(8) Obligation:

(9) PiDPToQDPProof (SOUND transformation)

(10) Obligation:

(11) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(12) Obligation:

(13) PisEmptyProof (EQUIVALENT transformation)

(14) YES