Runtime Complexity proof of /tmp/tmpPh0CGl/divminus2.pl

Runtime Complexity of the query pattern
div(g,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), 178 ms)

↳2 CdtProblem

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

    ↳4 CdtProblem

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

    ↳6 CdtProblem

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

    ↳8 CdtProblem

    ↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 89 ms)

    ↳10 CdtProblem

    ↳11 CdtKnowledgeProof (⇔, 0 ms)

    ↳12 CdtProblem

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

↳14 CdtProblem

    ↳15 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 6 ms)

    ↳16 CdtProblem

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

    ↳18 CdtProblem

    ↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 272 ms)

    ↳20 CdtProblem

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

    ↳22 CdtProblem

    ↳23 CdtKnowledgeProof (⇔, 0 ms)

    ↳24 CdtProblem

    ↳25 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 335 ms)

    ↳26 CdtProblem

    ↳27 SIsEmptyProof (⇔, 0 ms)

    ↳28 BOUNDS(O(1), O(1))

(0) Obligation:

Clauses:

div(0, Y, 0) :- no(zero(Y)).
div(X, Y, s(Z)) :- ','(no(zero(X)), ','(no(zero(Y)), ','(minus(X, Y, U), div(U, Y, Z)))).
minus(0, Y, 0).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X1).
failure(b).

