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

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 201 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 7 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 12 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 4 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇔, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇔, 0 ms)

        ↳25 QDP

        ↳26 QDPOrderProof (⇔, 59 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

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

Query: ordered(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: 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];
10 [label="10: true | ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nordered(T1) !=? ordered([])", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(no(max1el_list([])), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14))))))))\n\nX11 is free\nX12 is free\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(no(max1el_list([])), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))), SCOPE: 2, CLAUSE: 14 | ','(no(max1el_list([])), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))), SCOPE: 2, CLAUSE: 15\n\nX11 is free\nX12 is free\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(','(call(max1el_list([])), ','(!_2, failure(a))), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))) | ','(no(max1el_list([])), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))), SCOPE: 2, CLAUSE: 15\n\nX11 is free\nX12 is free\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(max1el_list([]), ','(','(!_2, failure(a)), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14))))))))) | ?_3 | ','(no(max1el_list([])), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))), SCOPE: 2, CLAUSE: 15\n\nX11 is free\nX12 is free\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(max1el_list([]), ','(','(!_2, failure(a)), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14))))))))), SCOPE: 4, CLAUSE: 11 | ','(max1el_list([]), ','(','(!_2, failure(a)), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14))))))))), SCOPE: 4, CLAUSE: 12 | ?_4 | ?_3 | ','(no(max1el_list([])), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))), SCOPE: 2, CLAUSE: 15\n\nX11 is free\nX12 is free\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(','(!_2, failure(a)), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))) | ','(max1el_list([]), ','(','(!_2, failure(a)), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14))))))))), SCOPE: 4, CLAUSE: 12 | ?_4 | ?_3 | ','(no(max1el_list([])), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))), SCOPE: 2, CLAUSE: 15\n\nX11 is free\nX12 is free\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(failure(a), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14))))))))\n\nX11 is free\nX12 is free\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(failure(a), ','(head([], X11), ','(tail([], X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))), SCOPE: 5, CLAUSE: 16\n\nX11 is free\nX12 is free\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: true | ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX21 is free\nordered(T1) !=? ordered([])\nordered(T1) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(no(max1el_list(.(T5, []))), ','(head(.(T5, []), X24), ','(tail(.(T5, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27))))))))\n\nT5 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(no(max1el_list(.(T5, []))), ','(head(.(T5, []), X24), ','(tail(.(T5, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))), SCOPE: 6, CLAUSE: 14 | ','(no(max1el_list(.(T5, []))), ','(head(.(T5, []), X24), ','(tail(.(T5, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))), SCOPE: 6, CLAUSE: 15\n\nT5 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(','(call(max1el_list(.(T8, []))), ','(!_6, failure(a))), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))) | ','(no(max1el_list(.(T8, []))), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))), SCOPE: 6, CLAUSE: 15\n\nT8 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(max1el_list(.(T8, [])), ','(','(!_6, failure(a)), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27))))))))) | ?_7 | ','(no(max1el_list(.(T8, []))), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))), SCOPE: 6, CLAUSE: 15\n\nT8 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(max1el_list(.(T8, [])), ','(','(!_6, failure(a)), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27))))))))), SCOPE: 8, CLAUSE: 11 | ','(max1el_list(.(T8, [])), ','(','(!_6, failure(a)), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27))))))))), SCOPE: 8, CLAUSE: 12 | ?_8 | ?_7 | ','(no(max1el_list(.(T8, []))), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))), SCOPE: 6, CLAUSE: 15\n\nT8 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(max1el_list(.(T8, [])), ','(','(!_6, failure(a)), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27))))))))), SCOPE: 8, CLAUSE: 12 | ?_8 | ?_7 | ','(no(max1el_list(.(T8, []))), ','(head(.(T8, []), X24), ','(tail(.(T8, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))), SCOPE: 6, CLAUSE: 15\n\nT8 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(','(!_6, failure(a)), ','(head(.(T11, []), X24), ','(tail(.(T11, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))) | ?_8 | ?_7 | ','(no(max1el_list(.(T11, []))), ','(head(.(T11, []), X24), ','(tail(.(T11, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))), SCOPE: 6, CLAUSE: 15\n\nT11 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(failure(a), ','(head(.(T11, []), X24), ','(tail(.(T11, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27))))))))\n\nT11 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(failure(a), ','(head(.(T11, []), X24), ','(tail(.(T11, []), X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))), SCOPE: 9, CLAUSE: 16\n\nT11 is ground\nX24 is free\nX25 is free\nX26 is free\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(no(max1el_list(T13)), ','(head(T13, X38), ','(tail(T13, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41))))))))\n\nT13 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T13) !=? ordered([])\nordered(T13) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(no(max1el_list(T13)), ','(head(T13, X38), ','(tail(T13, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 14 | ','(no(max1el_list(T13)), ','(head(T13, X38), ','(tail(T13, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 15\n\nT13 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T13) !=? ordered([])\nordered(T13) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(','(call(max1el_list(T16)), ','(!_10, failure(a))), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))) | ','(no(max1el_list(T16)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 15\n\nT16 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(max1el_list(T16), ','(','(!_10, failure(a)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41))))))))) | ?_11 | ','(no(max1el_list(T16)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 15\n\nT16 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(max1el_list(T16), ','(','(!_10, failure(a)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41))))))))), SCOPE: 12, CLAUSE: 11 | ','(max1el_list(T16), ','(','(!_10, failure(a)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41))))))))), SCOPE: 12, CLAUSE: 12 | ?_12 | ?_11 | ','(no(max1el_list(T16)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 15\n\nT16 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(max1el_list(T16), ','(','(!_10, failure(a)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41))))))))), SCOPE: 12, CLAUSE: 12 | ?_12 | ?_11 | ','(no(max1el_list(T16)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 15\n\nT16 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ?_12 | ?_11 | ','(no(max1el_list(T16)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 15\n\nT16 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ?_11 | ','(no(max1el_list(T16)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 15\n\nT16 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(no(max1el_list(T16)), ','(head(T16, X38), ','(tail(T16, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))), SCOPE: 10, CLAUSE: 15\n\nT16 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(head(T20, X38), ','(tail(T20, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))\n\nT20 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T20) !=? ordered([])\nordered(T20) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(head(T20, X38), ','(tail(T20, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41))))))), SCOPE: 13, CLAUSE: 3 | ','(head(T20, X38), ','(tail(T20, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41))))))), SCOPE: 13, CLAUSE: 4\n\nT20 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T20) !=? ordered([])\nordered(T20) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(head(T20, X38), ','(tail(T20, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41))))))), SCOPE: 13, CLAUSE: 4\n\nT20 is ground\nX21 is free\nX38 is free\nX39 is free\nX40 is free\nX41 is free\nordered(T20) !=? ordered([])\nordered(T20) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(tail(.(T25, T26), X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(T25, s(X40)), ordered(.(X40, X41))))))\n\nT25 is ground\nT26 is ground\nX21 is free\nX39 is free\nX40 is free\nX41 is free\nordered(.(T25, T26)) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(tail(.(T25, T26), X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(T25, s(X40)), ordered(.(X40, X41)))))), SCOPE: 14, CLAUSE: 5 | ','(tail(.(T25, T26), X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(T25, s(X40)), ordered(.(X40, X41)))))), SCOPE: 14, CLAUSE: 6\n\nT25 is ground\nT26 is ground\nX21 is free\nX39 is free\nX40 is free\nX41 is free\nordered(.(T25, T26)) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(tail(.(T25, T26), X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(T25, s(X40)), ordered(.(X40, X41)))))), SCOPE: 14, CLAUSE: 6\n\nT25 is ground\nT26 is ground\nX21 is free\nX39 is free\nX40 is free\nX41 is free\nordered(.(T25, T26)) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(head(T32, X40), ','(tail(T32, X41), ','(less(T31, s(X40)), ordered(.(X40, X41)))))\n\nT31 is ground\nT32 is ground\nX21 is free\nX40 is free\nX41 is free\nordered(.(T31, T32)) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(head(T32, X40), ','(tail(T32, X41), ','(less(T31, s(X40)), ordered(.(X40, X41))))), SCOPE: 15, CLAUSE: 3 | ','(head(T32, X40), ','(tail(T32, X41), ','(less(T31, s(X40)), ordered(.(X40, X41))))), SCOPE: 15, CLAUSE: 4\n\nT31 is ground\nT32 is ground\nX21 is free\nX40 is free\nX41 is free\nordered(.(T31, T32)) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(head(T32, X40), ','(tail(T32, X41), ','(less(T31, s(X40)), ordered(.(X40, X41))))), SCOPE: 15, CLAUSE: 4\n\nT31 is ground\nT32 is ground\nX21 is free\nX40 is free\nX41 is free\nordered(.(T31, T32)) !=? ordered(.(X21, []))", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(tail(.(T37, T38), X41), ','(less(T31, s(T37)), ordered(.(T37, X41))))\n\nT31 is ground\nT37 is ground\nT38 is ground\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(tail(.(T37, T38), X41), ','(less(T31, s(T37)), ordered(.(T37, X41)))), SCOPE: 16, CLAUSE: 5 | ','(tail(.(T37, T38), X41), ','(less(T31, s(T37)), ordered(.(T37, X41)))), SCOPE: 16, CLAUSE: 6\n\nT31 is ground\nT37 is ground\nT38 is ground\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(tail(.(T37, T38), X41), ','(less(T31, s(T37)), ordered(.(T37, X41)))), SCOPE: 16, CLAUSE: 6\n\nT31 is ground\nT37 is ground\nT38 is ground\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="B: ','(less(T31, s(T47)), ordered(.(T47, T48)))\n\nT31 is ground\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="E: less(T31, s(T47))\n\nT31 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ordered(.(T47, T48))\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: less(T31, s(T47)), SCOPE: 17, CLAUSE: 7 | less(T31, s(T47)), SCOPE: 17, CLAUSE: 8\n\nT31 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: less(T31, s(T47)), SCOPE: 17, CLAUSE: 7\n\nT31 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: less(T31, s(T47)), SCOPE: 17, CLAUSE: 8\n\nT31 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(no(zero(T62)), ','(p(T62, X116), ','(p(s(T63), X117), less(X116, X117))))\n\nT62 is ground\nT63 is ground\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(no(zero(T62)), ','(p(T62, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 14 | ','(no(zero(T62)), ','(p(T62, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 15\n\nT62 is ground\nT63 is ground\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(','(call(zero(T66)), ','(!_18, failure(a))), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117)))) | ','(no(zero(T66)), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 15\n\nT63 is ground\nT66 is ground\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(zero(T66), ','(','(!_18, failure(a)), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117))))) | ?_19 | ','(no(zero(T66)), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 15\n\nT63 is ground\nT66 is ground\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(zero(T66), ','(','(!_18, failure(a)), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117))))), SCOPE: 20, CLAUSE: 13 | ?_20 | ?_19 | ','(no(zero(T66)), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 15\n\nT63 is ground\nT66 is ground\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(','(!_18, failure(a)), ','(p(0, X116), ','(p(s(T63), X117), less(X116, X117)))) | ?_20 | ?_19 | ','(no(zero(0)), ','(p(0, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 15\n\nT63 is ground\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ?_20 | ?_19 | ','(no(zero(T66)), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 15\n\nT63 is ground\nT66 is ground\nX116 is free\nX117 is free\nzero(T66) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(failure(a), ','(p(0, X116), ','(p(s(T63), X117), less(X116, X117))))\n\nT63 is ground\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(failure(a), ','(p(0, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 21, CLAUSE: 16\n\nT63 is ground\nX116 is free\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ?_19 | ','(no(zero(T66)), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 15\n\nT63 is ground\nT66 is ground\nX116 is free\nX117 is free\nzero(T66) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(no(zero(T66)), ','(p(T66, X116), ','(p(s(T63), X117), less(X116, X117)))), SCOPE: 18, CLAUSE: 15\n\nT63 is ground\nT66 is ground\nX116 is free\nX117 is free\nzero(T66) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: ','(p(T69, X116), ','(p(s(T63), X117), less(X116, X117)))\n\nT63 is ground\nT69 is ground\nX116 is free\nX117 is free\nzero(T69) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(p(T69, X116), ','(p(s(T63), X117), less(X116, X117))), SCOPE: 22, CLAUSE: 9 | ','(p(T69, X116), ','(p(s(T63), X117), less(X116, X117))), SCOPE: 22, CLAUSE: 10\n\nT63 is ground\nT69 is ground\nX116 is free\nX117 is free\nzero(T69) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: ','(p(T69, X116), ','(p(s(T63), X117), less(X116, X117))), SCOPE: 22, CLAUSE: 10\n\nT63 is ground\nT69 is ground\nX116 is free\nX117 is free\nzero(T69) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ','(p(s(T63), X117), less(T72, X117))\n\nT63 is ground\nT72 is ground\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: ','(p(s(T63), X117), less(T72, X117)), SCOPE: 23, CLAUSE: 9 | ','(p(s(T63), X117), less(T72, X117)), SCOPE: 23, CLAUSE: 10\n\nT63 is ground\nT72 is ground\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: ','(p(s(T63), X117), less(T72, X117)), SCOPE: 23, CLAUSE: 10\n\nT63 is ground\nT72 is ground\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="D: less(T72, T77)\n\nT72 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: less(T72, T77), SCOPE: 24, CLAUSE: 7 | less(T72, T77), SCOPE: 24, CLAUSE: 8\n\nT72 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: less(T72, T77), SCOPE: 24, CLAUSE: 7\n\nT72 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: less(T72, T77), SCOPE: 24, CLAUSE: 8\n\nT72 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: ','(no(zero(T89)), ','(p(T89, X161), ','(p(T90, X162), less(X161, X162))))\n\nT89 is ground\nT90 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: ','(no(zero(T89)), ','(p(T89, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 14 | ','(no(zero(T89)), ','(p(T89, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 15\n\nT89 is ground\nT90 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: ','(','(call(zero(T93)), ','(!_25, failure(a))), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162)))) | ','(no(zero(T93)), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 15\n\nT90 is ground\nT93 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: ','(zero(T93), ','(','(!_25, failure(a)), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162))))) | ?_26 | ','(no(zero(T93)), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 15\n\nT90 is ground\nT93 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
293 [label="293: ','(zero(T93), ','(','(!_25, failure(a)), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162))))), SCOPE: 27, CLAUSE: 13 | ?_27 | ?_26 | ','(no(zero(T93)), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 15\n\nT90 is ground\nT93 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: ','(','(!_25, failure(a)), ','(p(0, X161), ','(p(T90, X162), less(X161, X162)))) | ?_27 | ?_26 | ','(no(zero(0)), ','(p(0, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 15\n\nT90 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: ?_27 | ?_26 | ','(no(zero(T93)), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 15\n\nT90 is ground\nT93 is ground\nX161 is free\nX162 is free\nzero(T93) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: ','(failure(a), ','(p(0, X161), ','(p(T90, X162), less(X161, X162))))\n\nT90 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: ','(failure(a), ','(p(0, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 28, CLAUSE: 16\n\nT90 is ground\nX161 is free\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="327: ?_26 | ','(no(zero(T93)), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 15\n\nT90 is ground\nT93 is ground\nX161 is free\nX162 is free\nzero(T93) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: ','(no(zero(T93)), ','(p(T93, X161), ','(p(T90, X162), less(X161, X162)))), SCOPE: 25, CLAUSE: 15\n\nT90 is ground\nT93 is ground\nX161 is free\nX162 is free\nzero(T93) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: ','(p(T96, X161), ','(p(T90, X162), less(X161, X162)))\n\nT90 is ground\nT96 is ground\nX161 is free\nX162 is free\nzero(T96) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: ','(p(T96, X161), ','(p(T90, X162), less(X161, X162))), SCOPE: 29, CLAUSE: 9 | ','(p(T96, X161), ','(p(T90, X162), less(X161, X162))), SCOPE: 29, CLAUSE: 10\n\nT90 is ground\nT96 is ground\nX161 is free\nX162 is free\nzero(T96) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: ','(p(T96, X161), ','(p(T90, X162), less(X161, X162))), SCOPE: 29, CLAUSE: 10\n\nT90 is ground\nT96 is ground\nX161 is free\nX162 is free\nzero(T96) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: ','(p(T90, X162), less(T99, X162))\n\nT90 is ground\nT99 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: ','(p(T90, X162), less(T99, X162)), SCOPE: 30, CLAUSE: 9 | ','(p(T90, X162), less(T99, X162)), SCOPE: 30, CLAUSE: 10\n\nT90 is ground\nT99 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: ','(p(T90, X162), less(T99, X162)), SCOPE: 30, CLAUSE: 9\n\nT90 is ground\nT99 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
342 [label="342: ','(p(T90, X162), less(T99, X162)), SCOPE: 30, CLAUSE: 10\n\nT90 is ground\nT99 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
343 [label="C: less(T99, 0)\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
344 [label="344: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: less(T99, 0), SCOPE: 31, CLAUSE: 7 | less(T99, 0), SCOPE: 31, CLAUSE: 8\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
351 [label="351: less(T99, 0), SCOPE: 31, CLAUSE: 8\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
359 [label="359: ','(no(zero(T102)), ','(p(T102, X197), ','(p(0, X198), less(X197, X198))))\n\nT102 is ground\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
361 [label="361: ','(no(zero(T102)), ','(p(T102, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 14 | ','(no(zero(T102)), ','(p(T102, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 15\n\nT102 is ground\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
364 [label="364: ','(','(call(zero(T105)), ','(!_32, failure(a))), ','(p(T105, X197), ','(p(0, X198), less(X197, X198)))) | ','(no(zero(T105)), ','(p(T105, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 15\n\nT105 is ground\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: ','(zero(T105), ','(','(!_32, failure(a)), ','(p(T105, X197), ','(p(0, X198), less(X197, X198))))) | ?_33 | ','(no(zero(T105)), ','(p(T105, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 15\n\nT105 is ground\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: ','(zero(T105), ','(','(!_32, failure(a)), ','(p(T105, X197), ','(p(0, X198), less(X197, X198))))), SCOPE: 34, CLAUSE: 13 | ?_34 | ?_33 | ','(no(zero(T105)), ','(p(T105, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 15\n\nT105 is ground\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
369 [label="369: ','(','(!_32, failure(a)), ','(p(0, X197), ','(p(0, X198), less(X197, X198)))) | ?_34 | ?_33 | ','(no(zero(0)), ','(p(0, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 15\n\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: ?_34 | ?_33 | ','(no(zero(T105)), ','(p(T105, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 15\n\nT105 is ground\nX197 is free\nX198 is free\nzero(T105) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: ','(failure(a), ','(p(0, X197), ','(p(0, X198), less(X197, X198))))\n\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="373: ','(failure(a), ','(p(0, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 35, CLAUSE: 16\n\nX197 is free\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
374 [label="374: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: ?_33 | ','(no(zero(T105)), ','(p(T105, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 15\n\nT105 is ground\nX197 is free\nX198 is free\nzero(T105) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: ','(no(zero(T105)), ','(p(T105, X197), ','(p(0, X198), less(X197, X198)))), SCOPE: 32, CLAUSE: 15\n\nT105 is ground\nX197 is free\nX198 is free\nzero(T105) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
380 [label="380: ','(p(T108, X197), ','(p(0, X198), less(X197, X198)))\n\nT108 is ground\nX197 is free\nX198 is free\nzero(T108) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
381 [label="381: ','(p(T108, X197), ','(p(0, X198), less(X197, X198))), SCOPE: 36, CLAUSE: 9 | ','(p(T108, X197), ','(p(0, X198), less(X197, X198))), SCOPE: 36, CLAUSE: 10\n\nT108 is ground\nX197 is free\nX198 is free\nzero(T108) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: ','(p(T108, X197), ','(p(0, X198), less(X197, X198))), SCOPE: 36, CLAUSE: 10\n\nT108 is ground\nX197 is free\nX198 is free\nzero(T108) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
384 [label="384: ','(p(0, X198), less(T111, X198))\n\nT111 is ground\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
388 [label="388: ','(p(0, X198), less(T111, X198)), SCOPE: 37, CLAUSE: 9 | ','(p(0, X198), less(T111, X198)), SCOPE: 37, CLAUSE: 10\n\nT111 is ground\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: ','(p(0, X198), less(T111, X198)), SCOPE: 37, CLAUSE: 9\n\nT111 is ground\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
390 [label="390: ','(p(0, X198), less(T111, X198)), SCOPE: 37, CLAUSE: 10\n\nT111 is ground\nX198 is free", fontsize=16, style=filled, fillcolor=lightyellow];
391 [label="391: less(T111, 0)\n\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
392 [label="392: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
393 [label="393: less(T99, T114)\n\nT99 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
394 [label="394: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
395 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 395 [arrowhead = none ];
395 -> 6;

396 [label="EVAL with clause\nordered([]).\nand substitutionT1 -> []", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 396 [arrowhead = none ];
396 -> 10;

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

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

399 [label="EVAL with clause\nordered(.(X21, [])).\nand substitutionX21 -> T3,\nT1 -> .(T3, [])", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 399 [arrowhead = none ];
399 -> 65;

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

401 [label="BACKTRACK\nfor clause: ordered(.(X1, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 401 [arrowhead = none ];
401 -> 18;

402 [label="ONLY EVAL with clause\nordered(X10) :- ','(no(max1el_list(X10)), ','(head(X10, X11), ','(tail(X10, X12), ','(head(X12, X13), ','(tail(X12, X14), ','(less(X11, s(X13)), ordered(.(X13, X14)))))))).\nand substitutionX10 -> []", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 402 [arrowhead = none ];
402 -> 32;

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

404 [label="ONLY EVAL with clause\nno(X17) :- ','(call(X17), ','(!_2, failure(a))).\nand substitutionX17 -> max1el_list([])", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 404 [arrowhead = none ];
404 -> 50;

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

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

407 [label="ONLY EVAL with clause\nmax1el_list([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 407 [arrowhead = none ];
407 -> 55;

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

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

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

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

412 [label="ONLY EVAL with clause\nordered(X37) :- ','(no(max1el_list(X37)), ','(head(X37, X38), ','(tail(X37, X39), ','(head(X39, X40), ','(tail(X39, X41), ','(less(X38, s(X40)), ordered(.(X40, X41)))))))).\nand substitutionT1 -> T13,\nX37 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 412 [arrowhead = none ];
412 -> 93;

413 [label="ONLY EVAL with clause\nordered(X23) :- ','(no(max1el_list(X23)), ','(head(X23, X24), ','(tail(X23, X25), ','(head(X25, X26), ','(tail(X25, X27), ','(less(X24, s(X26)), ordered(.(X26, X27)))))))).\nand substitutionT3 -> T5,\nX23 -> .(T5, [])", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 413 [arrowhead = none ];
413 -> 72;

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

415 [label="ONLY EVAL with clause\nno(X30) :- ','(call(X30), ','(!_6, failure(a))).\nand substitutionT5 -> T8,\nX30 -> max1el_list(.(T8, []))", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 415 [arrowhead = none ];
415 -> 78;

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

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

418 [label="BACKTRACK\nfor clause: max1el_list([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 418 [arrowhead = none ];
418 -> 83;

419 [label="ONLY EVAL with clause\nmax1el_list(.(X33, [])).\nand substitutionT8 -> T11,\nX33 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 419 [arrowhead = none ];
419 -> 85;

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

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

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

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

424 [label="ONLY EVAL with clause\nno(X44) :- ','(call(X44), ','(!_10, failure(a))).\nand substitutionT13 -> T16,\nX44 -> max1el_list(T16)", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 424 [arrowhead = none ];
424 -> 97;

425 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
97 -> 425 [arrowhead = none ];
425 -> 100;

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

427 [label="BACKTRACK\nfor clause: max1el_list([])\nwith clash: (ordered(T16), ordered([]))", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 427 [arrowhead = none ];
427 -> 106;

428 [label="BACKTRACK\nfor clause: max1el_list(.(X6, []))\nwith clash: (ordered(T16), ordered(.(X21, [])))", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 428 [arrowhead = none ];
428 -> 107;

429 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 429 [arrowhead = none ];
429 -> 109;

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

431 [label="ONLY EVAL with clause\nno(X50).\nand substitutionT16 -> T20,\nX50 -> max1el_list(T20)", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 431 [arrowhead = none ];
431 -> 115;

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

433 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(T20), ordered([]))", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 433 [arrowhead = none ];
433 -> 117;

434 [label="EVAL with clause\nhead(.(X59, X60), X59).\nand substitutionX59 -> T25,\nX60 -> T26,\nT20 -> .(T25, T26),\nX38 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 434 [arrowhead = none ];
434 -> 119;

435 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 435 [arrowhead = none ];
435 -> 120;

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

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

438 [label="ONLY EVAL with clause\ntail(.(X73, X74), X74).\nand substitutionT25 -> T31,\nX73 -> T31,\nT26 -> T32,\nX74 -> T32,\nX39 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 438 [arrowhead = none ];
438 -> 130;

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

440 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(.(T31, T32)), ordered(.(X21, [])))", fontsize=14, style = filled, fillcolor = lightgreen];
133 -> 440 [arrowhead = none ];
440 -> 134;

441 [label="EVAL with clause\nhead(.(X85, X86), X85).\nand substitutionX85 -> T37,\nX86 -> T38,\nT32 -> .(T37, T38),\nX40 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 441 [arrowhead = none ];
441 -> 135;

442 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 442 [arrowhead = none ];
442 -> 137;

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

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

445 [label="ONLY EVAL with clause\ntail(.(X95, X96), X96).\nand substitutionT37 -> T47,\nX95 -> T47,\nT38 -> T48,\nX96 -> T48,\nX41 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 445 [arrowhead = none ];
445 -> 143;

446 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
143 -> 446 [arrowhead = none ];
446 -> 148;

447 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT47 is ground", fontsize=14, style = filled, fillcolor = violet];
143 -> 447 [arrowhead = none ];
447 -> 150;

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

449 [label="INSTANCE with matching:\nT1 -> .(T47, T48)", fontsize=14, style = filled, fillcolor = lightgrey];
150 -> 449 [arrowhead = none , style=dashed];
449 -> 3[style=dashed];

450 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
153 -> 450 [arrowhead = none ];
450 -> 155;

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

452 [label="EVAL with clause\nless(0, s(X105)).\nand substitutionT31 -> 0,\nT47 -> T57,\nX105 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 452 [arrowhead = none ];
452 -> 159;

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

454 [label="ONLY EVAL with clause\nless(X114, X115) :- ','(no(zero(X114)), ','(p(X114, X116), ','(p(X115, X117), less(X116, X117)))).\nand substitutionT31 -> T62,\nX114 -> T62,\nT47 -> T63,\nX115 -> s(T63)", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 454 [arrowhead = none ];
454 -> 192;

455 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
159 -> 455 [arrowhead = none ];
455 -> 163;

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

457 [label="ONLY EVAL with clause\nno(X122) :- ','(call(X122), ','(!_18, failure(a))).\nand substitutionT62 -> T66,\nX122 -> zero(T66)", fontsize=14, style = filled, fillcolor = lightblue];
193 -> 457 [arrowhead = none ];
457 -> 195;

458 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
195 -> 458 [arrowhead = none ];
458 -> 196;

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

460 [label="EVAL with clause\nzero(0).\nand substitutionT66 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 460 [arrowhead = none ];
460 -> 198;

461 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 461 [arrowhead = none ];
461 -> 200;

462 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
198 -> 462 [arrowhead = none ];
462 -> 201;

463 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 463 [arrowhead = none ];
463 -> 224;

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

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

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

467 [label="ONLY EVAL with clause\nno(X129).\nand substitutionT66 -> T69,\nX129 -> zero(T69)", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 467 [arrowhead = none ];
467 -> 230;

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

469 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T69), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
232 -> 469 [arrowhead = none ];
469 -> 235;

470 [label="EVAL with clause\np(s(X134), X134).\nand substitutionX134 -> T72,\nT69 -> s(T72),\nX116 -> T72", fontsize=14, style = filled, fillcolor = lightblue];
235 -> 470 [arrowhead = none ];
470 -> 238;

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

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

473 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
241 -> 473 [arrowhead = none ];
473 -> 242;

474 [label="ONLY EVAL with clause\np(s(X143), X143).\nand substitutionT63 -> T77,\nX143 -> T77,\nX117 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
242 -> 474 [arrowhead = none ];
474 -> 245;

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

476 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
249 -> 476 [arrowhead = none ];
476 -> 252;

477 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
249 -> 477 [arrowhead = none ];
477 -> 253;

478 [label="EVAL with clause\nless(0, s(X150)).\nand substitutionT72 -> 0,\nX150 -> T84,\nT77 -> s(T84)", fontsize=14, style = filled, fillcolor = lightblue];
252 -> 478 [arrowhead = none ];
478 -> 256;

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

480 [label="ONLY EVAL with clause\nless(X159, X160) :- ','(no(zero(X159)), ','(p(X159, X161), ','(p(X160, X162), less(X161, X162)))).\nand substitutionT72 -> T89,\nX159 -> T89,\nT77 -> T90,\nX160 -> T90", fontsize=14, style = filled, fillcolor = lightblue];
253 -> 480 [arrowhead = none ];
480 -> 286;

481 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
256 -> 481 [arrowhead = none ];
481 -> 258;

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

483 [label="ONLY EVAL with clause\nno(X167) :- ','(call(X167), ','(!_25, failure(a))).\nand substitutionT89 -> T93,\nX167 -> zero(T93)", fontsize=14, style = filled, fillcolor = lightblue];
288 -> 483 [arrowhead = none ];
483 -> 291;

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

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

486 [label="EVAL with clause\nzero(0).\nand substitutionT93 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
293 -> 486 [arrowhead = none ];
486 -> 295;

487 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
293 -> 487 [arrowhead = none ];
487 -> 296;

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

489 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
296 -> 489 [arrowhead = none ];
489 -> 327;

490 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
297 -> 490 [arrowhead = none ];
490 -> 324;

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

492 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
327 -> 492 [arrowhead = none ];
492 -> 330;

493 [label="ONLY EVAL with clause\nno(X174).\nand substitutionT93 -> T96,\nX174 -> zero(T96)", fontsize=14, style = filled, fillcolor = lightblue];
330 -> 493 [arrowhead = none ];
493 -> 333;

494 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
333 -> 494 [arrowhead = none ];
494 -> 334;

495 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T96), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
334 -> 495 [arrowhead = none ];
495 -> 335;

496 [label="EVAL with clause\np(s(X179), X179).\nand substitutionX179 -> T99,\nT96 -> s(T99),\nX161 -> T99", fontsize=14, style = filled, fillcolor = lightblue];
335 -> 496 [arrowhead = none ];
496 -> 338;

497 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
335 -> 497 [arrowhead = none ];
497 -> 339;

498 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
338 -> 498 [arrowhead = none ];
498 -> 340;

499 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
340 -> 499 [arrowhead = none ];
499 -> 341;

500 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
340 -> 500 [arrowhead = none ];
500 -> 342;

501 [label="EVAL with clause\np(0, 0).\nand substitutionT90 -> 0,\nX162 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
341 -> 501 [arrowhead = none ];
501 -> 343;

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

503 [label="EVAL with clause\np(s(X229), X229).\nand substitutionX229 -> T114,\nT90 -> s(T114),\nX162 -> T114", fontsize=14, style = filled, fillcolor = lightblue];
342 -> 503 [arrowhead = none ];
503 -> 393;

504 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
342 -> 504 [arrowhead = none ];
504 -> 394;

505 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
343 -> 505 [arrowhead = none ];
505 -> 349;

506 [label="BACKTRACK\nfor clause: less(0, s(X5))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
349 -> 506 [arrowhead = none ];
506 -> 351;

507 [label="ONLY EVAL with clause\nless(X195, X196) :- ','(no(zero(X195)), ','(p(X195, X197), ','(p(X196, X198), less(X197, X198)))).\nand substitutionT99 -> T102,\nX195 -> T102,\nX196 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
351 -> 507 [arrowhead = none ];
507 -> 359;

508 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
359 -> 508 [arrowhead = none ];
508 -> 361;

509 [label="ONLY EVAL with clause\nno(X203) :- ','(call(X203), ','(!_32, failure(a))).\nand substitutionT102 -> T105,\nX203 -> zero(T105)", fontsize=14, style = filled, fillcolor = lightblue];
361 -> 509 [arrowhead = none ];
509 -> 364;

510 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
364 -> 510 [arrowhead = none ];
510 -> 365;

511 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
365 -> 511 [arrowhead = none ];
511 -> 366;

512 [label="EVAL with clause\nzero(0).\nand substitutionT105 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
366 -> 512 [arrowhead = none ];
512 -> 369;

513 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
366 -> 513 [arrowhead = none ];
513 -> 370;

514 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
369 -> 514 [arrowhead = none ];
514 -> 371;

515 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
370 -> 515 [arrowhead = none ];
515 -> 375;

516 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
371 -> 516 [arrowhead = none ];
516 -> 373;

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

518 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
375 -> 518 [arrowhead = none ];
518 -> 376;

519 [label="ONLY EVAL with clause\nno(X210).\nand substitutionT105 -> T108,\nX210 -> zero(T108)", fontsize=14, style = filled, fillcolor = lightblue];
376 -> 519 [arrowhead = none ];
519 -> 380;

520 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
380 -> 520 [arrowhead = none ];
520 -> 381;

521 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T108), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
381 -> 521 [arrowhead = none ];
521 -> 382;

522 [label="EVAL with clause\np(s(X215), X215).\nand substitutionX215 -> T111,\nT108 -> s(T111),\nX197 -> T111", fontsize=14, style = filled, fillcolor = lightblue];
382 -> 522 [arrowhead = none ];
522 -> 384;

523 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
382 -> 523 [arrowhead = none ];
523 -> 387;

524 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
384 -> 524 [arrowhead = none ];
524 -> 388;

525 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
388 -> 525 [arrowhead = none ];
525 -> 389;

526 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
388 -> 526 [arrowhead = none ];
526 -> 390;

527 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX198 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
389 -> 527 [arrowhead = none ];
527 -> 391;

528 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
390 -> 528 [arrowhead = none ];
528 -> 392;

529 [label="INSTANCE with matching:\nT99 -> T111", fontsize=14, style = filled, fillcolor = lightgrey];
391 -> 529 [arrowhead = none , style=dashed];
529 -> 343[style=dashed];

530 [label="INSTANCE with matching:\nT72 -> T99\nT77 -> T114", fontsize=14, style = filled, fillcolor = lightgrey];
393 -> 530 [arrowhead = none , style=dashed];
530 -> 245[style=dashed];

}

(2) Obligation:

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

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T31, .(T47, T48))) → U1_g(T31, T47, T48, pB_in_ggg(T31, T47, T48))
pB_in_ggg(T31, T47, T48) → U6_ggg(T31, T47, T48, lessE_in_gg(T31, T47))
lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
U6_ggg(T31, T47, T48, lessE_out_gg(T31, T47)) → U7_ggg(T31, T47, T48, orderedA_in_g(.(T47, T48)))
U7_ggg(T31, T47, T48, orderedA_out_g(.(T47, T48))) → pB_out_ggg(T31, T47, T48)
U1_g(T31, T47, T48, pB_out_ggg(T31, T47, T48)) → orderedA_out_g(.(T31, .(T47, T48)))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

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

ORDEREDA_IN_G(.(T31, .(T47, T48))) → U1_G(T31, T47, T48, pB_in_ggg(T31, T47, T48))
ORDEREDA_IN_G(.(T31, .(T47, T48))) → PB_IN_GGG(T31, T47, T48)
PB_IN_GGG(T31, T47, T48) → U6_GGG(T31, T47, T48, lessE_in_gg(T31, T47))
PB_IN_GGG(T31, T47, T48) → LESSE_IN_GG(T31, T47)
LESSE_IN_GG(s(T72), T77) → U5_GG(T72, T77, lessD_in_gg(T72, T77))
LESSE_IN_GG(s(T72), T77) → LESSD_IN_GG(T72, T77)
LESSD_IN_GG(s(T99), 0) → U3_GG(T99, lessC_in_g(T99))
LESSD_IN_GG(s(T99), 0) → LESSC_IN_G(T99)
LESSC_IN_G(s(T111)) → U2_G(T111, lessC_in_g(T111))
LESSC_IN_G(s(T111)) → LESSC_IN_G(T111)
LESSD_IN_GG(s(T99), s(T114)) → U4_GG(T99, T114, lessD_in_gg(T99, T114))
LESSD_IN_GG(s(T99), s(T114)) → LESSD_IN_GG(T99, T114)
U6_GGG(T31, T47, T48, lessE_out_gg(T31, T47)) → U7_GGG(T31, T47, T48, orderedA_in_g(.(T47, T48)))
U6_GGG(T31, T47, T48, lessE_out_gg(T31, T47)) → ORDEREDA_IN_G(.(T47, T48))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T31, .(T47, T48))) → U1_g(T31, T47, T48, pB_in_ggg(T31, T47, T48))
pB_in_ggg(T31, T47, T48) → U6_ggg(T31, T47, T48, lessE_in_gg(T31, T47))
lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
U6_ggg(T31, T47, T48, lessE_out_gg(T31, T47)) → U7_ggg(T31, T47, T48, orderedA_in_g(.(T47, T48)))
U7_ggg(T31, T47, T48, orderedA_out_g(.(T47, T48))) → pB_out_ggg(T31, T47, T48)
U1_g(T31, T47, T48, pB_out_ggg(T31, T47, T48)) → orderedA_out_g(.(T31, .(T47, T48)))

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

(4) Obligation:

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

ORDEREDA_IN_G(.(T31, .(T47, T48))) → U1_G(T31, T47, T48, pB_in_ggg(T31, T47, T48))
ORDEREDA_IN_G(.(T31, .(T47, T48))) → PB_IN_GGG(T31, T47, T48)
PB_IN_GGG(T31, T47, T48) → U6_GGG(T31, T47, T48, lessE_in_gg(T31, T47))
PB_IN_GGG(T31, T47, T48) → LESSE_IN_GG(T31, T47)
LESSE_IN_GG(s(T72), T77) → U5_GG(T72, T77, lessD_in_gg(T72, T77))
LESSE_IN_GG(s(T72), T77) → LESSD_IN_GG(T72, T77)
LESSD_IN_GG(s(T99), 0) → U3_GG(T99, lessC_in_g(T99))
LESSD_IN_GG(s(T99), 0) → LESSC_IN_G(T99)
LESSC_IN_G(s(T111)) → U2_G(T111, lessC_in_g(T111))
LESSC_IN_G(s(T111)) → LESSC_IN_G(T111)
LESSD_IN_GG(s(T99), s(T114)) → U4_GG(T99, T114, lessD_in_gg(T99, T114))
LESSD_IN_GG(s(T99), s(T114)) → LESSD_IN_GG(T99, T114)
U6_GGG(T31, T47, T48, lessE_out_gg(T31, T47)) → U7_GGG(T31, T47, T48, orderedA_in_g(.(T47, T48)))
U6_GGG(T31, T47, T48, lessE_out_gg(T31, T47)) → ORDEREDA_IN_G(.(T47, T48))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T31, .(T47, T48))) → U1_g(T31, T47, T48, pB_in_ggg(T31, T47, T48))
pB_in_ggg(T31, T47, T48) → U6_ggg(T31, T47, T48, lessE_in_gg(T31, T47))
lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
U6_ggg(T31, T47, T48, lessE_out_gg(T31, T47)) → U7_ggg(T31, T47, T48, orderedA_in_g(.(T47, T48)))
U7_ggg(T31, T47, T48, orderedA_out_g(.(T47, T48))) → pB_out_ggg(T31, T47, T48)
U1_g(T31, T47, T48, pB_out_ggg(T31, T47, T48)) → orderedA_out_g(.(T31, .(T47, T48)))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LESSC_IN_G(s(T111)) → LESSC_IN_G(T111)

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T31, .(T47, T48))) → U1_g(T31, T47, T48, pB_in_ggg(T31, T47, T48))
pB_in_ggg(T31, T47, T48) → U6_ggg(T31, T47, T48, lessE_in_gg(T31, T47))
lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
U6_ggg(T31, T47, T48, lessE_out_gg(T31, T47)) → U7_ggg(T31, T47, T48, orderedA_in_g(.(T47, T48)))
U7_ggg(T31, T47, T48, orderedA_out_g(.(T47, T48))) → pB_out_ggg(T31, T47, T48)
U1_g(T31, T47, T48, pB_out_ggg(T31, T47, T48)) → orderedA_out_g(.(T31, .(T47, T48)))

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

LESSC_IN_G(s(T111)) → LESSC_IN_G(T111)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

LESSC_IN_G(s(T111)) → LESSC_IN_G(T111)

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

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

LESSC_IN_G(s(T111)) → LESSC_IN_G(T111)
The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

LESSD_IN_GG(s(T99), s(T114)) → LESSD_IN_GG(T99, T114)

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T31, .(T47, T48))) → U1_g(T31, T47, T48, pB_in_ggg(T31, T47, T48))
pB_in_ggg(T31, T47, T48) → U6_ggg(T31, T47, T48, lessE_in_gg(T31, T47))
lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
U6_ggg(T31, T47, T48, lessE_out_gg(T31, T47)) → U7_ggg(T31, T47, T48, orderedA_in_g(.(T47, T48)))
U7_ggg(T31, T47, T48, orderedA_out_g(.(T47, T48))) → pB_out_ggg(T31, T47, T48)
U1_g(T31, T47, T48, pB_out_ggg(T31, T47, T48)) → orderedA_out_g(.(T31, .(T47, T48)))

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

LESSD_IN_GG(s(T99), s(T114)) → LESSD_IN_GG(T99, T114)

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

LESSD_IN_GG(s(T99), s(T114)) → LESSD_IN_GG(T99, T114)

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

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

LESSD_IN_GG(s(T99), s(T114)) → LESSD_IN_GG(T99, T114)
The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

ORDEREDA_IN_G(.(T31, .(T47, T48))) → PB_IN_GGG(T31, T47, T48)
PB_IN_GGG(T31, T47, T48) → U6_GGG(T31, T47, T48, lessE_in_gg(T31, T47))
U6_GGG(T31, T47, T48, lessE_out_gg(T31, T47)) → ORDEREDA_IN_G(.(T47, T48))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T31, .(T47, T48))) → U1_g(T31, T47, T48, pB_in_ggg(T31, T47, T48))
pB_in_ggg(T31, T47, T48) → U6_ggg(T31, T47, T48, lessE_in_gg(T31, T47))
lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
U6_ggg(T31, T47, T48, lessE_out_gg(T31, T47)) → U7_ggg(T31, T47, T48, orderedA_in_g(.(T47, T48)))
U7_ggg(T31, T47, T48, orderedA_out_g(.(T47, T48))) → pB_out_ggg(T31, T47, T48)
U1_g(T31, T47, T48, pB_out_ggg(T31, T47, T48)) → orderedA_out_g(.(T31, .(T47, T48)))

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

ORDEREDA_IN_G(.(T31, .(T47, T48))) → PB_IN_GGG(T31, T47, T48)
PB_IN_GGG(T31, T47, T48) → U6_GGG(T31, T47, T48, lessE_in_gg(T31, T47))
U6_GGG(T31, T47, T48, lessE_out_gg(T31, T47)) → ORDEREDA_IN_G(.(T47, T48))

The TRS R consists of the following rules:

lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))

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

(24) PiDPToQDPProof (EQUIVALENT transformation)

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

(25) Obligation:

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

ORDEREDA_IN_G(.(T31, .(T47, T48))) → PB_IN_GGG(T31, T47, T48)
PB_IN_GGG(T31, T47, T48) → U6_GGG(T31, T47, T48, lessE_in_gg(T31, T47))
U6_GGG(T31, T47, T48, lessE_out_gg(T31, T47)) → ORDEREDA_IN_G(.(T47, T48))

The TRS R consists of the following rules:

lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))

The set Q consists of the following terms:

lessE_in_gg(x0, x1)
U5_gg(x0, x1, x2)
lessD_in_gg(x0, x1)
U3_gg(x0, x1)
U4_gg(x0, x1, x2)
lessC_in_g(x0)
U2_g(x0, x1)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

ORDEREDA_IN_G(.(T31, .(T47, T48))) → PB_IN_GGG(T31, T47, T48)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(0) = 0
POL(ORDEREDA_IN_G(x₁)) = x₁
POL(PB_IN_GGG(x₁, x₂, x₃)) = 1 + x₃
POL(U2_g(x₁, x₂)) = 0
POL(U3_gg(x₁, x₂)) = 0
POL(U4_gg(x₁, x₂, x₃)) = 0
POL(U5_gg(x₁, x₂, x₃)) = 0
POL(U6_GGG(x₁, x₂, x₃, x₄)) = 1 + x₃
POL(lessC_in_g(x₁)) = 0
POL(lessC_out_g(x₁)) = 0
POL(lessD_in_gg(x₁, x₂)) = 0
POL(lessD_out_gg(x₁, x₂)) = 0
POL(lessE_in_gg(x₁, x₂)) = 0
POL(lessE_out_gg(x₁, x₂)) = 0
POL(s(x₁)) = 0

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(27) Obligation:

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

PB_IN_GGG(T31, T47, T48) → U6_GGG(T31, T47, T48, lessE_in_gg(T31, T47))
U6_GGG(T31, T47, T48, lessE_out_gg(T31, T47)) → ORDEREDA_IN_G(.(T47, T48))

The TRS R consists of the following rules:

lessE_in_gg(0, T57) → lessE_out_gg(0, T57)
lessE_in_gg(s(T72), T77) → U5_gg(T72, T77, lessD_in_gg(T72, T77))
U5_gg(T72, T77, lessD_out_gg(T72, T77)) → lessE_out_gg(s(T72), T77)
lessD_in_gg(0, s(T84)) → lessD_out_gg(0, s(T84))
lessD_in_gg(s(T99), 0) → U3_gg(T99, lessC_in_g(T99))
lessD_in_gg(s(T99), s(T114)) → U4_gg(T99, T114, lessD_in_gg(T99, T114))
U3_gg(T99, lessC_out_g(T99)) → lessD_out_gg(s(T99), 0)
U4_gg(T99, T114, lessD_out_gg(T99, T114)) → lessD_out_gg(s(T99), s(T114))
lessC_in_g(s(T111)) → U2_g(T111, lessC_in_g(T111))
U2_g(T111, lessC_out_g(T111)) → lessC_out_g(s(T111))

The set Q consists of the following terms:

lessE_in_gg(x0, x1)
U5_gg(x0, x1, x2)
lessD_in_gg(x0, x1)
U3_gg(x0, x1)
U4_gg(x0, x1, x2)
lessC_in_g(x0)
U2_g(x0, x1)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (EQUIVALENT transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) TRUE