Runtime Complexity proof of /tmp/tmpFT6dV5/ordered3.pl

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

0 Prolog

↳1 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 278 ms)

↳2 CdtProblem

    ↳3 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳4 CdtProblem

    ↳5 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 500 ms)

    ↳8 CdtProblem

    ↳9 CdtKnowledgeProof (⇔, 0 ms)

    ↳10 CdtProblem

    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 166 ms)

    ↳12 CdtProblem

    ↳13 CdtKnowledgeProof (⇔, 0 ms)

    ↳14 BOUNDS(O(1), O(1))

↳15 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 253 ms)

↳16 CdtProblem

    ↳17 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 411 ms)

    ↳22 CdtProblem

    ↳23 CdtKnowledgeProof (⇔, 0 ms)

    ↳24 CdtProblem

(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) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: 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];
6 [label="6: true | ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: 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];
10 [label="10: ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(no(max1el_list([])), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21))))))))\n\nX18 is free\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(no(max1el_list([])), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))), SCOPE: 2, CLAUSE: 14 | ','(no(max1el_list([])), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))), SCOPE: 2, CLAUSE: 15\n\nX18 is free\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(','(call(max1el_list([])), ','(!_2, failure(a))), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))) | ','(no(max1el_list([])), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))), SCOPE: 2, CLAUSE: 15\n\nX18 is free\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(max1el_list([]), ','(','(!_2, failure(a)), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21))))))))) | ?_3 | ','(no(max1el_list([])), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))), SCOPE: 2, CLAUSE: 15\n\nX18 is free\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(max1el_list([]), ','(','(!_2, failure(a)), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21))))))))), SCOPE: 4, CLAUSE: 11 | ','(max1el_list([]), ','(','(!_2, failure(a)), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21))))))))), SCOPE: 4, CLAUSE: 12 | ?_4 | ?_3 | ','(no(max1el_list([])), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))), SCOPE: 2, CLAUSE: 15\n\nX18 is free\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(','(!_2, failure(a)), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))) | ','(max1el_list([]), ','(','(!_2, failure(a)), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21))))))))), SCOPE: 4, CLAUSE: 12 | ?_4 | ?_3 | ','(no(max1el_list([])), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))), SCOPE: 2, CLAUSE: 15\n\nX18 is free\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(failure(a), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21))))))))\n\nX18 is free\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(failure(a), ','(head([], X18), ','(tail([], X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))), SCOPE: 5, CLAUSE: 16\n\nX18 is free\nX19 is free\nX20 is free\nX21 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: true | ordered(.(T4, [])), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX31 is free\nordered(T1) !=? ordered([])\nordered(T1) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ordered(.(T4, [])), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(no(max1el_list(.(T7, []))), ','(head(.(T7, []), X41), ','(tail(.(T7, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44))))))))\n\nT7 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(no(max1el_list(.(T7, []))), ','(head(.(T7, []), X41), ','(tail(.(T7, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))), SCOPE: 6, CLAUSE: 14 | ','(no(max1el_list(.(T7, []))), ','(head(.(T7, []), X41), ','(tail(.(T7, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))), SCOPE: 6, CLAUSE: 15\n\nT7 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(','(call(max1el_list(.(T10, []))), ','(!_6, failure(a))), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))) | ','(no(max1el_list(.(T10, []))), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))), SCOPE: 6, CLAUSE: 15\n\nT10 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(max1el_list(.(T10, [])), ','(','(!_6, failure(a)), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44))))))))) | ?_7 | ','(no(max1el_list(.(T10, []))), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))), SCOPE: 6, CLAUSE: 15\n\nT10 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(max1el_list(.(T10, [])), ','(','(!_6, failure(a)), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44))))))))), SCOPE: 8, CLAUSE: 11 | ','(max1el_list(.(T10, [])), ','(','(!_6, failure(a)), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44))))))))), SCOPE: 8, CLAUSE: 12 | ?_8 | ?_7 | ','(no(max1el_list(.(T10, []))), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))), SCOPE: 6, CLAUSE: 15\n\nT10 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(max1el_list(.(T10, [])), ','(','(!_6, failure(a)), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44))))))))), SCOPE: 8, CLAUSE: 12 | ?_8 | ?_7 | ','(no(max1el_list(.(T10, []))), ','(head(.(T10, []), X41), ','(tail(.(T10, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))), SCOPE: 6, CLAUSE: 15\n\nT10 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(','(!_6, failure(a)), ','(head(.(T13, []), X41), ','(tail(.(T13, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))) | ?_8 | ?_7 | ','(no(max1el_list(.(T13, []))), ','(head(.(T13, []), X41), ','(tail(.(T13, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))), SCOPE: 6, CLAUSE: 15\n\nT13 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(failure(a), ','(head(.(T13, []), X41), ','(tail(.(T13, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44))))))))\n\nT13 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(failure(a), ','(head(.(T13, []), X41), ','(tail(.(T13, []), X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))), SCOPE: 9, CLAUSE: 16\n\nT13 is ground\nX41 is free\nX42 is free\nX43 is free\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(no(max1el_list(T16)), ','(head(T16, X64), ','(tail(T16, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67))))))))\n\nT16 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(no(max1el_list(T16)), ','(head(T16, X64), ','(tail(T16, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 14 | ','(no(max1el_list(T16)), ','(head(T16, X64), ','(tail(T16, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 15\n\nT16 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T16) !=? ordered([])\nordered(T16) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(','(call(max1el_list(T19)), ','(!_10, failure(a))), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))) | ','(no(max1el_list(T19)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 15\n\nT19 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T19) !=? ordered([])\nordered(T19) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(max1el_list(T19), ','(','(!_10, failure(a)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67))))))))) | ?_11 | ','(no(max1el_list(T19)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 15\n\nT19 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T19) !=? ordered([])\nordered(T19) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(max1el_list(T19), ','(','(!_10, failure(a)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67))))))))), SCOPE: 12, CLAUSE: 11 | ','(max1el_list(T19), ','(','(!_10, failure(a)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67))))))))), SCOPE: 12, CLAUSE: 12 | ?_12 | ?_11 | ','(no(max1el_list(T19)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 15\n\nT19 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T19) !=? ordered([])\nordered(T19) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(max1el_list(T19), ','(','(!_10, failure(a)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67))))))))), SCOPE: 12, CLAUSE: 12 | ?_12 | ?_11 | ','(no(max1el_list(T19)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 15\n\nT19 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T19) !=? ordered([])\nordered(T19) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ?_12 | ?_11 | ','(no(max1el_list(T19)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 15\n\nT19 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T19) !=? ordered([])\nordered(T19) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ?_11 | ','(no(max1el_list(T19)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 15\n\nT19 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T19) !=? ordered([])\nordered(T19) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(no(max1el_list(T19)), ','(head(T19, X64), ','(tail(T19, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))), SCOPE: 10, CLAUSE: 15\n\nT19 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T19) !=? ordered([])\nordered(T19) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(head(T23, X64), ','(tail(T23, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))\n\nT23 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T23) !=? ordered([])\nordered(T23) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(head(T23, X64), ','(tail(T23, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67))))))), SCOPE: 13, CLAUSE: 3 | ','(head(T23, X64), ','(tail(T23, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67))))))), SCOPE: 13, CLAUSE: 4\n\nT23 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T23) !=? ordered([])\nordered(T23) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(head(T23, X64), ','(tail(T23, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67))))))), SCOPE: 13, CLAUSE: 4\n\nT23 is ground\nX31 is free\nX64 is free\nX65 is free\nX66 is free\nX67 is free\nordered(T23) !=? ordered([])\nordered(T23) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(tail(.(T28, T29), X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(T28, s(X66)), ordered(.(X66, X67))))))\n\nT28 is ground\nT29 is ground\nX31 is free\nX65 is free\nX66 is free\nX67 is free\nordered(.(T28, T29)) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(tail(.(T28, T29), X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(T28, s(X66)), ordered(.(X66, X67)))))), SCOPE: 14, CLAUSE: 5 | ','(tail(.(T28, T29), X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(T28, s(X66)), ordered(.(X66, X67)))))), SCOPE: 14, CLAUSE: 6\n\nT28 is ground\nT29 is ground\nX31 is free\nX65 is free\nX66 is free\nX67 is free\nordered(.(T28, T29)) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(tail(.(T28, T29), X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(T28, s(X66)), ordered(.(X66, X67)))))), SCOPE: 14, CLAUSE: 6\n\nT28 is ground\nT29 is ground\nX31 is free\nX65 is free\nX66 is free\nX67 is free\nordered(.(T28, T29)) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(head(T35, X66), ','(tail(T35, X67), ','(less(T34, s(X66)), ordered(.(X66, X67)))))\n\nT34 is ground\nT35 is ground\nX31 is free\nX66 is free\nX67 is free\nordered(.(T34, T35)) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(head(T35, X66), ','(tail(T35, X67), ','(less(T34, s(X66)), ordered(.(X66, X67))))), SCOPE: 15, CLAUSE: 3 | ','(head(T35, X66), ','(tail(T35, X67), ','(less(T34, s(X66)), ordered(.(X66, X67))))), SCOPE: 15, CLAUSE: 4\n\nT34 is ground\nT35 is ground\nX31 is free\nX66 is free\nX67 is free\nordered(.(T34, T35)) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(head(T35, X66), ','(tail(T35, X67), ','(less(T34, s(X66)), ordered(.(X66, X67))))), SCOPE: 15, CLAUSE: 4\n\nT34 is ground\nT35 is ground\nX31 is free\nX66 is free\nX67 is free\nordered(.(T34, T35)) !=? ordered(.(X31, []))", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(tail(.(T40, T41), X67), ','(less(T34, s(T40)), ordered(.(T40, X67))))\n\nT34 is ground\nT40 is ground\nT41 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(tail(.(T40, T41), X67), ','(less(T34, s(T40)), ordered(.(T40, X67)))), SCOPE: 16, CLAUSE: 5 | ','(tail(.(T40, T41), X67), ','(less(T34, s(T40)), ordered(.(T40, X67)))), SCOPE: 16, CLAUSE: 6\n\nT34 is ground\nT40 is ground\nT41 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(tail(.(T40, T41), X67), ','(less(T34, s(T40)), ordered(.(T40, X67)))), SCOPE: 16, CLAUSE: 6\n\nT34 is ground\nT40 is ground\nT41 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(less(T34, s(T50)), ordered(.(T50, T51)))\n\nT34 is ground\nT50 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: less(T34, s(T50))\n\nT34 is ground\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ordered(.(T50, T51))\n\nT50 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: less(T34, s(T50)), SCOPE: 17, CLAUSE: 7 | less(T34, s(T50)), SCOPE: 17, CLAUSE: 8\n\nT34 is ground\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: true | less(0, s(T58)), SCOPE: 17, CLAUSE: 8\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: less(T34, s(T50)), SCOPE: 17, CLAUSE: 8\n\nT34 is ground\nT50 is ground\nX131 is free\nless(T34, s(T50)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: less(0, s(T58)), SCOPE: 17, CLAUSE: 8\n\nT58 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(no(zero(0)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143))))\n\nT61 is ground\nX142 is free\nX143 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(no(zero(0)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))), SCOPE: 18, CLAUSE: 14 | ','(no(zero(0)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))), SCOPE: 18, CLAUSE: 15\n\nT61 is ground\nX142 is free\nX143 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(','(call(zero(0)), ','(!_18, failure(a))), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))) | ','(no(zero(0)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))), SCOPE: 18, CLAUSE: 15\n\nT61 is ground\nX142 is free\nX143 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(zero(0), ','(','(!_18, failure(a)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143))))) | ?_19 | ','(no(zero(0)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))), SCOPE: 18, CLAUSE: 15\n\nT61 is ground\nX142 is free\nX143 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(zero(0), ','(','(!_18, failure(a)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143))))), SCOPE: 20, CLAUSE: 13 | ?_20 | ?_19 | ','(no(zero(0)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))), SCOPE: 18, CLAUSE: 15\n\nT61 is ground\nX142 is free\nX143 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(','(!_18, failure(a)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))) | ?_20 | ?_19 | ','(no(zero(0)), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))), SCOPE: 18, CLAUSE: 15\n\nT61 is ground\nX142 is free\nX143 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(failure(a), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143))))\n\nT61 is ground\nX142 is free\nX143 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(failure(a), ','(p(0, X142), ','(p(s(T61), X143), less(X142, X143)))), SCOPE: 21, CLAUSE: 16\n\nT61 is ground\nX142 is free\nX143 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(no(zero(T66)), ','(p(T66, X161), ','(p(s(T67), X162), less(X161, X162))))\n\nT66 is ground\nT67 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T66, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(no(zero(T66)), ','(p(T66, X161), ','(p(s(T67), X162), less(X161, X162)))), SCOPE: 22, CLAUSE: 14 | ','(no(zero(T66)), ','(p(T66, X161), ','(p(s(T67), X162), less(X161, X162)))), SCOPE: 22, CLAUSE: 15\n\nT66 is ground\nT67 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T66, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(','(call(zero(T70)), ','(!_22, failure(a))), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162)))) | ','(no(zero(T70)), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162)))), SCOPE: 22, CLAUSE: 15\n\nT67 is ground\nT70 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T70, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(zero(T70), ','(','(!_22, failure(a)), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162))))) | ?_23 | ','(no(zero(T70)), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162)))), SCOPE: 22, CLAUSE: 15\n\nT67 is ground\nT70 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T70, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(zero(T70), ','(','(!_22, failure(a)), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162))))), SCOPE: 24, CLAUSE: 13 | ?_24 | ?_23 | ','(no(zero(T70)), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162)))), SCOPE: 22, CLAUSE: 15\n\nT67 is ground\nT70 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T70, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ?_24 | ?_23 | ','(no(zero(T70)), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162)))), SCOPE: 22, CLAUSE: 15\n\nT67 is ground\nT70 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T70, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ?_23 | ','(no(zero(T70)), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162)))), SCOPE: 22, CLAUSE: 15\n\nT67 is ground\nT70 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T70, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(no(zero(T70)), ','(p(T70, X161), ','(p(s(T67), X162), less(X161, X162)))), SCOPE: 22, CLAUSE: 15\n\nT67 is ground\nT70 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T70, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(p(T73, X161), ','(p(s(T67), X162), less(X161, X162)))\n\nT67 is ground\nT73 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T73, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(p(T73, X161), ','(p(s(T67), X162), less(X161, X162))), SCOPE: 25, CLAUSE: 9 | ','(p(T73, X161), ','(p(s(T67), X162), less(X161, X162))), SCOPE: 25, CLAUSE: 10\n\nT67 is ground\nT73 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T73, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(p(T73, X161), ','(p(s(T67), X162), less(X161, X162))), SCOPE: 25, CLAUSE: 10\n\nT67 is ground\nT73 is ground\nX131 is free\nX161 is free\nX162 is free\nless(T73, s(T67)) !=? less(0, s(X131))", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(p(s(T67), X162), less(T76, X162))\n\nT67 is ground\nT76 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(p(s(T67), X162), less(T76, X162)), SCOPE: 26, CLAUSE: 9 | ','(p(s(T67), X162), less(T76, X162)), SCOPE: 26, CLAUSE: 10\n\nT67 is ground\nT76 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ','(p(s(T67), X162), less(T76, X162)), SCOPE: 26, CLAUSE: 10\n\nT67 is ground\nT76 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: less(T76, T81)\n\nT76 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: less(T76, T81), SCOPE: 27, CLAUSE: 7 | less(T76, T81), SCOPE: 27, CLAUSE: 8\n\nT76 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: true | less(0, s(T86)), SCOPE: 27, CLAUSE: 8\n\nT86 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: less(T76, T81), SCOPE: 27, CLAUSE: 8\n\nT76 is ground\nT81 is ground\nX191 is free\nless(T76, T81) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: less(0, s(T86)), SCOPE: 27, CLAUSE: 8\n\nT86 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ','(no(zero(0)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203))))\n\nT89 is ground\nX202 is free\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(no(zero(0)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))), SCOPE: 28, CLAUSE: 14 | ','(no(zero(0)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))), SCOPE: 28, CLAUSE: 15\n\nT89 is ground\nX202 is free\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: ','(','(call(zero(0)), ','(!_28, failure(a))), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))) | ','(no(zero(0)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))), SCOPE: 28, CLAUSE: 15\n\nT89 is ground\nX202 is free\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ','(zero(0), ','(','(!_28, failure(a)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203))))) | ?_29 | ','(no(zero(0)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))), SCOPE: 28, CLAUSE: 15\n\nT89 is ground\nX202 is free\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(zero(0), ','(','(!_28, failure(a)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203))))), SCOPE: 30, CLAUSE: 13 | ?_30 | ?_29 | ','(no(zero(0)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))), SCOPE: 28, CLAUSE: 15\n\nT89 is ground\nX202 is free\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(','(!_28, failure(a)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))) | ?_30 | ?_29 | ','(no(zero(0)), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))), SCOPE: 28, CLAUSE: 15\n\nT89 is ground\nX202 is free\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(failure(a), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203))))\n\nT89 is ground\nX202 is free\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ','(failure(a), ','(p(0, X202), ','(p(s(T89), X203), less(X202, X203)))), SCOPE: 31, CLAUSE: 16\n\nT89 is ground\nX202 is free\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(no(zero(T94)), ','(p(T94, X221), ','(p(T95, X222), less(X221, X222))))\n\nT94 is ground\nT95 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T94, T95) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(no(zero(T94)), ','(p(T94, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 14 | ','(no(zero(T94)), ','(p(T94, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 15\n\nT94 is ground\nT95 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T94, T95) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(','(call(zero(T98)), ','(!_32, failure(a))), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222)))) | ','(no(zero(T98)), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 15\n\nT95 is ground\nT98 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T98, T95) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(zero(T98), ','(','(!_32, failure(a)), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222))))) | ?_33 | ','(no(zero(T98)), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 15\n\nT95 is ground\nT98 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T98, T95) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ','(zero(T98), ','(','(!_32, failure(a)), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222))))), SCOPE: 34, CLAUSE: 13 | ?_34 | ?_33 | ','(no(zero(T98)), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 15\n\nT95 is ground\nT98 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T98, T95) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ','(','(!_32, failure(a)), ','(p(0, X221), ','(p(T95, X222), less(X221, X222)))) | ?_34 | ?_33 | ','(no(zero(0)), ','(p(0, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 15\n\nT95 is ground\nX191 is free\nX221 is free\nX222 is free\nless(0, T95) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ?_34 | ?_33 | ','(no(zero(T98)), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 15\n\nT95 is ground\nT98 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T98, T95) !=? less(0, s(X191))\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ','(failure(a), ','(p(0, X221), ','(p(T95, X222), less(X221, X222))))\n\nT95 is ground\nX191 is free\nX221 is free\nX222 is free\nless(0, T95) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(failure(a), ','(p(0, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 35, CLAUSE: 16\n\nT95 is ground\nX191 is free\nX221 is free\nX222 is free\nless(0, T95) !=? less(0, s(X191))", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: ?_33 | ','(no(zero(T98)), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 15\n\nT95 is ground\nT98 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T98, T95) !=? less(0, s(X191))\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: ','(no(zero(T98)), ','(p(T98, X221), ','(p(T95, X222), less(X221, X222)))), SCOPE: 32, CLAUSE: 15\n\nT95 is ground\nT98 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T98, T95) !=? less(0, s(X191))\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: ','(p(T101, X221), ','(p(T95, X222), less(X221, X222)))\n\nT95 is ground\nT101 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T101, T95) !=? less(0, s(X191))\nzero(T101) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: ','(p(T101, X221), ','(p(T95, X222), less(X221, X222))), SCOPE: 36, CLAUSE: 9 | ','(p(T101, X221), ','(p(T95, X222), less(X221, X222))), SCOPE: 36, CLAUSE: 10\n\nT95 is ground\nT101 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T101, T95) !=? less(0, s(X191))\nzero(T101) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(p(T101, X221), ','(p(T95, X222), less(X221, X222))), SCOPE: 36, CLAUSE: 10\n\nT95 is ground\nT101 is ground\nX191 is free\nX221 is free\nX222 is free\nless(T101, T95) !=? less(0, s(X191))\nzero(T101) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(p(T95, X222), less(T104, X222))\n\nT95 is ground\nT104 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: ','(p(T95, X222), less(T104, X222)), SCOPE: 37, CLAUSE: 9 | ','(p(T95, X222), less(T104, X222)), SCOPE: 37, CLAUSE: 10\n\nT95 is ground\nT104 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: less(T104, 0) | ','(p(0, X222), less(T104, X222)), SCOPE: 37, CLAUSE: 10\n\nT104 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: ','(p(T95, X222), less(T104, X222)), SCOPE: 37, CLAUSE: 10\n\nT95 is ground\nT104 is ground\nX222 is free\np(T95, X222) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: less(T104, 0)\n\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: ','(p(0, X222), less(T104, X222)), SCOPE: 37, CLAUSE: 10\n\nT104 is ground\nX222 is free", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: less(T104, 0), SCOPE: 38, CLAUSE: 7 | less(T104, 0), SCOPE: 38, CLAUSE: 8\n\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: less(T104, 0), SCOPE: 38, CLAUSE: 8\n\nT104 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: ','(no(zero(T107)), ','(p(T107, X259), ','(p(0, X260), less(X259, X260))))\n\nT107 is ground\nX259 is free\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: ','(no(zero(T107)), ','(p(T107, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 14 | ','(no(zero(T107)), ','(p(T107, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 15\n\nT107 is ground\nX259 is free\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: ','(','(call(zero(T110)), ','(!_39, failure(a))), ','(p(T110, X259), ','(p(0, X260), less(X259, X260)))) | ','(no(zero(T110)), ','(p(T110, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 15\n\nT110 is ground\nX259 is free\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: ','(zero(T110), ','(','(!_39, failure(a)), ','(p(T110, X259), ','(p(0, X260), less(X259, X260))))) | ?_40 | ','(no(zero(T110)), ','(p(T110, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 15\n\nT110 is ground\nX259 is free\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: ','(zero(T110), ','(','(!_39, failure(a)), ','(p(T110, X259), ','(p(0, X260), less(X259, X260))))), SCOPE: 41, CLAUSE: 13 | ?_41 | ?_40 | ','(no(zero(T110)), ','(p(T110, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 15\n\nT110 is ground\nX259 is free\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: ','(','(!_39, failure(a)), ','(p(0, X259), ','(p(0, X260), less(X259, X260)))) | ?_41 | ?_40 | ','(no(zero(0)), ','(p(0, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 15\n\nX259 is free\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: ?_41 | ?_40 | ','(no(zero(T110)), ','(p(T110, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 15\n\nT110 is ground\nX259 is free\nX260 is free\nzero(T110) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: ','(failure(a), ','(p(0, X259), ','(p(0, X260), less(X259, X260))))\n\nX259 is free\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: ','(failure(a), ','(p(0, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 42, CLAUSE: 16\n\nX259 is free\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: ?_40 | ','(no(zero(T110)), ','(p(T110, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 15\n\nT110 is ground\nX259 is free\nX260 is free\nzero(T110) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: ','(no(zero(T110)), ','(p(T110, X259), ','(p(0, X260), less(X259, X260)))), SCOPE: 39, CLAUSE: 15\n\nT110 is ground\nX259 is free\nX260 is free\nzero(T110) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: ','(p(T113, X259), ','(p(0, X260), less(X259, X260)))\n\nT113 is ground\nX259 is free\nX260 is free\nzero(T113) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(p(T113, X259), ','(p(0, X260), less(X259, X260))), SCOPE: 43, CLAUSE: 9 | ','(p(T113, X259), ','(p(0, X260), less(X259, X260))), SCOPE: 43, CLAUSE: 10\n\nT113 is ground\nX259 is free\nX260 is free\nzero(T113) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: ','(p(T113, X259), ','(p(0, X260), less(X259, X260))), SCOPE: 43, CLAUSE: 10\n\nT113 is ground\nX259 is free\nX260 is free\nzero(T113) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: ','(p(0, X260), less(T116, X260))\n\nT116 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: ','(p(0, X260), less(T116, X260)), SCOPE: 44, CLAUSE: 9 | ','(p(0, X260), less(T116, X260)), SCOPE: 44, CLAUSE: 10\n\nT116 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: less(T116, 0) | ','(p(0, X260), less(T116, X260)), SCOPE: 44, CLAUSE: 10\n\nT116 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: less(T116, 0)\n\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: ','(p(0, X260), less(T116, X260)), SCOPE: 44, CLAUSE: 10\n\nT116 is ground\nX260 is free", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: less(T104, T119)\n\nT104 is ground\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 287 [arrowhead = none ];
287 -> 4;

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

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

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