Query: div(g,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: div(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: div(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: no(zero(T6)) | div(0, T6, T3), SCOPE: 1, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: div(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nX4 is free\ndiv(T1, T2, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: no(zero(T6)), SCOPE: 2, CLAUSE: 6 | no(zero(T6)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T6, T3), SCOPE: 1, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(call(zero(T9)), ','(!_2, failure(a))) | no(zero(T9)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T9, T3), SCOPE: 1, CLAUSE: 1\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(zero(T9), ','(!_2, failure(a))) | ?_3 | no(zero(T9)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T9, T3), SCOPE: 1, CLAUSE: 1\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(zero(T9), ','(!_2, failure(a))), SCOPE: 4, CLAUSE: 5 | ?_4 | ?_3 | no(zero(T9)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T9, T3), SCOPE: 1, CLAUSE: 1\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(!_2, failure(a)) | ?_4 | ?_3 | no(zero(0)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ?_4 | ?_3 | no(zero(T9)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T9, T3), SCOPE: 1, CLAUSE: 1\n\nT9 is ground\nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: failure(a) | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: failure(a), SCOPE: 5, CLAUSE: 8 | ?_5 | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ?_5 | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13))))\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))), SCOPE: 6, CLAUSE: 6 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))), SCOPE: 6, CLAUSE: 7\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(','(call(zero(0)), ','(!_6, failure(a))), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))) | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))), SCOPE: 6, CLAUSE: 7\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(zero(0), ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13))))) | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))), SCOPE: 6, CLAUSE: 7\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(zero(0), ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13))))), SCOPE: 8, CLAUSE: 5 | ?_8 | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))), SCOPE: 6, CLAUSE: 7\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))) | ?_8 | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))), SCOPE: 6, CLAUSE: 7\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13))))\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X18), div(X18, 0, T13)))), SCOPE: 9, CLAUSE: 8\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ?_3 | no(zero(T9)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T9, T3), SCOPE: 1, CLAUSE: 1\n\nT9 is ground\nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: no(zero(T9)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T9, T3), SCOPE: 1, CLAUSE: 1\n\nT9 is ground\nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: true | ?_2 | div(0, T16, T3), SCOPE: 1, CLAUSE: 1\n\nT16 is ground\nzero(T16) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ?_2 | div(0, T16, T3), SCOPE: 1, CLAUSE: 1\n\nT16 is ground\nzero(T16) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: div(0, T16, T3), SCOPE: 1, CLAUSE: 1\n\nT16 is ground\nzero(T16) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(no(zero(0)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23))))\n\nT21 is ground\nX39 is free\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(no(zero(0)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))), SCOPE: 10, CLAUSE: 6 | ','(no(zero(0)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))), SCOPE: 10, CLAUSE: 7\n\nT21 is ground\nX39 is free\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(','(call(zero(0)), ','(!_10, failure(a))), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))) | ','(no(zero(0)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))), SCOPE: 10, CLAUSE: 7\n\nT21 is ground\nX39 is free\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(zero(0), ','(','(!_10, failure(a)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23))))) | ?_11 | ','(no(zero(0)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))), SCOPE: 10, CLAUSE: 7\n\nT21 is ground\nX39 is free\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(zero(0), ','(','(!_10, failure(a)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23))))), SCOPE: 12, CLAUSE: 5 | ?_12 | ?_11 | ','(no(zero(0)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))), SCOPE: 10, CLAUSE: 7\n\nT21 is ground\nX39 is free\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(','(!_10, failure(a)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))) | ?_12 | ?_11 | ','(no(zero(0)), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))), SCOPE: 10, CLAUSE: 7\n\nT21 is ground\nX39 is free\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(failure(a), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23))))\n\nT21 is ground\nX39 is free\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(failure(a), ','(no(zero(T21)), ','(minus(0, T21, X39), div(X39, T21, T23)))), SCOPE: 13, CLAUSE: 8\n\nT21 is ground\nX39 is free\nzero(T21) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(no(zero(T34)), ','(no(zero(T35)), ','(minus(T34, T35, X57), div(X57, T35, T37))))\n\nT34 is ground\nT35 is ground\nX4 is free\nX57 is free\ndiv(T34, T35, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(no(zero(T34)), ','(no(zero(T35)), ','(minus(T34, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 6 | ','(no(zero(T34)), ','(no(zero(T35)), ','(minus(T34, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 7\n\nT34 is ground\nT35 is ground\nX4 is free\nX57 is free\ndiv(T34, T35, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(','(call(zero(T42)), ','(!_14, failure(a))), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37)))) | ','(no(zero(T42)), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 7\n\nT35 is ground\nT42 is ground\nX4 is free\nX57 is free\ndiv(T42, T35, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(zero(T42), ','(','(!_14, failure(a)), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37))))) | ?_15 | ','(no(zero(T42)), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 7\n\nT35 is ground\nT42 is ground\nX4 is free\nX57 is free\ndiv(T42, T35, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(zero(T42), ','(','(!_14, failure(a)), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37))))), SCOPE: 16, CLAUSE: 5 | ?_16 | ?_15 | ','(no(zero(T42)), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 7\n\nT35 is ground\nT42 is ground\nX4 is free\nX57 is free\ndiv(T42, T35, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(','(!_14, failure(a)), ','(no(zero(T35)), ','(minus(0, T35, X57), div(X57, T35, T37)))) | ?_16 | ?_15 | ','(no(zero(0)), ','(no(zero(T35)), ','(minus(0, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 7\n\nT35 is ground\nX4 is free\nX57 is free\ndiv(0, T35, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ?_16 | ?_15 | ','(no(zero(T42)), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 7\n\nT35 is ground\nT42 is ground\nX4 is free\nX57 is free\ndiv(T42, T35, T3) !=? div(0, X4, 0)\nzero(T42) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(failure(a), ','(no(zero(T35)), ','(minus(0, T35, X57), div(X57, T35, T37))))\n\nT35 is ground\nX4 is free\nX57 is free\ndiv(0, T35, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(failure(a), ','(no(zero(T35)), ','(minus(0, T35, X57), div(X57, T35, T37)))), SCOPE: 17, CLAUSE: 8\n\nT35 is ground\nX4 is free\nX57 is free\ndiv(0, T35, T3) !=? div(0, X4, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ?_15 | ','(no(zero(T42)), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 7\n\nT35 is ground\nT42 is ground\nX4 is free\nX57 is free\ndiv(T42, T35, T3) !=? div(0, X4, 0)\nzero(T42) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(no(zero(T42)), ','(no(zero(T35)), ','(minus(T42, T35, X57), div(X57, T35, T37)))), SCOPE: 14, CLAUSE: 7\n\nT35 is ground\nT42 is ground\nX4 is free\nX57 is free\ndiv(T42, T35, T3) !=? div(0, X4, 0)\nzero(T42) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(no(zero(T35)), ','(minus(T51, T35, X57), div(X57, T35, T37)))\n\nT35 is ground\nT51 is ground\nX4 is free\nX57 is free\ndiv(T51, T35, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(no(zero(T35)), ','(minus(T51, T35, X57), div(X57, T35, T37))), SCOPE: 18, CLAUSE: 6 | ','(no(zero(T35)), ','(minus(T51, T35, X57), div(X57, T35, T37))), SCOPE: 18, CLAUSE: 7\n\nT35 is ground\nT51 is ground\nX4 is free\nX57 is free\ndiv(T51, T35, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ','(','(call(zero(T58)), ','(!_18, failure(a))), ','(minus(T51, T58, X57), div(X57, T58, T37))) | ','(no(zero(T58)), ','(minus(T51, T58, X57), div(X57, T58, T37))), SCOPE: 18, CLAUSE: 7\n\nT51 is ground\nT58 is ground\nX4 is free\nX57 is free\ndiv(T51, T58, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(zero(T58), ','(','(!_18, failure(a)), ','(minus(T51, T58, X57), div(X57, T58, T37)))) | ?_19 | ','(no(zero(T58)), ','(minus(T51, T58, X57), div(X57, T58, T37))), SCOPE: 18, CLAUSE: 7\n\nT51 is ground\nT58 is ground\nX4 is free\nX57 is free\ndiv(T51, T58, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(zero(T58), ','(','(!_18, failure(a)), ','(minus(T51, T58, X57), div(X57, T58, T37)))), SCOPE: 20, CLAUSE: 5 | ?_20 | ?_19 | ','(no(zero(T58)), ','(minus(T51, T58, X57), div(X57, T58, T37))), SCOPE: 18, CLAUSE: 7\n\nT51 is ground\nT58 is ground\nX4 is free\nX57 is free\ndiv(T51, T58, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(','(!_18, failure(a)), ','(minus(T51, 0, X57), div(X57, 0, T37))) | ?_20 | ?_19 | ','(no(zero(0)), ','(minus(T51, 0, X57), div(X57, 0, T37))), SCOPE: 18, CLAUSE: 7\n\nT51 is ground\nX4 is free\nX57 is free\ndiv(T51, 0, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ?_20 | ?_19 | ','(no(zero(T58)), ','(minus(T51, T58, X57), div(X57, T58, T37))), SCOPE: 18, CLAUSE: 7\n\nT51 is ground\nT58 is ground\nX4 is free\nX57 is free\ndiv(T51, T58, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)\nzero(T58) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(failure(a), ','(minus(T51, 0, X57), div(X57, 0, T37)))\n\nT51 is ground\nX4 is free\nX57 is free\ndiv(T51, 0, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(failure(a), ','(minus(T51, 0, X57), div(X57, 0, T37))), SCOPE: 21, CLAUSE: 8\n\nT51 is ground\nX4 is free\nX57 is free\ndiv(T51, 0, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ?_19 | ','(no(zero(T58)), ','(minus(T51, T58, X57), div(X57, T58, T37))), SCOPE: 18, CLAUSE: 7\n\nT51 is ground\nT58 is ground\nX4 is free\nX57 is free\ndiv(T51, T58, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)\nzero(T58) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(no(zero(T58)), ','(minus(T51, T58, X57), div(X57, T58, T37))), SCOPE: 18, CLAUSE: 7\n\nT51 is ground\nT58 is ground\nX4 is free\nX57 is free\ndiv(T51, T58, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)\nzero(T58) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ','(minus(T51, T68, X57), div(X57, T68, T37))\n\nT51 is ground\nT68 is ground\nX4 is free\nX57 is free\ndiv(T51, T68, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)\nzero(T68) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: minus(T51, T68, X57)\n\nT51 is ground\nT68 is ground\nX4 is free\nX57 is free\ndiv(T51, T68, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)\nzero(T68) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: div(T75, T68, T37)\n\nT51 is ground\nT68 is ground\nT75 is ground\nX4 is free\ndiv(T51, T68, T3) !=? div(0, X4, 0)\nzero(T68) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: minus(T51, T68, X57), SCOPE: 22, CLAUSE: 2 | minus(T51, T68, X57), SCOPE: 22, CLAUSE: 3 | minus(T51, T68, X57), SCOPE: 22, CLAUSE: 4\n\nT51 is ground\nT68 is ground\nX4 is free\nX57 is free\ndiv(T51, T68, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)\nzero(T68) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: minus(T51, T68, X57), SCOPE: 22, CLAUSE: 3 | minus(T51, T68, X57), SCOPE: 22, CLAUSE: 4\n\nT51 is ground\nT68 is ground\nX4 is free\nX57 is free\ndiv(T51, T68, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)\nzero(T68) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: minus(T51, T68, X57), SCOPE: 22, CLAUSE: 4\n\nT51 is ground\nT68 is ground\nX4 is free\nX57 is free\ndiv(T51, T68, T3) !=? div(0, X4, 0)\nzero(T51) !=? zero(0)\nzero(T68) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: minus(T88, T89, X123)\n\nT88 is ground\nT89 is ground\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: minus(T88, T89, X123), SCOPE: 23, CLAUSE: 2 | minus(T88, T89, X123), SCOPE: 23, CLAUSE: 3 | minus(T88, T89, X123), SCOPE: 23, CLAUSE: 4\n\nT88 is ground\nT89 is ground\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: true | minus(0, T94, X123), SCOPE: 23, CLAUSE: 3 | minus(0, T94, X123), SCOPE: 23, CLAUSE: 4\n\nT94 is ground\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: minus(T88, T89, X123), SCOPE: 23, CLAUSE: 3 | minus(T88, T89, X123), SCOPE: 23, CLAUSE: 4\n\nT88 is ground\nT89 is ground\nX123 is free\nX128 is free\nminus(T88, T89, X123) !=? minus(0, X128, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: minus(0, T94, X123), SCOPE: 23, CLAUSE: 3 | minus(0, T94, X123), SCOPE: 23, CLAUSE: 4\n\nT94 is ground\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: true | minus(0, 0, X123), SCOPE: 23, CLAUSE: 4\n\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: minus(0, T94, X123), SCOPE: 23, CLAUSE: 4\n\nT94 is ground\nX123 is free\nX131 is free\nminus(0, T94, X123) !=? minus(X131, 0, X131)", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: minus(0, 0, X123), SCOPE: 23, CLAUSE: 4\n\nX123 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: true | minus(T97, 0, X123), SCOPE: 23, CLAUSE: 4\n\nT97 is ground\nX123 is free\nX128 is free\nminus(T97, 0, X123) !=? minus(0, X128, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: minus(T88, T89, X123), SCOPE: 23, CLAUSE: 4\n\nT88 is ground\nT89 is ground\nX123 is free\nX128 is free\nX140 is free\nminus(T88, T89, X123) !=? minus(0, X128, 0)\nminus(T88, T89, X123) !=? minus(X140, 0, X140)", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: minus(T97, 0, X123), SCOPE: 23, CLAUSE: 4\n\nT97 is ground\nX123 is free\nX128 is free\nminus(T97, 0, X123) !=? minus(0, X128, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: minus(T103, T104, X155)\n\nT103 is ground\nT104 is ground\nX155 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 173 [arrowhead = none ];
173 -> 3;

174 [label="EVAL with clause\ndiv(0, X4, 0) :- no(zero(X4)).\nand substitutionT1 -> 0,\nT2 -> T6,\nX4 -> T6,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 174 [arrowhead = none ];
174 -> 6;

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

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

177 [label="EVAL with clause\ndiv(X54, X55, s(X56)) :- ','(no(zero(X54)), ','(no(zero(X55)), ','(minus(X54, X55, X57), div(X57, X55, X56)))).\nand substitutionT1 -> T34,\nX54 -> T34,\nT2 -> T35,\nX55 -> T35,\nX56 -> T37,\nT3 -> s(T37),\nT36 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 177 [arrowhead = none ];
177 -> 80;

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

179 [label="ONLY EVAL with clause\nno(X7) :- ','(call(X7), ','(!_2, failure(a))).\nand substitutionT6 -> T9,\nX7 -> zero(T9)", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 179 [arrowhead = none ];
179 -> 11;

180 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
11 -> 180 [arrowhead = none ];
180 -> 13;

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

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

183 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 183 [arrowhead = none ];
183 -> 19;

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

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

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

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

188 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 188 [arrowhead = none ];
188 -> 27;

189 [label="EVAL with clause\ndiv(X15, X16, s(X17)) :- ','(no(zero(X15)), ','(no(zero(X16)), ','(minus(X15, X16, X18), div(X18, X16, X17)))).\nand substitutionX15 -> 0,\nX16 -> 0,\nX17 -> T13,\nT3 -> s(T13),\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 189 [arrowhead = none ];
189 -> 29;

190 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 190 [arrowhead = none ];
190 -> 31;

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

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

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

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

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

196 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 196 [arrowhead = none ];
196 -> 43;

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

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

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

200 [label="ONLY EVAL with clause\nno(X28).\nand substitutionT9 -> T16,\nX28 -> zero(T16)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 200 [arrowhead = none ];
200 -> 53;

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

202 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 202 [arrowhead = none ];
202 -> 58;

203 [label="EVAL with clause\ndiv(X36, X37, s(X38)) :- ','(no(zero(X36)), ','(no(zero(X37)), ','(minus(X36, X37, X39), div(X39, X37, X38)))).\nand substitutionX36 -> 0,\nT16 -> T21,\nX37 -> T21,\nX38 -> T23,\nT3 -> s(T23),\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 203 [arrowhead = none ];
203 -> 59;

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

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

206 [label="ONLY EVAL with clause\nno(X44) :- ','(call(X44), ','(!_10, failure(a))).\nand substitutionX44 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 206 [arrowhead = none ];
206 -> 65;

207 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
65 -> 207 [arrowhead = none ];
207 -> 67;

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

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

210 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 210 [arrowhead = none ];
210 -> 72;

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

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

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

214 [label="ONLY EVAL with clause\nno(X62) :- ','(call(X62), ','(!_14, failure(a))).\nand substitutionT34 -> T42,\nX62 -> zero(T42)", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 214 [arrowhead = none ];
214 -> 87;

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

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

217 [label="EVAL with clause\nzero(0).\nand substitutionT42 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 217 [arrowhead = none ];
217 -> 93;

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

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

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

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

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

223 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 223 [arrowhead = none ];
223 -> 104;

224 [label="ONLY EVAL with clause\nno(X71).\nand substitutionT42 -> T51,\nX71 -> zero(T51)", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 224 [arrowhead = none ];
224 -> 106;

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

226 [label="ONLY EVAL with clause\nno(X78) :- ','(call(X78), ','(!_18, failure(a))).\nand substitutionT35 -> T58,\nX78 -> zero(T58)", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 226 [arrowhead = none ];
226 -> 110;

227 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
110 -> 227 [arrowhead = none ];
227 -> 112;

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

229 [label="EVAL with clause\nzero(0).\nand substitutionT58 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 229 [arrowhead = none ];
229 -> 116;

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

231 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 231 [arrowhead = none ];
231 -> 119;

232 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 232 [arrowhead = none ];
232 -> 125;

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

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

235 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 235 [arrowhead = none ];
235 -> 127;

236 [label="ONLY EVAL with clause\nno(X93).\nand substitutionT58 -> T68,\nX93 -> zero(T68)", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 236 [arrowhead = none ];
236 -> 129;

237 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
129 -> 237 [arrowhead = none ];
237 -> 132;

238 [label="SPLIT 2\nnew knowledge:\nT51 is ground\nT68 is ground\nT75 is ground\nreplacements:X57 -> T75", fontsize=14, style = filled, fillcolor = violet];
129 -> 238 [arrowhead = none ];
238 -> 134;

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

240 [label="INSTANCE with matching:\nT1 -> T75\nT2 -> T68\nT3 -> T37", fontsize=14, style = filled, fillcolor = lightgrey];
134 -> 240 [arrowhead = none , style=dashed];
240 -> 2[style=dashed];

241 [label="BACKTRACK\nfor clause: minus(0, Y, 0)\nwith clash: (zero(T51), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 241 [arrowhead = none ];
241 -> 137;

242 [label="BACKTRACK\nfor clause: minus(X, 0, X)\nwith clash: (zero(T68), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 242 [arrowhead = none ];
242 -> 139;

243 [label="EVAL with clause\nminus(s(X120), s(X121), X122) :- minus(X120, X121, X122).\nand substitutionX120 -> T88,\nT51 -> s(T88),\nX121 -> T89,\nT68 -> s(T89),\nX57 -> X123,\nX122 -> X123", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 243 [arrowhead = none ];
243 -> 141;

244 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 244 [arrowhead = none ];
244 -> 143;

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

246 [label="EVAL with clause\nminus(0, X128, 0).\nand substitutionT88 -> 0,\nT89 -> T94,\nX128 -> T94,\nX123 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 246 [arrowhead = none ];
246 -> 147;

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

248 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 248 [arrowhead = none ];
248 -> 150;

249 [label="EVAL with clause\nminus(X140, 0, X140).\nand substitutionT88 -> T97,\nX140 -> T97,\nT89 -> 0,\nX123 -> T97", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 249 [arrowhead = none ];
249 -> 163;

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

251 [label="EVAL with clause\nminus(X131, 0, X131).\nand substitutionX131 -> 0,\nT94 -> 0,\nX123 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 251 [arrowhead = none ];
251 -> 153;

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

253 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
153 -> 253 [arrowhead = none ];
253 -> 155;

254 [label="BACKTRACK\nfor clause: minus(s(X), s(Y), Z) :- minus(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 254 [arrowhead = none ];
254 -> 160;

255 [label="BACKTRACK\nfor clause: minus(s(X), s(Y), Z) :- minus(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
155 -> 255 [arrowhead = none ];
255 -> 158;

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

257 [label="EVAL with clause\nminus(s(X152), s(X153), X154) :- minus(X152, X153, X154).\nand substitutionX152 -> T103,\nT88 -> s(T103),\nX153 -> T104,\nT89 -> s(T104),\nX123 -> X155,\nX154 -> X155", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 257 [arrowhead = none ];
257 -> 171;

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

259 [label="BACKTRACK\nfor clause: minus(s(X), s(Y), Z) :- minus(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
166 -> 259 [arrowhead = none ];
259 -> 168;

260 [label="INSTANCE with matching:\nT88 -> T103\nT89 -> T104\nX123 -> X155", fontsize=14, style = filled, fillcolor = lightgrey];
171 -> 260 [arrowhead = none , style=dashed];
260 -> 141[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1(0)
f2_in(z0, z1) → U1(f129_in(z0, z1), z0, z1)
U1(f129_out1(z0, z1), z2, z3) → f2_out1(s(z1))
f141_in(0, z0) → f141_out1(0)
f141_in(0, 0) → f141_out1(0)
f141_in(z0, 0) → f141_out1(z0)
f141_in(s(z0), s(z1)) → U2(f141_in(z0, z1), s(z0), s(z1))
U2(f141_out1(z0), s(z1), s(z2)) → f141_out1(z0)
f132_in(s(z0), s(z1)) → U3(f141_in(z0, z1), s(z0), s(z1))
U3(f141_out1(z0), s(z1), s(z2)) → f132_out1(z0)
f129_in(z0, z1) → U4(f132_in(z0, z1), z0, z1)
U4(f132_out1(z0), z1, z2) → U5(f2_in(z0, z2), z1, z2, z0)
U5(f2_out1(z0), z1, z2, z3) → f129_out1(z3, z0)

Tuples:

F2_IN(z0, z1) → c1(U1'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(U2'(f141_in(z0, z1), s(z0), s(z1)), F141_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c8(U3'(f141_in(z0, z1), s(z0), s(z1)), F141_IN(z0, z1))
F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(U5'(f2_in(z0, z2), z1, z2, z0), F2_IN(z0, z2))

S tuples:

F2_IN(z0, z1) → c1(U1'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(U2'(f141_in(z0, z1), s(z0), s(z1)), F141_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c8(U3'(f141_in(z0, z1), s(z0), s(z1)), F141_IN(z0, z1))
F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(U5'(f2_in(z0, z2), z1, z2, z0), F2_IN(z0, z2))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f141_in, U2, f132_in, U3, f129_in, U4, U5

Defined Pair Symbols:

F2_IN, F141_IN, F132_IN, F129_IN, U4'

Compound Symbols:

c1, c6, c8, c10, c11

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1(0)
f2_in(z0, z1) → U1(f129_in(z0, z1), z0, z1)
U1(f129_out1(z0, z1), z2, z3) → f2_out1(s(z1))
f141_in(0, z0) → f141_out1(0)
f141_in(0, 0) → f141_out1(0)
f141_in(z0, 0) → f141_out1(z0)
f141_in(s(z0), s(z1)) → U2(f141_in(z0, z1), s(z0), s(z1))
U2(f141_out1(z0), s(z1), s(z2)) → f141_out1(z0)
f132_in(s(z0), s(z1)) → U3(f141_in(z0, z1), s(z0), s(z1))
U3(f141_out1(z0), s(z1), s(z2)) → f132_out1(z0)
f129_in(z0, z1) → U4(f132_in(z0, z1), z0, z1)
U4(f132_out1(z0), z1, z2) → U5(f2_in(z0, z2), z1, z2, z0)
U5(f2_out1(z0), z1, z2, z3) → f129_out1(z3, z0)

Tuples:

F2_IN(z0, z1) → c1(U1'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(U2'(f141_in(z0, z1), s(z0), s(z1)), F141_IN(z0, z1))
F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(U5'(f2_in(z0, z2), z1, z2, z0), F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c(U3'(f141_in(z0, z1), s(z0), s(z1)))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))

S tuples:

F2_IN(z0, z1) → c1(U1'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(U2'(f141_in(z0, z1), s(z0), s(z1)), F141_IN(z0, z1))
F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(U5'(f2_in(z0, z2), z1, z2, z0), F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c(U3'(f141_in(z0, z1), s(z0), s(z1)))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f141_in, U2, f132_in, U3, f129_in, U4, U5

Defined Pair Symbols:

F2_IN, F141_IN, F129_IN, U4', F132_IN

Compound Symbols:

c1, c6, c10, c11, c

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

Removed 4 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1(0)
f2_in(z0, z1) → U1(f129_in(z0, z1), z0, z1)
U1(f129_out1(z0, z1), z2, z3) → f2_out1(s(z1))
f141_in(0, z0) → f141_out1(0)
f141_in(0, 0) → f141_out1(0)
f141_in(z0, 0) → f141_out1(z0)
f141_in(s(z0), s(z1)) → U2(f141_in(z0, z1), s(z0), s(z1))
U2(f141_out1(z0), s(z1), s(z2)) → f141_out1(z0)
f132_in(s(z0), s(z1)) → U3(f141_in(z0, z1), s(z0), s(z1))
U3(f141_out1(z0), s(z1), s(z2)) → f132_out1(z0)
f129_in(z0, z1) → U4(f132_in(z0, z1), z0, z1)
U4(f132_out1(z0), z1, z2) → U5(f2_in(z0, z2), z1, z2, z0)
U5(f2_out1(z0), z1, z2, z3) → f129_out1(z3, z0)

Tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c

S tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f141_in, U2, f132_in, U3, f129_in, U4, U5

Defined Pair Symbols:

F129_IN, F132_IN, F2_IN, F141_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, 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.

F132_IN(s(z0), s(z1)) → c

We considered the (Usable) Rules:

f132_in(s(z0), s(z1)) → U3(f141_in(z0, z1), s(z0), s(z1))
f141_in(0, z0) → f141_out1(0)
f141_in(0, 0) → f141_out1(0)
f141_in(z0, 0) → f141_out1(z0)
f141_in(s(z0), s(z1)) → U2(f141_in(z0, z1), s(z0), s(z1))
U3(f141_out1(z0), s(z1), s(z2)) → f132_out1(z0)
U2(f141_out1(z0), s(z1), s(z2)) → f141_out1(z0)

And the Tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c

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

POL(0) = 0
POL(F129_IN(x₁, x₂)) = [2] + x₁
POL(F132_IN(x₁, x₂)) = [2]
POL(F141_IN(x₁, x₂)) = [2]
POL(F2_IN(x₁, x₂)) = [2] + x₁
POL(U2(x₁, x₂, x₃)) = x₁
POL(U3(x₁, x₂, x₃)) = [1] + x₁
POL(U4'(x₁, x₂, x₃)) = x₁
POL(c) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(f132_in(x₁, x₂)) = x₁
POL(f132_out1(x₁)) = [2] + x₁
POL(f141_in(x₁, x₂)) = [2] + x₁
POL(f141_out1(x₁)) = [1] + x₁
POL(s(x₁)) = [3] + x₁

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1(0)
f2_in(z0, z1) → U1(f129_in(z0, z1), z0, z1)
U1(f129_out1(z0, z1), z2, z3) → f2_out1(s(z1))
f141_in(0, z0) → f141_out1(0)
f141_in(0, 0) → f141_out1(0)
f141_in(z0, 0) → f141_out1(z0)
f141_in(s(z0), s(z1)) → U2(f141_in(z0, z1), s(z0), s(z1))
U2(f141_out1(z0), s(z1), s(z2)) → f141_out1(z0)
f132_in(s(z0), s(z1)) → U3(f141_in(z0, z1), s(z0), s(z1))
U3(f141_out1(z0), s(z1), s(z2)) → f132_out1(z0)
f129_in(z0, z1) → U4(f132_in(z0, z1), z0, z1)
U4(f132_out1(z0), z1, z2) → U5(f2_in(z0, z2), z1, z2, z0)
U5(f2_out1(z0), z1, z2, z3) → f129_out1(z3, z0)

Tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c

S tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))

K tuples:

F132_IN(s(z0), s(z1)) → c

Defined Rule Symbols:

f2_in, U1, f141_in, U2, f132_in, U3, f129_in, U4, U5

Defined Pair Symbols:

F129_IN, F132_IN, F2_IN, F141_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, c

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

U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))

We considered the (Usable) Rules:

f132_in(s(z0), s(z1)) → U3(f141_in(z0, z1), s(z0), s(z1))
f141_in(0, z0) → f141_out1(0)
f141_in(0, 0) → f141_out1(0)
f141_in(z0, 0) → f141_out1(z0)
f141_in(s(z0), s(z1)) → U2(f141_in(z0, z1), s(z0), s(z1))
U3(f141_out1(z0), s(z1), s(z2)) → f132_out1(z0)
U2(f141_out1(z0), s(z1), s(z2)) → f141_out1(z0)

And the Tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c

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

POL(0) = 0
POL(F129_IN(x₁, x₂)) = x₁
POL(F132_IN(x₁, x₂)) = 0
POL(F141_IN(x₁, x₂)) = 0
POL(F2_IN(x₁, x₂)) = x₁
POL(U2(x₁, x₂, x₃)) = x₁
POL(U3(x₁, x₂, x₃)) = [1] + x₁
POL(U4'(x₁, x₂, x₃)) = x₁
POL(c) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(f132_in(x₁, x₂)) = x₁
POL(f132_out1(x₁)) = [1] + x₁
POL(f141_in(x₁, x₂)) = x₁
POL(f141_out1(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1(0)
f2_in(z0, z1) → U1(f129_in(z0, z1), z0, z1)
U1(f129_out1(z0, z1), z2, z3) → f2_out1(s(z1))
f141_in(0, z0) → f141_out1(0)
f141_in(0, 0) → f141_out1(0)
f141_in(z0, 0) → f141_out1(z0)
f141_in(s(z0), s(z1)) → U2(f141_in(z0, z1), s(z0), s(z1))
U2(f141_out1(z0), s(z1), s(z2)) → f141_out1(z0)
f132_in(s(z0), s(z1)) → U3(f141_in(z0, z1), s(z0), s(z1))
U3(f141_out1(z0), s(z1), s(z2)) → f132_out1(z0)
f129_in(z0, z1) → U4(f132_in(z0, z1), z0, z1)
U4(f132_out1(z0), z1, z2) → U5(f2_in(z0, z2), z1, z2, z0)
U5(f2_out1(z0), z1, z2, z3) → f129_out1(z3, z0)

Tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c

S tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))

K tuples:

F132_IN(s(z0), s(z1)) → c
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))

Defined Rule Symbols:

f2_in, U1, f141_in, U2, f132_in, U3, f129_in, U4, U5

Defined Pair Symbols:

F129_IN, F132_IN, F2_IN, F141_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, c

(11) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1(0)
f2_in(z0, z1) → U1(f129_in(z0, z1), z0, z1)
U1(f129_out1(z0, z1), z2, z3) → f2_out1(s(z1))
f141_in(0, z0) → f141_out1(0)
f141_in(0, 0) → f141_out1(0)
f141_in(z0, 0) → f141_out1(z0)
f141_in(s(z0), s(z1)) → U2(f141_in(z0, z1), s(z0), s(z1))
U2(f141_out1(z0), s(z1), s(z2)) → f141_out1(z0)
f132_in(s(z0), s(z1)) → U3(f141_in(z0, z1), s(z0), s(z1))
U3(f141_out1(z0), s(z1), s(z2)) → f132_out1(z0)
f129_in(z0, z1) → U4(f132_in(z0, z1), z0, z1)
U4(f132_out1(z0), z1, z2) → U5(f2_in(z0, z2), z1, z2, z0)
U5(f2_out1(z0), z1, z2, z3) → f129_out1(z3, z0)

Tuples:

F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F132_IN(s(z0), s(z1)) → c

S tuples:

F141_IN(s(z0), s(z1)) → c6(F141_IN(z0, z1))

K tuples:

F132_IN(s(z0), s(z1)) → c
U4'(f132_out1(z0), z1, z2) → c11(F2_IN(z0, z2))
F2_IN(z0, z1) → c1(F129_IN(z0, z1))
F129_IN(z0, z1) → c10(U4'(f132_in(z0, z1), z0, z1), F132_IN(z0, z1))
F132_IN(s(z0), s(z1)) → c(F141_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f141_in, U2, f132_in, U3, f129_in, U4, U5

Defined Pair Symbols:

F129_IN, F132_IN, F2_IN, F141_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, c

(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: div(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: div(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: no(zero(T5)) | div(0, T5, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: div(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nX3 is free\ndiv(T1, T2, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: no(zero(T5)), SCOPE: 2, CLAUSE: 6 | no(zero(T5)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T5, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(call(zero(T8)), ','(!_2, failure(a))) | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(zero(T8), ','(!_2, failure(a))) | ?_3 | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(zero(T8), ','(!_2, failure(a))), SCOPE: 4, CLAUSE: 5 | ?_4 | ?_3 | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(!_2, failure(a)) | ?_4 | ?_3 | no(zero(0)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ?_4 | ?_3 | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: failure(a) | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: failure(a), SCOPE: 5, CLAUSE: 8 | ?_5 | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ?_5 | div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: div(0, 0, T3), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12))))\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 6 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(','(call(zero(0)), ','(!_6, failure(a))), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))) | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(zero(0), ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12))))) | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(zero(0), ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12))))), SCOPE: 8, CLAUSE: 5 | ?_8 | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(','(!_6, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))) | ?_8 | ?_7 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 6, CLAUSE: 7\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12))))\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X17), div(X17, 0, T12)))), SCOPE: 9, CLAUSE: 8\n\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ?_3 | no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: no(zero(T8)), SCOPE: 2, CLAUSE: 7 | ?_2 | div(0, T8, T3), SCOPE: 1, CLAUSE: 1\n\nT8 is ground\nzero(T8) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true | ?_2 | div(0, T15, T3), SCOPE: 1, CLAUSE: 1\n\nT15 is ground\nzero(T15) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ?_2 | div(0, T15, T3), SCOPE: 1, CLAUSE: 1\n\nT15 is ground\nzero(T15) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: div(0, T15, T3), SCOPE: 1, CLAUSE: 1\n\nT15 is ground\nzero(T15) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(no(zero(0)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22))))\n\nT20 is ground\nX38 is free\nzero(T20) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(no(zero(0)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))), SCOPE: 10, CLAUSE: 6 | ','(no(zero(0)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))), SCOPE: 10, CLAUSE: 7\n\nT20 is ground\nX38 is free\nzero(T20) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(','(call(zero(0)), ','(!_10, failure(a))), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))) | ','(no(zero(0)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))), SCOPE: 10, CLAUSE: 7\n\nT20 is ground\nX38 is free\nzero(T20) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(zero(0), ','(','(!_10, failure(a)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22))))) | ?_11 | ','(no(zero(0)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))), SCOPE: 10, CLAUSE: 7\n\nT20 is ground\nX38 is free\nzero(T20) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(zero(0), ','(','(!_10, failure(a)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22))))), SCOPE: 12, CLAUSE: 5 | ?_12 | ?_11 | ','(no(zero(0)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))), SCOPE: 10, CLAUSE: 7\n\nT20 is ground\nX38 is free\nzero(T20) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(','(!_10, failure(a)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))) | ?_12 | ?_11 | ','(no(zero(0)), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))), SCOPE: 10, CLAUSE: 7\n\nT20 is ground\nX38 is free\nzero(T20) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(failure(a), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22))))\n\nT20 is ground\nX38 is free\nzero(T20) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(failure(a), ','(no(zero(T20)), ','(minus(0, T20, X38), div(X38, T20, T22)))), SCOPE: 13, CLAUSE: 8\n\nT20 is ground\nX38 is free\nzero(T20) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(no(zero(T30)), ','(no(zero(T31)), ','(minus(T30, T31, X52), div(X52, T31, T33))))\n\nT30 is ground\nT31 is ground\nX3 is free\nX52 is free\ndiv(T30, T31, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(no(zero(T30)), ','(no(zero(T31)), ','(minus(T30, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 6 | ','(no(zero(T30)), ','(no(zero(T31)), ','(minus(T30, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 7\n\nT30 is ground\nT31 is ground\nX3 is free\nX52 is free\ndiv(T30, T31, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(','(call(zero(T36)), ','(!_14, failure(a))), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33)))) | ','(no(zero(T36)), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 7\n\nT31 is ground\nT36 is ground\nX3 is free\nX52 is free\ndiv(T36, T31, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(zero(T36), ','(','(!_14, failure(a)), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33))))) | ?_15 | ','(no(zero(T36)), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 7\n\nT31 is ground\nT36 is ground\nX3 is free\nX52 is free\ndiv(T36, T31, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(zero(T36), ','(','(!_14, failure(a)), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33))))), SCOPE: 16, CLAUSE: 5 | ?_16 | ?_15 | ','(no(zero(T36)), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 7\n\nT31 is ground\nT36 is ground\nX3 is free\nX52 is free\ndiv(T36, T31, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(','(!_14, failure(a)), ','(no(zero(T31)), ','(minus(0, T31, X52), div(X52, T31, T33)))) | ?_16 | ?_15 | ','(no(zero(0)), ','(no(zero(T31)), ','(minus(0, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 7\n\nT31 is ground\nX3 is free\nX52 is free\ndiv(0, T31, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ?_16 | ?_15 | ','(no(zero(T36)), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 7\n\nT31 is ground\nT36 is ground\nX3 is free\nX52 is free\ndiv(T36, T31, T3) !=? div(0, X3, 0)\nzero(T36) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(failure(a), ','(no(zero(T31)), ','(minus(0, T31, X52), div(X52, T31, T33))))\n\nT31 is ground\nX3 is free\nX52 is free\ndiv(0, T31, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(failure(a), ','(no(zero(T31)), ','(minus(0, T31, X52), div(X52, T31, T33)))), SCOPE: 17, CLAUSE: 8\n\nT31 is ground\nX3 is free\nX52 is free\ndiv(0, T31, T3) !=? div(0, X3, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ?_15 | ','(no(zero(T36)), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 7\n\nT31 is ground\nT36 is ground\nX3 is free\nX52 is free\ndiv(T36, T31, T3) !=? div(0, X3, 0)\nzero(T36) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(no(zero(T36)), ','(no(zero(T31)), ','(minus(T36, T31, X52), div(X52, T31, T33)))), SCOPE: 14, CLAUSE: 7\n\nT31 is ground\nT36 is ground\nX3 is free\nX52 is free\ndiv(T36, T31, T3) !=? div(0, X3, 0)\nzero(T36) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(no(zero(T31)), ','(minus(T45, T31, X52), div(X52, T31, T33)))\n\nT31 is ground\nT45 is ground\nX3 is free\nX52 is free\ndiv(T45, T31, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(no(zero(T31)), ','(minus(T45, T31, X52), div(X52, T31, T33))), SCOPE: 18, CLAUSE: 6 | ','(no(zero(T31)), ','(minus(T45, T31, X52), div(X52, T31, T33))), SCOPE: 18, CLAUSE: 7\n\nT31 is ground\nT45 is ground\nX3 is free\nX52 is free\ndiv(T45, T31, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(','(call(zero(T52)), ','(!_18, failure(a))), ','(minus(T45, T52, X52), div(X52, T52, T33))) | ','(no(zero(T52)), ','(minus(T45, T52, X52), div(X52, T52, T33))), SCOPE: 18, CLAUSE: 7\n\nT45 is ground\nT52 is ground\nX3 is free\nX52 is free\ndiv(T45, T52, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(zero(T52), ','(','(!_18, failure(a)), ','(minus(T45, T52, X52), div(X52, T52, T33)))) | ?_19 | ','(no(zero(T52)), ','(minus(T45, T52, X52), div(X52, T52, T33))), SCOPE: 18, CLAUSE: 7\n\nT45 is ground\nT52 is ground\nX3 is free\nX52 is free\ndiv(T45, T52, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(zero(T52), ','(','(!_18, failure(a)), ','(minus(T45, T52, X52), div(X52, T52, T33)))), SCOPE: 20, CLAUSE: 5 | ?_20 | ?_19 | ','(no(zero(T52)), ','(minus(T45, T52, X52), div(X52, T52, T33))), SCOPE: 18, CLAUSE: 7\n\nT45 is ground\nT52 is ground\nX3 is free\nX52 is free\ndiv(T45, T52, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(','(!_18, failure(a)), ','(minus(T45, 0, X52), div(X52, 0, T33))) | ?_20 | ?_19 | ','(no(zero(0)), ','(minus(T45, 0, X52), div(X52, 0, T33))), SCOPE: 18, CLAUSE: 7\n\nT45 is ground\nX3 is free\nX52 is free\ndiv(T45, 0, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ?_20 | ?_19 | ','(no(zero(T52)), ','(minus(T45, T52, X52), div(X52, T52, T33))), SCOPE: 18, CLAUSE: 7\n\nT45 is ground\nT52 is ground\nX3 is free\nX52 is free\ndiv(T45, T52, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)\nzero(T52) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(failure(a), ','(minus(T45, 0, X52), div(X52, 0, T33)))\n\nT45 is ground\nX3 is free\nX52 is free\ndiv(T45, 0, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(failure(a), ','(minus(T45, 0, X52), div(X52, 0, T33))), SCOPE: 21, CLAUSE: 8\n\nT45 is ground\nX3 is free\nX52 is free\ndiv(T45, 0, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ?_19 | ','(no(zero(T52)), ','(minus(T45, T52, X52), div(X52, T52, T33))), SCOPE: 18, CLAUSE: 7\n\nT45 is ground\nT52 is ground\nX3 is free\nX52 is free\ndiv(T45, T52, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)\nzero(T52) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(no(zero(T52)), ','(minus(T45, T52, X52), div(X52, T52, T33))), SCOPE: 18, CLAUSE: 7\n\nT45 is ground\nT52 is ground\nX3 is free\nX52 is free\ndiv(T45, T52, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)\nzero(T52) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(minus(T45, T62, X52), div(X52, T62, T33))\n\nT45 is ground\nT62 is ground\nX3 is free\nX52 is free\ndiv(T45, T62, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: minus(T45, T62, X52)\n\nT45 is ground\nT62 is ground\nX3 is free\nX52 is free\ndiv(T45, T62, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: div(T69, T62, T33)\n\nT45 is ground\nT62 is ground\nT69 is ground\nX3 is free\ndiv(T45, T62, T3) !=? div(0, X3, 0)\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: minus(T45, T62, X52), SCOPE: 22, CLAUSE: 2 | minus(T45, T62, X52), SCOPE: 22, CLAUSE: 3 | minus(T45, T62, X52), SCOPE: 22, CLAUSE: 4\n\nT45 is ground\nT62 is ground\nX3 is free\nX52 is free\ndiv(T45, T62, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: minus(T45, T62, X52), SCOPE: 22, CLAUSE: 3 | minus(T45, T62, X52), SCOPE: 22, CLAUSE: 4\n\nT45 is ground\nT62 is ground\nX3 is free\nX52 is free\ndiv(T45, T62, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: minus(T45, T62, X52), SCOPE: 22, CLAUSE: 4\n\nT45 is ground\nT62 is ground\nX3 is free\nX52 is free\ndiv(T45, T62, T3) !=? div(0, X3, 0)\nzero(T45) !=? zero(0)\nzero(T62) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: minus(T82, T83, X116)\n\nT82 is ground\nT83 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: minus(T82, T83, X116), SCOPE: 23, CLAUSE: 2 | minus(T82, T83, X116), SCOPE: 23, CLAUSE: 3 | minus(T82, T83, X116), SCOPE: 23, CLAUSE: 4\n\nT82 is ground\nT83 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: true | minus(0, T88, X116), SCOPE: 23, CLAUSE: 3 | minus(0, T88, X116), SCOPE: 23, CLAUSE: 4\n\nT88 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: minus(T82, T83, X116), SCOPE: 23, CLAUSE: 3 | minus(T82, T83, X116), SCOPE: 23, CLAUSE: 4\n\nT82 is ground\nT83 is ground\nX116 is free\nX121 is free\nminus(T82, T83, X116) !=? minus(0, X121, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: minus(0, T88, X116), SCOPE: 23, CLAUSE: 3 | minus(0, T88, X116), SCOPE: 23, CLAUSE: 4\n\nT88 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: true | minus(0, 0, X116), SCOPE: 23, CLAUSE: 4\n\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: minus(0, T88, X116), SCOPE: 23, CLAUSE: 4\n\nT88 is ground\nX116 is free\nX124 is free\nminus(0, T88, X116) !=? minus(X124, 0, X124)", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: minus(0, 0, X116), SCOPE: 23, CLAUSE: 4\n\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: true | minus(T91, 0, X116), SCOPE: 23, CLAUSE: 4\n\nT91 is ground\nX116 is free\nX121 is free\nminus(T91, 0, X116) !=? minus(0, X121, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: minus(T82, T83, X116), SCOPE: 23, CLAUSE: 4\n\nT82 is ground\nT83 is ground\nX116 is free\nX121 is free\nX133 is free\nminus(T82, T83, X116) !=? minus(0, X121, 0)\nminus(T82, T83, X116) !=? minus(X133, 0, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: minus(T91, 0, X116), SCOPE: 23, CLAUSE: 4\n\nT91 is ground\nX116 is free\nX121 is free\nminus(T91, 0, X116) !=? minus(0, X121, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: minus(T97, T98, X148)\n\nT97 is ground\nT98 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 175 [arrowhead = none ];
175 -> 4;

176 [label="EVAL with clause\ndiv(0, X3, 0) :- no(zero(X3)).\nand substitutionT1 -> 0,\nT2 -> T5,\nX3 -> T5,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 176 [arrowhead = none ];
176 -> 5;

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

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

179 [label="EVAL with clause\ndiv(X49, X50, s(X51)) :- ','(no(zero(X49)), ','(no(zero(X50)), ','(minus(X49, X50, X52), div(X52, X50, X51)))).\nand substitutionT1 -> T30,\nX49 -> T30,\nT2 -> T31,\nX50 -> T31,\nX51 -> T33,\nT3 -> s(T33),\nT32 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 179 [arrowhead = none ];
179 -> 79;

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

181 [label="ONLY EVAL with clause\nno(X6) :- ','(call(X6), ','(!_2, failure(a))).\nand substitutionT5 -> T8,\nX6 -> zero(T8)", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 181 [arrowhead = none ];
181 -> 12;

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

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

184 [label="EVAL with clause\nzero(0).\nand substitutionT8 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 184 [arrowhead = none ];
184 -> 18;

185 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 185 [arrowhead = none ];
185 -> 20;

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

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

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

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

190 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 190 [arrowhead = none ];
190 -> 28;

191 [label="EVAL with clause\ndiv(X14, X15, s(X16)) :- ','(no(zero(X14)), ','(no(zero(X15)), ','(minus(X14, X15, X17), div(X17, X15, X16)))).\nand substitutionX14 -> 0,\nX15 -> 0,\nX16 -> T12,\nT3 -> s(T12),\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 191 [arrowhead = none ];
191 -> 30;

192 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 192 [arrowhead = none ];
192 -> 32;

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

194 [label="ONLY EVAL with clause\nno(X22) :- ','(call(X22), ','(!_6, failure(a))).\nand substitutionX22 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 194 [arrowhead = none ];
194 -> 36;

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

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

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

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

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

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

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

202 [label="ONLY EVAL with clause\nno(X27).\nand substitutionT8 -> T15,\nX27 -> zero(T15)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 202 [arrowhead = none ];
202 -> 55;

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

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

205 [label="EVAL with clause\ndiv(X35, X36, s(X37)) :- ','(no(zero(X35)), ','(no(zero(X36)), ','(minus(X35, X36, X38), div(X38, X36, X37)))).\nand substitutionX35 -> 0,\nT15 -> T20,\nX36 -> T20,\nX37 -> T22,\nT3 -> s(T22),\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 205 [arrowhead = none ];
205 -> 60;

206 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 206 [arrowhead = none ];
206 -> 62;

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

208 [label="ONLY EVAL with clause\nno(X43) :- ','(call(X43), ','(!_10, failure(a))).\nand substitutionX43 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 208 [arrowhead = none ];
208 -> 66;

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

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

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

212 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 212 [arrowhead = none ];
212 -> 74;

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

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

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

216 [label="ONLY EVAL with clause\nno(X55) :- ','(call(X55), ','(!_14, failure(a))).\nand substitutionT30 -> T36,\nX55 -> zero(T36)", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 216 [arrowhead = none ];
216 -> 85;

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

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

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

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

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

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

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

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

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

226 [label="ONLY EVAL with clause\nno(X64).\nand substitutionT36 -> T45,\nX64 -> zero(T45)", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 226 [arrowhead = none ];
226 -> 105;

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

228 [label="ONLY EVAL with clause\nno(X71) :- ','(call(X71), ','(!_18, failure(a))).\nand substitutionT31 -> T52,\nX71 -> zero(T52)", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 228 [arrowhead = none ];
228 -> 109;

229 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
109 -> 229 [arrowhead = none ];
229 -> 111;

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

231 [label="EVAL with clause\nzero(0).\nand substitutionT52 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 231 [arrowhead = none ];
231 -> 115;

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

233 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 233 [arrowhead = none ];
233 -> 120;

234 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 234 [arrowhead = none ];
234 -> 126;

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

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

237 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 237 [arrowhead = none ];
237 -> 128;

238 [label="ONLY EVAL with clause\nno(X86).\nand substitutionT52 -> T62,\nX86 -> zero(T62)", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 238 [arrowhead = none ];
238 -> 130;

239 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
130 -> 239 [arrowhead = none ];
239 -> 131;

240 [label="SPLIT 2\nnew knowledge:\nT45 is ground\nT62 is ground\nT69 is ground\nreplacements:X52 -> T69", fontsize=14, style = filled, fillcolor = violet];
130 -> 240 [arrowhead = none ];
240 -> 133;

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

242 [label="INSTANCE with matching:\nT1 -> T69\nT2 -> T62\nT3 -> T33", fontsize=14, style = filled, fillcolor = lightgrey];
133 -> 242 [arrowhead = none , style=dashed];
242 -> 1[style=dashed];

243 [label="BACKTRACK\nfor clause: minus(0, Y, 0)\nwith clash: (zero(T45), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 243 [arrowhead = none ];
243 -> 138;

244 [label="BACKTRACK\nfor clause: minus(X, 0, X)\nwith clash: (zero(T62), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 244 [arrowhead = none ];
244 -> 140;

245 [label="EVAL with clause\nminus(s(X113), s(X114), X115) :- minus(X113, X114, X115).\nand substitutionX113 -> T82,\nT45 -> s(T82),\nX114 -> T83,\nT62 -> s(T83),\nX52 -> X116,\nX115 -> X116", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 245 [arrowhead = none ];
245 -> 142;

246 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
140 -> 246 [arrowhead = none ];
246 -> 144;

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

248 [label="EVAL with clause\nminus(0, X121, 0).\nand substitutionT82 -> 0,\nT83 -> T88,\nX121 -> T88,\nX116 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 248 [arrowhead = none ];
248 -> 149;

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

250 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 250 [arrowhead = none ];
250 -> 152;

251 [label="EVAL with clause\nminus(X133, 0, X133).\nand substitutionT82 -> T91,\nX133 -> T91,\nT83 -> 0,\nX116 -> T91", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 251 [arrowhead = none ];
251 -> 165;

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

253 [label="EVAL with clause\nminus(X124, 0, X124).\nand substitutionX124 -> 0,\nT88 -> 0,\nX116 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
152 -> 253 [arrowhead = none ];
253 -> 156;

254 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 254 [arrowhead = none ];
254 -> 157;

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

256 [label="BACKTRACK\nfor clause: minus(s(X), s(Y), Z) :- minus(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 256 [arrowhead = none ];
256 -> 162;

257 [label="BACKTRACK\nfor clause: minus(s(X), s(Y), Z) :- minus(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
159 -> 257 [arrowhead = none ];
257 -> 161;

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

259 [label="EVAL with clause\nminus(s(X145), s(X146), X147) :- minus(X145, X146, X147).\nand substitutionX145 -> T97,\nT82 -> s(T97),\nX146 -> T98,\nT83 -> s(T98),\nX116 -> X148,\nX147 -> X148", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 259 [arrowhead = none ];
259 -> 173;

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

261 [label="BACKTRACK\nfor clause: minus(s(X), s(Y), Z) :- minus(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
169 -> 261 [arrowhead = none ];
261 -> 170;

262 [label="INSTANCE with matching:\nT82 -> T97\nT83 -> T98\nX116 -> X148", fontsize=14, style = filled, fillcolor = lightgrey];
173 -> 262 [arrowhead = none , style=dashed];
262 -> 142[style=dashed];

}

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f130_in(z0, z1), z0, z1)
U1(f130_out1(z0, z1), z2, z3) → f1_out1(s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)
f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
f130_in(z0, z1) → U4(f131_in(z0, z1), z0, z1)
U4(f131_out1(z0), z1, z2) → U5(f1_in(z0, z2), z1, z2, z0)
U5(f1_out1(z0), z1, z2, z3) → f130_out1(z3, z0)

Tuples:

F1_IN(z0, z1) → c1(U1'(f130_in(z0, z1), z0, z1), F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(U2'(f142_in(z0, z1), s(z0), s(z1)), F142_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c8(U3'(f142_in(z0, z1), s(z0), s(z1)), F142_IN(z0, z1))
F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(U5'(f1_in(z0, z2), z1, z2, z0), F1_IN(z0, z2))

S tuples:

F1_IN(z0, z1) → c1(U1'(f130_in(z0, z1), z0, z1), F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(U2'(f142_in(z0, z1), s(z0), s(z1)), F142_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c8(U3'(f142_in(z0, z1), s(z0), s(z1)), F142_IN(z0, z1))
F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(U5'(f1_in(z0, z2), z1, z2, z0), F1_IN(z0, z2))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f142_in, U2, f131_in, U3, f130_in, U4, U5

Defined Pair Symbols:

F1_IN, F142_IN, F131_IN, F130_IN, U4'

Compound Symbols:

c1, c6, c8, c10, c11

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

Split RHS of tuples not part of any SCC

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f130_in(z0, z1), z0, z1)
U1(f130_out1(z0, z1), z2, z3) → f1_out1(s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)
f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
f130_in(z0, z1) → U4(f131_in(z0, z1), z0, z1)
U4(f131_out1(z0), z1, z2) → U5(f1_in(z0, z2), z1, z2, z0)
U5(f1_out1(z0), z1, z2, z3) → f130_out1(z3, z0)

Tuples:

F1_IN(z0, z1) → c1(U1'(f130_in(z0, z1), z0, z1), F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(U2'(f142_in(z0, z1), s(z0), s(z1)), F142_IN(z0, z1))
F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(U5'(f1_in(z0, z2), z1, z2, z0), F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c(U3'(f142_in(z0, z1), s(z0), s(z1)))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))

S tuples:

F1_IN(z0, z1) → c1(U1'(f130_in(z0, z1), z0, z1), F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(U2'(f142_in(z0, z1), s(z0), s(z1)), F142_IN(z0, z1))
F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(U5'(f1_in(z0, z2), z1, z2, z0), F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c(U3'(f142_in(z0, z1), s(z0), s(z1)))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f142_in, U2, f131_in, U3, f130_in, U4, U5

Defined Pair Symbols:

F1_IN, F142_IN, F130_IN, U4', F131_IN

Compound Symbols:

c1, c6, c10, c11, c

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

Removed 4 trailing tuple parts

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f130_in(z0, z1), z0, z1)
U1(f130_out1(z0, z1), z2, z3) → f1_out1(s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)
f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
f130_in(z0, z1) → U4(f131_in(z0, z1), z0, z1)
U4(f131_out1(z0), z1, z2) → U5(f1_in(z0, z2), z1, z2, z0)
U5(f1_out1(z0), z1, z2, z3) → f130_out1(z3, z0)

Tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

S tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f142_in, U2, f131_in, U3, f130_in, U4, U5

Defined Pair Symbols:

F130_IN, F131_IN, F1_IN, F142_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, c

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

F131_IN(s(z0), s(z1)) → c

We considered the (Usable) Rules:

f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)

And the Tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

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

POL(0) = 0
POL(F130_IN(x₁, x₂)) = [2] + x₁
POL(F131_IN(x₁, x₂)) = [2]
POL(F142_IN(x₁, x₂)) = [2]
POL(F1_IN(x₁, x₂)) = [2] + x₁
POL(U2(x₁, x₂, x₃)) = x₁
POL(U3(x₁, x₂, x₃)) = [1] + x₁
POL(U4'(x₁, x₂, x₃)) = x₁
POL(c) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(f131_in(x₁, x₂)) = x₁
POL(f131_out1(x₁)) = [2] + x₁
POL(f142_in(x₁, x₂)) = [2] + x₁
POL(f142_out1(x₁)) = [1] + x₁
POL(s(x₁)) = [3] + x₁

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f130_in(z0, z1), z0, z1)
U1(f130_out1(z0, z1), z2, z3) → f1_out1(s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)
f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
f130_in(z0, z1) → U4(f131_in(z0, z1), z0, z1)
U4(f131_out1(z0), z1, z2) → U5(f1_in(z0, z2), z1, z2, z0)
U5(f1_out1(z0), z1, z2, z3) → f130_out1(z3, z0)

Tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

S tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))

K tuples:

F131_IN(s(z0), s(z1)) → c

Defined Rule Symbols:

f1_in, U1, f142_in, U2, f131_in, U3, f130_in, U4, U5

Defined Pair Symbols:

F130_IN, F131_IN, F1_IN, F142_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, 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.

U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))

We considered the (Usable) Rules:

f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)

And the Tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

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

POL(0) = 0
POL(F130_IN(x₁, x₂)) = x₁
POL(F131_IN(x₁, x₂)) = 0
POL(F142_IN(x₁, x₂)) = 0
POL(F1_IN(x₁, x₂)) = x₁
POL(U2(x₁, x₂, x₃)) = x₁
POL(U3(x₁, x₂, x₃)) = [1] + x₁
POL(U4'(x₁, x₂, x₃)) = x₁
POL(c) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(f131_in(x₁, x₂)) = x₁
POL(f131_out1(x₁)) = [1] + x₁
POL(f142_in(x₁, x₂)) = x₁
POL(f142_out1(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f130_in(z0, z1), z0, z1)
U1(f130_out1(z0, z1), z2, z3) → f1_out1(s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)
f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
f130_in(z0, z1) → U4(f131_in(z0, z1), z0, z1)
U4(f131_out1(z0), z1, z2) → U5(f1_in(z0, z2), z1, z2, z0)
U5(f1_out1(z0), z1, z2, z3) → f130_out1(z3, z0)

Tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

S tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))

K tuples:

F131_IN(s(z0), s(z1)) → c
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))

Defined Rule Symbols:

f1_in, U1, f142_in, U2, f131_in, U3, f130_in, U4, U5

Defined Pair Symbols:

F130_IN, F131_IN, F1_IN, F142_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, c

(23) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f130_in(z0, z1), z0, z1)
U1(f130_out1(z0, z1), z2, z3) → f1_out1(s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)
f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
f130_in(z0, z1) → U4(f131_in(z0, z1), z0, z1)
U4(f131_out1(z0), z1, z2) → U5(f1_in(z0, z2), z1, z2, z0)
U5(f1_out1(z0), z1, z2, z3) → f130_out1(z3, z0)

Tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

S tuples:

F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))

K tuples:

F131_IN(s(z0), s(z1)) → c
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f142_in, U2, f131_in, U3, f130_in, U4, U5

Defined Pair Symbols:

F130_IN, F131_IN, F1_IN, F142_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, c

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

F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))

We considered the (Usable) Rules:

f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)

And the Tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

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

POL(0) = 0
POL(F130_IN(x₁, x₂)) = x₁ + x₂ + x₂² + x₁·x₂
POL(F131_IN(x₁, x₂)) = x₂
POL(F142_IN(x₁, x₂)) = x₂
POL(F1_IN(x₁, x₂)) = [1] + x₁ + x₂ + x₂² + x₁·x₂
POL(U2(x₁, x₂, x₃)) = x₁
POL(U3(x₁, x₂, x₃)) = x₁
POL(U4'(x₁, x₂, x₃)) = x₁ + x₃² + x₁·x₃
POL(c) = 0
POL(c(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c10(x₁, x₂)) = x₁ + x₂
POL(c11(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(f131_in(x₁, x₂)) = x₁
POL(f131_out1(x₁)) = [1] + x₁
POL(f142_in(x₁, x₂)) = [1] + x₁
POL(f142_out1(x₁)) = [1] + x₁
POL(s(x₁)) = [1] + x₁

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f130_in(z0, z1), z0, z1)
U1(f130_out1(z0, z1), z2, z3) → f1_out1(s(z1))
f142_in(0, z0) → f142_out1(0)
f142_in(0, 0) → f142_out1(0)
f142_in(z0, 0) → f142_out1(z0)
f142_in(s(z0), s(z1)) → U2(f142_in(z0, z1), s(z0), s(z1))
U2(f142_out1(z0), s(z1), s(z2)) → f142_out1(z0)
f131_in(s(z0), s(z1)) → U3(f142_in(z0, z1), s(z0), s(z1))
U3(f142_out1(z0), s(z1), s(z2)) → f131_out1(z0)
f130_in(z0, z1) → U4(f131_in(z0, z1), z0, z1)
U4(f131_out1(z0), z1, z2) → U5(f1_in(z0, z2), z1, z2, z0)
U5(f1_out1(z0), z1, z2, z3) → f130_out1(z3, z0)

Tuples:

F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F131_IN(s(z0), s(z1)) → c

S tuples:none
K tuples:

F131_IN(s(z0), s(z1)) → c
U4'(f131_out1(z0), z1, z2) → c11(F1_IN(z0, z2))
F1_IN(z0, z1) → c1(F130_IN(z0, z1))
F130_IN(z0, z1) → c10(U4'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F131_IN(s(z0), s(z1)) → c(F142_IN(z0, z1))
F142_IN(s(z0), s(z1)) → c6(F142_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f142_in, U2, f131_in, U3, f130_in, U4, U5

Defined Pair Symbols:

F130_IN, F131_IN, F1_IN, F142_IN, U4'

Compound Symbols:

c10, c, c1, c6, c11, c

(27) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(0) Obligation:

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

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

(10) Obligation:

(11) CdtKnowledgeProof (EQUIVALENT transformation)

(12) Obligation:

(13) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

(14) Obligation:

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

(16) Obligation:

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

(18) Obligation:

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

(20) Obligation:

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

(22) Obligation:

(23) CdtKnowledgeProof (EQUIVALENT transformation)

(24) Obligation:

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

(26) Obligation:

(27) SIsEmptyProof (EQUIVALENT transformation)

(28) BOUNDS(O(1), O(1))