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

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 PiDP

↳7 PiDPToQDPProof (⇐)

↳8 QDP

↳9 UsableRulesReductionPairsProof (⇔)

↳10 QDP

↳11 PisEmptyProof (⇔)

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

Queries:

countstack(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: countstack(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: 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];
3 [label="3: true | countstack(empty, T2), SCOPE: 1, CLAUSE: 1 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: 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];
5 [label="5: countstack(empty, T2), SCOPE: 1, CLAUSE: 1 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(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];
7 [label="7: ','(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];
8 [label="8: ','(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];
9 [label="9: ','(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];
10 [label="10: ','(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];
11 [label="11: ','(!_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];
12 [label="12: ','(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];
13 [label="13: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X12), countstack(X12, T5))))\n\nX12 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(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];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(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];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(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];
20 [label="20: ','(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];
21 [label="21: ','(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];
22 [label="22: ','(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];
23 [label="23: ','(!_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];
24 [label="24: ','(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];
25 [label="25: ','(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];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(no(empty_stack(T14)), ','(pop(T14, nil), ','(popped(T14, X51), countstack(X51, T16)))) | countstack(T14, T2), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nX51 is free; \ncountstack(T14, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(no(empty_stack(T14)), ','(pop(T14, nil), ','(popped(T14, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 13 | ','(no(empty_stack(T14)), ','(pop(T14, nil), ','(popped(T14, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T14, T2), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nX51 is free; \ncountstack(T14, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(call(empty_stack(T19)), ','(!_10, ','(failure(a), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))))) | ','(no(empty_stack(T19)), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T19, T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\nX51 is free; \ncountstack(T19, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(empty_stack(T19), ','(!_10, ','(failure(a), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))))) | ?_11 | ','(no(empty_stack(T19)), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T19, T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\nX51 is free; \ncountstack(T19, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(empty_stack(T19), ','(!_10, ','(failure(a), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))))), SCOPE: 12, CLAUSE: 11 | ?_12 | ?_11 | ','(no(empty_stack(T19)), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T19, T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\nX51 is free; \ncountstack(T19, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(!_10, ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X51), countstack(X51, T16))))) | ?_12 | ?_11 | ','(no(empty_stack(empty)), ','(pop(empty, nil), ','(popped(empty, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX51 is free\ncountstack(empty, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ?_12 | ?_11 | ','(no(empty_stack(T19)), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T19, T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\nX51 is free; \ncountstack(T19, T2) !=? countstack(empty, 0)\nempty_stack(T19) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X51), countstack(X51, T16)))) | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\nX51 is free\ncountstack(empty, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X51), countstack(X51, T16))))\n\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\ncountstack(empty, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(failure(a), ','(pop(empty, nil), ','(popped(empty, X51), countstack(X51, T16)))), SCOPE: 13, CLAUSE: 15\n\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(no(empty_stack(empty)), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23)))))))\n\nX65 is free\nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(no(empty_stack(empty)), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))), SCOPE: 14, CLAUSE: 13 | ','(no(empty_stack(empty)), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))), SCOPE: 14, CLAUSE: 14\n\nX65 is free\nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(call(empty_stack(empty)), ','(!_14, ','(failure(a), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))))) | ','(no(empty_stack(empty)), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))), SCOPE: 14, CLAUSE: 14\n\nX65 is free\nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(empty_stack(empty), ','(!_14, ','(failure(a), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))))) | ?_15 | ','(no(empty_stack(empty)), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))), SCOPE: 14, CLAUSE: 14\n\nX65 is free\nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(empty_stack(empty), ','(!_14, ','(failure(a), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))))), SCOPE: 16, CLAUSE: 11 | ?_16 | ?_15 | ','(no(empty_stack(empty)), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))), SCOPE: 14, CLAUSE: 14\n\nX65 is free\nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(!_14, ','(failure(a), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23)))))))) | ?_16 | ?_15 | ','(no(empty_stack(empty)), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))), SCOPE: 14, CLAUSE: 14\n\nX65 is free\nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(failure(a), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23)))))))\n\nX65 is free\nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(failure(a), ','(pop(empty, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(empty, X68), countstack(push(X66, push(X67, X68)), T23))))))), SCOPE: 17, CLAUSE: 15\n\nX65 is free\nX66 is free; \nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ?_11 | ','(no(empty_stack(T19)), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T19, T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\nX51 is free; \ncountstack(T19, T2) !=? countstack(empty, 0)\nempty_stack(T19) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(no(empty_stack(T19)), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14 | ?_10 | countstack(T19, T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\nX51 is free; \ncountstack(T19, T2) !=? countstack(empty, 0)\nempty_stack(T19) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(no(empty_stack(T19)), ','(pop(T19, nil), ','(popped(T19, X51), countstack(X51, T16)))), SCOPE: 10, CLAUSE: 14\n\nT19 is ground\nX51 is free; \ncountstack(T19, T2) !=? countstack(empty, 0)\nempty_stack(T19) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ?_10 | countstack(T19, T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\ncountstack(T19, T2) !=? countstack(empty, 0)\nempty_stack(T19) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(pop(T30, nil), ','(popped(T30, X51), countstack(X51, T16)))\n\nT30 is ground\nX51 is free; \ncountstack(T30, T2) !=? countstack(empty, 0)\nempty_stack(T30) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(pop(T30, nil), ','(popped(T30, X51), countstack(X51, T16))), SCOPE: 18, CLAUSE: 3 | ','(pop(T30, nil), ','(popped(T30, X51), countstack(X51, T16))), SCOPE: 18, CLAUSE: 4\n\nT30 is ground\nX51 is free; \ncountstack(T30, T2) !=? countstack(empty, 0)\nempty_stack(T30) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(pop(T30, nil), ','(popped(T30, X51), countstack(X51, T16))), SCOPE: 18, CLAUSE: 4\n\nT30 is ground\nX51 is free; \ncountstack(T30, T2) !=? countstack(empty, 0)\nempty_stack(T30) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(popped(push(nil, T36), X51), countstack(X51, T16))\n\nT36 is ground\nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(popped(push(nil, T36), X51), countstack(X51, T16)), SCOPE: 19, CLAUSE: 5 | ','(popped(push(nil, T36), X51), countstack(X51, T16)), SCOPE: 19, CLAUSE: 6\n\nT36 is ground\nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(popped(push(nil, T36), X51), countstack(X51, T16)), SCOPE: 19, CLAUSE: 6\n\nT36 is ground\nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: countstack(T39, T16)\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: countstack(T19, T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\ncountstack(T19, T2) !=? countstack(empty, 0)\nempty_stack(T19) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(no(empty_stack(T44)), ','(pop(T44, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T44, X119), countstack(push(X117, push(X118, X119)), T46)))))))\n\nT44 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T44, T2) !=? countstack(empty, 0)\nempty_stack(T44) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(no(empty_stack(T44)), ','(pop(T44, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T44, X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 20, CLAUSE: 13 | ','(no(empty_stack(T44)), ','(pop(T44, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T44, X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 20, CLAUSE: 14\n\nT44 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T44, T2) !=? countstack(empty, 0)\nempty_stack(T44) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(call(empty_stack(T50)), ','(!_20, ','(failure(a), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))))) | ','(no(empty_stack(T50)), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 20, CLAUSE: 14\n\nT50 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T50, T2) !=? countstack(empty, 0)\nempty_stack(T50) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(empty_stack(T50), ','(!_20, ','(failure(a), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))))) | ?_21 | ','(no(empty_stack(T50)), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 20, CLAUSE: 14\n\nT50 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T50, T2) !=? countstack(empty, 0)\nempty_stack(T50) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(empty_stack(T50), ','(!_20, ','(failure(a), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))))), SCOPE: 22, CLAUSE: 11 | ?_22 | ?_21 | ','(no(empty_stack(T50)), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 20, CLAUSE: 14\n\nT50 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T50, T2) !=? countstack(empty, 0)\nempty_stack(T50) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ?_22 | ?_21 | ','(no(empty_stack(T50)), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 20, CLAUSE: 14\n\nT50 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T50, T2) !=? countstack(empty, 0)\nempty_stack(T50) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ?_21 | ','(no(empty_stack(T50)), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 20, CLAUSE: 14\n\nT50 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T50, T2) !=? countstack(empty, 0)\nempty_stack(T50) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(no(empty_stack(T50)), ','(pop(T50, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T50, X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 20, CLAUSE: 14\n\nT50 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T50, T2) !=? countstack(empty, 0)\nempty_stack(T50) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(pop(T54, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T54, X119), countstack(push(X117, push(X118, X119)), T46))))))\n\nT54 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T54, T2) !=? countstack(empty, 0)\nempty_stack(T54) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(pop(T54, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T54, X119), countstack(push(X117, push(X118, X119)), T46)))))), SCOPE: 23, CLAUSE: 3 | ','(pop(T54, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T54, X119), countstack(push(X117, push(X118, X119)), T46)))))), SCOPE: 23, CLAUSE: 4\n\nT54 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T54, T2) !=? countstack(empty, 0)\nempty_stack(T54) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(pop(T54, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(T54, X119), countstack(push(X117, push(X118, X119)), T46)))))), SCOPE: 23, CLAUSE: 4\n\nT54 is ground\nX116 is free; \nX117 is free; \nX118 is free; \nX119 is free; \ncountstack(T54, T2) !=? countstack(empty, 0)\nempty_stack(T54) !=? empty_stack(empty)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(no(empty_list(T60)), ','(head(T60, X117), ','(tail(T60, X118), ','(popped(push(T60, T61), X119), countstack(push(X117, push(X118, X119)), T46)))))\n\nT60 is ground\nT61 is ground\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(no(empty_list(T60)), ','(head(T60, X117), ','(tail(T60, X118), ','(popped(push(T60, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 13 | ','(no(empty_list(T60)), ','(head(T60, X117), ','(tail(T60, X118), ','(popped(push(T60, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 14\n\nT60 is ground\nT61 is ground\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(call(empty_list(T65)), ','(!_24, ','(failure(a), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))))) | ','(no(empty_list(T65)), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 14\n\nT61 is ground\nT65 is ground\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(empty_list(T65), ','(!_24, ','(failure(a), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))))) | ?_25 | ','(no(empty_list(T65)), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 14\n\nT61 is ground\nT65 is ground\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(empty_list(T65), ','(!_24, ','(failure(a), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))))), SCOPE: 26, CLAUSE: 12 | ?_26 | ?_25 | ','(no(empty_list(T65)), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 14\n\nT61 is ground\nT65 is ground\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(!_24, ','(failure(a), ','(head(nil, X117), ','(tail(nil, X118), ','(popped(push(nil, T61), X119), countstack(push(X117, push(X118, X119)), T46)))))) | ?_26 | ?_25 | ','(no(empty_list(nil)), ','(head(nil, X117), ','(tail(nil, X118), ','(popped(push(nil, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 14\n\nT61 is ground\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ?_26 | ?_25 | ','(no(empty_list(T65)), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 14\n\nT61 is ground\nT65 is ground\nX117 is free; \nX118 is free; \nX119 is free; \nempty_list(T65) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(failure(a), ','(head(nil, X117), ','(tail(nil, X118), ','(popped(push(nil, T61), X119), countstack(push(X117, push(X118, X119)), T46)))))\n\nT61 is ground\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(failure(a), ','(head(nil, X117), ','(tail(nil, X118), ','(popped(push(nil, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 27, CLAUSE: 15\n\nT61 is ground\nX117 is free; \nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ?_25 | ','(no(empty_list(T65)), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 14\n\nT61 is ground\nT65 is ground\nX117 is free; \nX118 is free; \nX119 is free; \nempty_list(T65) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(no(empty_list(T65)), ','(head(T65, X117), ','(tail(T65, X118), ','(popped(push(T65, T61), X119), countstack(push(X117, push(X118, X119)), T46))))), SCOPE: 24, CLAUSE: 14\n\nT61 is ground\nT65 is ground\nX117 is free; \nX118 is free; \nX119 is free; \nempty_list(T65) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(head(T70, X117), ','(tail(T70, X118), ','(popped(push(T70, T61), X119), countstack(push(X117, push(X118, X119)), T46))))\n\nT61 is ground\nT70 is ground\nX117 is free; \nX118 is free; \nX119 is free; \nempty_list(T70) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(head(T70, X117), ','(tail(T70, X118), ','(popped(push(T70, T61), X119), countstack(push(X117, push(X118, X119)), T46)))), SCOPE: 28, CLAUSE: 7 | ','(head(T70, X117), ','(tail(T70, X118), ','(popped(push(T70, T61), X119), countstack(push(X117, push(X118, X119)), T46)))), SCOPE: 28, CLAUSE: 8\n\nT61 is ground\nT70 is ground\nX117 is free; \nX118 is free; \nX119 is free; \nempty_list(T70) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(head(T70, X117), ','(tail(T70, X118), ','(popped(push(T70, T61), X119), countstack(push(X117, push(X118, X119)), T46)))), SCOPE: 28, CLAUSE: 8\n\nT61 is ground\nT70 is ground\nX117 is free; \nX118 is free; \nX119 is free; \nempty_list(T70) !=? empty_list(nil)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(tail(cons(T76, T77), X118), ','(popped(push(cons(T76, T77), T61), X119), countstack(push(T76, push(X118, X119)), T46)))\n\nT61 is ground\nT76 is ground\nT77 is ground\nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(tail(cons(T76, T77), X118), ','(popped(push(cons(T76, T77), T61), X119), countstack(push(T76, push(X118, X119)), T46))), SCOPE: 29, CLAUSE: 9 | ','(tail(cons(T76, T77), X118), ','(popped(push(cons(T76, T77), T61), X119), countstack(push(T76, push(X118, X119)), T46))), SCOPE: 29, CLAUSE: 10\n\nT61 is ground\nT76 is ground\nT77 is ground\nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(tail(cons(T76, T77), X118), ','(popped(push(cons(T76, T77), T61), X119), countstack(push(T76, push(X118, X119)), T46))), SCOPE: 29, CLAUSE: 10\n\nT61 is ground\nT76 is ground\nT77 is ground\nX118 is free; \nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(popped(push(cons(T87, T88), T61), X119), countstack(push(T87, push(T88, X119)), T46))\n\nT61 is ground\nT87 is ground\nT88 is ground\nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(popped(push(cons(T87, T88), T61), X119), countstack(push(T87, push(T88, X119)), T46)), SCOPE: 30, CLAUSE: 5 | ','(popped(push(cons(T87, T88), T61), X119), countstack(push(T87, push(T88, X119)), T46)), SCOPE: 30, CLAUSE: 6\n\nT61 is ground\nT87 is ground\nT88 is ground\nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(popped(push(cons(T87, T88), T61), X119), countstack(push(T87, push(T88, X119)), T46)), SCOPE: 30, CLAUSE: 6\n\nT61 is ground\nT87 is ground\nT88 is ground\nX119 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: countstack(push(T102, push(T103, T104)), T46)\n\nT102 is ground\nT103 is ground\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 98 [arrowhead = none ];
98 -> 2;

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

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

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

102 [label="ONLY EVAL with clause\ncountstack(X49, X50) :- ','(no(empty_stack(X49)), ','(pop(X49, nil), ','(popped(X49, X51), countstack(X51, X50)))).\nand substitution\nT1 -> T14\nX49 -> T14\nT2 -> T16\nX50 -> T16\nT15 -> T16", fontsize=14, style = filled, fillcolor = white];
4 -> 102 [arrowhead = none ];
102 -> 27;

103 [label="ONLY EVAL with clause\ncountstack(X10, X11) :- ','(no(empty_stack(X10)), ','(pop(X10, nil), ','(popped(X10, X12), countstack(X12, X11)))).\nand substitution\nX10 -> empty\nT2 -> T5\nX11 -> T5\nT4 -> T5", fontsize=14, style = filled, fillcolor = white];
5 -> 103 [arrowhead = none ];
103 -> 6;

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

105 [label="ONLY EVAL with clause\nno(X15) :- ','(call(X15), ','(!_2, failure(a))).\nand substitution\nX15 -> empty_stack(empty)", fontsize=14, style = filled, fillcolor = white];
7 -> 105 [arrowhead = none ];
105 -> 8;

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

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

108 [label="ONLY EVAL with clause\nempty_stack(empty).\nand substitution", fontsize=14, style = filled, fillcolor = white];
10 -> 108 [arrowhead = none ];
108 -> 11;

109 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 109 [arrowhead = none ];
109 -> 12;

110 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
12 -> 110 [arrowhead = none ];
110 -> 13;

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

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

113 [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 substitution\nX24 -> empty\nX25 -> T9\nT2 -> s(T9)\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 113 [arrowhead = none ];
113 -> 17;

114 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 114 [arrowhead = none ];
114 -> 18;

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

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

117 [label="ONLY EVAL with clause\nno(X40) :- ','(call(X40), ','(!_6, failure(a))).\nand substitution\nX40 -> empty_stack(empty)", fontsize=14, style = filled, fillcolor = white];
19 -> 117 [arrowhead = none ];
117 -> 20;

118 [label="CALL", fontsize=14, style = filled, fillcolor = white];
20 -> 118 [arrowhead = none ];
118 -> 21;

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

120 [label="ONLY EVAL with clause\nempty_stack(empty).\nand substitution", fontsize=14, style = filled, fillcolor = white];
22 -> 120 [arrowhead = none ];
120 -> 23;

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

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

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

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

125 [label="ONLY EVAL with clause\nno(X54) :- ','(call(X54), ','(!_10, failure(a))).\nand substitution\nT14 -> T19\nX54 -> empty_stack(T19)", fontsize=14, style = filled, fillcolor = white];
28 -> 125 [arrowhead = none ];
125 -> 29;

126 [label="CALL", fontsize=14, style = filled, fillcolor = white];
29 -> 126 [arrowhead = none ];
126 -> 30;

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

128 [label="EVAL with clause\nempty_stack(empty).\nand substitution\nT19 -> empty", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 128 [arrowhead = none ];
128 -> 32;

129 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 129 [arrowhead = none ];
129 -> 33;

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

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

132 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 132 [arrowhead = none ];
132 -> 35;

133 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 133 [arrowhead = none ];
133 -> 36;

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

135 [label="EVAL with clause\ncountstack(X63, s(X64)) :- ','(no(empty_stack(X63)), ','(pop(X63, X65), ','(no(empty_list(X65)), ','(head(X65, X66), ','(tail(X65, X67), ','(popped(X63, X68), countstack(push(X66, push(X67, X68)), X64))))))).\nand substitution\nX63 -> empty\nX64 -> T23\nT2 -> s(T23)\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 135 [arrowhead = none ];
135 -> 39;

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

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

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

139 [label="ONLY EVAL with clause\nno(X79) :- ','(call(X79), ','(!_14, failure(a))).\nand substitution\nX79 -> empty_stack(empty)", fontsize=14, style = filled, fillcolor = white];
41 -> 139 [arrowhead = none ];
139 -> 42;

140 [label="CALL", fontsize=14, style = filled, fillcolor = white];
42 -> 140 [arrowhead = none ];
140 -> 43;

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

142 [label="ONLY EVAL with clause\nempty_stack(empty).\nand substitution", fontsize=14, style = filled, fillcolor = white];
44 -> 142 [arrowhead = none ];
142 -> 45;

143 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 143 [arrowhead = none ];
143 -> 46;

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

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

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

147 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 147 [arrowhead = none ];
147 -> 51;

148 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 148 [arrowhead = none ];
148 -> 52;

149 [label="ONLY EVAL with clause\nno(X90).\nand substitution\nT19 -> T30\nX90 -> empty_stack(T30)", fontsize=14, style = filled, fillcolor = white];
51 -> 149 [arrowhead = none ];
149 -> 53;

150 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 150 [arrowhead = none ];
150 -> 61;

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

152 [label="BACKTRACK\nfor clause: pop(empty, X1)\nwith clash: (empty_stack(T30), empty_stack(empty))", fontsize=14, style = filled, fillcolor = white];
54 -> 152 [arrowhead = none ];
152 -> 55;

153 [label="EVAL with clause\npop(push(X96, X97), X96).\nand substitution\nX96 -> nil\nX97 -> T36\nT30 -> push(nil, T36)\nT35 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 153 [arrowhead = none ];
153 -> 56;

154 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 154 [arrowhead = none ];
154 -> 57;

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

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

157 [label="ONLY EVAL with clause\npopped(push(X104, X105), X105).\nand substitution\nX104 -> nil\nT36 -> T39\nX105 -> T39\nX51 -> T39", fontsize=14, style = filled, fillcolor = white];
59 -> 157 [arrowhead = none ];
157 -> 60;

158 [label="INSTANCE with matching:\nT1 -> T39\nT2 -> T16", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 158 [arrowhead = none , style=dashed];
158 -> 1[style=dashed];

159 [label="EVAL with clause\ncountstack(X114, s(X115)) :- ','(no(empty_stack(X114)), ','(pop(X114, X116), ','(no(empty_list(X116)), ','(head(X116, X117), ','(tail(X116, X118), ','(popped(X114, X119), countstack(push(X117, push(X118, X119)), X115))))))).\nand substitution\nT19 -> T44\nX114 -> T44\nX115 -> T46\nT2 -> s(T46)\nT45 -> T46", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 159 [arrowhead = none ];
159 -> 62;

160 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 160 [arrowhead = none ];
160 -> 63;

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

162 [label="ONLY EVAL with clause\nno(X130) :- ','(call(X130), ','(!_20, failure(a))).\nand substitution\nT44 -> T50\nX130 -> empty_stack(T50)", fontsize=14, style = filled, fillcolor = white];
64 -> 162 [arrowhead = none ];
162 -> 65;

163 [label="CALL", fontsize=14, style = filled, fillcolor = white];
65 -> 163 [arrowhead = none ];
163 -> 66;

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

165 [label="BACKTRACK\nfor clause: empty_stack(empty)\nwith clash: (empty_stack(T50), empty_stack(empty))", fontsize=14, style = filled, fillcolor = white];
67 -> 165 [arrowhead = none ];
165 -> 68;

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

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

168 [label="ONLY EVAL with clause\nno(X139).\nand substitution\nT50 -> T54\nX139 -> empty_stack(T54)", fontsize=14, style = filled, fillcolor = white];
70 -> 168 [arrowhead = none ];
168 -> 71;

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

170 [label="BACKTRACK\nfor clause: pop(empty, X1)\nwith clash: (empty_stack(T54), empty_stack(empty))", fontsize=14, style = filled, fillcolor = white];
72 -> 170 [arrowhead = none ];
170 -> 73;

171 [label="EVAL with clause\npop(push(X152, X153), X152).\nand substitution\nX152 -> T60\nX153 -> T61\nT54 -> push(T60, T61)\nX116 -> T60", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 171 [arrowhead = none ];
171 -> 74;

172 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 172 [arrowhead = none ];
172 -> 75;

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

174 [label="ONLY EVAL with clause\nno(X164) :- ','(call(X164), ','(!_24, failure(a))).\nand substitution\nT60 -> T65\nX164 -> empty_list(T65)", fontsize=14, style = filled, fillcolor = white];
76 -> 174 [arrowhead = none ];
174 -> 77;

175 [label="CALL", fontsize=14, style = filled, fillcolor = white];
77 -> 175 [arrowhead = none ];
175 -> 78;

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

177 [label="EVAL with clause\nempty_list(nil).\nand substitution\nT65 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 177 [arrowhead = none ];
177 -> 80;

178 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 178 [arrowhead = none ];
178 -> 81;

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

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

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

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

183 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 183 [arrowhead = none ];
183 -> 86;

184 [label="ONLY EVAL with clause\nno(X179).\nand substitution\nT65 -> T70\nX179 -> empty_list(T70)", fontsize=14, style = filled, fillcolor = white];
86 -> 184 [arrowhead = none ];
184 -> 87;

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

186 [label="BACKTRACK\nfor clause: head(nil, X4)\nwith clash: (empty_list(T70), empty_list(nil))", fontsize=14, style = filled, fillcolor = white];
88 -> 186 [arrowhead = none ];
186 -> 89;

187 [label="EVAL with clause\nhead(cons(X192, X193), X192).\nand substitution\nX192 -> T76\nX193 -> T77\nT70 -> cons(T76, T77)\nX117 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 187 [arrowhead = none ];
187 -> 90;

188 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 188 [arrowhead = none ];
188 -> 91;

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

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

191 [label="ONLY EVAL with clause\ntail(cons(X209, X210), X210).\nand substitution\nT76 -> T87\nX209 -> T87\nT77 -> T88\nX210 -> T88\nX118 -> T88", fontsize=14, style = filled, fillcolor = white];
93 -> 191 [arrowhead = none ];
191 -> 94;

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

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

194 [label="ONLY EVAL with clause\npopped(push(X222, X223), X223).\nand substitution\nT87 -> T102\nT88 -> T103\nX222 -> cons(T102, T103)\nT61 -> T104\nX223 -> T104\nX119 -> T104", fontsize=14, style = filled, fillcolor = white];
96 -> 194 [arrowhead = none ];
194 -> 97;

195 [label="INSTANCE with matching:\nT1 -> push(T102, push(T103, T104))\nT2 -> T46", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 195 [arrowhead = none , style=dashed];
195 -> 1[style=dashed];

}

(2) Obligation:

Triples:

countstack1(push(nil, T39), T16) :- countstack1(T39, T16).
countstack1(push(cons(T102, T103), T104), s(T46)) :- countstack1(push(T102, push(T103, T104)), T46).

Clauses:

countstackc1(empty, 0).
countstackc1(push(nil, T39), T16) :- countstackc1(T39, T16).
countstackc1(push(cons(T102, T103), T104), s(T46)) :- countstackc1(push(T102, push(T103, T104)), T46).

Afs:

countstack1(x1, x2) = countstack1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

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

COUNTSTACK1_IN_GA(push(nil, T39), T16) → U1_GA(T39, T16, countstack1_in_ga(T39, T16))
COUNTSTACK1_IN_GA(push(nil, T39), T16) → COUNTSTACK1_IN_GA(T39, T16)
COUNTSTACK1_IN_GA(push(cons(T102, T103), T104), s(T46)) → U2_GA(T102, T103, T104, T46, countstack1_in_ga(push(T102, push(T103, T104)), T46))
COUNTSTACK1_IN_GA(push(cons(T102, T103), T104), s(T46)) → COUNTSTACK1_IN_GA(push(T102, push(T103, T104)), T46)

R is empty.
The argument filtering Pi contains the following mapping:
countstack1_in_ga(x1, x2) = countstack1_in_ga(x1)
push(x1, x2) = push(x1, x2)
nil = nil
cons(x1, x2) = cons(x1, x2)
s(x1) = s(x1)
COUNTSTACK1_IN_GA(x1, x2) = COUNTSTACK1_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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

COUNTSTACK1_IN_GA(push(nil, T39), T16) → U1_GA(T39, T16, countstack1_in_ga(T39, T16))
COUNTSTACK1_IN_GA(push(nil, T39), T16) → COUNTSTACK1_IN_GA(T39, T16)
COUNTSTACK1_IN_GA(push(cons(T102, T103), T104), s(T46)) → U2_GA(T102, T103, T104, T46, countstack1_in_ga(push(T102, push(T103, T104)), T46))
COUNTSTACK1_IN_GA(push(cons(T102, T103), T104), s(T46)) → COUNTSTACK1_IN_GA(push(T102, push(T103, T104)), T46)

(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:

COUNTSTACK1_IN_GA(push(cons(T102, T103), T104), s(T46)) → COUNTSTACK1_IN_GA(push(T102, push(T103, T104)), T46)
COUNTSTACK1_IN_GA(push(nil, T39), T16) → COUNTSTACK1_IN_GA(T39, T16)

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)
COUNTSTACK1_IN_GA(x1, x2) = COUNTSTACK1_IN_GA(x1)

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

(7) PiDPToQDPProof (SOUND transformation)

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

(8) Obligation:

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

COUNTSTACK1_IN_GA(push(cons(T102, T103), T104)) → COUNTSTACK1_IN_GA(push(T102, push(T103, T104)))
COUNTSTACK1_IN_GA(push(nil, T39)) → COUNTSTACK1_IN_GA(T39)

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

(9) 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:

COUNTSTACK1_IN_GA(push(cons(T102, T103), T104)) → COUNTSTACK1_IN_GA(push(T102, push(T103, T104)))
COUNTSTACK1_IN_GA(push(nil, T39)) → COUNTSTACK1_IN_GA(T39)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(COUNTSTACK1_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₂

(10) Obligation:

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

(11) PisEmptyProof (EQUIVALENT transformation)

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