291 [label="EVAL with clause\nordered(.(X31, [])).\nand substitutionX31 -> T4,\nT1 -> .(T4, [])", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 291 [arrowhead = none ];
291 -> 32;

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

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

294 [label="ONLY EVAL with clause\nordered(X17) :- ','(no(max1el_list(X17)), ','(head(X17, X18), ','(tail(X17, X19), ','(head(X19, X20), ','(tail(X19, X21), ','(less(X18, s(X20)), ordered(.(X20, X21)))))))).\nand substitutionX17 -> []", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 294 [arrowhead = none ];
294 -> 15;

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

296 [label="ONLY EVAL with clause\nno(X26) :- ','(call(X26), ','(!_2, failure(a))).\nand substitutionX26 -> max1el_list([])", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 296 [arrowhead = none ];
296 -> 19;

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

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

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

300 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 300 [arrowhead = none ];
300 -> 26;

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

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

303 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 303 [arrowhead = none ];
303 -> 36;

304 [label="ONLY EVAL with clause\nordered(X63) :- ','(no(max1el_list(X63)), ','(head(X63, X64), ','(tail(X63, X65), ','(head(X65, X66), ','(tail(X65, X67), ','(less(X64, s(X66)), ordered(.(X66, X67)))))))).\nand substitutionT1 -> T16,\nX63 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 304 [arrowhead = none ];
304 -> 63;

305 [label="ONLY EVAL with clause\nordered(X40) :- ','(no(max1el_list(X40)), ','(head(X40, X41), ','(tail(X40, X42), ','(head(X42, X43), ','(tail(X42, X44), ','(less(X41, s(X43)), ordered(.(X43, X44)))))))).\nand substitutionT4 -> T7,\nX40 -> .(T7, [])", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 305 [arrowhead = none ];
305 -> 39;

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

307 [label="ONLY EVAL with clause\nno(X49) :- ','(call(X49), ','(!_6, failure(a))).\nand substitutionT7 -> T10,\nX49 -> max1el_list(.(T10, []))", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 307 [arrowhead = none ];
307 -> 45;

308 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 308 [arrowhead = none ];
308 -> 46;

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

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

311 [label="ONLY EVAL with clause\nmax1el_list(.(X52, [])).\nand substitutionT10 -> T13,\nX52 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 311 [arrowhead = none ];
311 -> 53;

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

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

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

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

316 [label="ONLY EVAL with clause\nno(X72) :- ','(call(X72), ','(!_10, failure(a))).\nand substitutionT16 -> T19,\nX72 -> max1el_list(T19)", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 316 [arrowhead = none ];
316 -> 68;

317 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 317 [arrowhead = none ];
317 -> 70;

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

319 [label="BACKTRACK\nfor clause: max1el_list([])\nwith clash: (ordered(T19), ordered([]))", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 319 [arrowhead = none ];
319 -> 73;

320 [label="BACKTRACK\nfor clause: max1el_list(.(X6, []))\nwith clash: (ordered(T19), ordered(.(X31, [])))", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 320 [arrowhead = none ];
320 -> 75;

321 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 321 [arrowhead = none ];
321 -> 76;

322 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 322 [arrowhead = none ];
322 -> 77;

323 [label="ONLY EVAL with clause\nno(X78).\nand substitutionT19 -> T23,\nX78 -> max1el_list(T23)", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 323 [arrowhead = none ];
323 -> 80;

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

325 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(T23), ordered([]))", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 325 [arrowhead = none ];
325 -> 84;

326 [label="EVAL with clause\nhead(.(X87, X88), X87).\nand substitutionX87 -> T28,\nX88 -> T29,\nT23 -> .(T28, T29),\nX64 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 326 [arrowhead = none ];
326 -> 85;

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

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

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

330 [label="ONLY EVAL with clause\ntail(.(X101, X102), X102).\nand substitutionT28 -> T34,\nX101 -> T34,\nT29 -> T35,\nX102 -> T35,\nX65 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 330 [arrowhead = none ];
330 -> 94;

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

332 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(.(T34, T35)), ordered(.(X31, [])))", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 332 [arrowhead = none ];
332 -> 98;

333 [label="EVAL with clause\nhead(.(X113, X114), X113).\nand substitutionX113 -> T40,\nX114 -> T41,\nT35 -> .(T40, T41),\nX66 -> T40", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 333 [arrowhead = none ];
333 -> 100;

334 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 334 [arrowhead = none ];
334 -> 101;

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

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

337 [label="ONLY EVAL with clause\ntail(.(X123, X124), X124).\nand substitutionT40 -> T50,\nX123 -> T50,\nT41 -> T51,\nX124 -> T51,\nX67 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 337 [arrowhead = none ];
337 -> 104;

338 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
104 -> 338 [arrowhead = none ];
338 -> 105;

339 [label="SPLIT 2\nnew knowledge:\nT34 is ground\nT50 is ground", fontsize=14, style = filled, fillcolor = violet];
104 -> 339 [arrowhead = none ];
339 -> 107;

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

341 [label="INSTANCE with matching:\nT1 -> .(T50, T51)", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 341 [arrowhead = none , style=dashed];
341 -> 1[style=dashed];

342 [label="EVAL with clause\nless(0, s(X131)).\nand substitutionT34 -> 0,\nT50 -> T58,\nX131 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 342 [arrowhead = none ];
342 -> 111;

343 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 343 [arrowhead = none ];
343 -> 113;

344 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 344 [arrowhead = none ];
344 -> 115;

345 [label="ONLY EVAL with clause\nless(X159, X160) :- ','(no(zero(X159)), ','(p(X159, X161), ','(p(X160, X162), less(X161, X162)))).\nand substitutionT34 -> T66,\nX159 -> T66,\nT50 -> T67,\nX160 -> s(T67)", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 345 [arrowhead = none ];
345 -> 135;

346 [label="ONLY EVAL with clause\nless(X140, X141) :- ','(no(zero(X140)), ','(p(X140, X142), ','(p(X141, X143), less(X142, X143)))).\nand substitutionX140 -> 0,\nT58 -> T61,\nX141 -> s(T61)", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 346 [arrowhead = none ];
346 -> 117;

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

348 [label="ONLY EVAL with clause\nno(X148) :- ','(call(X148), ','(!_18, failure(a))).\nand substitutionX148 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 348 [arrowhead = none ];
348 -> 121;

349 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
121 -> 349 [arrowhead = none ];
349 -> 123;

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

351 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 351 [arrowhead = none ];
351 -> 127;

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

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

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

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

356 [label="ONLY EVAL with clause\nno(X167) :- ','(call(X167), ','(!_22, failure(a))).\nand substitutionT66 -> T70,\nX167 -> zero(T70)", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 356 [arrowhead = none ];
356 -> 137;

357 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
137 -> 357 [arrowhead = none ];
357 -> 138;

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

359 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (less(T70, s(T67)), less(0, s(X131)))", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 359 [arrowhead = none ];
359 -> 140;

360 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 360 [arrowhead = none ];
360 -> 141;

361 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 361 [arrowhead = none ];
361 -> 142;

362 [label="ONLY EVAL with clause\nno(X172).\nand substitutionT70 -> T73,\nX172 -> zero(T73)", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 362 [arrowhead = none ];
362 -> 143;

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

364 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T73, s(T67)), less(0, s(X131)))", fontsize=14, style = filled, fillcolor = lightgreen];
144 -> 364 [arrowhead = none ];
364 -> 146;

365 [label="EVAL with clause\np(s(X177), X177).\nand substitutionX177 -> T76,\nT73 -> s(T76),\nX161 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 365 [arrowhead = none ];
365 -> 148;

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

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

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

369 [label="ONLY EVAL with clause\np(s(X186), X186).\nand substitutionT67 -> T81,\nX186 -> T81,\nX162 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
152 -> 369 [arrowhead = none ];
369 -> 158;

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

371 [label="EVAL with clause\nless(0, s(X191)).\nand substitutionT76 -> 0,\nX191 -> T86,\nT81 -> s(T86)", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 371 [arrowhead = none ];
371 -> 163;

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

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

374 [label="ONLY EVAL with clause\nless(X219, X220) :- ','(no(zero(X219)), ','(p(X219, X221), ','(p(X220, X222), less(X221, X222)))).\nand substitutionT76 -> T94,\nX219 -> T94,\nT81 -> T95,\nX220 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 374 [arrowhead = none ];
374 -> 186;

375 [label="ONLY EVAL with clause\nless(X200, X201) :- ','(no(zero(X200)), ','(p(X200, X202), ','(p(X201, X203), less(X202, X203)))).\nand substitutionX200 -> 0,\nT86 -> T89,\nX201 -> s(T89)", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 375 [arrowhead = none ];
375 -> 171;

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

377 [label="ONLY EVAL with clause\nno(X208) :- ','(call(X208), ','(!_28, failure(a))).\nand substitutionX208 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 377 [arrowhead = none ];
377 -> 173;

378 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
173 -> 378 [arrowhead = none ];
378 -> 175;

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

380 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 380 [arrowhead = none ];
380 -> 177;

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

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

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

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

385 [label="ONLY EVAL with clause\nno(X227) :- ','(call(X227), ','(!_32, failure(a))).\nand substitutionT94 -> T98,\nX227 -> zero(T98)", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 385 [arrowhead = none ];
385 -> 193;

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

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

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

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

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

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

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

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

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

395 [label="ONLY EVAL with clause\nno(X234).\nand substitutionT98 -> T101,\nX234 -> zero(T101)", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 395 [arrowhead = none ];
395 -> 207;

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

397 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T101), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
208 -> 397 [arrowhead = none ];
397 -> 210;

398 [label="EVAL with clause\np(s(X239), X239).\nand substitutionX239 -> T104,\nT101 -> s(T104),\nX221 -> T104", fontsize=14, style = filled, fillcolor = lightblue];
210 -> 398 [arrowhead = none ];
398 -> 215;

399 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
210 -> 399 [arrowhead = none ];
399 -> 217;

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

401 [label="EVAL with clause\np(0, 0).\nand substitutionT95 -> 0,\nX222 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
220 -> 401 [arrowhead = none ];
401 -> 223;

402 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
220 -> 402 [arrowhead = none ];
402 -> 224;

403 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
223 -> 403 [arrowhead = none ];
403 -> 228;

404 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
223 -> 404 [arrowhead = none ];
404 -> 229;

405 [label="EVAL with clause\np(s(X292), X292).\nand substitutionX292 -> T119,\nT95 -> s(T119),\nX222 -> T119", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 405 [arrowhead = none ];
405 -> 285;

406 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
224 -> 406 [arrowhead = none ];
406 -> 286;

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

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

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

410 [label="ONLY EVAL with clause\nless(X257, X258) :- ','(no(zero(X257)), ','(p(X257, X259), ','(p(X258, X260), less(X259, X260)))).\nand substitutionT104 -> T107,\nX257 -> T107,\nX258 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
236 -> 410 [arrowhead = none ];
410 -> 239;

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

412 [label="ONLY EVAL with clause\nno(X265) :- ','(call(X265), ','(!_39, failure(a))).\nand substitutionT107 -> T110,\nX265 -> zero(T110)", fontsize=14, style = filled, fillcolor = lightblue];
242 -> 412 [arrowhead = none ];
412 -> 243;

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

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

415 [label="EVAL with clause\nzero(0).\nand substitutionT110 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
245 -> 415 [arrowhead = none ];
415 -> 246;

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

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

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

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

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

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

422 [label="ONLY EVAL with clause\nno(X272).\nand substitutionT110 -> T113,\nX272 -> zero(T113)", fontsize=14, style = filled, fillcolor = lightblue];
253 -> 422 [arrowhead = none ];
422 -> 256;

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

424 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T113), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
261 -> 424 [arrowhead = none ];
424 -> 262;

425 [label="EVAL with clause\np(s(X277), X277).\nand substitutionX277 -> T116,\nT113 -> s(T116),\nX259 -> T116", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 425 [arrowhead = none ];
425 -> 268;

426 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
262 -> 426 [arrowhead = none ];
426 -> 269;

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

428 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX260 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
270 -> 428 [arrowhead = none ];
428 -> 272;

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

430 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
272 -> 430 [arrowhead = none ];
430 -> 278;

431 [label="INSTANCE with matching:\nT104 -> T116", fontsize=14, style = filled, fillcolor = lightgrey];
277 -> 431 [arrowhead = none , style=dashed];
431 -> 228[style=dashed];

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

433 [label="INSTANCE with matching:\nT76 -> T104\nT81 -> T119", fontsize=14, style = filled, fillcolor = lightgrey];
285 -> 433 [arrowhead = none , style=dashed];
433 -> 158[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f104_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f104_out1, .(z0, .(z1, z2))) → f1_out1
f158_in(0, s(z0)) → f158_out1
f158_in(s(z0), 0) → U2(f223_in(z0), s(z0), 0)
f158_in(s(z0), s(z1)) → U3(f158_in(z0, z1), s(z0), s(z1))
U2(f223_out1, s(z0), 0) → f158_out1
U2(f223_out2(z0), s(z1), 0) → f158_out1
U3(f158_out1, s(z0), s(z1)) → f158_out1
f228_in(s(z0)) → U4(f272_in(z0), s(z0))
U4(f272_out1, s(z0)) → f228_out1
U4(f272_out2(z0), s(z1)) → f228_out1
f105_in(0, z0) → f105_out1
f105_in(s(z0), z1) → U5(f158_in(z0, z1), s(z0), z1)
U5(f158_out1, s(z0), z1) → f105_out1
f104_in(z0, z1, z2) → U6(f105_in(z0, z1), z0, z1, z2)
U6(f105_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f104_out1
f223_in(z0) → U8(f228_in(z0), f229_in(z0), z0)
U8(f228_out1, z0, z1) → f223_out1
U8(z0, f229_out1(z1), z2) → f223_out2(z1)
f272_in(z0) → U9(f228_in(z0), f278_in(z0), z0)
U9(f228_out1, z0, z1) → f272_out1
U9(z0, f278_out1(z1), z2) → f272_out2(z1)

Tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f104_in(z0, z1, z2), .(z0, .(z1, z2))), F104_IN(z0, z1, z2))
F158_IN(s(z0), 0) → c5(U2'(f223_in(z0), s(z0), 0), F223_IN(z0))
F158_IN(s(z0), s(z1)) → c6(U3'(f158_in(z0, z1), s(z0), s(z1)), F158_IN(z0, z1))
F228_IN(s(z0)) → c10(U4'(f272_in(z0), s(z0)), F272_IN(z0))
F105_IN(s(z0), z1) → c14(U5'(f158_in(z0, z1), s(z0), z1), F158_IN(z0, z1))
F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
U6'(f105_out1, z0, z1, z2) → c17(U7'(f1_in(.(z1, z2)), z0, z1, z2), F1_IN(.(z1, z2)))
F223_IN(z0) → c19(U8'(f228_in(z0), f229_in(z0), z0), F228_IN(z0))
F272_IN(z0) → c22(U9'(f228_in(z0), f278_in(z0), z0), F228_IN(z0))

S tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f104_in(z0, z1, z2), .(z0, .(z1, z2))), F104_IN(z0, z1, z2))
F158_IN(s(z0), 0) → c5(U2'(f223_in(z0), s(z0), 0), F223_IN(z0))
F158_IN(s(z0), s(z1)) → c6(U3'(f158_in(z0, z1), s(z0), s(z1)), F158_IN(z0, z1))
F228_IN(s(z0)) → c10(U4'(f272_in(z0), s(z0)), F272_IN(z0))
F105_IN(s(z0), z1) → c14(U5'(f158_in(z0, z1), s(z0), z1), F158_IN(z0, z1))
F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
U6'(f105_out1, z0, z1, z2) → c17(U7'(f1_in(.(z1, z2)), z0, z1, z2), F1_IN(.(z1, z2)))
F223_IN(z0) → c19(U8'(f228_in(z0), f229_in(z0), z0), F228_IN(z0))
F272_IN(z0) → c22(U9'(f228_in(z0), f278_in(z0), z0), F228_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f158_in, U2, U3, f228_in, U4, f105_in, U5, f104_in, U6, U7, f223_in, U8, f272_in, U9

Defined Pair Symbols:

F1_IN, F158_IN, F228_IN, F105_IN, F104_IN, U6', F223_IN, F272_IN

Compound Symbols:

c2, c5, c6, c10, c14, c16, c17, c19, c22

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f104_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f104_out1, .(z0, .(z1, z2))) → f1_out1
f158_in(0, s(z0)) → f158_out1
f158_in(s(z0), 0) → U2(f223_in(z0), s(z0), 0)
f158_in(s(z0), s(z1)) → U3(f158_in(z0, z1), s(z0), s(z1))
U2(f223_out1, s(z0), 0) → f158_out1
U2(f223_out2(z0), s(z1), 0) → f158_out1
U3(f158_out1, s(z0), s(z1)) → f158_out1
f228_in(s(z0)) → U4(f272_in(z0), s(z0))
U4(f272_out1, s(z0)) → f228_out1
U4(f272_out2(z0), s(z1)) → f228_out1
f105_in(0, z0) → f105_out1
f105_in(s(z0), z1) → U5(f158_in(z0, z1), s(z0), z1)
U5(f158_out1, s(z0), z1) → f105_out1
f104_in(z0, z1, z2) → U6(f105_in(z0, z1), z0, z1, z2)
U6(f105_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f104_out1
f223_in(z0) → U8(f228_in(z0), f229_in(z0), z0)
U8(f228_out1, z0, z1) → f223_out1
U8(z0, f229_out1(z1), z2) → f223_out2(z1)
f272_in(z0) → U9(f228_in(z0), f278_in(z0), z0)
U9(f228_out1, z0, z1) → f272_out1
U9(z0, f278_out1(z1), z2) → f272_out2(z1)

Tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f104_in(z0, z1, z2), .(z0, .(z1, z2))), F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(U3'(f158_in(z0, z1), s(z0), s(z1)), F158_IN(z0, z1))
F228_IN(s(z0)) → c10(U4'(f272_in(z0), s(z0)), F272_IN(z0))
F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
U6'(f105_out1, z0, z1, z2) → c17(U7'(f1_in(.(z1, z2)), z0, z1, z2), F1_IN(.(z1, z2)))
F272_IN(z0) → c22(U9'(f228_in(z0), f278_in(z0), z0), F228_IN(z0))
F158_IN(s(z0), 0) → c(U2'(f223_in(z0), s(z0), 0))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(U5'(f158_in(z0, z1), s(z0), z1))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(U8'(f228_in(z0), f229_in(z0), z0))
F223_IN(z0) → c(F228_IN(z0))

S tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f104_in(z0, z1, z2), .(z0, .(z1, z2))), F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(U3'(f158_in(z0, z1), s(z0), s(z1)), F158_IN(z0, z1))
F228_IN(s(z0)) → c10(U4'(f272_in(z0), s(z0)), F272_IN(z0))
F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
U6'(f105_out1, z0, z1, z2) → c17(U7'(f1_in(.(z1, z2)), z0, z1, z2), F1_IN(.(z1, z2)))
F272_IN(z0) → c22(U9'(f228_in(z0), f278_in(z0), z0), F228_IN(z0))
F158_IN(s(z0), 0) → c(U2'(f223_in(z0), s(z0), 0))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(U5'(f158_in(z0, z1), s(z0), z1))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(U8'(f228_in(z0), f229_in(z0), z0))
F223_IN(z0) → c(F228_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f158_in, U2, U3, f228_in, U4, f105_in, U5, f104_in, U6, U7, f223_in, U8, f272_in, U9

Defined Pair Symbols:

F1_IN, F158_IN, F228_IN, F104_IN, U6', F272_IN, F105_IN, F223_IN

Compound Symbols:

c2, c6, c10, c16, c17, c22, c

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

Removed 8 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f104_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f104_out1, .(z0, .(z1, z2))) → f1_out1
f158_in(0, s(z0)) → f158_out1
f158_in(s(z0), 0) → U2(f223_in(z0), s(z0), 0)
f158_in(s(z0), s(z1)) → U3(f158_in(z0, z1), s(z0), s(z1))
U2(f223_out1, s(z0), 0) → f158_out1
U2(f223_out2(z0), s(z1), 0) → f158_out1
U3(f158_out1, s(z0), s(z1)) → f158_out1
f228_in(s(z0)) → U4(f272_in(z0), s(z0))
U4(f272_out1, s(z0)) → f228_out1
U4(f272_out2(z0), s(z1)) → f228_out1
f105_in(0, z0) → f105_out1
f105_in(s(z0), z1) → U5(f158_in(z0, z1), s(z0), z1)
U5(f158_out1, s(z0), z1) → f105_out1
f104_in(z0, z1, z2) → U6(f105_in(z0, z1), z0, z1, z2)
U6(f105_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f104_out1
f223_in(z0) → U8(f228_in(z0), f229_in(z0), z0)
U8(f228_out1, z0, z1) → f223_out1
U8(z0, f229_out1(z1), z2) → f223_out2(z1)
f272_in(z0) → U9(f228_in(z0), f278_in(z0), z0)
U9(f228_out1, z0, z1) → f272_out1
U9(z0, f278_out1(z1), z2) → f272_out2(z1)

Tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F272_IN(z0) → c22(F228_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

S tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F272_IN(z0) → c22(F228_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f158_in, U2, U3, f228_in, U4, f105_in, U5, f104_in, U6, U7, f223_in, U8, f272_in, U9

Defined Pair Symbols:

F104_IN, F158_IN, F105_IN, F223_IN, F1_IN, F228_IN, U6', F272_IN

Compound Symbols:

c16, c, c2, c6, c10, c17, c22, c

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

We considered the (Usable) Rules:

f105_in(0, z0) → f105_out1
f105_in(s(z0), z1) → U5(f158_in(z0, z1), s(z0), z1)
f158_in(0, s(z0)) → f158_out1
f158_in(s(z0), 0) → U2(f223_in(z0), s(z0), 0)
f158_in(s(z0), s(z1)) → U3(f158_in(z0, z1), s(z0), s(z1))
U5(f158_out1, s(z0), z1) → f105_out1
U3(f158_out1, s(z0), s(z1)) → f158_out1
f223_in(z0) → U8(f228_in(z0), f229_in(z0), z0)
U2(f223_out1, s(z0), 0) → f158_out1
U2(f223_out2(z0), s(z1), 0) → f158_out1
f228_in(s(z0)) → U4(f272_in(z0), s(z0))
U8(f228_out1, z0, z1) → f223_out1
f272_in(z0) → U9(f228_in(z0), f278_in(z0), z0)
U4(f272_out1, s(z0)) → f228_out1
U4(f272_out2(z0), s(z1)) → f228_out1
U9(f228_out1, z0, z1) → f272_out1

And the Tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F272_IN(z0) → c22(F228_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₁ + x₂
POL(0) = 0
POL(F104_IN(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃
POL(F105_IN(x₁, x₂)) = [1] + x₁
POL(F158_IN(x₁, x₂)) = [2] + x₁
POL(F1_IN(x₁)) = x₁
POL(F223_IN(x₁)) = [3] + x₁
POL(F228_IN(x₁)) = x₁
POL(F272_IN(x₁)) = x₁
POL(U2(x₁, x₂, x₃)) = 0
POL(U3(x₁, x₂, x₃)) = 0
POL(U4(x₁, x₂)) = [3]x₂
POL(U5(x₁, x₂, x₃)) = 0
POL(U6'(x₁, x₂, x₃, x₄)) = [1] + x₃ + x₄
POL(U8(x₁, x₂, x₃)) = 0
POL(U9(x₁, x₂, x₃)) = 0
POL(c) = 0
POL(c(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(f105_in(x₁, x₂)) = 0
POL(f105_out1) = 0
POL(f158_in(x₁, x₂)) = 0
POL(f158_out1) = 0
POL(f223_in(x₁)) = 0
POL(f223_out1) = 0
POL(f223_out2(x₁)) = 0
POL(f228_in(x₁)) = [2] + [3]x₁
POL(f228_out1) = 0
POL(f229_in(x₁)) = 0
POL(f272_in(x₁)) = 0
POL(f272_out1) = 0
POL(f272_out2(x₁)) = 0
POL(f278_in(x₁)) = 0
POL(s(x₁)) = [2] + x₁

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f104_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f104_out1, .(z0, .(z1, z2))) → f1_out1
f158_in(0, s(z0)) → f158_out1
f158_in(s(z0), 0) → U2(f223_in(z0), s(z0), 0)
f158_in(s(z0), s(z1)) → U3(f158_in(z0, z1), s(z0), s(z1))
U2(f223_out1, s(z0), 0) → f158_out1
U2(f223_out2(z0), s(z1), 0) → f158_out1
U3(f158_out1, s(z0), s(z1)) → f158_out1
f228_in(s(z0)) → U4(f272_in(z0), s(z0))
U4(f272_out1, s(z0)) → f228_out1
U4(f272_out2(z0), s(z1)) → f228_out1
f105_in(0, z0) → f105_out1
f105_in(s(z0), z1) → U5(f158_in(z0, z1), s(z0), z1)
U5(f158_out1, s(z0), z1) → f105_out1
f104_in(z0, z1, z2) → U6(f105_in(z0, z1), z0, z1, z2)
U6(f105_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f104_out1
f223_in(z0) → U8(f228_in(z0), f229_in(z0), z0)
U8(f228_out1, z0, z1) → f223_out1
U8(z0, f229_out1(z1), z2) → f223_out2(z1)
f272_in(z0) → U9(f228_in(z0), f278_in(z0), z0)
U9(f228_out1, z0, z1) → f272_out1
U9(z0, f278_out1(z1), z2) → f272_out2(z1)

Tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F272_IN(z0) → c22(F228_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

S tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F272_IN(z0) → c22(F228_IN(z0))

K tuples:

F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

Defined Rule Symbols:

f1_in, U1, f158_in, U2, U3, f228_in, U4, f105_in, U5, f104_in, U6, U7, f223_in, U8, f272_in, U9

Defined Pair Symbols:

F104_IN, F158_IN, F105_IN, F223_IN, F1_IN, F228_IN, U6', F272_IN

Compound Symbols:

c16, c, c2, c6, c10, c17, c22, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F272_IN(z0) → c22(F228_IN(z0))
F228_IN(s(z0)) → c10(F272_IN(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f104_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f104_out1, .(z0, .(z1, z2))) → f1_out1
f158_in(0, s(z0)) → f158_out1
f158_in(s(z0), 0) → U2(f223_in(z0), s(z0), 0)
f158_in(s(z0), s(z1)) → U3(f158_in(z0, z1), s(z0), s(z1))
U2(f223_out1, s(z0), 0) → f158_out1
U2(f223_out2(z0), s(z1), 0) → f158_out1
U3(f158_out1, s(z0), s(z1)) → f158_out1
f228_in(s(z0)) → U4(f272_in(z0), s(z0))
U4(f272_out1, s(z0)) → f228_out1
U4(f272_out2(z0), s(z1)) → f228_out1
f105_in(0, z0) → f105_out1
f105_in(s(z0), z1) → U5(f158_in(z0, z1), s(z0), z1)
U5(f158_out1, s(z0), z1) → f105_out1
f104_in(z0, z1, z2) → U6(f105_in(z0, z1), z0, z1, z2)
U6(f105_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f104_out1
f223_in(z0) → U8(f228_in(z0), f229_in(z0), z0)
U8(f228_out1, z0, z1) → f223_out1
U8(z0, f229_out1(z1), z2) → f223_out2(z1)
f272_in(z0) → U9(f228_in(z0), f278_in(z0), z0)
U9(f228_out1, z0, z1) → f272_out1
U9(z0, f278_out1(z1), z2) → f272_out2(z1)

Tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F272_IN(z0) → c22(F228_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

S tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))

K tuples:

F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c
F272_IN(z0) → c22(F228_IN(z0))

Defined Rule Symbols:

f1_in, U1, f158_in, U2, U3, f228_in, U4, f105_in, U5, f104_in, U6, U7, f223_in, U8, f272_in, U9

Defined Pair Symbols:

F104_IN, F158_IN, F105_IN, F223_IN, F1_IN, F228_IN, U6', F272_IN

Compound Symbols:

c16, c, c2, c6, c10, c17, c22, c

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))

We considered the (Usable) Rules:

f105_in(0, z0) → f105_out1
f105_in(s(z0), z1) → U5(f158_in(z0, z1), s(z0), z1)
f158_in(0, s(z0)) → f158_out1
f158_in(s(z0), 0) → U2(f223_in(z0), s(z0), 0)
f158_in(s(z0), s(z1)) → U3(f158_in(z0, z1), s(z0), s(z1))
U5(f158_out1, s(z0), z1) → f105_out1
U3(f158_out1, s(z0), s(z1)) → f158_out1
f223_in(z0) → U8(f228_in(z0), f229_in(z0), z0)
U2(f223_out1, s(z0), 0) → f158_out1
U2(f223_out2(z0), s(z1), 0) → f158_out1
f228_in(s(z0)) → U4(f272_in(z0), s(z0))
U8(f228_out1, z0, z1) → f223_out1
f272_in(z0) → U9(f228_in(z0), f278_in(z0), z0)
U4(f272_out1, s(z0)) → f228_out1
U4(f272_out2(z0), s(z1)) → f228_out1
U9(f228_out1, z0, z1) → f272_out1

And the Tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F272_IN(z0) → c22(F228_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₂
POL(0) = 0
POL(F104_IN(x₁, x₂, x₃)) = [1] + x₃
POL(F105_IN(x₁, x₂)) = 0
POL(F158_IN(x₁, x₂)) = 0
POL(F1_IN(x₁)) = x₁
POL(F223_IN(x₁)) = 0
POL(F228_IN(x₁)) = 0
POL(F272_IN(x₁)) = 0
POL(U2(x₁, x₂, x₃)) = 0
POL(U3(x₁, x₂, x₃)) = 0
POL(U4(x₁, x₂)) = 0
POL(U5(x₁, x₂, x₃)) = 0
POL(U6'(x₁, x₂, x₃, x₄)) = [1] + x₄
POL(U8(x₁, x₂, x₃)) = 0
POL(U9(x₁, x₂, x₃)) = x₁
POL(c) = 0
POL(c(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(f105_in(x₁, x₂)) = 0
POL(f105_out1) = 0
POL(f158_in(x₁, x₂)) = 0
POL(f158_out1) = 0
POL(f223_in(x₁)) = [3] + x₁
POL(f223_out1) = 0
POL(f223_out2(x₁)) = 0
POL(f228_in(x₁)) = [1] + x₁
POL(f228_out1) = 0
POL(f229_in(x₁)) = 0
POL(f272_in(x₁)) = [1] + [2]x₁
POL(f272_out1) = 0
POL(f272_out2(x₁)) = 0
POL(f278_in(x₁)) = 0
POL(s(x₁)) = 0

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f104_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f104_out1, .(z0, .(z1, z2))) → f1_out1
f158_in(0, s(z0)) → f158_out1
f158_in(s(z0), 0) → U2(f223_in(z0), s(z0), 0)
f158_in(s(z0), s(z1)) → U3(f158_in(z0, z1), s(z0), s(z1))
U2(f223_out1, s(z0), 0) → f158_out1
U2(f223_out2(z0), s(z1), 0) → f158_out1
U3(f158_out1, s(z0), s(z1)) → f158_out1
f228_in(s(z0)) → U4(f272_in(z0), s(z0))
U4(f272_out1, s(z0)) → f228_out1
U4(f272_out2(z0), s(z1)) → f228_out1
f105_in(0, z0) → f105_out1
f105_in(s(z0), z1) → U5(f158_in(z0, z1), s(z0), z1)
U5(f158_out1, s(z0), z1) → f105_out1
f104_in(z0, z1, z2) → U6(f105_in(z0, z1), z0, z1, z2)
U6(f105_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f104_out1
f223_in(z0) → U8(f228_in(z0), f229_in(z0), z0)
U8(f228_out1, z0, z1) → f223_out1
U8(z0, f229_out1(z1), z2) → f223_out2(z1)
f272_in(z0) → U9(f228_in(z0), f278_in(z0), z0)
U9(f228_out1, z0, z1) → f272_out1
U9(z0, f278_out1(z1), z2) → f272_out2(z1)

Tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F272_IN(z0) → c22(F228_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c

S tuples:

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))

K tuples:

F158_IN(s(z0), 0) → c(F223_IN(z0))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
F223_IN(z0) → c(F228_IN(z0))
F158_IN(s(z0), s(z1)) → c6(F158_IN(z0, z1))
F228_IN(s(z0)) → c10(F272_IN(z0))
F158_IN(s(z0), 0) → c
F105_IN(s(z0), z1) → c
F223_IN(z0) → c
F272_IN(z0) → c22(F228_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))

Defined Rule Symbols:

f1_in, U1, f158_in, U2, U3, f228_in, U4, f105_in, U5, f104_in, U6, U7, f223_in, U8, f272_in, U9

Defined Pair Symbols:

F104_IN, F158_IN, F105_IN, F223_IN, F1_IN, F228_IN, U6', F272_IN

Compound Symbols:

c16, c, c2, c6, c10, c17, c22, c

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

F104_IN(z0, z1, z2) → c16(U6'(f105_in(z0, z1), z0, z1, z2), F105_IN(z0, z1))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F105_IN(s(z0), z1) → c(F158_IN(z0, z1))
U6'(f105_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F105_IN(s(z0), z1) → c
F1_IN(.(z0, .(z1, z2))) → c2(F104_IN(z0, z1, z2))

Now S is empty

(14) BOUNDS(O(1), O(1))

(15) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: 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];
5 [label="5: true | ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: 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];
9 [label="9: ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(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];
14 [label="14: ','(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];
17 [label="17: ','(','(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];
18 [label="18: ','(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];
21 [label="21: ','(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];
23 [label="23: ','(','(!_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];
24 [label="24: ','(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];
27 [label="27: ','(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];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: true | ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: 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];
35 [label="35: ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(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];
38 [label="38: ','(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];
40 [label="40: ','(','(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];
41 [label="41: ','(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];
43 [label="43: ','(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];
44 [label="44: ','(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];
47 [label="47: ','(','(!_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];
48 [label="48: ','(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];
51 [label="51: ','(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];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(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];
56 [label="56: ','(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];
59 [label="59: ','(','(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];
60 [label="60: ','(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];
61 [label="61: ','(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];
62 [label="62: ','(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];
64 [label="64: ?_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];
65 [label="65: ?_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];
67 [label="67: ','(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];
69 [label="69: ','(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];
72 [label="72: ','(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];
74 [label="74: ','(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];
78 [label="78: ','(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];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(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];
83 [label="83: ','(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];
87 [label="87: ','(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];
89 [label="89: ','(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];
91 [label="91: ','(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];
92 [label="92: ','(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];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(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];
96 [label="96: ','(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];
99 [label="99: ','(less(T31, s(T47)), ordered(.(T47, T48)))\n\nT31 is ground\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: less(T31, s(T47))\n\nT31 is ground\nT47 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ordered(.(T47, T48))\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: 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];
112 [label="112: true | less(0, s(T55)), SCOPE: 17, CLAUSE: 8\n\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: less(T31, s(T47)), SCOPE: 17, CLAUSE: 8\n\nT31 is ground\nT47 is ground\nX103 is free\nless(T31, s(T47)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: less(0, s(T55)), SCOPE: 17, CLAUSE: 8\n\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(no(zero(0)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115))))\n\nT58 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(no(zero(0)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))), SCOPE: 18, CLAUSE: 14 | ','(no(zero(0)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))), SCOPE: 18, CLAUSE: 15\n\nT58 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(','(call(zero(0)), ','(!_18, failure(a))), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))) | ','(no(zero(0)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))), SCOPE: 18, CLAUSE: 15\n\nT58 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(zero(0), ','(','(!_18, failure(a)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115))))) | ?_19 | ','(no(zero(0)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))), SCOPE: 18, CLAUSE: 15\n\nT58 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(zero(0), ','(','(!_18, failure(a)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115))))), SCOPE: 20, CLAUSE: 13 | ?_20 | ?_19 | ','(no(zero(0)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))), SCOPE: 18, CLAUSE: 15\n\nT58 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(','(!_18, failure(a)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))) | ?_20 | ?_19 | ','(no(zero(0)), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))), SCOPE: 18, CLAUSE: 15\n\nT58 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(failure(a), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115))))\n\nT58 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(failure(a), ','(p(0, X114), ','(p(s(T58), X115), less(X114, X115)))), SCOPE: 21, CLAUSE: 16\n\nT58 is ground\nX114 is free\nX115 is free", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(no(zero(T63)), ','(p(T63, X133), ','(p(s(T64), X134), less(X133, X134))))\n\nT63 is ground\nT64 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T63, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(no(zero(T63)), ','(p(T63, X133), ','(p(s(T64), X134), less(X133, X134)))), SCOPE: 22, CLAUSE: 14 | ','(no(zero(T63)), ','(p(T63, X133), ','(p(s(T64), X134), less(X133, X134)))), SCOPE: 22, CLAUSE: 15\n\nT63 is ground\nT64 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T63, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(','(call(zero(T67)), ','(!_22, failure(a))), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134)))) | ','(no(zero(T67)), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134)))), SCOPE: 22, CLAUSE: 15\n\nT64 is ground\nT67 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T67, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(zero(T67), ','(','(!_22, failure(a)), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134))))) | ?_23 | ','(no(zero(T67)), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134)))), SCOPE: 22, CLAUSE: 15\n\nT64 is ground\nT67 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T67, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: ','(zero(T67), ','(','(!_22, failure(a)), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134))))), SCOPE: 24, CLAUSE: 13 | ?_24 | ?_23 | ','(no(zero(T67)), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134)))), SCOPE: 22, CLAUSE: 15\n\nT64 is ground\nT67 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T67, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ?_24 | ?_23 | ','(no(zero(T67)), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134)))), SCOPE: 22, CLAUSE: 15\n\nT64 is ground\nT67 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T67, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ?_23 | ','(no(zero(T67)), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134)))), SCOPE: 22, CLAUSE: 15\n\nT64 is ground\nT67 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T67, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(no(zero(T67)), ','(p(T67, X133), ','(p(s(T64), X134), less(X133, X134)))), SCOPE: 22, CLAUSE: 15\n\nT64 is ground\nT67 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T67, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: ','(p(T70, X133), ','(p(s(T64), X134), less(X133, X134)))\n\nT64 is ground\nT70 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T70, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(p(T70, X133), ','(p(s(T64), X134), less(X133, X134))), SCOPE: 25, CLAUSE: 9 | ','(p(T70, X133), ','(p(s(T64), X134), less(X133, X134))), SCOPE: 25, CLAUSE: 10\n\nT64 is ground\nT70 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T70, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: ','(p(T70, X133), ','(p(s(T64), X134), less(X133, X134))), SCOPE: 25, CLAUSE: 10\n\nT64 is ground\nT70 is ground\nX103 is free\nX133 is free\nX134 is free\nless(T70, s(T64)) !=? less(0, s(X103))", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(p(s(T64), X134), less(T73, X134))\n\nT64 is ground\nT73 is ground\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(p(s(T64), X134), less(T73, X134)), SCOPE: 26, CLAUSE: 9 | ','(p(s(T64), X134), less(T73, X134)), SCOPE: 26, CLAUSE: 10\n\nT64 is ground\nT73 is ground\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(p(s(T64), X134), less(T73, X134)), SCOPE: 26, CLAUSE: 10\n\nT64 is ground\nT73 is ground\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: less(T73, T78)\n\nT73 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: less(T73, T78), SCOPE: 27, CLAUSE: 7 | less(T73, T78), SCOPE: 27, CLAUSE: 8\n\nT73 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: true | less(0, s(T83)), SCOPE: 27, CLAUSE: 8\n\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: less(T73, T78), SCOPE: 27, CLAUSE: 8\n\nT73 is ground\nT78 is ground\nX163 is free\nless(T73, T78) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: less(0, s(T83)), SCOPE: 27, CLAUSE: 8\n\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ','(no(zero(0)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175))))\n\nT86 is ground\nX174 is free\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(no(zero(0)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))), SCOPE: 28, CLAUSE: 14 | ','(no(zero(0)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))), SCOPE: 28, CLAUSE: 15\n\nT86 is ground\nX174 is free\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(','(call(zero(0)), ','(!_28, failure(a))), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))) | ','(no(zero(0)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))), SCOPE: 28, CLAUSE: 15\n\nT86 is ground\nX174 is free\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ','(zero(0), ','(','(!_28, failure(a)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175))))) | ?_29 | ','(no(zero(0)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))), SCOPE: 28, CLAUSE: 15\n\nT86 is ground\nX174 is free\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(zero(0), ','(','(!_28, failure(a)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175))))), SCOPE: 30, CLAUSE: 13 | ?_30 | ?_29 | ','(no(zero(0)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))), SCOPE: 28, CLAUSE: 15\n\nT86 is ground\nX174 is free\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(','(!_28, failure(a)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))) | ?_30 | ?_29 | ','(no(zero(0)), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))), SCOPE: 28, CLAUSE: 15\n\nT86 is ground\nX174 is free\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(failure(a), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175))))\n\nT86 is ground\nX174 is free\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(failure(a), ','(p(0, X174), ','(p(s(T86), X175), less(X174, X175)))), SCOPE: 31, CLAUSE: 16\n\nT86 is ground\nX174 is free\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(no(zero(T91)), ','(p(T91, X193), ','(p(T92, X194), less(X193, X194))))\n\nT91 is ground\nT92 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T91, T92) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(no(zero(T91)), ','(p(T91, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 14 | ','(no(zero(T91)), ','(p(T91, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 15\n\nT91 is ground\nT92 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T91, T92) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(','(call(zero(T95)), ','(!_32, failure(a))), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194)))) | ','(no(zero(T95)), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 15\n\nT92 is ground\nT95 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T95, T92) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: ','(zero(T95), ','(','(!_32, failure(a)), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194))))) | ?_33 | ','(no(zero(T95)), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 15\n\nT92 is ground\nT95 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T95, T92) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ','(zero(T95), ','(','(!_32, failure(a)), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194))))), SCOPE: 34, CLAUSE: 13 | ?_34 | ?_33 | ','(no(zero(T95)), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 15\n\nT92 is ground\nT95 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T95, T92) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(','(!_32, failure(a)), ','(p(0, X193), ','(p(T92, X194), less(X193, X194)))) | ?_34 | ?_33 | ','(no(zero(0)), ','(p(0, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 15\n\nT92 is ground\nX163 is free\nX193 is free\nX194 is free\nless(0, T92) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ?_34 | ?_33 | ','(no(zero(T95)), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 15\n\nT92 is ground\nT95 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T95, T92) !=? less(0, s(X163))\nzero(T95) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(failure(a), ','(p(0, X193), ','(p(T92, X194), less(X193, X194))))\n\nT92 is ground\nX163 is free\nX193 is free\nX194 is free\nless(0, T92) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ','(failure(a), ','(p(0, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 35, CLAUSE: 16\n\nT92 is ground\nX163 is free\nX193 is free\nX194 is free\nless(0, T92) !=? less(0, s(X163))", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ?_33 | ','(no(zero(T95)), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 15\n\nT92 is ground\nT95 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T95, T92) !=? less(0, s(X163))\nzero(T95) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: ','(no(zero(T95)), ','(p(T95, X193), ','(p(T92, X194), less(X193, X194)))), SCOPE: 32, CLAUSE: 15\n\nT92 is ground\nT95 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T95, T92) !=? less(0, s(X163))\nzero(T95) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(p(T98, X193), ','(p(T92, X194), less(X193, X194)))\n\nT92 is ground\nT98 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T98, T92) !=? less(0, s(X163))\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: ','(p(T98, X193), ','(p(T92, X194), less(X193, X194))), SCOPE: 36, CLAUSE: 9 | ','(p(T98, X193), ','(p(T92, X194), less(X193, X194))), SCOPE: 36, CLAUSE: 10\n\nT92 is ground\nT98 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T98, T92) !=? less(0, s(X163))\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: ','(p(T98, X193), ','(p(T92, X194), less(X193, X194))), SCOPE: 36, CLAUSE: 10\n\nT92 is ground\nT98 is ground\nX163 is free\nX193 is free\nX194 is free\nless(T98, T92) !=? less(0, s(X163))\nzero(T98) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: ','(p(T92, X194), less(T101, X194))\n\nT92 is ground\nT101 is ground\nX194 is free", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(p(T92, X194), less(T101, X194)), SCOPE: 37, CLAUSE: 9 | ','(p(T92, X194), less(T101, X194)), SCOPE: 37, CLAUSE: 10\n\nT92 is ground\nT101 is ground\nX194 is free", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: less(T101, 0) | ','(p(0, X194), less(T101, X194)), SCOPE: 37, CLAUSE: 10\n\nT101 is ground\nX194 is free", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(p(T92, X194), less(T101, X194)), SCOPE: 37, CLAUSE: 10\n\nT92 is ground\nT101 is ground\nX194 is free\np(T92, X194) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: less(T101, 0)\n\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ','(p(0, X194), less(T101, X194)), SCOPE: 37, CLAUSE: 10\n\nT101 is ground\nX194 is free", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: less(T101, 0), SCOPE: 38, CLAUSE: 7 | less(T101, 0), SCOPE: 38, CLAUSE: 8\n\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: less(T101, 0), SCOPE: 38, CLAUSE: 8\n\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: ','(no(zero(T104)), ','(p(T104, X231), ','(p(0, X232), less(X231, X232))))\n\nT104 is ground\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: ','(no(zero(T104)), ','(p(T104, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 14 | ','(no(zero(T104)), ','(p(T104, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 15\n\nT104 is ground\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: ','(','(call(zero(T107)), ','(!_39, failure(a))), ','(p(T107, X231), ','(p(0, X232), less(X231, X232)))) | ','(no(zero(T107)), ','(p(T107, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 15\n\nT107 is ground\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: ','(zero(T107), ','(','(!_39, failure(a)), ','(p(T107, X231), ','(p(0, X232), less(X231, X232))))) | ?_40 | ','(no(zero(T107)), ','(p(T107, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 15\n\nT107 is ground\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: ','(zero(T107), ','(','(!_39, failure(a)), ','(p(T107, X231), ','(p(0, X232), less(X231, X232))))), SCOPE: 41, CLAUSE: 13 | ?_41 | ?_40 | ','(no(zero(T107)), ','(p(T107, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 15\n\nT107 is ground\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: ','(','(!_39, failure(a)), ','(p(0, X231), ','(p(0, X232), less(X231, X232)))) | ?_41 | ?_40 | ','(no(zero(0)), ','(p(0, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 15\n\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: ?_41 | ?_40 | ','(no(zero(T107)), ','(p(T107, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 15\n\nT107 is ground\nX231 is free\nX232 is free\nzero(T107) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: ','(failure(a), ','(p(0, X231), ','(p(0, X232), less(X231, X232))))\n\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: ','(failure(a), ','(p(0, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 42, CLAUSE: 16\n\nX231 is free\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: ?_40 | ','(no(zero(T107)), ','(p(T107, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 15\n\nT107 is ground\nX231 is free\nX232 is free\nzero(T107) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: ','(no(zero(T107)), ','(p(T107, X231), ','(p(0, X232), less(X231, X232)))), SCOPE: 39, CLAUSE: 15\n\nT107 is ground\nX231 is free\nX232 is free\nzero(T107) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: ','(p(T110, X231), ','(p(0, X232), less(X231, X232)))\n\nT110 is ground\nX231 is free\nX232 is free\nzero(T110) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: ','(p(T110, X231), ','(p(0, X232), less(X231, X232))), SCOPE: 43, CLAUSE: 9 | ','(p(T110, X231), ','(p(0, X232), less(X231, X232))), SCOPE: 43, CLAUSE: 10\n\nT110 is ground\nX231 is free\nX232 is free\nzero(T110) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: ','(p(T110, X231), ','(p(0, X232), less(X231, X232))), SCOPE: 43, CLAUSE: 10\n\nT110 is ground\nX231 is free\nX232 is free\nzero(T110) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: ','(p(0, X232), less(T113, X232))\n\nT113 is ground\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: ','(p(0, X232), less(T113, X232)), SCOPE: 44, CLAUSE: 9 | ','(p(0, X232), less(T113, X232)), SCOPE: 44, CLAUSE: 10\n\nT113 is ground\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: less(T113, 0) | ','(p(0, X232), less(T113, X232)), SCOPE: 44, CLAUSE: 10\n\nT113 is ground\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: less(T113, 0)\n\nT113 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: ','(p(0, X232), less(T113, X232)), SCOPE: 44, CLAUSE: 10\n\nT113 is ground\nX232 is free", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: less(T101, T116)\n\nT101 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 291 [arrowhead = none ];
291 -> 3;

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

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

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

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

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

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

298 [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];
12 -> 298 [arrowhead = none ];
298 -> 13;

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

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

301 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 301 [arrowhead = none ];
301 -> 18;

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

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

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

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

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

307 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 307 [arrowhead = none ];
307 -> 35;

308 [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];
33 -> 308 [arrowhead = none ];
308 -> 55;

309 [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];
35 -> 309 [arrowhead = none ];
309 -> 37;

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

311 [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];
38 -> 311 [arrowhead = none ];
311 -> 40;

312 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
40 -> 312 [arrowhead = none ];
312 -> 41;

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

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

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

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

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

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

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

320 [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];
56 -> 320 [arrowhead = none ];
320 -> 59;

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

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

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

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

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

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

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

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

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

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

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

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

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

334 [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];
83 -> 334 [arrowhead = none ];
334 -> 87;

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

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

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

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

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

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

341 [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];
96 -> 341 [arrowhead = none ];
341 -> 99;

342 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
99 -> 342 [arrowhead = none ];
342 -> 106;

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

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

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

346 [label="EVAL with clause\nless(0, s(X103)).\nand substitutionT31 -> 0,\nT47 -> T55,\nX103 -> T55", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 346 [arrowhead = none ];
346 -> 112;

347 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 347 [arrowhead = none ];
347 -> 114;

348 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 348 [arrowhead = none ];
348 -> 116;

349 [label="ONLY EVAL with clause\nless(X131, X132) :- ','(no(zero(X131)), ','(p(X131, X133), ','(p(X132, X134), less(X133, X134)))).\nand substitutionT31 -> T63,\nX131 -> T63,\nT47 -> T64,\nX132 -> s(T64)", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 349 [arrowhead = none ];
349 -> 145;

350 [label="ONLY EVAL with clause\nless(X112, X113) :- ','(no(zero(X112)), ','(p(X112, X114), ','(p(X113, X115), less(X114, X115)))).\nand substitutionX112 -> 0,\nT55 -> T58,\nX113 -> s(T58)", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 350 [arrowhead = none ];
350 -> 118;

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

352 [label="ONLY EVAL with clause\nno(X120) :- ','(call(X120), ','(!_18, failure(a))).\nand substitutionX120 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 352 [arrowhead = none ];
352 -> 122;

353 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
122 -> 353 [arrowhead = none ];
353 -> 124;

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

355 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
126 -> 355 [arrowhead = none ];
355 -> 128;

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

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

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

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

360 [label="ONLY EVAL with clause\nno(X139) :- ','(call(X139), ','(!_22, failure(a))).\nand substitutionT63 -> T67,\nX139 -> zero(T67)", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 360 [arrowhead = none ];
360 -> 150;

361 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
150 -> 361 [arrowhead = none ];
361 -> 153;

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

363 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (less(T67, s(T64)), less(0, s(X103)))", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 363 [arrowhead = none ];
363 -> 155;

364 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 364 [arrowhead = none ];
364 -> 156;

365 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
156 -> 365 [arrowhead = none ];
365 -> 157;

366 [label="ONLY EVAL with clause\nno(X144).\nand substitutionT67 -> T70,\nX144 -> zero(T70)", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 366 [arrowhead = none ];
366 -> 159;

367 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
159 -> 367 [arrowhead = none ];
367 -> 160;

368 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T70, s(T64)), less(0, s(X103)))", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 368 [arrowhead = none ];
368 -> 162;

369 [label="EVAL with clause\np(s(X149), X149).\nand substitutionX149 -> T73,\nT70 -> s(T73),\nX133 -> T73", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 369 [arrowhead = none ];
369 -> 164;

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

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

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

373 [label="ONLY EVAL with clause\np(s(X158), X158).\nand substitutionT64 -> T78,\nX158 -> T78,\nX134 -> T78", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 373 [arrowhead = none ];
373 -> 170;

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

375 [label="EVAL with clause\nless(0, s(X163)).\nand substitutionT73 -> 0,\nX163 -> T83,\nT78 -> s(T83)", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 375 [arrowhead = none ];
375 -> 178;

376 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
174 -> 376 [arrowhead = none ];
376 -> 180;

377 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
178 -> 377 [arrowhead = none ];
377 -> 181;

378 [label="ONLY EVAL with clause\nless(X191, X192) :- ','(no(zero(X191)), ','(p(X191, X193), ','(p(X192, X194), less(X193, X194)))).\nand substitutionT73 -> T91,\nX191 -> T91,\nT78 -> T92,\nX192 -> T92", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 378 [arrowhead = none ];
378 -> 205;

379 [label="ONLY EVAL with clause\nless(X172, X173) :- ','(no(zero(X172)), ','(p(X172, X174), ','(p(X173, X175), less(X174, X175)))).\nand substitutionX172 -> 0,\nT83 -> T86,\nX173 -> s(T86)", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 379 [arrowhead = none ];
379 -> 184;

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

381 [label="ONLY EVAL with clause\nno(X180) :- ','(call(X180), ','(!_28, failure(a))).\nand substitutionX180 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 381 [arrowhead = none ];
381 -> 187;

382 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
187 -> 382 [arrowhead = none ];
382 -> 188;

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

384 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 384 [arrowhead = none ];
384 -> 191;

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

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

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

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

389 [label="ONLY EVAL with clause\nno(X199) :- ','(call(X199), ','(!_32, failure(a))).\nand substitutionT91 -> T95,\nX199 -> zero(T95)", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 389 [arrowhead = none ];
389 -> 209;

390 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
209 -> 390 [arrowhead = none ];
390 -> 211;

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

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

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

394 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
213 -> 394 [arrowhead = none ];
394 -> 216;

395 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
214 -> 395 [arrowhead = none ];
395 -> 221;

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

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

398 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
221 -> 398 [arrowhead = none ];
398 -> 222;

399 [label="ONLY EVAL with clause\nno(X206).\nand substitutionT95 -> T98,\nX206 -> zero(T98)", fontsize=14, style = filled, fillcolor = lightblue];
222 -> 399 [arrowhead = none ];
399 -> 225;

400 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
225 -> 400 [arrowhead = none ];
400 -> 226;

401 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T98), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
226 -> 401 [arrowhead = none ];
401 -> 227;

402 [label="EVAL with clause\np(s(X211), X211).\nand substitutionX211 -> T101,\nT98 -> s(T101),\nX193 -> T101", fontsize=14, style = filled, fillcolor = lightblue];
227 -> 402 [arrowhead = none ];
402 -> 230;

403 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
227 -> 403 [arrowhead = none ];
403 -> 231;

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

405 [label="EVAL with clause\np(0, 0).\nand substitutionT92 -> 0,\nX194 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
232 -> 405 [arrowhead = none ];
405 -> 233;

406 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
232 -> 406 [arrowhead = none ];
406 -> 234;

407 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
233 -> 407 [arrowhead = none ];
407 -> 237;

408 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
233 -> 408 [arrowhead = none ];
408 -> 238;

409 [label="EVAL with clause\np(s(X264), X264).\nand substitutionX264 -> T116,\nT92 -> s(T116),\nX194 -> T116", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 409 [arrowhead = none ];
409 -> 289;

410 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
234 -> 410 [arrowhead = none ];
410 -> 290;

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

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

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

414 [label="ONLY EVAL with clause\nless(X229, X230) :- ','(no(zero(X229)), ','(p(X229, X231), ','(p(X230, X232), less(X231, X232)))).\nand substitutionT101 -> T104,\nX229 -> T104,\nX230 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
241 -> 414 [arrowhead = none ];
414 -> 249;

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

416 [label="ONLY EVAL with clause\nno(X237) :- ','(call(X237), ','(!_39, failure(a))).\nand substitutionT104 -> T107,\nX237 -> zero(T107)", fontsize=14, style = filled, fillcolor = lightblue];
254 -> 416 [arrowhead = none ];
416 -> 255;

417 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
255 -> 417 [arrowhead = none ];
417 -> 257;

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

419 [label="EVAL with clause\nzero(0).\nand substitutionT107 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
258 -> 419 [arrowhead = none ];
419 -> 259;

420 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
258 -> 420 [arrowhead = none ];
420 -> 260;

421 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
259 -> 421 [arrowhead = none ];
421 -> 263;

422 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
260 -> 422 [arrowhead = none ];
422 -> 266;

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

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

425 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
266 -> 425 [arrowhead = none ];
425 -> 267;

426 [label="ONLY EVAL with clause\nno(X244).\nand substitutionT107 -> T110,\nX244 -> zero(T110)", fontsize=14, style = filled, fillcolor = lightblue];
267 -> 426 [arrowhead = none ];
426 -> 271;

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

428 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T110), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
273 -> 428 [arrowhead = none ];
428 -> 274;

429 [label="EVAL with clause\np(s(X249), X249).\nand substitutionX249 -> T113,\nT110 -> s(T113),\nX231 -> T113", fontsize=14, style = filled, fillcolor = lightblue];
274 -> 429 [arrowhead = none ];
429 -> 275;

430 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
274 -> 430 [arrowhead = none ];
430 -> 276;

431 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
275 -> 431 [arrowhead = none ];
431 -> 279;

432 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX232 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
279 -> 432 [arrowhead = none ];
432 -> 280;

433 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
280 -> 433 [arrowhead = none ];
433 -> 281;

434 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
280 -> 434 [arrowhead = none ];
434 -> 282;

435 [label="INSTANCE with matching:\nT101 -> T113", fontsize=14, style = filled, fillcolor = lightgrey];
281 -> 435 [arrowhead = none , style=dashed];
435 -> 237[style=dashed];

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

437 [label="INSTANCE with matching:\nT73 -> T101\nT78 -> T116", fontsize=14, style = filled, fillcolor = lightgrey];
289 -> 437 [arrowhead = none , style=dashed];
437 -> 170[style=dashed];

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f99_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f99_out1, .(z0, .(z1, z2))) → f2_out1
f170_in(0, s(z0)) → f170_out1
f170_in(s(z0), 0) → U2(f233_in(z0), s(z0), 0)
f170_in(s(z0), s(z1)) → U3(f170_in(z0, z1), s(z0), s(z1))
U2(f233_out1, s(z0), 0) → f170_out1
U2(f233_out2(z0), s(z1), 0) → f170_out1
U3(f170_out1, s(z0), s(z1)) → f170_out1
f237_in(s(z0)) → U4(f280_in(z0), s(z0))
U4(f280_out1, s(z0)) → f237_out1
U4(f280_out2(z0), s(z1)) → f237_out1
f106_in(0, z0) → f106_out1
f106_in(s(z0), z1) → U5(f170_in(z0, z1), s(z0), z1)
U5(f170_out1, s(z0), z1) → f106_out1
f99_in(z0, z1, z2) → U6(f106_in(z0, z1), z0, z1, z2)
U6(f106_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f99_out1
f233_in(z0) → U8(f237_in(z0), f238_in(z0), z0)
U8(f237_out1, z0, z1) → f233_out1
U8(z0, f238_out1(z1), z2) → f233_out2(z1)
f280_in(z0) → U9(f237_in(z0), f282_in(z0), z0)
U9(f237_out1, z0, z1) → f280_out1
U9(z0, f282_out1(z1), z2) → f280_out2(z1)

Tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f99_in(z0, z1, z2), .(z0, .(z1, z2))), F99_IN(z0, z1, z2))
F170_IN(s(z0), 0) → c5(U2'(f233_in(z0), s(z0), 0), F233_IN(z0))
F170_IN(s(z0), s(z1)) → c6(U3'(f170_in(z0, z1), s(z0), s(z1)), F170_IN(z0, z1))
F237_IN(s(z0)) → c10(U4'(f280_in(z0), s(z0)), F280_IN(z0))
F106_IN(s(z0), z1) → c14(U5'(f170_in(z0, z1), s(z0), z1), F170_IN(z0, z1))
F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
U6'(f106_out1, z0, z1, z2) → c17(U7'(f2_in(.(z1, z2)), z0, z1, z2), F2_IN(.(z1, z2)))
F233_IN(z0) → c19(U8'(f237_in(z0), f238_in(z0), z0), F237_IN(z0))
F280_IN(z0) → c22(U9'(f237_in(z0), f282_in(z0), z0), F237_IN(z0))

S tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f99_in(z0, z1, z2), .(z0, .(z1, z2))), F99_IN(z0, z1, z2))
F170_IN(s(z0), 0) → c5(U2'(f233_in(z0), s(z0), 0), F233_IN(z0))
F170_IN(s(z0), s(z1)) → c6(U3'(f170_in(z0, z1), s(z0), s(z1)), F170_IN(z0, z1))
F237_IN(s(z0)) → c10(U4'(f280_in(z0), s(z0)), F280_IN(z0))
F106_IN(s(z0), z1) → c14(U5'(f170_in(z0, z1), s(z0), z1), F170_IN(z0, z1))
F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
U6'(f106_out1, z0, z1, z2) → c17(U7'(f2_in(.(z1, z2)), z0, z1, z2), F2_IN(.(z1, z2)))
F233_IN(z0) → c19(U8'(f237_in(z0), f238_in(z0), z0), F237_IN(z0))
F280_IN(z0) → c22(U9'(f237_in(z0), f282_in(z0), z0), F237_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f170_in, U2, U3, f237_in, U4, f106_in, U5, f99_in, U6, U7, f233_in, U8, f280_in, U9

Defined Pair Symbols:

F2_IN, F170_IN, F237_IN, F106_IN, F99_IN, U6', F233_IN, F280_IN

Compound Symbols:

c2, c5, c6, c10, c14, c16, c17, c19, c22

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

Split RHS of tuples not part of any SCC

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f99_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f99_out1, .(z0, .(z1, z2))) → f2_out1
f170_in(0, s(z0)) → f170_out1
f170_in(s(z0), 0) → U2(f233_in(z0), s(z0), 0)
f170_in(s(z0), s(z1)) → U3(f170_in(z0, z1), s(z0), s(z1))
U2(f233_out1, s(z0), 0) → f170_out1
U2(f233_out2(z0), s(z1), 0) → f170_out1
U3(f170_out1, s(z0), s(z1)) → f170_out1
f237_in(s(z0)) → U4(f280_in(z0), s(z0))
U4(f280_out1, s(z0)) → f237_out1
U4(f280_out2(z0), s(z1)) → f237_out1
f106_in(0, z0) → f106_out1
f106_in(s(z0), z1) → U5(f170_in(z0, z1), s(z0), z1)
U5(f170_out1, s(z0), z1) → f106_out1
f99_in(z0, z1, z2) → U6(f106_in(z0, z1), z0, z1, z2)
U6(f106_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f99_out1
f233_in(z0) → U8(f237_in(z0), f238_in(z0), z0)
U8(f237_out1, z0, z1) → f233_out1
U8(z0, f238_out1(z1), z2) → f233_out2(z1)
f280_in(z0) → U9(f237_in(z0), f282_in(z0), z0)
U9(f237_out1, z0, z1) → f280_out1
U9(z0, f282_out1(z1), z2) → f280_out2(z1)

Tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f99_in(z0, z1, z2), .(z0, .(z1, z2))), F99_IN(z0, z1, z2))
F170_IN(s(z0), s(z1)) → c6(U3'(f170_in(z0, z1), s(z0), s(z1)), F170_IN(z0, z1))
F237_IN(s(z0)) → c10(U4'(f280_in(z0), s(z0)), F280_IN(z0))
F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
U6'(f106_out1, z0, z1, z2) → c17(U7'(f2_in(.(z1, z2)), z0, z1, z2), F2_IN(.(z1, z2)))
F280_IN(z0) → c22(U9'(f237_in(z0), f282_in(z0), z0), F237_IN(z0))
F170_IN(s(z0), 0) → c(U2'(f233_in(z0), s(z0), 0))
F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(U5'(f170_in(z0, z1), s(z0), z1))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(U8'(f237_in(z0), f238_in(z0), z0))
F233_IN(z0) → c(F237_IN(z0))

S tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f99_in(z0, z1, z2), .(z0, .(z1, z2))), F99_IN(z0, z1, z2))
F170_IN(s(z0), s(z1)) → c6(U3'(f170_in(z0, z1), s(z0), s(z1)), F170_IN(z0, z1))
F237_IN(s(z0)) → c10(U4'(f280_in(z0), s(z0)), F280_IN(z0))
F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
U6'(f106_out1, z0, z1, z2) → c17(U7'(f2_in(.(z1, z2)), z0, z1, z2), F2_IN(.(z1, z2)))
F280_IN(z0) → c22(U9'(f237_in(z0), f282_in(z0), z0), F237_IN(z0))
F170_IN(s(z0), 0) → c(U2'(f233_in(z0), s(z0), 0))
F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(U5'(f170_in(z0, z1), s(z0), z1))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(U8'(f237_in(z0), f238_in(z0), z0))
F233_IN(z0) → c(F237_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f170_in, U2, U3, f237_in, U4, f106_in, U5, f99_in, U6, U7, f233_in, U8, f280_in, U9

Defined Pair Symbols:

F2_IN, F170_IN, F237_IN, F99_IN, U6', F280_IN, F106_IN, F233_IN

Compound Symbols:

c2, c6, c10, c16, c17, c22, c

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

Removed 8 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f99_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f99_out1, .(z0, .(z1, z2))) → f2_out1
f170_in(0, s(z0)) → f170_out1
f170_in(s(z0), 0) → U2(f233_in(z0), s(z0), 0)
f170_in(s(z0), s(z1)) → U3(f170_in(z0, z1), s(z0), s(z1))
U2(f233_out1, s(z0), 0) → f170_out1
U2(f233_out2(z0), s(z1), 0) → f170_out1
U3(f170_out1, s(z0), s(z1)) → f170_out1
f237_in(s(z0)) → U4(f280_in(z0), s(z0))
U4(f280_out1, s(z0)) → f237_out1
U4(f280_out2(z0), s(z1)) → f237_out1
f106_in(0, z0) → f106_out1
f106_in(s(z0), z1) → U5(f170_in(z0, z1), s(z0), z1)
U5(f170_out1, s(z0), z1) → f106_out1
f99_in(z0, z1, z2) → U6(f106_in(z0, z1), z0, z1, z2)
U6(f106_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f99_out1
f233_in(z0) → U8(f237_in(z0), f238_in(z0), z0)
U8(f237_out1, z0, z1) → f233_out1
U8(z0, f238_out1(z1), z2) → f233_out2(z1)
f280_in(z0) → U9(f237_in(z0), f282_in(z0), z0)
U9(f237_out1, z0, z1) → f280_out1
U9(z0, f282_out1(z1), z2) → f280_out2(z1)

Tuples:

F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(F237_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F99_IN(z0, z1, z2))
F170_IN(s(z0), s(z1)) → c6(F170_IN(z0, z1))
F237_IN(s(z0)) → c10(F280_IN(z0))
U6'(f106_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F280_IN(z0) → c22(F237_IN(z0))
F170_IN(s(z0), 0) → c
F106_IN(s(z0), z1) → c
F233_IN(z0) → c

S tuples:

F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(F237_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F99_IN(z0, z1, z2))
F170_IN(s(z0), s(z1)) → c6(F170_IN(z0, z1))
F237_IN(s(z0)) → c10(F280_IN(z0))
U6'(f106_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F280_IN(z0) → c22(F237_IN(z0))
F170_IN(s(z0), 0) → c
F106_IN(s(z0), z1) → c
F233_IN(z0) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f170_in, U2, U3, f237_in, U4, f106_in, U5, f99_in, U6, U7, f233_in, U8, f280_in, U9

Defined Pair Symbols:

F99_IN, F170_IN, F106_IN, F233_IN, F2_IN, F237_IN, U6', F280_IN

Compound Symbols:

c16, c, c2, c6, c10, c17, c22, c

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(F237_IN(z0))
F170_IN(s(z0), s(z1)) → c6(F170_IN(z0, z1))
F237_IN(s(z0)) → c10(F280_IN(z0))
F170_IN(s(z0), 0) → c
F106_IN(s(z0), z1) → c
F233_IN(z0) → c

We considered the (Usable) Rules:

f106_in(0, z0) → f106_out1
f106_in(s(z0), z1) → U5(f170_in(z0, z1), s(z0), z1)
f170_in(0, s(z0)) → f170_out1
f170_in(s(z0), 0) → U2(f233_in(z0), s(z0), 0)
f170_in(s(z0), s(z1)) → U3(f170_in(z0, z1), s(z0), s(z1))
U5(f170_out1, s(z0), z1) → f106_out1
U3(f170_out1, s(z0), s(z1)) → f170_out1
f233_in(z0) → U8(f237_in(z0), f238_in(z0), z0)
U2(f233_out1, s(z0), 0) → f170_out1
U2(f233_out2(z0), s(z1), 0) → f170_out1
f237_in(s(z0)) → U4(f280_in(z0), s(z0))
U8(f237_out1, z0, z1) → f233_out1
f280_in(z0) → U9(f237_in(z0), f282_in(z0), z0)
U4(f280_out1, s(z0)) → f237_out1
U4(f280_out2(z0), s(z1)) → f237_out1
U9(f237_out1, z0, z1) → f280_out1

And the Tuples:

F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(F237_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F99_IN(z0, z1, z2))
F170_IN(s(z0), s(z1)) → c6(F170_IN(z0, z1))
F237_IN(s(z0)) → c10(F280_IN(z0))
U6'(f106_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F280_IN(z0) → c22(F237_IN(z0))
F170_IN(s(z0), 0) → c
F106_IN(s(z0), z1) → c
F233_IN(z0) → c

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₁ + x₂
POL(0) = 0
POL(F106_IN(x₁, x₂)) = [1] + x₁
POL(F170_IN(x₁, x₂)) = [2] + x₁
POL(F233_IN(x₁)) = [3] + x₁
POL(F237_IN(x₁)) = x₁
POL(F280_IN(x₁)) = x₁
POL(F2_IN(x₁)) = x₁
POL(F99_IN(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃
POL(U2(x₁, x₂, x₃)) = 0
POL(U3(x₁, x₂, x₃)) = 0
POL(U4(x₁, x₂)) = [3]x₂
POL(U5(x₁, x₂, x₃)) = 0
POL(U6'(x₁, x₂, x₃, x₄)) = [1] + x₃ + x₄
POL(U8(x₁, x₂, x₃)) = 0
POL(U9(x₁, x₂, x₃)) = 0
POL(c) = 0
POL(c(x₁)) = x₁
POL(c10(x₁)) = x₁
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c17(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c22(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(f106_in(x₁, x₂)) = 0
POL(f106_out1) = 0
POL(f170_in(x₁, x₂)) = 0
POL(f170_out1) = 0
POL(f233_in(x₁)) = 0
POL(f233_out1) = 0
POL(f233_out2(x₁)) = 0
POL(f237_in(x₁)) = [2] + [3]x₁
POL(f237_out1) = 0
POL(f238_in(x₁)) = 0
POL(f280_in(x₁)) = 0
POL(f280_out1) = 0
POL(f280_out2(x₁)) = 0
POL(f282_in(x₁)) = 0
POL(s(x₁)) = [2] + x₁

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f99_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f99_out1, .(z0, .(z1, z2))) → f2_out1
f170_in(0, s(z0)) → f170_out1
f170_in(s(z0), 0) → U2(f233_in(z0), s(z0), 0)
f170_in(s(z0), s(z1)) → U3(f170_in(z0, z1), s(z0), s(z1))
U2(f233_out1, s(z0), 0) → f170_out1
U2(f233_out2(z0), s(z1), 0) → f170_out1
U3(f170_out1, s(z0), s(z1)) → f170_out1
f237_in(s(z0)) → U4(f280_in(z0), s(z0))
U4(f280_out1, s(z0)) → f237_out1
U4(f280_out2(z0), s(z1)) → f237_out1
f106_in(0, z0) → f106_out1
f106_in(s(z0), z1) → U5(f170_in(z0, z1), s(z0), z1)
U5(f170_out1, s(z0), z1) → f106_out1
f99_in(z0, z1, z2) → U6(f106_in(z0, z1), z0, z1, z2)
U6(f106_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f99_out1
f233_in(z0) → U8(f237_in(z0), f238_in(z0), z0)
U8(f237_out1, z0, z1) → f233_out1
U8(z0, f238_out1(z1), z2) → f233_out2(z1)
f280_in(z0) → U9(f237_in(z0), f282_in(z0), z0)
U9(f237_out1, z0, z1) → f280_out1
U9(z0, f282_out1(z1), z2) → f280_out2(z1)

Tuples:

F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(F237_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F99_IN(z0, z1, z2))
F170_IN(s(z0), s(z1)) → c6(F170_IN(z0, z1))
F237_IN(s(z0)) → c10(F280_IN(z0))
U6'(f106_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F280_IN(z0) → c22(F237_IN(z0))
F170_IN(s(z0), 0) → c
F106_IN(s(z0), z1) → c
F233_IN(z0) → c

S tuples:

F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
F2_IN(.(z0, .(z1, z2))) → c2(F99_IN(z0, z1, z2))
U6'(f106_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F280_IN(z0) → c22(F237_IN(z0))

K tuples:

F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(F237_IN(z0))
F170_IN(s(z0), s(z1)) → c6(F170_IN(z0, z1))
F237_IN(s(z0)) → c10(F280_IN(z0))
F170_IN(s(z0), 0) → c
F106_IN(s(z0), z1) → c
F233_IN(z0) → c

Defined Rule Symbols:

f2_in, U1, f170_in, U2, U3, f237_in, U4, f106_in, U5, f99_in, U6, U7, f233_in, U8, f280_in, U9

Defined Pair Symbols:

F99_IN, F170_IN, F106_IN, F233_IN, F2_IN, F237_IN, U6', F280_IN

Compound Symbols:

c16, c, c2, c6, c10, c17, c22, c

(23) CdtKnowledgeProof (EQUIVALENT transformation)

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

F280_IN(z0) → c22(F237_IN(z0))
F237_IN(s(z0)) → c10(F280_IN(z0))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f99_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f99_out1, .(z0, .(z1, z2))) → f2_out1
f170_in(0, s(z0)) → f170_out1
f170_in(s(z0), 0) → U2(f233_in(z0), s(z0), 0)
f170_in(s(z0), s(z1)) → U3(f170_in(z0, z1), s(z0), s(z1))
U2(f233_out1, s(z0), 0) → f170_out1
U2(f233_out2(z0), s(z1), 0) → f170_out1
U3(f170_out1, s(z0), s(z1)) → f170_out1
f237_in(s(z0)) → U4(f280_in(z0), s(z0))
U4(f280_out1, s(z0)) → f237_out1
U4(f280_out2(z0), s(z1)) → f237_out1
f106_in(0, z0) → f106_out1
f106_in(s(z0), z1) → U5(f170_in(z0, z1), s(z0), z1)
U5(f170_out1, s(z0), z1) → f106_out1
f99_in(z0, z1, z2) → U6(f106_in(z0, z1), z0, z1, z2)
U6(f106_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f99_out1
f233_in(z0) → U8(f237_in(z0), f238_in(z0), z0)
U8(f237_out1, z0, z1) → f233_out1
U8(z0, f238_out1(z1), z2) → f233_out2(z1)
f280_in(z0) → U9(f237_in(z0), f282_in(z0), z0)
U9(f237_out1, z0, z1) → f280_out1
U9(z0, f282_out1(z1), z2) → f280_out2(z1)

Tuples:

F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(F237_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F99_IN(z0, z1, z2))
F170_IN(s(z0), s(z1)) → c6(F170_IN(z0, z1))
F237_IN(s(z0)) → c10(F280_IN(z0))
U6'(f106_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F280_IN(z0) → c22(F237_IN(z0))
F170_IN(s(z0), 0) → c
F106_IN(s(z0), z1) → c
F233_IN(z0) → c

S tuples:

F99_IN(z0, z1, z2) → c16(U6'(f106_in(z0, z1), z0, z1, z2), F106_IN(z0, z1))
F2_IN(.(z0, .(z1, z2))) → c2(F99_IN(z0, z1, z2))
U6'(f106_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))

K tuples:

F170_IN(s(z0), 0) → c(F233_IN(z0))
F106_IN(s(z0), z1) → c(F170_IN(z0, z1))
F233_IN(z0) → c(F237_IN(z0))
F170_IN(s(z0), s(z1)) → c6(F170_IN(z0, z1))
F237_IN(s(z0)) → c10(F280_IN(z0))
F170_IN(s(z0), 0) → c
F106_IN(s(z0), z1) → c
F233_IN(z0) → c
F280_IN(z0) → c22(F237_IN(z0))

Defined Rule Symbols:

f2_in, U1, f170_in, U2, U3, f237_in, U4, f106_in, U5, f99_in, U6, U7, f233_in, U8, f280_in, U9

Defined Pair Symbols:

F99_IN, F170_IN, F106_IN, F233_IN, F2_IN, F237_IN, U6', F280_IN

Compound Symbols:

c16, c, c2, c6, c10, c17, c22, c