Left Termination proof of /tmp/tmpNi5Mln/ordered3.pl

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

0 Prolog

↳1 PrologToPrologProblemTransformerProof (⇐)

↳2 Prolog

↳3 PrologToPiTRSProof (⇐)

↳4 PiTRS

↳5 DependencyPairsProof (⇔)

↳6 PiDP

↳7 DependencyGraphProof (⇔)

↳8 AND

    ↳9 PiDP

        ↳10 UsableRulesProof (⇔)

            ↳11 PiDP

                ↳12 PiDPToQDPProof (⇐)

                    ↳13 QDP

                        ↳14 QDPSizeChangeProof (⇔)

                            ↳15 TRUE

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔)

            ↳18 PiDP

                ↳19 PiDPToQDPProof (⇔)

                    ↳20 QDP

                        ↳21 QDPSizeChangeProof (⇔)

                            ↳22 TRUE

    ↳23 PiDP

        ↳24 UsableRulesProof (⇔)

            ↳25 PiDP

                ↳26 PiDPToQDPProof (⇐)

                    ↳27 QDP

                        ↳28 UsableRulesReductionPairsProof (⇔)

                            ↳29 QDP

                                ↳30 DependencyGraphProof (⇔)

                                    ↳31 TRUE

(0) Obligation:

Clauses:

ordered([]).
ordered(.(X1, [])).
ordered(Xs) :- ','(no(max1el_list(Xs)), ','(head(Xs, X), ','(tail(Xs, Ys), ','(head(Ys, Y), ','(tail(Ys, Zs), ','(less(X, s(Y)), ordered(.(Y, Zs)))))))).
head([], X2).
head(.(X, X3), X).
tail([], []).
tail(.(X4, Xs), Xs).
less(0, s(X5)).
less(X, Y) :- ','(no(zero(X)), ','(p(X, Px), ','(p(Y, Py), less(Px, Py)))).
p(0, 0).
p(s(X), X).
max1el_list([]).
max1el_list(.(X6, [])).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X7).
failure(b).

Queries:

