Runtime Complexity proof of /tmp/tmpaPe9QF/less.pl

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

0 Prolog

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

↳2 CdtProblem

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

    ↳4 CdtProblem

    ↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 190 ms)

    ↳6 CdtProblem

    ↳7 CdtKnowledgeProof (⇔, 0 ms)

    ↳8 CdtProblem

    ↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 16 ms)

    ↳10 CdtProblem

    ↳11 CdtKnowledgeProof (⇔, 0 ms)

    ↳12 BOUNDS(O(1), O(1))

↳13 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 178 ms)

↳14 CdtProblem

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

    ↳16 CdtProblem

    ↳17 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 159 ms)

    ↳18 CdtProblem

    ↳19 CdtKnowledgeProof (⇔, 0 ms)

    ↳20 CdtProblem

    ↳21 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 17 ms)

    ↳22 CdtProblem

(0) Obligation:

Clauses:

less(0, s(X2)).
less(X, Y) :- ','(no(zero(X)), ','(p(X, X1), ','(p(Y, Y1), less(X1, Y1)))).
p(0, 0).
p(s(X), X).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X3).
failure(b).

Query: less(g,a)

(1) 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: less(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: less(T1, T2), SCOPE: 1, CLAUSE: 0 | less(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: true | less(0, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: less(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX6 is free\nless(T1, T2) !=? less(0, s(X6))", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: less(0, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(no(zero(0)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18))))\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(no(zero(0)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))), SCOPE: 2, CLAUSE: 5 | ','(no(zero(0)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))), SCOPE: 2, CLAUSE: 6\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(','(call(zero(0)), ','(!_2, failure(a))), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))) | ','(no(zero(0)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))), SCOPE: 2, CLAUSE: 6\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(zero(0), ','(','(!_2, failure(a)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18))))) | ?_3 | ','(no(zero(0)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))), SCOPE: 2, CLAUSE: 6\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(zero(0), ','(','(!_2, failure(a)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18))))), SCOPE: 4, CLAUSE: 4 | ?_4 | ?_3 | ','(no(zero(0)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))), SCOPE: 2, CLAUSE: 6\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(','(!_2, failure(a)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))) | ?_4 | ?_3 | ','(no(zero(0)), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))), SCOPE: 2, CLAUSE: 6\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(failure(a), ','(p(0, X17), ','(p(T10, X18), less(X17, X18))))\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(failure(a), ','(p(0, X17), ','(p(T10, X18), less(X17, X18)))), SCOPE: 5, CLAUSE: 7\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(no(zero(T16)), ','(p(T16, X36), ','(p(T18, X37), less(X36, X37))))\n\nT16 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T16, T2) !=? less(0, s(X6))", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(no(zero(T16)), ','(p(T16, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 5 | ','(no(zero(T16)), ','(p(T16, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 6\n\nT16 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T16, T2) !=? less(0, s(X6))", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(','(call(zero(T21)), ','(!_6, failure(a))), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37)))) | ','(no(zero(T21)), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 6\n\nT21 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T21, T2) !=? less(0, s(X6))", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(zero(T21), ','(','(!_6, failure(a)), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37))))) | ?_7 | ','(no(zero(T21)), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 6\n\nT21 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T21, T2) !=? less(0, s(X6))", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(zero(T21), ','(','(!_6, failure(a)), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37))))), SCOPE: 8, CLAUSE: 4 | ?_8 | ?_7 | ','(no(zero(T21)), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 6\n\nT21 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T21, T2) !=? less(0, s(X6))", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(','(!_6, failure(a)), ','(p(0, X36), ','(p(T18, X37), less(X36, X37)))) | ?_8 | ?_7 | ','(no(zero(0)), ','(p(0, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 6\n\nX36 is free\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ?_8 | ?_7 | ','(no(zero(T21)), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 6\n\nT21 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T21, T2) !=? less(0, s(X6))\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(failure(a), ','(p(0, X36), ','(p(T18, X37), less(X36, X37))))\n\nX36 is free\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(failure(a), ','(p(0, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 9, CLAUSE: 7\n\nX36 is free\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ?_7 | ','(no(zero(T21)), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 6\n\nT21 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T21, T2) !=? less(0, s(X6))\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(no(zero(T21)), ','(p(T21, X36), ','(p(T18, X37), less(X36, X37)))), SCOPE: 6, CLAUSE: 6\n\nT21 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T21, T2) !=? less(0, s(X6))\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(p(T24, X36), ','(p(T18, X37), less(X36, X37)))\n\nT24 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T24, T2) !=? less(0, s(X6))\nzero(T24) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(p(T24, X36), ','(p(T18, X37), less(X36, X37))), SCOPE: 10, CLAUSE: 2 | ','(p(T24, X36), ','(p(T18, X37), less(X36, X37))), SCOPE: 10, CLAUSE: 3\n\nT24 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T24, T2) !=? less(0, s(X6))\nzero(T24) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(p(T24, X36), ','(p(T18, X37), less(X36, X37))), SCOPE: 10, CLAUSE: 3\n\nT24 is ground\nX6 is free\nX36 is free\nX37 is free\nless(T24, T2) !=? less(0, s(X6))\nzero(T24) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(p(T18, X37), less(T27, X37))\n\nT27 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(p(T18, X37), less(T27, X37)), SCOPE: 11, CLAUSE: 2 | ','(p(T18, X37), less(T27, X37)), SCOPE: 11, CLAUSE: 3\n\nT27 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: less(T27, 0) | ','(p(T18, X37), less(T27, X37)), SCOPE: 11, CLAUSE: 3\n\nT27 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(p(T18, X37), less(T27, X37)), SCOPE: 11, CLAUSE: 3\n\nT27 is ground\nX37 is free\np(T18, X37) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: less(T27, 0)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(p(T18, X37), less(T27, X37)), SCOPE: 11, CLAUSE: 3\n\nT27 is ground\nX37 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: less(T27, 0), SCOPE: 12, CLAUSE: 0 | less(T27, 0), SCOPE: 12, CLAUSE: 1\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: less(T27, 0), SCOPE: 12, CLAUSE: 1\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(no(zero(T30)), ','(p(T30, X74), ','(p(0, X75), less(X74, X75))))\n\nT30 is ground\nX74 is free\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(no(zero(T30)), ','(p(T30, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 5 | ','(no(zero(T30)), ','(p(T30, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 6\n\nT30 is ground\nX74 is free\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(','(call(zero(T33)), ','(!_13, failure(a))), ','(p(T33, X74), ','(p(0, X75), less(X74, X75)))) | ','(no(zero(T33)), ','(p(T33, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 6\n\nT33 is ground\nX74 is free\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(zero(T33), ','(','(!_13, failure(a)), ','(p(T33, X74), ','(p(0, X75), less(X74, X75))))) | ?_14 | ','(no(zero(T33)), ','(p(T33, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 6\n\nT33 is ground\nX74 is free\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(zero(T33), ','(','(!_13, failure(a)), ','(p(T33, X74), ','(p(0, X75), less(X74, X75))))), SCOPE: 15, CLAUSE: 4 | ?_15 | ?_14 | ','(no(zero(T33)), ','(p(T33, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 6\n\nT33 is ground\nX74 is free\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(','(!_13, failure(a)), ','(p(0, X74), ','(p(0, X75), less(X74, X75)))) | ?_15 | ?_14 | ','(no(zero(0)), ','(p(0, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 6\n\nX74 is free\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ?_15 | ?_14 | ','(no(zero(T33)), ','(p(T33, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 6\n\nT33 is ground\nX74 is free\nX75 is free\nzero(T33) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(failure(a), ','(p(0, X74), ','(p(0, X75), less(X74, X75))))\n\nX74 is free\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(failure(a), ','(p(0, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 16, CLAUSE: 7\n\nX74 is free\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ?_14 | ','(no(zero(T33)), ','(p(T33, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 6\n\nT33 is ground\nX74 is free\nX75 is free\nzero(T33) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(no(zero(T33)), ','(p(T33, X74), ','(p(0, X75), less(X74, X75)))), SCOPE: 13, CLAUSE: 6\n\nT33 is ground\nX74 is free\nX75 is free\nzero(T33) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(p(T36, X74), ','(p(0, X75), less(X74, X75)))\n\nT36 is ground\nX74 is free\nX75 is free\nzero(T36) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(p(T36, X74), ','(p(0, X75), less(X74, X75))), SCOPE: 17, CLAUSE: 2 | ','(p(T36, X74), ','(p(0, X75), less(X74, X75))), SCOPE: 17, CLAUSE: 3\n\nT36 is ground\nX74 is free\nX75 is free\nzero(T36) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(p(T36, X74), ','(p(0, X75), less(X74, X75))), SCOPE: 17, CLAUSE: 3\n\nT36 is ground\nX74 is free\nX75 is free\nzero(T36) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(p(0, X75), less(T39, X75))\n\nT39 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(p(0, X75), less(T39, X75)), SCOPE: 18, CLAUSE: 2 | ','(p(0, X75), less(T39, X75)), SCOPE: 18, CLAUSE: 3\n\nT39 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: less(T39, 0) | ','(p(0, X75), less(T39, X75)), SCOPE: 18, CLAUSE: 3\n\nT39 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: less(T39, 0)\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(p(0, X75), less(T39, X75)), SCOPE: 18, CLAUSE: 3\n\nT39 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: less(T27, T43)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: less(T27, T49)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 129 [arrowhead = none ];
129 -> 3;

130 [label="EVAL with clause\nless(0, s(X6)).\nand substitutionT1 -> 0,\nX6 -> T5,\nT2 -> s(T5)", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 130 [arrowhead = none ];
130 -> 8;

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

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

133 [label="ONLY EVAL with clause\nless(X34, X35) :- ','(no(zero(X34)), ','(p(X34, X36), ','(p(X35, X37), less(X36, X37)))).\nand substitutionT1 -> T16,\nX34 -> T16,\nT2 -> T18,\nX35 -> T18,\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 133 [arrowhead = none ];
133 -> 32;

134 [label="ONLY EVAL with clause\nless(X15, X16) :- ','(no(zero(X15)), ','(p(X15, X17), ','(p(X16, X18), less(X17, X18)))).\nand substitutionX15 -> 0,\nT2 -> T10,\nX16 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 134 [arrowhead = none ];
134 -> 13;

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

136 [label="ONLY EVAL with clause\nno(X23) :- ','(call(X23), ','(!_2, failure(a))).\nand substitutionX23 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 136 [arrowhead = none ];
136 -> 18;

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

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

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

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

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

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

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

144 [label="ONLY EVAL with clause\nno(X42) :- ','(call(X42), ','(!_6, failure(a))).\nand substitutionT16 -> T21,\nX42 -> zero(T21)", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 144 [arrowhead = none ];
144 -> 39;

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

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

147 [label="EVAL with clause\nzero(0).\nand substitutionT21 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 147 [arrowhead = none ];
147 -> 46;

148 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 148 [arrowhead = none ];
148 -> 47;

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

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

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

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

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

154 [label="ONLY EVAL with clause\nno(X49).\nand substitutionT21 -> T24,\nX49 -> zero(T24)", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 154 [arrowhead = none ];
154 -> 57;

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

156 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T24), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 156 [arrowhead = none ];
156 -> 61;

157 [label="EVAL with clause\np(s(X54), X54).\nand substitutionX54 -> T27,\nT24 -> s(T27),\nX36 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 157 [arrowhead = none ];
157 -> 64;

158 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 158 [arrowhead = none ];
158 -> 65;

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

160 [label="EVAL with clause\np(0, 0).\nand substitutionT18 -> 0,\nX37 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 160 [arrowhead = none ];
160 -> 67;

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

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

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

164 [label="EVAL with clause\np(s(X111), X111).\nand substitutionX111 -> T49,\nT18 -> s(T49),\nX37 -> T49,\nT48 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 164 [arrowhead = none ];
164 -> 127;

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

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

167 [label="EVAL with clause\np(s(X106), X106).\nand substitutionX106 -> T43,\nT18 -> s(T43),\nX37 -> T43,\nT42 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 167 [arrowhead = none ];
167 -> 123;

168 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 168 [arrowhead = none ];
168 -> 124;

169 [label="BACKTRACK\nfor clause: less(0, s(X2))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 169 [arrowhead = none ];
169 -> 76;

170 [label="ONLY EVAL with clause\nless(X72, X73) :- ','(no(zero(X72)), ','(p(X72, X74), ','(p(X73, X75), less(X74, X75)))).\nand substitutionT27 -> T30,\nX72 -> T30,\nX73 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 170 [arrowhead = none ];
170 -> 78;

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

172 [label="ONLY EVAL with clause\nno(X80) :- ','(call(X80), ','(!_13, failure(a))).\nand substitutionT30 -> T33,\nX80 -> zero(T33)", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 172 [arrowhead = none ];
172 -> 84;

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

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

175 [label="EVAL with clause\nzero(0).\nand substitutionT33 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 175 [arrowhead = none ];
175 -> 90;

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

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

178 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 178 [arrowhead = none ];
178 -> 99;

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

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

181 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 181 [arrowhead = none ];
181 -> 100;

182 [label="ONLY EVAL with clause\nno(X87).\nand substitutionT33 -> T36,\nX87 -> zero(T36)", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 182 [arrowhead = none ];
182 -> 104;

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

184 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T36), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 184 [arrowhead = none ];
184 -> 108;

185 [label="EVAL with clause\np(s(X92), X92).\nand substitutionX92 -> T39,\nT36 -> s(T39),\nX74 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 185 [arrowhead = none ];
185 -> 110;

186 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 186 [arrowhead = none ];
186 -> 111;

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

188 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX75 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 188 [arrowhead = none ];
188 -> 116;

189 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
116 -> 189 [arrowhead = none ];
189 -> 117;

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

191 [label="INSTANCE with matching:\nT27 -> T39", fontsize=14, style = filled, fillcolor = lightgrey];
117 -> 191 [arrowhead = none , style=dashed];
191 -> 69[style=dashed];

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

193 [label="INSTANCE with matching:\nT1 -> T27\nT2 -> T43", fontsize=14, style = filled, fillcolor = lightgrey];
123 -> 193 [arrowhead = none , style=dashed];
193 -> 2[style=dashed];

194 [label="INSTANCE with matching:\nT1 -> T27\nT2 -> T49", fontsize=14, style = filled, fillcolor = lightgrey];
127 -> 194 [arrowhead = none , style=dashed];
194 -> 2[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f67_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f67_out1, s(z0)) → f2_out1
U1(f67_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f69_in(s(z0)) → U3(f116_in(z0), s(z0))
U3(f116_out1, s(z0)) → f69_out1
U3(f116_out2(z0), s(z1)) → f69_out1
f71_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f71_out1
f67_in(z0) → U5(f69_in(z0), f71_in(z0), z0)
U5(f69_out1, z0, z1) → f67_out1
U5(z0, f71_out1, z1) → f67_out2
f116_in(z0) → U6(f69_in(z0), f118_in(z0), z0)
U6(f69_out1, z0, z1) → f116_out1
U6(z0, f118_out1(z1), z2) → f116_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(U1'(f67_in(z0), s(z0)), F67_IN(z0))
F2_IN(s(z0)) → c2(U2'(f2_in(z0), s(z0)), F2_IN(z0))
F69_IN(s(z0)) → c6(U3'(f116_in(z0), s(z0)), F116_IN(z0))
F71_IN(z0) → c9(U4'(f2_in(z0), z0), F2_IN(z0))
F67_IN(z0) → c11(U5'(f69_in(z0), f71_in(z0), z0), F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(U6'(f69_in(z0), f118_in(z0), z0), F69_IN(z0))

S tuples:

F2_IN(s(z0)) → c1(U1'(f67_in(z0), s(z0)), F67_IN(z0))
F2_IN(s(z0)) → c2(U2'(f2_in(z0), s(z0)), F2_IN(z0))
F69_IN(s(z0)) → c6(U3'(f116_in(z0), s(z0)), F116_IN(z0))
F71_IN(z0) → c9(U4'(f2_in(z0), z0), F2_IN(z0))
F67_IN(z0) → c11(U5'(f69_in(z0), f71_in(z0), z0), F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(U6'(f69_in(z0), f118_in(z0), z0), F69_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f69_in, U3, f71_in, U4, f67_in, U5, f116_in, U6

Defined Pair Symbols:

F2_IN, F69_IN, F71_IN, F67_IN, F116_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

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

Removed 6 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f67_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f67_out1, s(z0)) → f2_out1
U1(f67_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f69_in(s(z0)) → U3(f116_in(z0), s(z0))
U3(f116_out1, s(z0)) → f69_out1
U3(f116_out2(z0), s(z1)) → f69_out1
f71_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f71_out1
f67_in(z0) → U5(f69_in(z0), f71_in(z0), z0)
U5(f69_out1, z0, z1) → f67_out1
U5(z0, f71_out1, z1) → f67_out2
f116_in(z0) → U6(f69_in(z0), f118_in(z0), z0)
U6(f69_out1, z0, z1) → f116_out1
U6(z0, f118_out1(z1), z2) → f116_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

S tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f69_in, U3, f71_in, U4, f67_in, U5, f116_in, U6

Defined Pair Symbols:

F2_IN, F69_IN, F71_IN, F67_IN, F116_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

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

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))

We considered the (Usable) Rules:none
And the Tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

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

POL(F116_IN(x₁)) = 0
POL(F2_IN(x₁)) = x₁
POL(F67_IN(x₁)) = x₁
POL(F69_IN(x₁)) = 0
POL(F71_IN(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f67_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f67_out1, s(z0)) → f2_out1
U1(f67_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f69_in(s(z0)) → U3(f116_in(z0), s(z0))
U3(f116_out1, s(z0)) → f69_out1
U3(f116_out2(z0), s(z1)) → f69_out1
f71_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f71_out1
f67_in(z0) → U5(f69_in(z0), f71_in(z0), z0)
U5(f69_out1, z0, z1) → f67_out1
U5(z0, f71_out1, z1) → f67_out2
f116_in(z0) → U6(f69_in(z0), f118_in(z0), z0)
U6(f69_out1, z0, z1) → f116_out1
U6(z0, f118_out1(z1), z2) → f116_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

S tuples:

F69_IN(s(z0)) → c6(F116_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

K tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))

Defined Rule Symbols:

f2_in, U1, U2, f69_in, U3, f71_in, U4, f67_in, U5, f116_in, U6

Defined Pair Symbols:

F2_IN, F69_IN, F71_IN, F67_IN, F116_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(7) CdtKnowledgeProof (EQUIVALENT transformation)

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

F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f67_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f67_out1, s(z0)) → f2_out1
U1(f67_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f69_in(s(z0)) → U3(f116_in(z0), s(z0))
U3(f116_out1, s(z0)) → f69_out1
U3(f116_out2(z0), s(z1)) → f69_out1
f71_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f71_out1
f67_in(z0) → U5(f69_in(z0), f71_in(z0), z0)
U5(f69_out1, z0, z1) → f67_out1
U5(z0, f71_out1, z1) → f67_out2
f116_in(z0) → U6(f69_in(z0), f118_in(z0), z0)
U6(f69_out1, z0, z1) → f116_out1
U6(z0, f118_out1(z1), z2) → f116_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

S tuples:

F69_IN(s(z0)) → c6(F116_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

K tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))

Defined Rule Symbols:

f2_in, U1, U2, f69_in, U3, f71_in, U4, f67_in, U5, f116_in, U6

Defined Pair Symbols:

F2_IN, F69_IN, F71_IN, F67_IN, F116_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

F69_IN(s(z0)) → c6(F116_IN(z0))

We considered the (Usable) Rules:none
And the Tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

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

POL(F116_IN(x₁)) = x₁
POL(F2_IN(x₁)) = x₁²
POL(F67_IN(x₁)) = x₁ + x₁²
POL(F69_IN(x₁)) = x₁
POL(F71_IN(x₁)) = x₁²
POL(c1(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f67_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f67_out1, s(z0)) → f2_out1
U1(f67_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f69_in(s(z0)) → U3(f116_in(z0), s(z0))
U3(f116_out1, s(z0)) → f69_out1
U3(f116_out2(z0), s(z1)) → f69_out1
f71_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f71_out1
f67_in(z0) → U5(f69_in(z0), f71_in(z0), z0)
U5(f69_out1, z0, z1) → f67_out1
U5(z0, f71_out1, z1) → f67_out2
f116_in(z0) → U6(f69_in(z0), f118_in(z0), z0)
U6(f69_out1, z0, z1) → f116_out1
U6(z0, f118_out1(z1), z2) → f116_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F116_IN(z0) → c14(F69_IN(z0))

S tuples:

F116_IN(z0) → c14(F69_IN(z0))

K tuples:

F2_IN(s(z0)) → c1(F67_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F67_IN(z0) → c11(F69_IN(z0), F71_IN(z0))
F71_IN(z0) → c9(F2_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))

Defined Rule Symbols:

f2_in, U1, U2, f69_in, U3, f71_in, U4, f67_in, U5, f116_in, U6

Defined Pair Symbols:

F2_IN, F69_IN, F71_IN, F67_IN, F116_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(11) CdtKnowledgeProof (EQUIVALENT transformation)

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

F116_IN(z0) → c14(F69_IN(z0))
F69_IN(s(z0)) → c6(F116_IN(z0))

Now S is empty

(12) BOUNDS(O(1), O(1))

(13) 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: less(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: less(T1, T2), SCOPE: 1, CLAUSE: 0 | less(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | less(0, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: less(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX5 is free\nless(T1, T2) !=? less(0, s(X5))", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: less(0, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(no(zero(0)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11))))\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(no(zero(0)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))), SCOPE: 2, CLAUSE: 5 | ','(no(zero(0)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))), SCOPE: 2, CLAUSE: 6\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(','(call(zero(0)), ','(!_2, failure(a))), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))) | ','(no(zero(0)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))), SCOPE: 2, CLAUSE: 6\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(zero(0), ','(','(!_2, failure(a)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11))))) | ?_3 | ','(no(zero(0)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))), SCOPE: 2, CLAUSE: 6\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(zero(0), ','(','(!_2, failure(a)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11))))), SCOPE: 4, CLAUSE: 4 | ?_4 | ?_3 | ','(no(zero(0)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))), SCOPE: 2, CLAUSE: 6\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(','(!_2, failure(a)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))) | ?_4 | ?_3 | ','(no(zero(0)), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))), SCOPE: 2, CLAUSE: 6\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(failure(a), ','(p(0, X10), ','(p(T7, X11), less(X10, X11))))\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(failure(a), ','(p(0, X10), ','(p(T7, X11), less(X10, X11)))), SCOPE: 5, CLAUSE: 7\n\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(no(zero(T10)), ','(p(T10, X21), ','(p(T12, X22), less(X21, X22))))\n\nT10 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T10, T2) !=? less(0, s(X5))", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(no(zero(T10)), ','(p(T10, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 5 | ','(no(zero(T10)), ','(p(T10, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 6\n\nT10 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T10, T2) !=? less(0, s(X5))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(','(call(zero(T15)), ','(!_6, failure(a))), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22)))) | ','(no(zero(T15)), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T15, T2) !=? less(0, s(X5))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(zero(T15), ','(','(!_6, failure(a)), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22))))) | ?_7 | ','(no(zero(T15)), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T15, T2) !=? less(0, s(X5))", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(zero(T15), ','(','(!_6, failure(a)), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22))))), SCOPE: 8, CLAUSE: 4 | ?_8 | ?_7 | ','(no(zero(T15)), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T15, T2) !=? less(0, s(X5))", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(','(!_6, failure(a)), ','(p(0, X21), ','(p(T12, X22), less(X21, X22)))) | ?_8 | ?_7 | ','(no(zero(0)), ','(p(0, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 6\n\nX21 is free\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ?_8 | ?_7 | ','(no(zero(T15)), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T15, T2) !=? less(0, s(X5))\nzero(T15) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(failure(a), ','(p(0, X21), ','(p(T12, X22), less(X21, X22))))\n\nX21 is free\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(failure(a), ','(p(0, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 9, CLAUSE: 7\n\nX21 is free\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ?_7 | ','(no(zero(T15)), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T15, T2) !=? less(0, s(X5))\nzero(T15) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(no(zero(T15)), ','(p(T15, X21), ','(p(T12, X22), less(X21, X22)))), SCOPE: 6, CLAUSE: 6\n\nT15 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T15, T2) !=? less(0, s(X5))\nzero(T15) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(p(T18, X21), ','(p(T12, X22), less(X21, X22)))\n\nT18 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T18, T2) !=? less(0, s(X5))\nzero(T18) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(p(T18, X21), ','(p(T12, X22), less(X21, X22))), SCOPE: 10, CLAUSE: 2 | ','(p(T18, X21), ','(p(T12, X22), less(X21, X22))), SCOPE: 10, CLAUSE: 3\n\nT18 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T18, T2) !=? less(0, s(X5))\nzero(T18) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(p(T18, X21), ','(p(T12, X22), less(X21, X22))), SCOPE: 10, CLAUSE: 3\n\nT18 is ground\nX5 is free\nX21 is free\nX22 is free\nless(T18, T2) !=? less(0, s(X5))\nzero(T18) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(p(T12, X22), less(T21, X22))\n\nT21 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(p(T12, X22), less(T21, X22)), SCOPE: 11, CLAUSE: 2 | ','(p(T12, X22), less(T21, X22)), SCOPE: 11, CLAUSE: 3\n\nT21 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: less(T21, 0) | ','(p(T12, X22), less(T21, X22)), SCOPE: 11, CLAUSE: 3\n\nT21 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(p(T12, X22), less(T21, X22)), SCOPE: 11, CLAUSE: 3\n\nT21 is ground\nX22 is free\np(T12, X22) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: less(T21, 0)\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(p(T12, X22), less(T21, X22)), SCOPE: 11, CLAUSE: 3\n\nT21 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: less(T21, 0), SCOPE: 12, CLAUSE: 0 | less(T21, 0), SCOPE: 12, CLAUSE: 1\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: less(T21, 0), SCOPE: 12, CLAUSE: 1\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(no(zero(T24)), ','(p(T24, X57), ','(p(0, X58), less(X57, X58))))\n\nT24 is ground\nX57 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(no(zero(T24)), ','(p(T24, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 5 | ','(no(zero(T24)), ','(p(T24, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 6\n\nT24 is ground\nX57 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(','(call(zero(T27)), ','(!_13, failure(a))), ','(p(T27, X57), ','(p(0, X58), less(X57, X58)))) | ','(no(zero(T27)), ','(p(T27, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 6\n\nT27 is ground\nX57 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(zero(T27), ','(','(!_13, failure(a)), ','(p(T27, X57), ','(p(0, X58), less(X57, X58))))) | ?_14 | ','(no(zero(T27)), ','(p(T27, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 6\n\nT27 is ground\nX57 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(zero(T27), ','(','(!_13, failure(a)), ','(p(T27, X57), ','(p(0, X58), less(X57, X58))))), SCOPE: 15, CLAUSE: 4 | ?_15 | ?_14 | ','(no(zero(T27)), ','(p(T27, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 6\n\nT27 is ground\nX57 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(','(!_13, failure(a)), ','(p(0, X57), ','(p(0, X58), less(X57, X58)))) | ?_15 | ?_14 | ','(no(zero(0)), ','(p(0, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 6\n\nX57 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ?_15 | ?_14 | ','(no(zero(T27)), ','(p(T27, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 6\n\nT27 is ground\nX57 is free\nX58 is free\nzero(T27) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(failure(a), ','(p(0, X57), ','(p(0, X58), less(X57, X58))))\n\nX57 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(failure(a), ','(p(0, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 16, CLAUSE: 7\n\nX57 is free\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ?_14 | ','(no(zero(T27)), ','(p(T27, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 6\n\nT27 is ground\nX57 is free\nX58 is free\nzero(T27) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(no(zero(T27)), ','(p(T27, X57), ','(p(0, X58), less(X57, X58)))), SCOPE: 13, CLAUSE: 6\n\nT27 is ground\nX57 is free\nX58 is free\nzero(T27) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(p(T30, X57), ','(p(0, X58), less(X57, X58)))\n\nT30 is ground\nX57 is free\nX58 is free\nzero(T30) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(p(T30, X57), ','(p(0, X58), less(X57, X58))), SCOPE: 17, CLAUSE: 2 | ','(p(T30, X57), ','(p(0, X58), less(X57, X58))), SCOPE: 17, CLAUSE: 3\n\nT30 is ground\nX57 is free\nX58 is free\nzero(T30) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(p(T30, X57), ','(p(0, X58), less(X57, X58))), SCOPE: 17, CLAUSE: 3\n\nT30 is ground\nX57 is free\nX58 is free\nzero(T30) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(p(0, X58), less(T33, X58))\n\nT33 is ground\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(p(0, X58), less(T33, X58)), SCOPE: 18, CLAUSE: 2 | ','(p(0, X58), less(T33, X58)), SCOPE: 18, CLAUSE: 3\n\nT33 is ground\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: less(T33, 0) | ','(p(0, X58), less(T33, X58)), SCOPE: 18, CLAUSE: 3\n\nT33 is ground\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: less(T33, 0)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(p(0, X58), less(T33, X58)), SCOPE: 18, CLAUSE: 3\n\nT33 is ground\nX58 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: less(T21, T37)\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: less(T21, T43)\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 127 [arrowhead = none ];
127 -> 4;

128 [label="EVAL with clause\nless(0, s(X5)).\nand substitutionT1 -> 0,\nX5 -> T4,\nT2 -> s(T4)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 128 [arrowhead = none ];
128 -> 5;

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

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

131 [label="ONLY EVAL with clause\nless(X19, X20) :- ','(no(zero(X19)), ','(p(X19, X21), ','(p(X20, X22), less(X21, X22)))).\nand substitutionT1 -> T10,\nX19 -> T10,\nT2 -> T12,\nX20 -> T12,\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 131 [arrowhead = none ];
131 -> 29;

132 [label="ONLY EVAL with clause\nless(X8, X9) :- ','(no(zero(X8)), ','(p(X8, X10), ','(p(X9, X11), less(X10, X11)))).\nand substitutionX8 -> 0,\nT2 -> T7,\nX9 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 132 [arrowhead = none ];
132 -> 11;

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

134 [label="ONLY EVAL with clause\nno(X14) :- ','(call(X14), ','(!_2, failure(a))).\nand substitutionX14 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 134 [arrowhead = none ];
134 -> 14;

135 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
14 -> 135 [arrowhead = none ];
135 -> 15;

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

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

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

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

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

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

142 [label="ONLY EVAL with clause\nno(X25) :- ','(call(X25), ','(!_6, failure(a))).\nand substitutionT10 -> T15,\nX25 -> zero(T15)", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 142 [arrowhead = none ];
142 -> 31;

143 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
31 -> 143 [arrowhead = none ];
143 -> 33;

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

145 [label="EVAL with clause\nzero(0).\nand substitutionT15 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 145 [arrowhead = none ];
145 -> 36;

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

147 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 147 [arrowhead = none ];
147 -> 38;

148 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 148 [arrowhead = none ];
148 -> 43;

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

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

151 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 151 [arrowhead = none ];
151 -> 45;

152 [label="ONLY EVAL with clause\nno(X32).\nand substitutionT15 -> T18,\nX32 -> zero(T18)", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 152 [arrowhead = none ];
152 -> 50;

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

154 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T18), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 154 [arrowhead = none ];
154 -> 55;

155 [label="EVAL with clause\np(s(X37), X37).\nand substitutionX37 -> T21,\nT18 -> s(T21),\nX21 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 155 [arrowhead = none ];
155 -> 56;

156 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 156 [arrowhead = none ];
156 -> 58;

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

158 [label="EVAL with clause\np(0, 0).\nand substitutionT12 -> 0,\nX22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 158 [arrowhead = none ];
158 -> 62;

159 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 159 [arrowhead = none ];
159 -> 63;

160 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 160 [arrowhead = none ];
160 -> 70;

161 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
62 -> 161 [arrowhead = none ];
161 -> 72;

162 [label="EVAL with clause\np(s(X94), X94).\nand substitutionX94 -> T43,\nT12 -> s(T43),\nX22 -> T43,\nT42 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 162 [arrowhead = none ];
162 -> 125;

163 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 163 [arrowhead = none ];
163 -> 126;

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

165 [label="EVAL with clause\np(s(X89), X89).\nand substitutionX89 -> T37,\nT12 -> s(T37),\nX22 -> T37,\nT36 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 165 [arrowhead = none ];
165 -> 121;

166 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 166 [arrowhead = none ];
166 -> 122;

167 [label="BACKTRACK\nfor clause: less(0, s(X2))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 167 [arrowhead = none ];
167 -> 75;

168 [label="ONLY EVAL with clause\nless(X55, X56) :- ','(no(zero(X55)), ','(p(X55, X57), ','(p(X56, X58), less(X57, X58)))).\nand substitutionT21 -> T24,\nX55 -> T24,\nX56 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 168 [arrowhead = none ];
168 -> 77;

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

170 [label="ONLY EVAL with clause\nno(X63) :- ','(call(X63), ','(!_13, failure(a))).\nand substitutionT24 -> T27,\nX63 -> zero(T27)", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 170 [arrowhead = none ];
170 -> 81;

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

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

173 [label="EVAL with clause\nzero(0).\nand substitutionT27 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 173 [arrowhead = none ];
173 -> 86;

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

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

176 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
87 -> 176 [arrowhead = none ];
176 -> 95;

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

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

179 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 179 [arrowhead = none ];
179 -> 96;

180 [label="ONLY EVAL with clause\nno(X70).\nand substitutionT27 -> T30,\nX70 -> zero(T30)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 180 [arrowhead = none ];
180 -> 101;

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

182 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T30), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 182 [arrowhead = none ];
182 -> 103;

183 [label="EVAL with clause\np(s(X75), X75).\nand substitutionX75 -> T33,\nT30 -> s(T33),\nX57 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 183 [arrowhead = none ];
183 -> 105;

184 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 184 [arrowhead = none ];
184 -> 107;

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

186 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX58 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 186 [arrowhead = none ];
186 -> 112;

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

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

189 [label="INSTANCE with matching:\nT21 -> T33", fontsize=14, style = filled, fillcolor = lightgrey];
114 -> 189 [arrowhead = none , style=dashed];
189 -> 70[style=dashed];

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

191 [label="INSTANCE with matching:\nT1 -> T21\nT2 -> T37", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 191 [arrowhead = none , style=dashed];
191 -> 1[style=dashed];

192 [label="INSTANCE with matching:\nT1 -> T21\nT2 -> T43", fontsize=14, style = filled, fillcolor = lightgrey];
125 -> 192 [arrowhead = none , style=dashed];
192 -> 1[style=dashed];

}

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f62_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f62_out1, s(z0)) → f1_out1
U1(f62_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f70_in(s(z0)) → U3(f112_in(z0), s(z0))
U3(f112_out1, s(z0)) → f70_out1
U3(f112_out2(z0), s(z1)) → f70_out1
f72_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f72_out1
f62_in(z0) → U5(f70_in(z0), f72_in(z0), z0)
U5(f70_out1, z0, z1) → f62_out1
U5(z0, f72_out1, z1) → f62_out2
f112_in(z0) → U6(f70_in(z0), f115_in(z0), z0)
U6(f70_out1, z0, z1) → f112_out1
U6(z0, f115_out1(z1), z2) → f112_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(U1'(f62_in(z0), s(z0)), F62_IN(z0))
F1_IN(s(z0)) → c2(U2'(f1_in(z0), s(z0)), F1_IN(z0))
F70_IN(s(z0)) → c6(U3'(f112_in(z0), s(z0)), F112_IN(z0))
F72_IN(z0) → c9(U4'(f1_in(z0), z0), F1_IN(z0))
F62_IN(z0) → c11(U5'(f70_in(z0), f72_in(z0), z0), F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(U6'(f70_in(z0), f115_in(z0), z0), F70_IN(z0))

S tuples:

F1_IN(s(z0)) → c1(U1'(f62_in(z0), s(z0)), F62_IN(z0))
F1_IN(s(z0)) → c2(U2'(f1_in(z0), s(z0)), F1_IN(z0))
F70_IN(s(z0)) → c6(U3'(f112_in(z0), s(z0)), F112_IN(z0))
F72_IN(z0) → c9(U4'(f1_in(z0), z0), F1_IN(z0))
F62_IN(z0) → c11(U5'(f70_in(z0), f72_in(z0), z0), F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(U6'(f70_in(z0), f115_in(z0), z0), F70_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f70_in, U3, f72_in, U4, f62_in, U5, f112_in, U6

Defined Pair Symbols:

F1_IN, F70_IN, F72_IN, F62_IN, F112_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

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

Removed 6 trailing tuple parts

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f62_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f62_out1, s(z0)) → f1_out1
U1(f62_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f70_in(s(z0)) → U3(f112_in(z0), s(z0))
U3(f112_out1, s(z0)) → f70_out1
U3(f112_out2(z0), s(z1)) → f70_out1
f72_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f72_out1
f62_in(z0) → U5(f70_in(z0), f72_in(z0), z0)
U5(f70_out1, z0, z1) → f62_out1
U5(z0, f72_out1, z1) → f62_out2
f112_in(z0) → U6(f70_in(z0), f115_in(z0), z0)
U6(f70_out1, z0, z1) → f112_out1
U6(z0, f115_out1(z1), z2) → f112_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F70_IN(s(z0)) → c6(F112_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

S tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F70_IN(s(z0)) → c6(F112_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f70_in, U3, f72_in, U4, f62_in, U5, f112_in, U6

Defined Pair Symbols:

F1_IN, F70_IN, F72_IN, F62_IN, F112_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(17) 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(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F70_IN(s(z0)) → c6(F112_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

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

POL(F112_IN(x₁)) = 0
POL(F1_IN(x₁)) = x₁
POL(F62_IN(x₁)) = x₁
POL(F70_IN(x₁)) = 0
POL(F72_IN(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f62_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f62_out1, s(z0)) → f1_out1
U1(f62_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f70_in(s(z0)) → U3(f112_in(z0), s(z0))
U3(f112_out1, s(z0)) → f70_out1
U3(f112_out2(z0), s(z1)) → f70_out1
f72_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f72_out1
f62_in(z0) → U5(f70_in(z0), f72_in(z0), z0)
U5(f70_out1, z0, z1) → f62_out1
U5(z0, f72_out1, z1) → f62_out2
f112_in(z0) → U6(f70_in(z0), f115_in(z0), z0)
U6(f70_out1, z0, z1) → f112_out1
U6(z0, f115_out1(z1), z2) → f112_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F70_IN(s(z0)) → c6(F112_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

S tuples:

F70_IN(s(z0)) → c6(F112_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

K tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))

Defined Rule Symbols:

f1_in, U1, U2, f70_in, U3, f72_in, U4, f62_in, U5, f112_in, U6

Defined Pair Symbols:

F1_IN, F70_IN, F72_IN, F62_IN, F112_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(19) CdtKnowledgeProof (EQUIVALENT transformation)

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

F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f62_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f62_out1, s(z0)) → f1_out1
U1(f62_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f70_in(s(z0)) → U3(f112_in(z0), s(z0))
U3(f112_out1, s(z0)) → f70_out1
U3(f112_out2(z0), s(z1)) → f70_out1
f72_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f72_out1
f62_in(z0) → U5(f70_in(z0), f72_in(z0), z0)
U5(f70_out1, z0, z1) → f62_out1
U5(z0, f72_out1, z1) → f62_out2
f112_in(z0) → U6(f70_in(z0), f115_in(z0), z0)
U6(f70_out1, z0, z1) → f112_out1
U6(z0, f115_out1(z1), z2) → f112_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F70_IN(s(z0)) → c6(F112_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

S tuples:

F70_IN(s(z0)) → c6(F112_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

K tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))

Defined Rule Symbols:

f1_in, U1, U2, f70_in, U3, f72_in, U4, f62_in, U5, f112_in, U6

Defined Pair Symbols:

F1_IN, F70_IN, F72_IN, F62_IN, F112_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

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

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

F70_IN(s(z0)) → c6(F112_IN(z0))

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F70_IN(s(z0)) → c6(F112_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

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

POL(F112_IN(x₁)) = x₁
POL(F1_IN(x₁)) = x₁²
POL(F62_IN(x₁)) = x₁ + x₁²
POL(F70_IN(x₁)) = x₁
POL(F72_IN(x₁)) = x₁²
POL(c1(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f62_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f62_out1, s(z0)) → f1_out1
U1(f62_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f70_in(s(z0)) → U3(f112_in(z0), s(z0))
U3(f112_out1, s(z0)) → f70_out1
U3(f112_out2(z0), s(z1)) → f70_out1
f72_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f72_out1
f62_in(z0) → U5(f70_in(z0), f72_in(z0), z0)
U5(f70_out1, z0, z1) → f62_out1
U5(z0, f72_out1, z1) → f62_out2
f112_in(z0) → U6(f70_in(z0), f115_in(z0), z0)
U6(f70_out1, z0, z1) → f112_out1
U6(z0, f115_out1(z1), z2) → f112_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F70_IN(s(z0)) → c6(F112_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F112_IN(z0) → c14(F70_IN(z0))

S tuples:

F112_IN(z0) → c14(F70_IN(z0))

K tuples:

F1_IN(s(z0)) → c1(F62_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F62_IN(z0) → c11(F70_IN(z0), F72_IN(z0))
F72_IN(z0) → c9(F1_IN(z0))
F70_IN(s(z0)) → c6(F112_IN(z0))

Defined Rule Symbols:

f1_in, U1, U2, f70_in, U3, f72_in, U4, f62_in, U5, f112_in, U6

Defined Pair Symbols:

F1_IN, F70_IN, F72_IN, F62_IN, F112_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14