ordered(g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: ordered(T1), SCOPE: 1, CLAUSE: 0 | ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ordered(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ordered(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(no(max1el_list(T3)), ','(head(T3, X13), ','(tail(T3, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16))))))))\n\nT3 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(no(max1el_list(T3)), ','(head(T3, X13), ','(tail(T3, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 2, CLAUSE: 14 | ','(no(max1el_list(T3)), ','(head(T3, X13), ','(tail(T3, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 2, CLAUSE: 15 | ?_2\n\nT3 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(max1el_list(T4), ','(!_2, ','(failure(a), ','(head(T4, X13), ','(tail(T4, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))))) | ','(no(max1el_list(T4)), ','(head(T4, X13), ','(tail(T4, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 2, CLAUSE: 15 | ?_2\n\nT4 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(max1el_list(T4), ','(!_2, ','(failure(a), ','(head(T4, X13), ','(tail(T4, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))))), SCOPE: 3, CLAUSE: 11 | ','(max1el_list(T4), ','(!_2, ','(failure(a), ','(head(T4, X13), ','(tail(T4, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))))), SCOPE: 3, CLAUSE: 12 | ','(no(max1el_list(T4)), ','(head(T4, X13), ','(tail(T4, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 2, CLAUSE: 15 | ?_2\n\nT4 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(!_2, ','(failure(a), ','(head([], X13), ','(tail([], X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16))))))))) | ','(max1el_list([]), ','(!_2, ','(failure(a), ','(head([], X13), ','(tail([], X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))))), SCOPE: 3, CLAUSE: 12 | ','(no(max1el_list([])), ','(head([], X13), ','(tail([], X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 2, CLAUSE: 15 | ?_2\n\nX13 is free\nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(max1el_list(T4), ','(!_2, ','(failure(a), ','(head(T4, X13), ','(tail(T4, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))))), SCOPE: 3, CLAUSE: 12 | ','(no(max1el_list(T4)), ','(head(T4, X13), ','(tail(T4, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 2, CLAUSE: 15 | ?_2\n\nT4 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; \nmax1el_list(T4) !=? max1el_list([])", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(failure(a), ','(head([], X13), ','(tail([], X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16))))))))\n\nX13 is free\nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(failure(a), ','(head([], X13), ','(tail([], X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 4, CLAUSE: 16\n\nX13 is free\nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(!_2, ','(failure(a), ','(head(.(T5, []), X13), ','(tail(.(T5, []), X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16))))))))) | ','(no(max1el_list(.(T5, []))), ','(head(.(T5, []), X13), ','(tail(.(T5, []), X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 2, CLAUSE: 15 | ?_2\n\nT5 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(no(max1el_list(T4)), ','(head(T4, X13), ','(tail(T4, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 2, CLAUSE: 15\n\nT4 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; \nX20 is free; \nmax1el_list(T4) !=? max1el_list([])\nmax1el_list(T4) !=? max1el_list(.(X20, []))", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(failure(a), ','(head(.(T5, []), X13), ','(tail(.(T5, []), X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16))))))))\n\nT5 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(failure(a), ','(head(.(T5, []), X13), ','(tail(.(T5, []), X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))), SCOPE: 5, CLAUSE: 16\n\nT5 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(head(T6, X13), ','(tail(T6, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))\n\nT6 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; \nX20 is free; \nmax1el_list(T6) !=? max1el_list([])\nmax1el_list(T6) !=? max1el_list(.(X20, []))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(head(T6, X13), ','(tail(T6, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16))))))), SCOPE: 6, CLAUSE: 3 | ','(head(T6, X13), ','(tail(T6, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16))))))), SCOPE: 6, CLAUSE: 4\n\nT6 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; \nX20 is free; \nmax1el_list(T6) !=? max1el_list([])\nmax1el_list(T6) !=? max1el_list(.(X20, []))", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(head(T6, X13), ','(tail(T6, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16))))))), SCOPE: 6, CLAUSE: 4\n\nT6 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; \nX20 is free; \nX24 is free; \nmax1el_list(T6) !=? max1el_list([])\nmax1el_list(T6) !=? max1el_list(.(X20, []))\nhead(T6, X13) !=? head([], X24)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(tail(.(T7, T8), X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(T7, s(X15)), ordered(.(X15, X16))))))\n\nT7 is ground\nT8 is ground\nX13 is free; \nX14 is free; \nX15 is free; \nX16 is free; \nX20 is free; \nX24 is free; \nmax1el_list(.(T7, T8)) !=? max1el_list(.(X20, []))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\nX13 is free\nX20 is free; \nX24 is free; \nX27 is free; \nX28 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(tail(.(T7, T8), X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(T7, s(X15)), ordered(.(X15, X16)))))), SCOPE: 7, CLAUSE: 5 | ','(tail(.(T7, T8), X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(T7, s(X15)), ordered(.(X15, X16)))))), SCOPE: 7, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX14 is free; \nX15 is free; \nX16 is free; \nX20 is free; \nmax1el_list(.(T7, T8)) !=? max1el_list(.(X20, []))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(tail(.(T7, T8), X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(T7, s(X15)), ordered(.(X15, X16)))))), SCOPE: 7, CLAUSE: 6\n\nT7 is ground\nT8 is ground\nX14 is free; \nX15 is free; \nX16 is free; \nX20 is free; \nmax1el_list(.(T7, T8)) !=? max1el_list(.(X20, []))", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(head(T10, X15), ','(tail(T10, X16), ','(less(T9, s(X15)), ordered(.(X15, X16)))))\n\nT9 is ground\nT10 is ground\nX15 is free; \nX16 is free; \nX20 is free; \nmax1el_list(.(T9, T10)) !=? max1el_list(.(X20, []))", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(head(T10, X15), ','(tail(T10, X16), ','(less(T9, s(X15)), ordered(.(X15, X16))))), SCOPE: 8, CLAUSE: 3 | ','(head(T10, X15), ','(tail(T10, X16), ','(less(T9, s(X15)), ordered(.(X15, X16))))), SCOPE: 8, CLAUSE: 4\n\nT9 is ground\nT10 is ground\nX15 is free; \nX16 is free; \nX20 is free; \nmax1el_list(.(T9, T10)) !=? max1el_list(.(X20, []))", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(head(T10, X15), ','(tail(T10, X16), ','(less(T9, s(X15)), ordered(.(X15, X16))))), SCOPE: 8, CLAUSE: 4\n\nT9 is ground\nT10 is ground\nX15 is free; \nX16 is free; \nX20 is free; \nX34 is free; \nmax1el_list(.(T9, T10)) !=? max1el_list(.(X20, []))\nhead(T10, X15) !=? head([], X34)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(tail(.(T11, T12), X16), ','(less(T9, s(T11)), ordered(.(T11, X16))))\n\nT9 is ground\nT11 is ground\nT12 is ground\nX15 is free; \nX16 is free; \nX20 is free; \nX34 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\nX15 is free\nX20 is free; \nX34 is free; \nX37 is free; \nX38 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(tail(.(T11, T12), X16), ','(less(T9, s(T11)), ordered(.(T11, X16)))), SCOPE: 9, CLAUSE: 5 | ','(tail(.(T11, T12), X16), ','(less(T9, s(T11)), ordered(.(T11, X16)))), SCOPE: 9, CLAUSE: 6\n\nT9 is ground\nT11 is ground\nT12 is ground\nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(tail(.(T11, T12), X16), ','(less(T9, s(T11)), ordered(.(T11, X16)))), SCOPE: 9, CLAUSE: 6\n\nT9 is ground\nT11 is ground\nT12 is ground\nX16 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(less(T9, s(T13)), ordered(.(T13, T14)))\n\nT9 is ground\nT13 is ground\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: less(T9, s(T13))\n\nT9 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ordered(.(T13, T14))\n\nT13 is ground\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: less(T9, s(T13)), SCOPE: 10, CLAUSE: 7 | less(T9, s(T13)), SCOPE: 10, CLAUSE: 8\n\nT9 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: less(T9, s(T13)), SCOPE: 10, CLAUSE: 7\n\nT9 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: less(T9, s(T13)), SCOPE: 10, CLAUSE: 8\n\nT9 is ground\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\nX45 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(no(zero(T16)), ','(p(T16, X50), ','(p(s(T17), X51), less(X50, X51))))\n\nT16 is ground\nT17 is ground\nX50 is free; \nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(no(zero(T16)), ','(p(T16, X50), ','(p(s(T17), X51), less(X50, X51)))), SCOPE: 11, CLAUSE: 14 | ','(no(zero(T16)), ','(p(T16, X50), ','(p(s(T17), X51), less(X50, X51)))), SCOPE: 11, CLAUSE: 15 | ?_11\n\nT16 is ground\nT17 is ground\nX50 is free; \nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(zero(T18), ','(!_11, ','(failure(a), ','(p(T18, X50), ','(p(s(T17), X51), less(X50, X51)))))) | ','(no(zero(T18)), ','(p(T18, X50), ','(p(s(T17), X51), less(X50, X51)))), SCOPE: 11, CLAUSE: 15 | ?_11\n\nT17 is ground\nT18 is ground\nX50 is free; \nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(zero(T18), ','(!_11, ','(failure(a), ','(p(T18, X50), ','(p(s(T17), X51), less(X50, X51)))))), SCOPE: 12, CLAUSE: 13 | ','(no(zero(T18)), ','(p(T18, X50), ','(p(s(T17), X51), less(X50, X51)))), SCOPE: 11, CLAUSE: 15 | ?_11\n\nT17 is ground\nT18 is ground\nX50 is free; \nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(!_11, ','(failure(a), ','(p(0, X50), ','(p(s(T17), X51), less(X50, X51))))) | ','(no(zero(0)), ','(p(0, X50), ','(p(s(T17), X51), less(X50, X51)))), SCOPE: 11, CLAUSE: 15 | ?_11\n\nT17 is ground\nX50 is free; \nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(no(zero(T18)), ','(p(T18, X50), ','(p(s(T17), X51), less(X50, X51)))), SCOPE: 11, CLAUSE: 15\n\nT17 is ground\nT18 is ground\nX50 is free; \nX51 is free; \nzero(T18) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(failure(a), ','(p(0, X50), ','(p(s(T17), X51), less(X50, X51))))\n\nT17 is ground\nX50 is free; \nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(failure(a), ','(p(0, X50), ','(p(s(T17), X51), less(X50, X51)))), SCOPE: 13, CLAUSE: 16\n\nT17 is ground\nX50 is free; \nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(p(T19, X50), ','(p(s(T17), X51), less(X50, X51)))\n\nT17 is ground\nT19 is ground\nX50 is free; \nX51 is free; \nzero(T19) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(p(T19, X50), ','(p(s(T17), X51), less(X50, X51))), SCOPE: 14, CLAUSE: 9 | ','(p(T19, X50), ','(p(s(T17), X51), less(X50, X51))), SCOPE: 14, CLAUSE: 10\n\nT17 is ground\nT19 is ground\nX50 is free; \nX51 is free; \nzero(T19) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(p(T19, X50), ','(p(s(T17), X51), less(X50, X51))), SCOPE: 14, CLAUSE: 10\n\nT17 is ground\nT19 is ground\nX50 is free; \nX51 is free; \nzero(T19) !=? zero(0)\np(T19, X50) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(p(s(T17), X51), less(T20, X51))\n\nT17 is ground\nT20 is ground\nX50 is free; \nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\nX50 is free\nX57 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(p(s(T17), X51), less(T20, X51)), SCOPE: 15, CLAUSE: 9 | ','(p(s(T17), X51), less(T20, X51)), SCOPE: 15, CLAUSE: 10\n\nT17 is ground\nT20 is ground\nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(p(s(T17), X51), less(T20, X51)), SCOPE: 15, CLAUSE: 10\n\nT17 is ground\nT20 is ground\nX51 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: less(T20, T21)\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: less(T20, T21), SCOPE: 16, CLAUSE: 7 | less(T20, T21), SCOPE: 16, CLAUSE: 8\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: less(T20, T21), SCOPE: 16, CLAUSE: 7\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: less(T20, T21), SCOPE: 16, CLAUSE: 8\n\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(no(zero(T23)), ','(p(T23, X67), ','(p(T24, X68), less(X67, X68))))\n\nT23 is ground\nT24 is ground\nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(no(zero(T23)), ','(p(T23, X67), ','(p(T24, X68), less(X67, X68)))), SCOPE: 17, CLAUSE: 14 | ','(no(zero(T23)), ','(p(T23, X67), ','(p(T24, X68), less(X67, X68)))), SCOPE: 17, CLAUSE: 15 | ?_17\n\nT23 is ground\nT24 is ground\nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(zero(T25), ','(!_17, ','(failure(a), ','(p(T25, X67), ','(p(T24, X68), less(X67, X68)))))) | ','(no(zero(T25)), ','(p(T25, X67), ','(p(T24, X68), less(X67, X68)))), SCOPE: 17, CLAUSE: 15 | ?_17\n\nT24 is ground\nT25 is ground\nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(zero(T25), ','(!_17, ','(failure(a), ','(p(T25, X67), ','(p(T24, X68), less(X67, X68)))))), SCOPE: 18, CLAUSE: 13 | ','(no(zero(T25)), ','(p(T25, X67), ','(p(T24, X68), less(X67, X68)))), SCOPE: 17, CLAUSE: 15 | ?_17\n\nT24 is ground\nT25 is ground\nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(!_17, ','(failure(a), ','(p(0, X67), ','(p(T24, X68), less(X67, X68))))) | ','(no(zero(0)), ','(p(0, X67), ','(p(T24, X68), less(X67, X68)))), SCOPE: 17, CLAUSE: 15 | ?_17\n\nT24 is ground\nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(no(zero(T25)), ','(p(T25, X67), ','(p(T24, X68), less(X67, X68)))), SCOPE: 17, CLAUSE: 15\n\nT24 is ground\nT25 is ground\nX67 is free; \nX68 is free; \nzero(T25) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(failure(a), ','(p(0, X67), ','(p(T24, X68), less(X67, X68))))\n\nT24 is ground\nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(failure(a), ','(p(0, X67), ','(p(T24, X68), less(X67, X68)))), SCOPE: 19, CLAUSE: 16\n\nT24 is ground\nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(p(T26, X67), ','(p(T24, X68), less(X67, X68)))\n\nT24 is ground\nT26 is ground\nX67 is free; \nX68 is free; \nzero(T26) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(p(T26, X67), ','(p(T24, X68), less(X67, X68))), SCOPE: 20, CLAUSE: 9 | ','(p(T26, X67), ','(p(T24, X68), less(X67, X68))), SCOPE: 20, CLAUSE: 10\n\nT24 is ground\nT26 is ground\nX67 is free; \nX68 is free; \nzero(T26) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(p(T26, X67), ','(p(T24, X68), less(X67, X68))), SCOPE: 20, CLAUSE: 10\n\nT24 is ground\nT26 is ground\nX67 is free; \nX68 is free; \nzero(T26) !=? zero(0)\np(T26, X67) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(p(T24, X68), less(T27, X68))\n\nT24 is ground\nT27 is ground\nX67 is free; \nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\nX67 is free\nX74 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(p(T24, X68), less(T27, X68)), SCOPE: 21, CLAUSE: 9 | ','(p(T24, X68), less(T27, X68)), SCOPE: 21, CLAUSE: 10\n\nT24 is ground\nT27 is ground\nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: less(T27, 0) | ','(p(0, X68), less(T27, X68)), SCOPE: 21, CLAUSE: 10\n\nT27 is ground\nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(p(T24, X68), less(T27, X68)), SCOPE: 21, CLAUSE: 10\n\nT24 is ground\nT27 is ground\nX68 is free; \np(T24, X68) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: less(T27, 0)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(p(0, X68), less(T27, X68)), SCOPE: 21, CLAUSE: 10\n\nT27 is ground\nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: less(T27, 0), SCOPE: 22, CLAUSE: 7 | less(T27, 0), SCOPE: 22, CLAUSE: 8\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: less(T27, 0), SCOPE: 22, CLAUSE: 8\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(no(zero(T28)), ','(p(T28, X80), ','(p(0, X81), less(X80, X81))))\n\nT28 is ground\nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(no(zero(T28)), ','(p(T28, X80), ','(p(0, X81), less(X80, X81)))), SCOPE: 23, CLAUSE: 14 | ','(no(zero(T28)), ','(p(T28, X80), ','(p(0, X81), less(X80, X81)))), SCOPE: 23, CLAUSE: 15 | ?_23\n\nT28 is ground\nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(zero(T29), ','(!_23, ','(failure(a), ','(p(T29, X80), ','(p(0, X81), less(X80, X81)))))) | ','(no(zero(T29)), ','(p(T29, X80), ','(p(0, X81), less(X80, X81)))), SCOPE: 23, CLAUSE: 15 | ?_23\n\nT29 is ground\nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(zero(T29), ','(!_23, ','(failure(a), ','(p(T29, X80), ','(p(0, X81), less(X80, X81)))))), SCOPE: 24, CLAUSE: 13 | ','(no(zero(T29)), ','(p(T29, X80), ','(p(0, X81), less(X80, X81)))), SCOPE: 23, CLAUSE: 15 | ?_23\n\nT29 is ground\nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(!_23, ','(failure(a), ','(p(0, X80), ','(p(0, X81), less(X80, X81))))) | ','(no(zero(0)), ','(p(0, X80), ','(p(0, X81), less(X80, X81)))), SCOPE: 23, CLAUSE: 15 | ?_23\n\nX80 is free\nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(no(zero(T29)), ','(p(T29, X80), ','(p(0, X81), less(X80, X81)))), SCOPE: 23, CLAUSE: 15\n\nT29 is ground\nX80 is free; \nX81 is free; \nzero(T29) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(failure(a), ','(p(0, X80), ','(p(0, X81), less(X80, X81))))\n\nX80 is free\nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(failure(a), ','(p(0, X80), ','(p(0, X81), less(X80, X81)))), SCOPE: 25, CLAUSE: 16\n\nX80 is free\nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(p(T30, X80), ','(p(0, X81), less(X80, X81)))\n\nT30 is ground\nX80 is free; \nX81 is free; \nzero(T30) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(p(T30, X80), ','(p(0, X81), less(X80, X81))), SCOPE: 26, CLAUSE: 9 | ','(p(T30, X80), ','(p(0, X81), less(X80, X81))), SCOPE: 26, CLAUSE: 10\n\nT30 is ground\nX80 is free; \nX81 is free; \nzero(T30) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(p(T30, X80), ','(p(0, X81), less(X80, X81))), SCOPE: 26, CLAUSE: 10\n\nT30 is ground\nX80 is free; \nX81 is free; \nzero(T30) !=? zero(0)\np(T30, X80) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(p(0, X81), less(T31, X81))\n\nT31 is ground\nX80 is free; \nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\nX80 is free\nX87 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(p(0, X81), less(T31, X81)), SCOPE: 27, CLAUSE: 9 | ','(p(0, X81), less(T31, X81)), SCOPE: 27, CLAUSE: 10\n\nT31 is ground\nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: less(T31, 0) | ','(p(0, X81), less(T31, X81)), SCOPE: 27, CLAUSE: 10\n\nT31 is ground\nX81 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: less(T27, T32)\n\nT27 is ground\nT32 is ground\nX68 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\nX68 is free\nX90 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 113 [arrowhead = none ];
113 -> 2;

114 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
2 -> 114 [arrowhead = none ];
114 -> 3;

115 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
2 -> 115 [arrowhead = none ];
115 -> 4;

116 [label="EVAL with clause\nordered([]).\nand substitution\nT1 -> []", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 116 [arrowhead = none ];
116 -> 5;

117 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 117 [arrowhead = none ];
117 -> 6;

118 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 118 [arrowhead = none ];
118 -> 8;

119 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 119 [arrowhead = none ];
119 -> 9;

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

121 [label="EVAL with clause\nordered(.(X10, [])).\nand substitution\nX10 -> T2\nT1 -> .(T2, [])", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 121 [arrowhead = none ];
121 -> 10;

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

123 [label="EVAL with clause\nordered(X12) :- ','(no(max1el_list(X12)), ','(head(X12, X13), ','(tail(X12, X14), ','(head(X14, X15), ','(tail(X14, X16), ','(less(X13, s(X15)), ordered(.(X15, X16)))))))).\nand substitution\nT1 -> T3\nX12 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 123 [arrowhead = none ];
123 -> 13;

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

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

126 [label="EVAL with clause\nno(X18) :- ','(X18, ','(!, failure(a))).\nand substitution\nT3 -> T4\nX18 -> max1el_list(T4)", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 126 [arrowhead = none ];
126 -> 15;

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

128 [label="EVAL with clause\nmax1el_list([]).\nand substitution\nT4 -> []", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 128 [arrowhead = none ];
128 -> 17;

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

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

131 [label="EVAL with clause\nmax1el_list(.(X20, [])).\nand substitution\nX20 -> T5\nT4 -> .(T5, [])", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 131 [arrowhead = none ];
131 -> 22;

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

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

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

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

136 [label="EVAL with clause\nno(X22).\nand substitution\nT4 -> T6\nX22 -> max1el_list(T6)", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 136 [arrowhead = none ];
136 -> 27;

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

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

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

140 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (max1el_list(T6), max1el_list([]))", fontsize=14, style = filled, fillcolor = white];
28 -> 140 [arrowhead = none ];
140 -> 29;

141 [label="EVAL with clause\nhead(.(X27, X28), X27).\nand substitution\nX27 -> T7\nX28 -> T8\nT6 -> .(T7, T8)\nX13 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 141 [arrowhead = none ];
141 -> 30;

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

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

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

145 [label="EVAL with clause\ntail(.(X31, X32), X32).\nand substitution\nT7 -> T9\nX31 -> T9\nT8 -> T10\nX32 -> T10\nX14 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 145 [arrowhead = none ];
145 -> 34;

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

147 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (max1el_list(.(T9, T10)), max1el_list(.(X20, [])))", fontsize=14, style = filled, fillcolor = white];
35 -> 147 [arrowhead = none ];
147 -> 36;

148 [label="EVAL with clause\nhead(.(X37, X38), X37).\nand substitution\nX37 -> T11\nX38 -> T12\nT10 -> .(T11, T12)\nX15 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 148 [arrowhead = none ];
148 -> 37;

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

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

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

152 [label="EVAL with clause\ntail(.(X41, X42), X42).\nand substitution\nT11 -> T13\nX41 -> T13\nT12 -> T14\nX42 -> T14\nX16 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 152 [arrowhead = none ];
152 -> 41;

153 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
41 -> 153 [arrowhead = none ];
153 -> 42;

154 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
41 -> 154 [arrowhead = none ];
154 -> 43;

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

156 [label="INSTANCE with matching:\nT1 -> .(T13, T14)", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 156 [arrowhead = none , style=dashed];
156 -> 1[style=dashed];

157 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 157 [arrowhead = none ];
157 -> 45;

158 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 158 [arrowhead = none ];
158 -> 46;

159 [label="EVAL with clause\nless(0, s(X45)).\nand substitution\nT9 -> 0\nT13 -> T15\nX45 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 159 [arrowhead = none ];
159 -> 47;

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

161 [label="EVAL with clause\nless(X48, X49) :- ','(no(zero(X48)), ','(p(X48, X50), ','(p(X49, X51), less(X50, X51)))).\nand substitution\nT9 -> T16\nX48 -> T16\nT13 -> T17\nX49 -> s(T17)", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 161 [arrowhead = none ];
161 -> 50;

162 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 162 [arrowhead = none ];
162 -> 49;

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

164 [label="EVAL with clause\nno(X53) :- ','(X53, ','(!, failure(a))).\nand substitution\nT16 -> T18\nX53 -> zero(T18)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 164 [arrowhead = none ];
164 -> 52;

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

166 [label="EVAL with clause\nzero(0).\nand substitution\nT18 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 166 [arrowhead = none ];
166 -> 54;

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

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

169 [label="EVAL with clause\nno(X55).\nand substitution\nT18 -> T19\nX55 -> zero(T19)", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 169 [arrowhead = none ];
169 -> 59;

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

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

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

173 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T19), zero(0))", fontsize=14, style = filled, fillcolor = white];
60 -> 173 [arrowhead = none ];
173 -> 61;

174 [label="EVAL with clause\np(s(X57), X57).\nand substitution\nX57 -> T20\nT19 -> s(T20)\nX50 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 174 [arrowhead = none ];
174 -> 62;

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

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

177 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
64 -> 177 [arrowhead = none ];
177 -> 65;

178 [label="EVAL with clause\np(s(X59), X59).\nand substitution\nT17 -> T21\nX59 -> T21\nX51 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 178 [arrowhead = none ];
178 -> 66;

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

180 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 180 [arrowhead = none ];
180 -> 68;

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

182 [label="EVAL with clause\nless(0, s(X62)).\nand substitution\nT20 -> 0\nX62 -> T22\nT21 -> s(T22)", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 182 [arrowhead = none ];
182 -> 70;

183 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 183 [arrowhead = none ];
183 -> 71;

184 [label="EVAL with clause\nless(X65, X66) :- ','(no(zero(X65)), ','(p(X65, X67), ','(p(X66, X68), less(X67, X68)))).\nand substitution\nT20 -> T23\nX65 -> T23\nT21 -> T24\nX66 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 184 [arrowhead = none ];
184 -> 73;

185 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 185 [arrowhead = none ];
185 -> 72;

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

187 [label="EVAL with clause\nno(X70) :- ','(X70, ','(!, failure(a))).\nand substitution\nT23 -> T25\nX70 -> zero(T25)", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 187 [arrowhead = none ];
187 -> 75;

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

189 [label="EVAL with clause\nzero(0).\nand substitution\nT25 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 189 [arrowhead = none ];
189 -> 77;

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

191 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 191 [arrowhead = none ];
191 -> 79;

192 [label="EVAL with clause\nno(X72).\nand substitution\nT25 -> T26\nX72 -> zero(T26)", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 192 [arrowhead = none ];
192 -> 82;

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

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

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

196 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T26), zero(0))", fontsize=14, style = filled, fillcolor = white];
83 -> 196 [arrowhead = none ];
196 -> 84;

197 [label="EVAL with clause\np(s(X74), X74).\nand substitution\nX74 -> T27\nT26 -> s(T27)\nX67 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 197 [arrowhead = none ];
197 -> 85;

198 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 198 [arrowhead = none ];
198 -> 86;

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

200 [label="EVAL with clause\np(0, 0).\nand substitution\nT24 -> 0\nX68 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 200 [arrowhead = none ];
200 -> 88;

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

202 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 202 [arrowhead = none ];
202 -> 90;

203 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
88 -> 203 [arrowhead = none ];
203 -> 91;

204 [label="EVAL with clause\np(s(X90), X90).\nand substitution\nX90 -> T32\nT24 -> s(T32)\nX68 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 204 [arrowhead = none ];
204 -> 111;

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

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

207 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = white];
91 -> 207 [arrowhead = none ];
207 -> 110;

208 [label="BACKTRACK\nfor clause: less(0, s(X5))because of non-unification", fontsize=14, style = filled, fillcolor = white];
92 -> 208 [arrowhead = none ];
208 -> 93;

209 [label="EVAL with clause\nless(X78, X79) :- ','(no(zero(X78)), ','(p(X78, X80), ','(p(X79, X81), less(X80, X81)))).\nand substitution\nT27 -> T28\nX78 -> T28\nX79 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 209 [arrowhead = none ];
209 -> 94;

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

211 [label="EVAL with clause\nno(X83) :- ','(X83, ','(!, failure(a))).\nand substitution\nT28 -> T29\nX83 -> zero(T29)", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 211 [arrowhead = none ];
211 -> 96;

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

213 [label="EVAL with clause\nzero(0).\nand substitution\nT29 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 213 [arrowhead = none ];
213 -> 98;

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

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

216 [label="EVAL with clause\nno(X85).\nand substitution\nT29 -> T30\nX85 -> zero(T30)", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 216 [arrowhead = none ];
216 -> 103;

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

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

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

220 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T30), zero(0))", fontsize=14, style = filled, fillcolor = white];
104 -> 220 [arrowhead = none ];
220 -> 105;

221 [label="EVAL with clause\np(s(X87), X87).\nand substitution\nX87 -> T31\nT30 -> s(T31)\nX80 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 221 [arrowhead = none ];
221 -> 106;

222 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 222 [arrowhead = none ];
222 -> 107;

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

224 [label="EVAL with clause\np(0, 0).\nand substitution\nX81 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 224 [arrowhead = none ];
224 -> 109;

225 [label="INSTANCE with matching:\nT27 -> T31\nX68 -> X81", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 225 [arrowhead = none , style=dashed];
225 -> 88[style=dashed];

226 [label="INSTANCE with matching:\nT20 -> T27\nT21 -> T32", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 226 [arrowhead = none , style=dashed];
226 -> 66[style=dashed];

}

(2) Obligation:

Clauses:

ordered1([]).
ordered1(.(T2, [])).
ordered1(.(T9, .(T13, T14))) :- less42(T9, T13).
ordered1(.(T9, .(T13, T14))) :- ','(less42(T9, T13), ordered1(.(T13, T14))).
less88(s(T31), X68) :- less88(T31, X81).
less66(0, s(T22)).
less66(s(s(T31)), 0) :- less88(T31, X81).
less66(s(T27), s(T32)) :- less66(T27, T32).
less42(0, T15).
less42(s(0), s(T22)).
less42(s(s(s(T31))), 0) :- less88(T31, X81).
less42(s(s(T27)), s(T32)) :- less66(T27, T32).

Queries:

ordered1(g).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
ordered1_in: (b)
less42_in: (b,b)
less88_in: (b,f)
less66_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ordered1_in_g([]) → ordered1_out_g([])
ordered1_in_g(.(T2, [])) → ordered1_out_g(.(T2, []))
ordered1_in_g(.(T9, .(T13, T14))) → U1_g(T9, T13, T14, less42_in_gg(T9, T13))
less42_in_gg(0, T15) → less42_out_gg(0, T15)
less42_in_gg(s(0), s(T22)) → less42_out_gg(s(0), s(T22))
less42_in_gg(s(s(s(T31))), 0) → U6_gg(T31, less88_in_ga(T31, X81))
less88_in_ga(s(T31), X68) → U3_ga(T31, X68, less88_in_ga(T31, X81))
U3_ga(T31, X68, less88_out_ga(T31, X81)) → less88_out_ga(s(T31), X68)
U6_gg(T31, less88_out_ga(T31, X81)) → less42_out_gg(s(s(s(T31))), 0)
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(T27, T32, less66_in_gg(T27, T32))
less66_in_gg(0, s(T22)) → less66_out_gg(0, s(T22))
less66_in_gg(s(s(T31)), 0) → U4_gg(T31, less88_in_ga(T31, X81))
U4_gg(T31, less88_out_ga(T31, X81)) → less66_out_gg(s(s(T31)), 0)
less66_in_gg(s(T27), s(T32)) → U5_gg(T27, T32, less66_in_gg(T27, T32))
U5_gg(T27, T32, less66_out_gg(T27, T32)) → less66_out_gg(s(T27), s(T32))
U7_gg(T27, T32, less66_out_gg(T27, T32)) → less42_out_gg(s(s(T27)), s(T32))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → ordered1_out_g(.(T9, .(T13, T14)))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → U2_g(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U2_g(T9, T13, T14, ordered1_out_g(.(T13, T14))) → ordered1_out_g(.(T9, .(T13, T14)))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

ordered1_in_g([]) → ordered1_out_g([])
ordered1_in_g(.(T2, [])) → ordered1_out_g(.(T2, []))
ordered1_in_g(.(T9, .(T13, T14))) → U1_g(T9, T13, T14, less42_in_gg(T9, T13))
less42_in_gg(0, T15) → less42_out_gg(0, T15)
less42_in_gg(s(0), s(T22)) → less42_out_gg(s(0), s(T22))
less42_in_gg(s(s(s(T31))), 0) → U6_gg(T31, less88_in_ga(T31, X81))
less88_in_ga(s(T31), X68) → U3_ga(T31, X68, less88_in_ga(T31, X81))
U3_ga(T31, X68, less88_out_ga(T31, X81)) → less88_out_ga(s(T31), X68)
U6_gg(T31, less88_out_ga(T31, X81)) → less42_out_gg(s(s(s(T31))), 0)
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(T27, T32, less66_in_gg(T27, T32))
less66_in_gg(0, s(T22)) → less66_out_gg(0, s(T22))
less66_in_gg(s(s(T31)), 0) → U4_gg(T31, less88_in_ga(T31, X81))
U4_gg(T31, less88_out_ga(T31, X81)) → less66_out_gg(s(s(T31)), 0)
less66_in_gg(s(T27), s(T32)) → U5_gg(T27, T32, less66_in_gg(T27, T32))
U5_gg(T27, T32, less66_out_gg(T27, T32)) → less66_out_gg(s(T27), s(T32))
U7_gg(T27, T32, less66_out_gg(T27, T32)) → less42_out_gg(s(s(T27)), s(T32))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → ordered1_out_g(.(T9, .(T13, T14)))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → U2_g(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U2_g(T9, T13, T14, ordered1_out_g(.(T13, T14))) → ordered1_out_g(.(T9, .(T13, T14)))

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

ORDERED1_IN_G(.(T9, .(T13, T14))) → U1_G(T9, T13, T14, less42_in_gg(T9, T13))
ORDERED1_IN_G(.(T9, .(T13, T14))) → LESS42_IN_GG(T9, T13)
LESS42_IN_GG(s(s(s(T31))), 0) → U6_GG(T31, less88_in_ga(T31, X81))
LESS42_IN_GG(s(s(s(T31))), 0) → LESS88_IN_GA(T31, X81)
LESS88_IN_GA(s(T31), X68) → U3_GA(T31, X68, less88_in_ga(T31, X81))
LESS88_IN_GA(s(T31), X68) → LESS88_IN_GA(T31, X81)
LESS42_IN_GG(s(s(T27)), s(T32)) → U7_GG(T27, T32, less66_in_gg(T27, T32))
LESS42_IN_GG(s(s(T27)), s(T32)) → LESS66_IN_GG(T27, T32)
LESS66_IN_GG(s(s(T31)), 0) → U4_GG(T31, less88_in_ga(T31, X81))
LESS66_IN_GG(s(s(T31)), 0) → LESS88_IN_GA(T31, X81)
LESS66_IN_GG(s(T27), s(T32)) → U5_GG(T27, T32, less66_in_gg(T27, T32))
LESS66_IN_GG(s(T27), s(T32)) → LESS66_IN_GG(T27, T32)
U1_G(T9, T13, T14, less42_out_gg(T9, T13)) → U2_G(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U1_G(T9, T13, T14, less42_out_gg(T9, T13)) → ORDERED1_IN_G(.(T13, T14))

The TRS R consists of the following rules:

ordered1_in_g([]) → ordered1_out_g([])
ordered1_in_g(.(T2, [])) → ordered1_out_g(.(T2, []))
ordered1_in_g(.(T9, .(T13, T14))) → U1_g(T9, T13, T14, less42_in_gg(T9, T13))
less42_in_gg(0, T15) → less42_out_gg(0, T15)
less42_in_gg(s(0), s(T22)) → less42_out_gg(s(0), s(T22))
less42_in_gg(s(s(s(T31))), 0) → U6_gg(T31, less88_in_ga(T31, X81))
less88_in_ga(s(T31), X68) → U3_ga(T31, X68, less88_in_ga(T31, X81))
U3_ga(T31, X68, less88_out_ga(T31, X81)) → less88_out_ga(s(T31), X68)
U6_gg(T31, less88_out_ga(T31, X81)) → less42_out_gg(s(s(s(T31))), 0)
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(T27, T32, less66_in_gg(T27, T32))
less66_in_gg(0, s(T22)) → less66_out_gg(0, s(T22))
less66_in_gg(s(s(T31)), 0) → U4_gg(T31, less88_in_ga(T31, X81))
U4_gg(T31, less88_out_ga(T31, X81)) → less66_out_gg(s(s(T31)), 0)
less66_in_gg(s(T27), s(T32)) → U5_gg(T27, T32, less66_in_gg(T27, T32))
U5_gg(T27, T32, less66_out_gg(T27, T32)) → less66_out_gg(s(T27), s(T32))
U7_gg(T27, T32, less66_out_gg(T27, T32)) → less42_out_gg(s(s(T27)), s(T32))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → ordered1_out_g(.(T9, .(T13, T14)))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → U2_g(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U2_g(T9, T13, T14, ordered1_out_g(.(T13, T14))) → ordered1_out_g(.(T9, .(T13, T14)))

The argument filtering Pi contains the following mapping:
ordered1_in_g(x1) = ordered1_in_g(x1)
[] = []
ordered1_out_g(x1) = ordered1_out_g
.(x1, x2) = .(x1, x2)
U1_g(x1, x2, x3, x4) = U1_g(x2, x3, x4)
less42_in_gg(x1, x2) = less42_in_gg(x1, x2)
0 = 0
less42_out_gg(x1, x2) = less42_out_gg
s(x1) = s(x1)
U6_gg(x1, x2) = U6_gg(x2)
less88_in_ga(x1, x2) = less88_in_ga(x1)
U3_ga(x1, x2, x3) = U3_ga(x3)
less88_out_ga(x1, x2) = less88_out_ga
U7_gg(x1, x2, x3) = U7_gg(x3)
less66_in_gg(x1, x2) = less66_in_gg(x1, x2)
less66_out_gg(x1, x2) = less66_out_gg
U4_gg(x1, x2) = U4_gg(x2)
U5_gg(x1, x2, x3) = U5_gg(x3)
U2_g(x1, x2, x3, x4) = U2_g(x4)
ORDERED1_IN_G(x1) = ORDERED1_IN_G(x1)
U1_G(x1, x2, x3, x4) = U1_G(x2, x3, x4)
LESS42_IN_GG(x1, x2) = LESS42_IN_GG(x1, x2)
U6_GG(x1, x2) = U6_GG(x2)
LESS88_IN_GA(x1, x2) = LESS88_IN_GA(x1)
U3_GA(x1, x2, x3) = U3_GA(x3)
U7_GG(x1, x2, x3) = U7_GG(x3)
LESS66_IN_GG(x1, x2) = LESS66_IN_GG(x1, x2)
U4_GG(x1, x2) = U4_GG(x2)
U5_GG(x1, x2, x3) = U5_GG(x3)
U2_G(x1, x2, x3, x4) = U2_G(x4)

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

(6) Obligation:

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

ORDERED1_IN_G(.(T9, .(T13, T14))) → U1_G(T9, T13, T14, less42_in_gg(T9, T13))
ORDERED1_IN_G(.(T9, .(T13, T14))) → LESS42_IN_GG(T9, T13)
LESS42_IN_GG(s(s(s(T31))), 0) → U6_GG(T31, less88_in_ga(T31, X81))
LESS42_IN_GG(s(s(s(T31))), 0) → LESS88_IN_GA(T31, X81)
LESS88_IN_GA(s(T31), X68) → U3_GA(T31, X68, less88_in_ga(T31, X81))
LESS88_IN_GA(s(T31), X68) → LESS88_IN_GA(T31, X81)
LESS42_IN_GG(s(s(T27)), s(T32)) → U7_GG(T27, T32, less66_in_gg(T27, T32))
LESS42_IN_GG(s(s(T27)), s(T32)) → LESS66_IN_GG(T27, T32)
LESS66_IN_GG(s(s(T31)), 0) → U4_GG(T31, less88_in_ga(T31, X81))
LESS66_IN_GG(s(s(T31)), 0) → LESS88_IN_GA(T31, X81)
LESS66_IN_GG(s(T27), s(T32)) → U5_GG(T27, T32, less66_in_gg(T27, T32))
LESS66_IN_GG(s(T27), s(T32)) → LESS66_IN_GG(T27, T32)
U1_G(T9, T13, T14, less42_out_gg(T9, T13)) → U2_G(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U1_G(T9, T13, T14, less42_out_gg(T9, T13)) → ORDERED1_IN_G(.(T13, T14))

The TRS R consists of the following rules:

ordered1_in_g([]) → ordered1_out_g([])
ordered1_in_g(.(T2, [])) → ordered1_out_g(.(T2, []))
ordered1_in_g(.(T9, .(T13, T14))) → U1_g(T9, T13, T14, less42_in_gg(T9, T13))
less42_in_gg(0, T15) → less42_out_gg(0, T15)
less42_in_gg(s(0), s(T22)) → less42_out_gg(s(0), s(T22))
less42_in_gg(s(s(s(T31))), 0) → U6_gg(T31, less88_in_ga(T31, X81))
less88_in_ga(s(T31), X68) → U3_ga(T31, X68, less88_in_ga(T31, X81))
U3_ga(T31, X68, less88_out_ga(T31, X81)) → less88_out_ga(s(T31), X68)
U6_gg(T31, less88_out_ga(T31, X81)) → less42_out_gg(s(s(s(T31))), 0)
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(T27, T32, less66_in_gg(T27, T32))
less66_in_gg(0, s(T22)) → less66_out_gg(0, s(T22))
less66_in_gg(s(s(T31)), 0) → U4_gg(T31, less88_in_ga(T31, X81))
U4_gg(T31, less88_out_ga(T31, X81)) → less66_out_gg(s(s(T31)), 0)
less66_in_gg(s(T27), s(T32)) → U5_gg(T27, T32, less66_in_gg(T27, T32))
U5_gg(T27, T32, less66_out_gg(T27, T32)) → less66_out_gg(s(T27), s(T32))
U7_gg(T27, T32, less66_out_gg(T27, T32)) → less42_out_gg(s(s(T27)), s(T32))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → ordered1_out_g(.(T9, .(T13, T14)))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → U2_g(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U2_g(T9, T13, T14, ordered1_out_g(.(T13, T14))) → ordered1_out_g(.(T9, .(T13, T14)))

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 10 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

LESS88_IN_GA(s(T31), X68) → LESS88_IN_GA(T31, X81)

The TRS R consists of the following rules:

ordered1_in_g([]) → ordered1_out_g([])
ordered1_in_g(.(T2, [])) → ordered1_out_g(.(T2, []))
ordered1_in_g(.(T9, .(T13, T14))) → U1_g(T9, T13, T14, less42_in_gg(T9, T13))
less42_in_gg(0, T15) → less42_out_gg(0, T15)
less42_in_gg(s(0), s(T22)) → less42_out_gg(s(0), s(T22))
less42_in_gg(s(s(s(T31))), 0) → U6_gg(T31, less88_in_ga(T31, X81))
less88_in_ga(s(T31), X68) → U3_ga(T31, X68, less88_in_ga(T31, X81))
U3_ga(T31, X68, less88_out_ga(T31, X81)) → less88_out_ga(s(T31), X68)
U6_gg(T31, less88_out_ga(T31, X81)) → less42_out_gg(s(s(s(T31))), 0)
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(T27, T32, less66_in_gg(T27, T32))
less66_in_gg(0, s(T22)) → less66_out_gg(0, s(T22))
less66_in_gg(s(s(T31)), 0) → U4_gg(T31, less88_in_ga(T31, X81))
U4_gg(T31, less88_out_ga(T31, X81)) → less66_out_gg(s(s(T31)), 0)
less66_in_gg(s(T27), s(T32)) → U5_gg(T27, T32, less66_in_gg(T27, T32))
U5_gg(T27, T32, less66_out_gg(T27, T32)) → less66_out_gg(s(T27), s(T32))
U7_gg(T27, T32, less66_out_gg(T27, T32)) → less42_out_gg(s(s(T27)), s(T32))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → ordered1_out_g(.(T9, .(T13, T14)))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → U2_g(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U2_g(T9, T13, T14, ordered1_out_g(.(T13, T14))) → ordered1_out_g(.(T9, .(T13, T14)))

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

LESS88_IN_GA(s(T31), X68) → LESS88_IN_GA(T31, X81)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

LESS88_IN_GA(s(T31)) → LESS88_IN_GA(T31)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LESS88_IN_GA(s(T31)) → LESS88_IN_GA(T31)
The graph contains the following edges 1 > 1

(15) TRUE

(16) Obligation:

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

LESS66_IN_GG(s(T27), s(T32)) → LESS66_IN_GG(T27, T32)

The TRS R consists of the following rules:

ordered1_in_g([]) → ordered1_out_g([])
ordered1_in_g(.(T2, [])) → ordered1_out_g(.(T2, []))
ordered1_in_g(.(T9, .(T13, T14))) → U1_g(T9, T13, T14, less42_in_gg(T9, T13))
less42_in_gg(0, T15) → less42_out_gg(0, T15)
less42_in_gg(s(0), s(T22)) → less42_out_gg(s(0), s(T22))
less42_in_gg(s(s(s(T31))), 0) → U6_gg(T31, less88_in_ga(T31, X81))
less88_in_ga(s(T31), X68) → U3_ga(T31, X68, less88_in_ga(T31, X81))
U3_ga(T31, X68, less88_out_ga(T31, X81)) → less88_out_ga(s(T31), X68)
U6_gg(T31, less88_out_ga(T31, X81)) → less42_out_gg(s(s(s(T31))), 0)
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(T27, T32, less66_in_gg(T27, T32))
less66_in_gg(0, s(T22)) → less66_out_gg(0, s(T22))
less66_in_gg(s(s(T31)), 0) → U4_gg(T31, less88_in_ga(T31, X81))
U4_gg(T31, less88_out_ga(T31, X81)) → less66_out_gg(s(s(T31)), 0)
less66_in_gg(s(T27), s(T32)) → U5_gg(T27, T32, less66_in_gg(T27, T32))
U5_gg(T27, T32, less66_out_gg(T27, T32)) → less66_out_gg(s(T27), s(T32))
U7_gg(T27, T32, less66_out_gg(T27, T32)) → less42_out_gg(s(s(T27)), s(T32))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → ordered1_out_g(.(T9, .(T13, T14)))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → U2_g(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U2_g(T9, T13, T14, ordered1_out_g(.(T13, T14))) → ordered1_out_g(.(T9, .(T13, T14)))

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

LESS66_IN_GG(s(T27), s(T32)) → LESS66_IN_GG(T27, T32)

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

(19) PiDPToQDPProof (EQUIVALENT transformation)

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

(20) Obligation:

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

LESS66_IN_GG(s(T27), s(T32)) → LESS66_IN_GG(T27, T32)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

LESS66_IN_GG(s(T27), s(T32)) → LESS66_IN_GG(T27, T32)
The graph contains the following edges 1 > 1, 2 > 2

(22) TRUE

(23) Obligation:

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

U1_G(T9, T13, T14, less42_out_gg(T9, T13)) → ORDERED1_IN_G(.(T13, T14))
ORDERED1_IN_G(.(T9, .(T13, T14))) → U1_G(T9, T13, T14, less42_in_gg(T9, T13))

The TRS R consists of the following rules:

ordered1_in_g([]) → ordered1_out_g([])
ordered1_in_g(.(T2, [])) → ordered1_out_g(.(T2, []))
ordered1_in_g(.(T9, .(T13, T14))) → U1_g(T9, T13, T14, less42_in_gg(T9, T13))
less42_in_gg(0, T15) → less42_out_gg(0, T15)
less42_in_gg(s(0), s(T22)) → less42_out_gg(s(0), s(T22))
less42_in_gg(s(s(s(T31))), 0) → U6_gg(T31, less88_in_ga(T31, X81))
less88_in_ga(s(T31), X68) → U3_ga(T31, X68, less88_in_ga(T31, X81))
U3_ga(T31, X68, less88_out_ga(T31, X81)) → less88_out_ga(s(T31), X68)
U6_gg(T31, less88_out_ga(T31, X81)) → less42_out_gg(s(s(s(T31))), 0)
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(T27, T32, less66_in_gg(T27, T32))
less66_in_gg(0, s(T22)) → less66_out_gg(0, s(T22))
less66_in_gg(s(s(T31)), 0) → U4_gg(T31, less88_in_ga(T31, X81))
U4_gg(T31, less88_out_ga(T31, X81)) → less66_out_gg(s(s(T31)), 0)
less66_in_gg(s(T27), s(T32)) → U5_gg(T27, T32, less66_in_gg(T27, T32))
U5_gg(T27, T32, less66_out_gg(T27, T32)) → less66_out_gg(s(T27), s(T32))
U7_gg(T27, T32, less66_out_gg(T27, T32)) → less42_out_gg(s(s(T27)), s(T32))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → ordered1_out_g(.(T9, .(T13, T14)))
U1_g(T9, T13, T14, less42_out_gg(T9, T13)) → U2_g(T9, T13, T14, ordered1_in_g(.(T13, T14)))
U2_g(T9, T13, T14, ordered1_out_g(.(T13, T14))) → ordered1_out_g(.(T9, .(T13, T14)))

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

U1_G(T9, T13, T14, less42_out_gg(T9, T13)) → ORDERED1_IN_G(.(T13, T14))
ORDERED1_IN_G(.(T9, .(T13, T14))) → U1_G(T9, T13, T14, less42_in_gg(T9, T13))

The TRS R consists of the following rules:

less42_in_gg(0, T15) → less42_out_gg(0, T15)
less42_in_gg(s(0), s(T22)) → less42_out_gg(s(0), s(T22))
less42_in_gg(s(s(s(T31))), 0) → U6_gg(T31, less88_in_ga(T31, X81))
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(T27, T32, less66_in_gg(T27, T32))
U6_gg(T31, less88_out_ga(T31, X81)) → less42_out_gg(s(s(s(T31))), 0)
U7_gg(T27, T32, less66_out_gg(T27, T32)) → less42_out_gg(s(s(T27)), s(T32))
less88_in_ga(s(T31), X68) → U3_ga(T31, X68, less88_in_ga(T31, X81))
less66_in_gg(0, s(T22)) → less66_out_gg(0, s(T22))
less66_in_gg(s(s(T31)), 0) → U4_gg(T31, less88_in_ga(T31, X81))
less66_in_gg(s(T27), s(T32)) → U5_gg(T27, T32, less66_in_gg(T27, T32))
U3_ga(T31, X68, less88_out_ga(T31, X81)) → less88_out_ga(s(T31), X68)
U4_gg(T31, less88_out_ga(T31, X81)) → less66_out_gg(s(s(T31)), 0)
U5_gg(T27, T32, less66_out_gg(T27, T32)) → less66_out_gg(s(T27), s(T32))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
less42_in_gg(x1, x2) = less42_in_gg(x1, x2)
0 = 0
less42_out_gg(x1, x2) = less42_out_gg
s(x1) = s(x1)
U6_gg(x1, x2) = U6_gg(x2)
less88_in_ga(x1, x2) = less88_in_ga(x1)
U3_ga(x1, x2, x3) = U3_ga(x3)
less88_out_ga(x1, x2) = less88_out_ga
U7_gg(x1, x2, x3) = U7_gg(x3)
less66_in_gg(x1, x2) = less66_in_gg(x1, x2)
less66_out_gg(x1, x2) = less66_out_gg
U4_gg(x1, x2) = U4_gg(x2)
U5_gg(x1, x2, x3) = U5_gg(x3)
ORDERED1_IN_G(x1) = ORDERED1_IN_G(x1)
U1_G(x1, x2, x3, x4) = U1_G(x2, x3, x4)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

U1_G(T13, T14, less42_out_gg) → ORDERED1_IN_G(.(T13, T14))
ORDERED1_IN_G(.(T9, .(T13, T14))) → U1_G(T13, T14, less42_in_gg(T9, T13))

The TRS R consists of the following rules:

less42_in_gg(0, T15) → less42_out_gg
less42_in_gg(s(0), s(T22)) → less42_out_gg
less42_in_gg(s(s(s(T31))), 0) → U6_gg(less88_in_ga(T31))
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(less66_in_gg(T27, T32))
U6_gg(less88_out_ga) → less42_out_gg
U7_gg(less66_out_gg) → less42_out_gg
less88_in_ga(s(T31)) → U3_ga(less88_in_ga(T31))
less66_in_gg(0, s(T22)) → less66_out_gg
less66_in_gg(s(s(T31)), 0) → U4_gg(less88_in_ga(T31))
less66_in_gg(s(T27), s(T32)) → U5_gg(less66_in_gg(T27, T32))
U3_ga(less88_out_ga) → less88_out_ga
U4_gg(less88_out_ga) → less66_out_gg
U5_gg(less66_out_gg) → less66_out_gg

The set Q consists of the following terms:

less42_in_gg(x0, x1)
U6_gg(x0)
U7_gg(x0)
less88_in_ga(x0)
less66_in_gg(x0, x1)
U3_ga(x0)
U4_gg(x0)
U5_gg(x0)

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

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

ORDERED1_IN_G(.(T9, .(T13, T14))) → U1_G(T13, T14, less42_in_gg(T9, T13))

The following rules are removed from R:

less42_in_gg(0, T15) → less42_out_gg
less42_in_gg(s(0), s(T22)) → less42_out_gg
less42_in_gg(s(s(s(T31))), 0) → U6_gg(less88_in_ga(T31))
less42_in_gg(s(s(T27)), s(T32)) → U7_gg(less66_in_gg(T27, T32))
less66_in_gg(0, s(T22)) → less66_out_gg
less66_in_gg(s(s(T31)), 0) → U4_gg(less88_in_ga(T31))
less66_in_gg(s(T27), s(T32)) → U5_gg(less66_in_gg(T27, T32))
U7_gg(less66_out_gg) → less42_out_gg
U5_gg(less66_out_gg) → less66_out_gg
less88_in_ga(s(T31)) → U3_ga(less88_in_ga(T31))
U4_gg(less88_out_ga) → less66_out_gg
U3_ga(less88_out_ga) → less88_out_ga
U6_gg(less88_out_ga) → less42_out_gg

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(0) = 0
POL(ORDERED1_IN_G(x₁)) = 2 + x₁
POL(U1_G(x₁, x₂, x₃)) = 2 + 2·x₁ + 2·x₂ + x₃
POL(U3_ga(x₁)) = 1 + 2·x₁
POL(U4_gg(x₁)) = 2 + x₁
POL(U5_gg(x₁)) = 2 + 2·x₁
POL(U6_gg(x₁)) = 1 + 2·x₁
POL(U7_gg(x₁)) = 2 + x₁
POL(less42_in_gg(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(less42_out_gg) = 2
POL(less66_in_gg(x₁, x₂)) = 1 + x₁ + x₂
POL(less66_out_gg) = 1
POL(less88_in_ga(x₁)) = x₁
POL(less88_out_ga) = 2
POL(s(x₁)) = 2 + 2·x₁

(29) Obligation:

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

U1_G(T13, T14, less42_out_gg) → ORDERED1_IN_G(.(T13, T14))

R is empty.
The set Q consists of the following terms:

less42_in_gg(x0, x1)
U6_gg(x0)
U7_gg(x0)
less88_in_ga(x0)
less66_in_gg(x0, x1)
U3_ga(x0)
U4_gg(x0)
U5_gg(x0)

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

(30) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) PrologToPiTRSProof (SOUND transformation)

(4) Obligation:

(5) DependencyPairsProof (EQUIVALENT transformation)

(6) Obligation:

(7) DependencyGraphProof (EQUIVALENT transformation)

(8) Complex Obligation (AND)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) PiDPToQDPProof (SOUND transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) TRUE

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (EQUIVALENT transformation)

(20) Obligation:

(21) QDPSizeChangeProof (EQUIVALENT transformation)

(22) TRUE

(23) Obligation:

(24) UsableRulesProof (EQUIVALENT transformation)

(25) Obligation:

(26) PiDPToQDPProof (SOUND transformation)

(27) Obligation:

(28) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(29) Obligation:

(30) DependencyGraphProof (EQUIVALENT transformation)

(31) TRUE