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) Obligation:

Clauses:

minus(X, Y, Z) :- ','(=(X, 0), ','(!, =(Z, 0))).
minus(X, Y, Z) :- ','(=(Y, 0), ','(!, =(Z, X))).
minus(X, Y, Z) :- ','(=(X, s(A)), ','(=(Y, s(B)), minus(A, B, Z))).
div(X, Y, Z) :- ','(=(Y, 0), ','(!, fail)).
div(X, Y, Z) :- ','(=(X, 0), ','(!, =(Z, 0))).
div(X, Y, Z) :- ','(minus(X, Y, U), ','(div(U, Y, V), =(Z, s(V)))).
=(X, X).

Query: div(g,g,a)

(1) BuiltinConflictTransformerProof (BOTH BOUNDS(ID, ID) transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

minus(X, Y, Z) :- ','(user_defined_=(X, 0), ','(!, user_defined_=(Z, 0))).
minus(X, Y, Z) :- ','(user_defined_=(Y, 0), ','(!, user_defined_=(Z, X))).
minus(X, Y, Z) :- ','(user_defined_=(X, s(A)), ','(user_defined_=(Y, s(B)), minus(A, B, Z))).
div(X, Y, Z) :- ','(user_defined_=(Y, 0), ','(!, fail)).
div(X, Y, Z) :- ','(user_defined_=(X, 0), ','(!, user_defined_=(Z, 0))).
div(X, Y, Z) :- ','(minus(X, Y, U), ','(div(U, Y, V), user_defined_=(Z, s(V)))).
user_defined_=(X, X).

Query: div(g,g,a)

(3) 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: 3 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 4 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(user_defined_=(T11, 0), ','(!_1, fail)) | div(T10, T11, T3), SCOPE: 1, CLAUSE: 4 | div(T10, T11, T3), SCOPE: 1, CLAUSE: 5\n\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(user_defined_=(T11, 0), ','(!_1, fail)), SCOPE: 2, CLAUSE: 6 | ?_2 | div(T10, T11, T3), SCOPE: 1, CLAUSE: 4 | div(T10, T11, T3), SCOPE: 1, CLAUSE: 5\n\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(!_1, fail) | ?_2 | div(T10, 0, T3), SCOPE: 1, CLAUSE: 4 | div(T10, 0, T3), SCOPE: 1, CLAUSE: 5\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ?_2 | div(T10, T11, T3), SCOPE: 1, CLAUSE: 4 | div(T10, T11, T3), SCOPE: 1, CLAUSE: 5\n\nT10 is ground\nT11 is ground\nX12 is free\nuser_defined_=(T11, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: fail\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: div(T10, T11, T3), SCOPE: 1, CLAUSE: 4 | div(T10, T11, T3), SCOPE: 1, CLAUSE: 5\n\nT10 is ground\nT11 is ground\nX12 is free\nuser_defined_=(T11, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(user_defined_=(T23, 0), ','(!_1, user_defined_=(T26, 0))) | div(T23, T24, T3), SCOPE: 1, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX12 is free\nuser_defined_=(T24, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(user_defined_=(T23, 0), ','(!_1, user_defined_=(T26, 0))), SCOPE: 3, CLAUSE: 6 | ?_3 | div(T23, T24, T3), SCOPE: 1, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX12 is free\nuser_defined_=(T24, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(!_1, user_defined_=(T26, 0)) | ?_3 | div(0, T24, T3), SCOPE: 1, CLAUSE: 5\n\nT24 is ground\nX12 is free\nuser_defined_=(T24, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ?_3 | div(T23, T24, T3), SCOPE: 1, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX12 is free\nX24 is free\nuser_defined_=(T24, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T23, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: user_defined_=(T26, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: user_defined_=(T26, 0), SCOPE: 4, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: div(T23, T24, T3), SCOPE: 1, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX12 is free\nX24 is free\nuser_defined_=(T24, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T23, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(minus(T42, T43, X43), ','(div(X43, T43, X44), user_defined_=(T45, s(X44))))\n\nT42 is ground\nT43 is ground\nX12 is free\nX24 is free\nX43 is free\nX44 is free\nuser_defined_=(T43, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T42, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: minus(T42, T43, X43)\n\nT42 is ground\nT43 is ground\nX12 is free\nX24 is free\nX43 is free\nuser_defined_=(T43, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T42, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(div(T48, T43, X44), user_defined_=(T45, s(X44)))\n\nT43 is ground\nT48 is ground\nX12 is free\nX44 is free\nuser_defined_=(T43, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: minus(T42, T43, X43), SCOPE: 5, CLAUSE: 0 | minus(T42, T43, X43), SCOPE: 5, CLAUSE: 1 | minus(T42, T43, X43), SCOPE: 5, CLAUSE: 2\n\nT42 is ground\nT43 is ground\nX12 is free\nX24 is free\nX43 is free\nuser_defined_=(T43, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T42, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(user_defined_=(T55, 0), ','(!_5, user_defined_=(X64, 0))) | minus(T55, T56, X43), SCOPE: 5, CLAUSE: 1 | minus(T55, T56, X43), SCOPE: 5, CLAUSE: 2\n\nT55 is ground\nT56 is ground\nX12 is free\nX24 is free\nX43 is free\nX64 is free\nuser_defined_=(T56, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T55, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(user_defined_=(T55, 0), ','(!_5, user_defined_=(X64, 0))), SCOPE: 6, CLAUSE: 6 | ?_6 | minus(T55, T56, X43), SCOPE: 5, CLAUSE: 1 | minus(T55, T56, X43), SCOPE: 5, CLAUSE: 2\n\nT55 is ground\nT56 is ground\nX12 is free\nX24 is free\nX43 is free\nX64 is free\nuser_defined_=(T56, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T55, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ?_6 | minus(T55, T56, X43), SCOPE: 5, CLAUSE: 1 | minus(T55, T56, X43), SCOPE: 5, CLAUSE: 2\n\nT55 is ground\nT56 is ground\nX12 is free\nX24 is free\nX43 is free\nuser_defined_=(T56, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T55, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: minus(T55, T56, X43), SCOPE: 5, CLAUSE: 1 | minus(T55, T56, X43), SCOPE: 5, CLAUSE: 2\n\nT55 is ground\nT56 is ground\nX12 is free\nX24 is free\nX43 is free\nuser_defined_=(T56, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T55, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(user_defined_=(T63, 0), ','(!_5, user_defined_=(X77, T62))) | minus(T62, T63, X43), SCOPE: 5, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX12 is free\nX24 is free\nX43 is free\nX77 is free\nuser_defined_=(T63, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T62, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(user_defined_=(T63, 0), ','(!_5, user_defined_=(X77, T62))), SCOPE: 7, CLAUSE: 6 | ?_7 | minus(T62, T63, X43), SCOPE: 5, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX12 is free\nX24 is free\nX43 is free\nX77 is free\nuser_defined_=(T63, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T62, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ?_7 | minus(T62, T63, X43), SCOPE: 5, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX12 is free\nX24 is free\nX43 is free\nuser_defined_=(T63, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T62, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: minus(T62, T63, X43), SCOPE: 5, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX12 is free\nX24 is free\nX43 is free\nuser_defined_=(T63, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T62, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(user_defined_=(T69, s(X98)), ','(user_defined_=(T70, s(X99)), minus(X98, X99, X100)))\n\nT69 is ground\nT70 is ground\nX12 is free\nX24 is free\nX100 is free\nX98 is free\nX99 is free\nuser_defined_=(T70, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T69, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(user_defined_=(T69, s(X98)), ','(user_defined_=(T70, s(X99)), minus(X98, X99, X100))), SCOPE: 8, CLAUSE: 6\n\nT69 is ground\nT70 is ground\nX12 is free\nX24 is free\nX100 is free\nX98 is free\nX99 is free\nuser_defined_=(T70, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T69, 0) !=? user_defined_=(X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(user_defined_=(T70, s(X99)), minus(T76, X99, X100))\n\nT70 is ground\nT76 is ground\nX12 is free\nX100 is free\nX99 is free\nuser_defined_=(T70, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(user_defined_=(T70, s(X99)), minus(T76, X99, X100)), SCOPE: 9, CLAUSE: 6\n\nT70 is ground\nT76 is ground\nX12 is free\nX100 is free\nX99 is free\nuser_defined_=(T70, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: minus(T76, T83, X100)\n\nT76 is ground\nT83 is ground\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: minus(T76, T83, X100), SCOPE: 10, CLAUSE: 0 | minus(T76, T83, X100), SCOPE: 10, CLAUSE: 1 | minus(T76, T83, X100), SCOPE: 10, CLAUSE: 2\n\nT76 is ground\nT83 is ground\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(user_defined_=(T90, 0), ','(!_10, user_defined_=(X133, 0))) | minus(T90, T91, X100), SCOPE: 10, CLAUSE: 1 | minus(T90, T91, X100), SCOPE: 10, CLAUSE: 2\n\nT90 is ground\nT91 is ground\nX100 is free\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(user_defined_=(T90, 0), ','(!_10, user_defined_=(X133, 0))), SCOPE: 11, CLAUSE: 6 | ?_11 | minus(T90, T91, X100), SCOPE: 10, CLAUSE: 1 | minus(T90, T91, X100), SCOPE: 10, CLAUSE: 2\n\nT90 is ground\nT91 is ground\nX100 is free\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(!_10, user_defined_=(X133, 0)) | ?_11 | minus(0, T91, X100), SCOPE: 10, CLAUSE: 1 | minus(0, T91, X100), SCOPE: 10, CLAUSE: 2\n\nT91 is ground\nX100 is free\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ?_11 | minus(T90, T91, X100), SCOPE: 10, CLAUSE: 1 | minus(T90, T91, X100), SCOPE: 10, CLAUSE: 2\n\nT90 is ground\nT91 is ground\nX100 is free\nX136 is free\nuser_defined_=(T90, 0) !=? user_defined_=(X136, X136)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: user_defined_=(X133, 0)\n\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: user_defined_=(X133, 0), SCOPE: 12, CLAUSE: 6\n\nX133 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: minus(T90, T91, X100), SCOPE: 10, CLAUSE: 1 | minus(T90, T91, X100), SCOPE: 10, CLAUSE: 2\n\nT90 is ground\nT91 is ground\nX100 is free\nX136 is free\nuser_defined_=(T90, 0) !=? user_defined_=(X136, X136)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(user_defined_=(T100, 0), ','(!_10, user_defined_=(X154, T99))) | minus(T99, T100, X100), SCOPE: 10, CLAUSE: 2\n\nT99 is ground\nT100 is ground\nX100 is free\nX136 is free\nX154 is free\nuser_defined_=(T99, 0) !=? user_defined_=(X136, X136)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(user_defined_=(T100, 0), ','(!_10, user_defined_=(X154, T99))), SCOPE: 13, CLAUSE: 6 | ?_13 | minus(T99, T100, X100), SCOPE: 10, CLAUSE: 2\n\nT99 is ground\nT100 is ground\nX100 is free\nX136 is free\nX154 is free\nuser_defined_=(T99, 0) !=? user_defined_=(X136, X136)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(!_10, user_defined_=(X154, T99)) | ?_13 | minus(T99, 0, X100), SCOPE: 10, CLAUSE: 2\n\nT99 is ground\nX100 is free\nX136 is free\nX154 is free\nuser_defined_=(T99, 0) !=? user_defined_=(X136, X136)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ?_13 | minus(T99, T100, X100), SCOPE: 10, CLAUSE: 2\n\nT99 is ground\nT100 is ground\nX100 is free\nX136 is free\nX157 is free\nuser_defined_=(T99, 0) !=? user_defined_=(X136, X136)\nuser_defined_=(T100, 0) !=? user_defined_=(X157, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: user_defined_=(X154, T99)\n\nT99 is ground\nX136 is free\nX154 is free\nuser_defined_=(T99, 0) !=? user_defined_=(X136, X136)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: user_defined_=(X154, T99), SCOPE: 14, CLAUSE: 6\n\nT99 is ground\nX136 is free\nX154 is free\nuser_defined_=(T99, 0) !=? user_defined_=(X136, X136)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: minus(T99, T100, X100), SCOPE: 10, CLAUSE: 2\n\nT99 is ground\nT100 is ground\nX100 is free\nX136 is free\nX157 is free\nuser_defined_=(T99, 0) !=? user_defined_=(X136, X136)\nuser_defined_=(T100, 0) !=? user_defined_=(X157, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(user_defined_=(T111, s(X183)), ','(user_defined_=(T112, s(X184)), minus(X183, X184, X185)))\n\nT111 is ground\nT112 is ground\nX136 is free\nX157 is free\nX185 is free\nX183 is free\nX184 is free\nuser_defined_=(T111, 0) !=? user_defined_=(X136, X136)\nuser_defined_=(T112, 0) !=? user_defined_=(X157, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(user_defined_=(T111, s(X183)), ','(user_defined_=(T112, s(X184)), minus(X183, X184, X185))), SCOPE: 15, CLAUSE: 6\n\nT111 is ground\nT112 is ground\nX136 is free\nX157 is free\nX185 is free\nX183 is free\nX184 is free\nuser_defined_=(T111, 0) !=? user_defined_=(X136, X136)\nuser_defined_=(T112, 0) !=? user_defined_=(X157, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(user_defined_=(T112, s(X184)), minus(T118, X184, X185))\n\nT112 is ground\nT118 is ground\nX157 is free\nX185 is free\nX184 is free\nuser_defined_=(T112, 0) !=? user_defined_=(X157, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(user_defined_=(T112, s(X184)), minus(T118, X184, X185)), SCOPE: 16, CLAUSE: 6\n\nT112 is ground\nT118 is ground\nX157 is free\nX185 is free\nX184 is free\nuser_defined_=(T112, 0) !=? user_defined_=(X157, X157)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: minus(T118, T125, X185)\n\nT118 is ground\nT125 is ground\nX185 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: div(T48, T43, X44)\n\nT43 is ground\nT48 is ground\nX12 is free\nX44 is free\nuser_defined_=(T43, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: user_defined_=(T45, s(T130))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: div(T48, T43, X44), SCOPE: 17, CLAUSE: 3 | div(T48, T43, X44), SCOPE: 17, CLAUSE: 4 | div(T48, T43, X44), SCOPE: 17, CLAUSE: 5\n\nT43 is ground\nT48 is ground\nX12 is free\nX44 is free\nuser_defined_=(T43, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(user_defined_=(T138, 0), ','(!_17, fail)) | div(T137, T138, X44), SCOPE: 17, CLAUSE: 4 | div(T137, T138, X44), SCOPE: 17, CLAUSE: 5\n\nT137 is ground\nT138 is ground\nX12 is free\nX44 is free\nuser_defined_=(T138, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(user_defined_=(T138, 0), ','(!_17, fail)), SCOPE: 18, CLAUSE: 6 | ?_18 | div(T137, T138, X44), SCOPE: 17, CLAUSE: 4 | div(T137, T138, X44), SCOPE: 17, CLAUSE: 5\n\nT137 is ground\nT138 is ground\nX12 is free\nX44 is free\nuser_defined_=(T138, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ?_18 | div(T137, T138, X44), SCOPE: 17, CLAUSE: 4 | div(T137, T138, X44), SCOPE: 17, CLAUSE: 5\n\nT137 is ground\nT138 is ground\nX12 is free\nX44 is free\nuser_defined_=(T138, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: div(T137, T138, X44), SCOPE: 17, CLAUSE: 4 | div(T137, T138, X44), SCOPE: 17, CLAUSE: 5\n\nT137 is ground\nT138 is ground\nX12 is free\nX44 is free\nuser_defined_=(T138, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ','(user_defined_=(T144, 0), ','(!_17, user_defined_=(X239, 0))) | div(T144, T145, X44), SCOPE: 17, CLAUSE: 5\n\nT144 is ground\nT145 is ground\nX12 is free\nX44 is free\nX239 is free\nuser_defined_=(T145, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(user_defined_=(T144, 0), ','(!_17, user_defined_=(X239, 0))), SCOPE: 19, CLAUSE: 6 | ?_19 | div(T144, T145, X44), SCOPE: 17, CLAUSE: 5\n\nT144 is ground\nT145 is ground\nX12 is free\nX44 is free\nX239 is free\nuser_defined_=(T145, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(!_17, user_defined_=(X239, 0)) | ?_19 | div(0, T145, X44), SCOPE: 17, CLAUSE: 5\n\nT145 is ground\nX12 is free\nX44 is free\nX239 is free\nuser_defined_=(T145, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ?_19 | div(T144, T145, X44), SCOPE: 17, CLAUSE: 5\n\nT144 is ground\nT145 is ground\nX12 is free\nX44 is free\nX242 is free\nuser_defined_=(T145, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T144, 0) !=? user_defined_=(X242, X242)", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: user_defined_=(X239, 0)\n\nX239 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: user_defined_=(X239, 0), SCOPE: 20, CLAUSE: 6\n\nX239 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: div(T144, T145, X44), SCOPE: 17, CLAUSE: 5\n\nT144 is ground\nT145 is ground\nX12 is free\nX44 is free\nX242 is free\nuser_defined_=(T145, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T144, 0) !=? user_defined_=(X242, X242)", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(minus(T155, T156, X266), ','(div(X266, T156, X267), user_defined_=(X268, s(X267))))\n\nT155 is ground\nT156 is ground\nX12 is free\nX242 is free\nX268 is free\nX266 is free\nX267 is free\nuser_defined_=(T156, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T155, 0) !=? user_defined_=(X242, X242)", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: minus(T155, T156, X266)\n\nT155 is ground\nT156 is ground\nX12 is free\nX242 is free\nX266 is free\nuser_defined_=(T156, 0) !=? user_defined_=(X12, X12)\nuser_defined_=(T155, 0) !=? user_defined_=(X242, X242)", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(div(T159, T156, X267), user_defined_=(X268, s(X267)))\n\nT156 is ground\nT159 is ground\nX12 is free\nX268 is free\nX267 is free\nuser_defined_=(T156, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: div(T159, T156, X267)\n\nT156 is ground\nT159 is ground\nX12 is free\nX267 is free\nuser_defined_=(T156, 0) !=? user_defined_=(X12, X12)", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: user_defined_=(X268, s(T164))\n\nX268 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: user_defined_=(X268, s(T164)), SCOPE: 21, CLAUSE: 6\n\nX268 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: user_defined_=(T45, s(T130)), SCOPE: 22, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 178 [arrowhead = none ];
178 -> 4;

179 [label="ONLY EVAL with clause\ndiv(X7, X8, X9) :- ','(user_defined_=(X8, 0), ','(!_1, fail)).\nand substitutionT1 -> T10,\nX7 -> T10,\nT2 -> T11,\nX8 -> T11,\nT3 -> T12,\nX9 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 179 [arrowhead = none ];
179 -> 6;

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

181 [label="EVAL with clause\nuser_defined_=(X12, X12).\nand substitutionT11 -> 0,\nX12 -> 0,\nT15 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 181 [arrowhead = none ];
181 -> 10;

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

183 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 183 [arrowhead = none ];
183 -> 14;

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

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

186 [label="ONLY EVAL with clause\ndiv(X19, X20, X21) :- ','(user_defined_=(X19, 0), ','(!_1, user_defined_=(X21, 0))).\nand substitutionT10 -> T23,\nX19 -> T23,\nT11 -> T24,\nX20 -> T24,\nT3 -> T26,\nX21 -> T26,\nT25 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 186 [arrowhead = none ];
186 -> 19;

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

188 [label="EVAL with clause\nuser_defined_=(X24, X24).\nand substitutionT23 -> 0,\nX24 -> 0,\nT29 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 188 [arrowhead = none ];
188 -> 23;

189 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 189 [arrowhead = none ];
189 -> 25;

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

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

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

193 [label="EVAL with clause\nuser_defined_=(X27, X27).\nand substitutionT26 -> 0,\nX27 -> 0,\nT32 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 193 [arrowhead = none ];
193 -> 31;

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

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

196 [label="ONLY EVAL with clause\ndiv(X40, X41, X42) :- ','(minus(X40, X41, X43), ','(div(X43, X41, X44), user_defined_=(X42, s(X44)))).\nand substitutionT23 -> T42,\nX40 -> T42,\nT24 -> T43,\nX41 -> T43,\nT3 -> T45,\nX42 -> T45,\nT44 -> T45", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 196 [arrowhead = none ];
196 -> 39;

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

198 [label="SPLIT 2\nnew knowledge:\nT42 is ground\nT43 is ground\nT48 is ground\nreplacements:X43 -> T48", fontsize=14, style = filled, fillcolor = violet];
39 -> 198 [arrowhead = none ];
198 -> 43;

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

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

201 [label="SPLIT 2\nnew knowledge:\nT48 is ground\nT43 is ground\nreplacements:X44 -> T130", fontsize=14, style = filled, fillcolor = violet];
43 -> 201 [arrowhead = none ];
201 -> 130;

202 [label="ONLY EVAL with clause\nminus(X61, X62, X63) :- ','(user_defined_=(X61, 0), ','(!_5, user_defined_=(X63, 0))).\nand substitutionT42 -> T55,\nX61 -> T55,\nT43 -> T56,\nX62 -> T56,\nX43 -> X64,\nX63 -> X64", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 202 [arrowhead = none ];
202 -> 47;

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

204 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T55, 0), user_defined_=(X24, X24))", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 204 [arrowhead = none ];
204 -> 51;

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

206 [label="ONLY EVAL with clause\nminus(X74, X75, X76) :- ','(user_defined_=(X75, 0), ','(!_5, user_defined_=(X76, X74))).\nand substitutionT55 -> T62,\nX74 -> T62,\nT56 -> T63,\nX75 -> T63,\nX43 -> X77,\nX76 -> X77", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 206 [arrowhead = none ];
206 -> 55;

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

208 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T63, 0), user_defined_=(X12, X12))", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 208 [arrowhead = none ];
208 -> 59;

209 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 209 [arrowhead = none ];
209 -> 61;

210 [label="ONLY EVAL with clause\nminus(X95, X96, X97) :- ','(user_defined_=(X95, s(X98)), ','(user_defined_=(X96, s(X99)), minus(X98, X99, X97))).\nand substitutionT62 -> T69,\nX95 -> T69,\nT63 -> T70,\nX96 -> T70,\nX43 -> X100,\nX97 -> X100", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 210 [arrowhead = none ];
210 -> 63;

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

212 [label="EVAL with clause\nuser_defined_=(X109, X109).\nand substitutionT69 -> s(T76),\nX109 -> s(T76),\nX98 -> T76,\nT75 -> s(T76)", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 212 [arrowhead = none ];
212 -> 67;

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

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

215 [label="EVAL with clause\nuser_defined_=(X117, X117).\nand substitutionT70 -> s(T83),\nX117 -> s(T83),\nX99 -> T83,\nT82 -> s(T83)", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 215 [arrowhead = none ];
215 -> 73;

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

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

218 [label="ONLY EVAL with clause\nminus(X130, X131, X132) :- ','(user_defined_=(X130, 0), ','(!_10, user_defined_=(X132, 0))).\nand substitutionT76 -> T90,\nX130 -> T90,\nT83 -> T91,\nX131 -> T91,\nX100 -> X133,\nX132 -> X133", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 218 [arrowhead = none ];
218 -> 79;

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

220 [label="EVAL with clause\nuser_defined_=(X136, X136).\nand substitutionT90 -> 0,\nX136 -> 0,\nT94 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 220 [arrowhead = none ];
220 -> 83;

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

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

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

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

225 [label="ONLY EVAL with clause\nuser_defined_=(X141, X141).\nand substitutionX133 -> 0,\nX141 -> 0,\nX142 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 225 [arrowhead = none ];
225 -> 91;

226 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 226 [arrowhead = none ];
226 -> 92;

227 [label="ONLY EVAL with clause\nminus(X151, X152, X153) :- ','(user_defined_=(X152, 0), ','(!_10, user_defined_=(X153, X151))).\nand substitutionT90 -> T99,\nX151 -> T99,\nT91 -> T100,\nX152 -> T100,\nX100 -> X154,\nX153 -> X154", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 227 [arrowhead = none ];
227 -> 97;

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

229 [label="EVAL with clause\nuser_defined_=(X157, X157).\nand substitutionT100 -> 0,\nX157 -> 0,\nT103 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 229 [arrowhead = none ];
229 -> 101;

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

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

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

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

234 [label="ONLY EVAL with clause\nuser_defined_=(X162, X162).\nand substitutionX154 -> T106,\nX162 -> T106,\nT99 -> T106,\nX163 -> T106", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 234 [arrowhead = none ];
234 -> 109;

235 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 235 [arrowhead = none ];
235 -> 110;

236 [label="ONLY EVAL with clause\nminus(X180, X181, X182) :- ','(user_defined_=(X180, s(X183)), ','(user_defined_=(X181, s(X184)), minus(X183, X184, X182))).\nand substitutionT99 -> T111,\nX180 -> T111,\nT100 -> T112,\nX181 -> T112,\nX100 -> X185,\nX182 -> X185", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 236 [arrowhead = none ];
236 -> 115;

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

238 [label="EVAL with clause\nuser_defined_=(X194, X194).\nand substitutionT111 -> s(T118),\nX194 -> s(T118),\nX183 -> T118,\nT117 -> s(T118)", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 238 [arrowhead = none ];
238 -> 119;

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

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

241 [label="EVAL with clause\nuser_defined_=(X202, X202).\nand substitutionT112 -> s(T125),\nX202 -> s(T125),\nX184 -> T125,\nT124 -> s(T125)", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 241 [arrowhead = none ];
241 -> 125;

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

243 [label="INSTANCE with matching:\nT76 -> T118\nT83 -> T125\nX100 -> X185", fontsize=14, style = filled, fillcolor = lightgrey];
125 -> 243 [arrowhead = none , style=dashed];
243 -> 73[style=dashed];

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

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

246 [label="ONLY EVAL with clause\ndiv(X223, X224, X225) :- ','(user_defined_=(X224, 0), ','(!_17, fail)).\nand substitutionT48 -> T137,\nX223 -> T137,\nT43 -> T138,\nX224 -> T138,\nX44 -> X226,\nX225 -> X226", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 246 [arrowhead = none ];
246 -> 135;

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

248 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T138, 0), user_defined_=(X12, X12))", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 248 [arrowhead = none ];
248 -> 139;

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

250 [label="ONLY EVAL with clause\ndiv(X236, X237, X238) :- ','(user_defined_=(X236, 0), ','(!_17, user_defined_=(X238, 0))).\nand substitutionT137 -> T144,\nX236 -> T144,\nT138 -> T145,\nX237 -> T145,\nX44 -> X239,\nX238 -> X239", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 250 [arrowhead = none ];
250 -> 143;

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

252 [label="EVAL with clause\nuser_defined_=(X242, X242).\nand substitutionT144 -> 0,\nX242 -> 0,\nT148 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 252 [arrowhead = none ];
252 -> 147;

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

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

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

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

257 [label="ONLY EVAL with clause\nuser_defined_=(X247, X247).\nand substitutionX239 -> 0,\nX247 -> 0,\nX248 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
152 -> 257 [arrowhead = none ];
257 -> 155;

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

259 [label="ONLY EVAL with clause\ndiv(X263, X264, X265) :- ','(minus(X263, X264, X266), ','(div(X266, X264, X267), user_defined_=(X265, s(X267)))).\nand substitutionT144 -> T155,\nX263 -> T155,\nT145 -> T156,\nX264 -> T156,\nX44 -> X268,\nX265 -> X268", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 259 [arrowhead = none ];
259 -> 160;

260 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
160 -> 260 [arrowhead = none ];
260 -> 162;

261 [label="SPLIT 2\nnew knowledge:\nT155 is ground\nT156 is ground\nT159 is ground\nreplacements:X266 -> T159", fontsize=14, style = filled, fillcolor = violet];
160 -> 261 [arrowhead = none ];
261 -> 163;

262 [label="INSTANCE with matching:\nT42 -> T155\nT43 -> T156\nX43 -> X266\nX24 -> X242", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 262 [arrowhead = none , style=dashed];
262 -> 41[style=dashed];

263 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
163 -> 263 [arrowhead = none ];
263 -> 167;

264 [label="SPLIT 2\nnew knowledge:\nT159 is ground\nT156 is ground\nreplacements:X267 -> T164", fontsize=14, style = filled, fillcolor = violet];
163 -> 264 [arrowhead = none ];
264 -> 168;

265 [label="INSTANCE with matching:\nT48 -> T159\nT43 -> T156\nX44 -> X267", fontsize=14, style = filled, fillcolor = lightgrey];
167 -> 265 [arrowhead = none , style=dashed];
265 -> 129[style=dashed];

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

267 [label="ONLY EVAL with clause\nuser_defined_=(X289, X289).\nand substitutionX268 -> s(T169),\nX289 -> s(T169),\nT164 -> T169,\nX290 -> s(T169)", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 267 [arrowhead = none ];
267 -> 170;

268 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
170 -> 268 [arrowhead = none ];
268 -> 171;

269 [label="EVAL with clause\nuser_defined_=(X293, X293).\nand substitutionT45 -> s(T175),\nX293 -> s(T175),\nT130 -> T175,\nT174 -> s(T175)", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 269 [arrowhead = none ];
269 -> 175;

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

271 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
175 -> 271 [arrowhead = none ];
271 -> 177;

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F1_IN(z0, z1) → c1(U1'(f39_in(z0, z1), z0, z1), F39_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c3(U2'(f73_in(z0, z1), s(z0), s(z1)), F73_IN(z0, z1))
F129_IN(z0, z1) → c6(U3'(f160_in(z0, z1), z0, z1), F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(U4'(f73_in(z0, z1), s(z0), s(z1)), F73_IN(z0, z1))
F39_IN(z0, z1) → c14(U5'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c15(U6'(f43_in(z0, z2), z1, z2, z0), F43_IN(z0, z2))
F43_IN(z0, z1) → c17(U7'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
U7'(f129_out1, z0, z1) → c18(U8'(f130_in, z0, z1), F130_IN)
F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(U10'(f163_in(z0, z2), z1, z2, z0), F163_IN(z0, z2))
F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
U11'(f129_out1, z0, z1) → c24(U12'(f168_in, z0, z1), F168_IN)

S tuples:

F1_IN(z0, z1) → c1(U1'(f39_in(z0, z1), z0, z1), F39_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c3(U2'(f73_in(z0, z1), s(z0), s(z1)), F73_IN(z0, z1))
F129_IN(z0, z1) → c6(U3'(f160_in(z0, z1), z0, z1), F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(U4'(f73_in(z0, z1), s(z0), s(z1)), F73_IN(z0, z1))
F39_IN(z0, z1) → c14(U5'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c15(U6'(f43_in(z0, z2), z1, z2, z0), F43_IN(z0, z2))
F43_IN(z0, z1) → c17(U7'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
U7'(f129_out1, z0, z1) → c18(U8'(f130_in, z0, z1), F130_IN)
F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(U10'(f163_in(z0, z2), z1, z2, z0), F163_IN(z0, z2))
F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
U11'(f129_out1, z0, z1) → c24(U12'(f168_in, z0, z1), F168_IN)

K tuples:none
Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F1_IN, F41_IN, F129_IN, F73_IN, F39_IN, U5', F43_IN, U7', F160_IN, U9', F163_IN, U11'

Compound Symbols:

c1, c3, c6, c10, c14, c15, c17, c18, c20, c21, c23, c24

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F129_IN(z0, z1) → c6(U3'(f160_in(z0, z1), z0, z1), F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(U4'(f73_in(z0, z1), s(z0), s(z1)), F73_IN(z0, z1))
F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(U10'(f163_in(z0, z2), z1, z2, z0), F163_IN(z0, z2))
F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F1_IN(z0, z1) → c(U1'(f39_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c(F39_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(U2'(f73_in(z0, z1), s(z0), s(z1)))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(U6'(f43_in(z0, z2), z1, z2, z0))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
U7'(f129_out1, z0, z1) → c(U8'(f130_in, z0, z1))
U7'(f129_out1, z0, z1) → c(F130_IN)
U11'(f129_out1, z0, z1) → c(U12'(f168_in, z0, z1))
U11'(f129_out1, z0, z1) → c(F168_IN)

S tuples:

F129_IN(z0, z1) → c6(U3'(f160_in(z0, z1), z0, z1), F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(U4'(f73_in(z0, z1), s(z0), s(z1)), F73_IN(z0, z1))
F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(U10'(f163_in(z0, z2), z1, z2, z0), F163_IN(z0, z2))
F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F1_IN(z0, z1) → c(U1'(f39_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c(F39_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(U2'(f73_in(z0, z1), s(z0), s(z1)))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(U6'(f43_in(z0, z2), z1, z2, z0))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
U7'(f129_out1, z0, z1) → c(U8'(f130_in, z0, z1))
U7'(f129_out1, z0, z1) → c(F130_IN)
U11'(f129_out1, z0, z1) → c(U12'(f168_in, z0, z1))
U11'(f129_out1, z0, z1) → c(F168_IN)

K tuples:none
Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F129_IN, F73_IN, F160_IN, U9', F163_IN, F1_IN, F41_IN, F39_IN, U5', F43_IN, U7', U11'

Compound Symbols:

c6, c10, c20, c21, c23, c

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

Removed 10 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F1_IN(z0, z1) → c(F39_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F1_IN(z0, z1) → c
F41_IN(s(z0), s(z1)) → c
U5'(f41_out1(z0), z1, z2) → c
U7'(f129_out1, z0, z1) → c
U11'(f129_out1, z0, z1) → c

S tuples:

F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F1_IN(z0, z1) → c(F39_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F1_IN(z0, z1) → c
F41_IN(s(z0), s(z1)) → c
U5'(f41_out1(z0), z1, z2) → c
U7'(f129_out1, z0, z1) → c
U11'(f129_out1, z0, z1) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F160_IN, F163_IN, F1_IN, F41_IN, F39_IN, U5', F43_IN, F129_IN, F73_IN, U9', U7', U11'

Compound Symbols:

c20, c23, c, c6, c10, c21, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0, z1) → c(F39_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F1_IN(z0, z1) → c
U5'(f41_out1(z0), z1, z2) → c
U7'(f129_out1, z0, z1) → c
U7'(f129_out1, z0, z1) → c
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
U5'(f41_out1(z0), z1, z2) → c
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
U7'(f129_out1, z0, z1) → c
U7'(f129_out1, z0, z1) → c

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F1_IN(z0, z1) → c(F39_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F1_IN(z0, z1) → c
F41_IN(s(z0), s(z1)) → c
U5'(f41_out1(z0), z1, z2) → c
U7'(f129_out1, z0, z1) → c
U11'(f129_out1, z0, z1) → c

S tuples:

F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1))
F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F41_IN(s(z0), s(z1)) → c
U11'(f129_out1, z0, z1) → c

K tuples:

F1_IN(z0, z1) → c(F39_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F1_IN(z0, z1) → c
U5'(f41_out1(z0), z1, z2) → c
U7'(f129_out1, z0, z1) → c

Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F160_IN, F163_IN, F1_IN, F41_IN, F39_IN, U5', F43_IN, F129_IN, F73_IN, U9', U7', U11'

Compound Symbols:

c20, c23, c, c6, c10, c21, c

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F160_IN(z0, z1) → c20(U9'(f41_in(z0, z1), z0, z1), F41_IN(z0, z1)) by

F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F1_IN(z0, z1) → c(F39_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F1_IN(z0, z1) → c
F41_IN(s(z0), s(z1)) → c
U5'(f41_out1(z0), z1, z2) → c
U7'(f129_out1, z0, z1) → c
U11'(f129_out1, z0, z1) → c
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))

S tuples:

F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F41_IN(s(z0), s(z1)) → c
U11'(f129_out1, z0, z1) → c
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))

K tuples:

F1_IN(z0, z1) → c(F39_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F1_IN(z0, z1) → c
U5'(f41_out1(z0), z1, z2) → c
U7'(f129_out1, z0, z1) → c

Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F163_IN, F1_IN, F41_IN, F39_IN, U5', F43_IN, F129_IN, F73_IN, U9', U7', U11', F160_IN

Compound Symbols:

c23, c, c6, c10, c21, c, c20

(13) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 6 of 18 dangling nodes:

F1_IN(z0, z1) → c(F39_IN(z0, z1))
F39_IN(z0, z1) → c(F41_IN(z0, z1))
U7'(f129_out1, z0, z1) → c
U5'(f41_out1(z0), z1, z2) → c
F43_IN(z0, z1) → c(U7'(f129_in(z0, z1), z0, z1))
F1_IN(z0, z1) → c

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F41_IN(s(z0), s(z1)) → c
U11'(f129_out1, z0, z1) → c
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))

S tuples:

F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F41_IN(s(z0), s(z1)) → c
U11'(f129_out1, z0, z1) → c
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))

K tuples:

F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F163_IN, F41_IN, F39_IN, U5', F43_IN, F129_IN, F73_IN, U9', U11', F160_IN

Compound Symbols:

c23, c, c6, c10, c21, c, c20

(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
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))

S tuples:

F163_IN(z0, z1) → c23(U11'(f129_in(z0, z1), z0, z1), F129_IN(z0, z1))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))

K tuples:

F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F163_IN, F41_IN, F39_IN, U5', F43_IN, F129_IN, F73_IN, U9', F160_IN

Compound Symbols:

c23, c, c6, c10, c21, c20

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

Removed 1 trailing tuple parts

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))
F163_IN(z0, z1) → c23(F129_IN(z0, z1))

S tuples:

F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))
F163_IN(z0, z1) → c23(F129_IN(z0, z1))

K tuples:

F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F41_IN, F39_IN, U5', F43_IN, F129_IN, F73_IN, U9', F160_IN, F163_IN

Compound Symbols:

c, c6, c10, c21, c20, c23

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

U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))

We considered the (Usable) Rules:

f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))

And the Tuples:

F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))
F163_IN(z0, z1) → c23(F129_IN(z0, z1))

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

POL(0) = 0   
POL(F129_IN(x₁, x₂)) = [3] + [3]x₁   
POL(F160_IN(x₁, x₂)) = [3] + [3]x₁   
POL(F163_IN(x₁, x₂)) = [3] + [3]x₁   
POL(F39_IN(x₁, x₂)) = [3] + [3]x₁ + [2]x₂   
POL(F41_IN(x₁, x₂)) = 0   
POL(F43_IN(x₁, x₂)) = [3] + [3]x₁ + [2]x₂   
POL(F73_IN(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = x₁   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U5'(x₁, x₂, x₃)) = [3]x₁ + [2]x₃   
POL(U9'(x₁, x₂, x₃)) = [3]x₁   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c20(x₁, x₂)) = x₁ + x₂   
POL(c21(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(f41_in(x₁, x₂)) = [1] + x₁   
POL(f41_out1(x₁)) = [2] + x₁   
POL(f73_in(x₁, x₂)) = [3] + x₁   
POL(f73_out1(x₁)) = [2] + x₁   
POL(s(x₁)) = [2] + x₁   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))
F163_IN(z0, z1) → c23(F129_IN(z0, z1))

S tuples:

F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))
F163_IN(z0, z1) → c23(F129_IN(z0, z1))

K tuples:

F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))

Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F41_IN, F39_IN, U5', F43_IN, F129_IN, F73_IN, U9', F160_IN, F163_IN

Compound Symbols:

c, c6, c10, c21, c20, c23

(21) CdtKnowledgeProof (EQUIVALENT transformation)

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

F163_IN(z0, z1) → c23(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0, z0) → f1_out1
f1_in(z0, z1) → U1(f39_in(z0, z1), z0, z1)
U1(f39_out1(z0), z1, z2) → f1_out1
f41_in(s(z0), s(z1)) → U2(f73_in(z0, z1), s(z0), s(z1))
U2(f73_out1(z0), s(z1), s(z2)) → f41_out1(z0)
f129_in(0, z0) → f129_out1
f129_in(z0, z1) → U3(f160_in(z0, z1), z0, z1)
U3(f160_out1(z0), z1, z2) → f129_out1
f73_in(0, z0) → f73_out1(0)
f73_in(z0, 0) → f73_out1(z0)
f73_in(s(z0), s(z1)) → U4(f73_in(z0, z1), s(z0), s(z1))
U4(f73_out1(z0), s(z1), s(z2)) → f73_out1(z0)
f130_in → f130_out1
f168_in → f168_out1
f39_in(z0, z1) → U5(f41_in(z0, z1), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f43_in(z0, z2), z1, z2, z0)
U6(f43_out1, z0, z1, z2) → f39_out1(z2)
f43_in(z0, z1) → U7(f129_in(z0, z1), z0, z1)
U7(f129_out1, z0, z1) → U8(f130_in, z0, z1)
U8(f130_out1, z0, z1) → f43_out1
f160_in(z0, z1) → U9(f41_in(z0, z1), z0, z1)
U9(f41_out1(z0), z1, z2) → U10(f163_in(z0, z2), z1, z2, z0)
U10(f163_out1, z0, z1, z2) → f160_out1(z2)
f163_in(z0, z1) → U11(f129_in(z0, z1), z0, z1)
U11(f129_out1, z0, z1) → U12(f168_in, z0, z1)
U12(f168_out1, z0, z1) → f163_out1

Tuples:

F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))
F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))
F163_IN(z0, z1) → c23(F129_IN(z0, z1))

S tuples:

F73_IN(s(z0), s(z1)) → c10(F73_IN(z0, z1))

K tuples:

F39_IN(z0, z1) → c(U5'(f41_in(z0, z1), z0, z1))
U5'(f41_out1(z0), z1, z2) → c(F43_IN(z0, z2))
F43_IN(z0, z1) → c(F129_IN(z0, z1))
U9'(f41_out1(z0), z1, z2) → c21(F163_IN(z0, z2))
F163_IN(z0, z1) → c23(F129_IN(z0, z1))
F129_IN(z0, z1) → c6(F160_IN(z0, z1))
F160_IN(s(z0), s(z1)) → c20(U9'(U2(f73_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F41_IN(s(z0), s(z1)))
F41_IN(s(z0), s(z1)) → c(F73_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f41_in, U2, f129_in, U3, f73_in, U4, f130_in, f168_in, f39_in, U5, U6, f43_in, U7, U8, f160_in, U9, U10, f163_in, U11, U12

Defined Pair Symbols:

F41_IN, F39_IN, U5', F43_IN, F129_IN, F73_IN, U9', F160_IN, F163_IN

Compound Symbols:

c, c6, c10, c21, c20, c23

(23) 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: 3 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 4 | div(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(user_defined_=(T8, 0), ','(!_1, fail)) | div(T7, T8, T3), SCOPE: 1, CLAUSE: 4 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(user_defined_=(T8, 0), ','(!_1, fail)), SCOPE: 2, CLAUSE: 6 | ?_2 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 4 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(!_1, fail) | ?_2 | div(T7, 0, T3), SCOPE: 1, CLAUSE: 4 | div(T7, 0, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ?_2 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 4 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground\nT8 is ground\nX9 is free\nuser_defined_=(T8, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: fail\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: div(T7, T8, T3), SCOPE: 1, CLAUSE: 4 | div(T7, T8, T3), SCOPE: 1, CLAUSE: 5\n\nT7 is ground\nT8 is ground\nX9 is free\nuser_defined_=(T8, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(user_defined_=(T20, 0), ','(!_1, user_defined_=(T23, 0))) | div(T20, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT20 is ground\nT21 is ground\nX9 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(user_defined_=(T20, 0), ','(!_1, user_defined_=(T23, 0))), SCOPE: 3, CLAUSE: 6 | ?_3 | div(T20, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT20 is ground\nT21 is ground\nX9 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(!_1, user_defined_=(T23, 0)) | ?_3 | div(0, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT21 is ground\nX9 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ?_3 | div(T20, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT20 is ground\nT21 is ground\nX9 is free\nX21 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T20, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: user_defined_=(T23, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: user_defined_=(T23, 0), SCOPE: 4, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: div(T20, T21, T3), SCOPE: 1, CLAUSE: 5\n\nT20 is ground\nT21 is ground\nX9 is free\nX21 is free\nuser_defined_=(T21, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T20, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(minus(T39, T40, X40), ','(div(X40, T40, X41), user_defined_=(T42, s(X41))))\n\nT39 is ground\nT40 is ground\nX9 is free\nX21 is free\nX40 is free\nX41 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T39, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: minus(T39, T40, X40)\n\nT39 is ground\nT40 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T39, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(div(T45, T40, X41), user_defined_=(T42, s(X41)))\n\nT40 is ground\nT45 is ground\nX9 is free\nX41 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: minus(T39, T40, X40), SCOPE: 5, CLAUSE: 0 | minus(T39, T40, X40), SCOPE: 5, CLAUSE: 1 | minus(T39, T40, X40), SCOPE: 5, CLAUSE: 2\n\nT39 is ground\nT40 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T39, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(user_defined_=(T52, 0), ','(!_5, user_defined_=(X61, 0))) | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 1 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 2\n\nT52 is ground\nT53 is ground\nX9 is free\nX21 is free\nX40 is free\nX61 is free\nuser_defined_=(T53, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T52, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(user_defined_=(T52, 0), ','(!_5, user_defined_=(X61, 0))), SCOPE: 6, CLAUSE: 6 | ?_6 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 1 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 2\n\nT52 is ground\nT53 is ground\nX9 is free\nX21 is free\nX40 is free\nX61 is free\nuser_defined_=(T53, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T52, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ?_6 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 1 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 2\n\nT52 is ground\nT53 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T53, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T52, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: minus(T52, T53, X40), SCOPE: 5, CLAUSE: 1 | minus(T52, T53, X40), SCOPE: 5, CLAUSE: 2\n\nT52 is ground\nT53 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T53, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T52, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(user_defined_=(T60, 0), ','(!_5, user_defined_=(X74, T59))) | minus(T59, T60, X40), SCOPE: 5, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nX9 is free\nX21 is free\nX40 is free\nX74 is free\nuser_defined_=(T60, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T59, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(user_defined_=(T60, 0), ','(!_5, user_defined_=(X74, T59))), SCOPE: 7, CLAUSE: 6 | ?_7 | minus(T59, T60, X40), SCOPE: 5, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nX9 is free\nX21 is free\nX40 is free\nX74 is free\nuser_defined_=(T60, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T59, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ?_7 | minus(T59, T60, X40), SCOPE: 5, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T60, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T59, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: minus(T59, T60, X40), SCOPE: 5, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nX9 is free\nX21 is free\nX40 is free\nuser_defined_=(T60, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T59, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(user_defined_=(T66, s(X95)), ','(user_defined_=(T67, s(X96)), minus(X95, X96, X97)))\n\nT66 is ground\nT67 is ground\nX9 is free\nX21 is free\nX97 is free\nX95 is free\nX96 is free\nuser_defined_=(T67, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T66, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(user_defined_=(T66, s(X95)), ','(user_defined_=(T67, s(X96)), minus(X95, X96, X97))), SCOPE: 8, CLAUSE: 6\n\nT66 is ground\nT67 is ground\nX9 is free\nX21 is free\nX97 is free\nX95 is free\nX96 is free\nuser_defined_=(T67, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T66, 0) !=? user_defined_=(X21, X21)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(user_defined_=(T67, s(X96)), minus(T73, X96, X97))\n\nT67 is ground\nT73 is ground\nX9 is free\nX97 is free\nX96 is free\nuser_defined_=(T67, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(user_defined_=(T67, s(X96)), minus(T73, X96, X97)), SCOPE: 9, CLAUSE: 6\n\nT67 is ground\nT73 is ground\nX9 is free\nX97 is free\nX96 is free\nuser_defined_=(T67, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: minus(T73, T80, X97)\n\nT73 is ground\nT80 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: minus(T73, T80, X97), SCOPE: 10, CLAUSE: 0 | minus(T73, T80, X97), SCOPE: 10, CLAUSE: 1 | minus(T73, T80, X97), SCOPE: 10, CLAUSE: 2\n\nT73 is ground\nT80 is ground\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(user_defined_=(T87, 0), ','(!_10, user_defined_=(X130, 0))) | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT87 is ground\nT88 is ground\nX97 is free\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(user_defined_=(T87, 0), ','(!_10, user_defined_=(X130, 0))), SCOPE: 11, CLAUSE: 6 | ?_11 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT87 is ground\nT88 is ground\nX97 is free\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(!_10, user_defined_=(X130, 0)) | ?_11 | minus(0, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(0, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT88 is ground\nX97 is free\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ?_11 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT87 is ground\nT88 is ground\nX97 is free\nX133 is free\nuser_defined_=(T87, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: user_defined_=(X130, 0)\n\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: user_defined_=(X130, 0), SCOPE: 12, CLAUSE: 6\n\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: minus(T87, T88, X97), SCOPE: 10, CLAUSE: 1 | minus(T87, T88, X97), SCOPE: 10, CLAUSE: 2\n\nT87 is ground\nT88 is ground\nX97 is free\nX133 is free\nuser_defined_=(T87, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(user_defined_=(T97, 0), ','(!_10, user_defined_=(X151, T96))) | minus(T96, T97, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nT97 is ground\nX97 is free\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(user_defined_=(T97, 0), ','(!_10, user_defined_=(X151, T96))), SCOPE: 13, CLAUSE: 6 | ?_13 | minus(T96, T97, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nT97 is ground\nX97 is free\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(!_10, user_defined_=(X151, T96)) | ?_13 | minus(T96, 0, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nX97 is free\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ?_13 | minus(T96, T97, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nT97 is ground\nX97 is free\nX133 is free\nX154 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)\nuser_defined_=(T97, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: user_defined_=(X151, T96)\n\nT96 is ground\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: user_defined_=(X151, T96), SCOPE: 14, CLAUSE: 6\n\nT96 is ground\nX133 is free\nX151 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: minus(T96, T97, X97), SCOPE: 10, CLAUSE: 2\n\nT96 is ground\nT97 is ground\nX97 is free\nX133 is free\nX154 is free\nuser_defined_=(T96, 0) !=? user_defined_=(X133, X133)\nuser_defined_=(T97, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(user_defined_=(T108, s(X180)), ','(user_defined_=(T109, s(X181)), minus(X180, X181, X182)))\n\nT108 is ground\nT109 is ground\nX133 is free\nX154 is free\nX182 is free\nX180 is free\nX181 is free\nuser_defined_=(T108, 0) !=? user_defined_=(X133, X133)\nuser_defined_=(T109, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(user_defined_=(T108, s(X180)), ','(user_defined_=(T109, s(X181)), minus(X180, X181, X182))), SCOPE: 15, CLAUSE: 6\n\nT108 is ground\nT109 is ground\nX133 is free\nX154 is free\nX182 is free\nX180 is free\nX181 is free\nuser_defined_=(T108, 0) !=? user_defined_=(X133, X133)\nuser_defined_=(T109, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(user_defined_=(T109, s(X181)), minus(T115, X181, X182))\n\nT109 is ground\nT115 is ground\nX154 is free\nX182 is free\nX181 is free\nuser_defined_=(T109, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(user_defined_=(T109, s(X181)), minus(T115, X181, X182)), SCOPE: 16, CLAUSE: 6\n\nT109 is ground\nT115 is ground\nX154 is free\nX182 is free\nX181 is free\nuser_defined_=(T109, 0) !=? user_defined_=(X154, X154)", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: minus(T115, T122, X182)\n\nT115 is ground\nT122 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: div(T45, T40, X41)\n\nT40 is ground\nT45 is ground\nX9 is free\nX41 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: user_defined_=(T42, s(T127))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: div(T45, T40, X41), SCOPE: 17, CLAUSE: 3 | div(T45, T40, X41), SCOPE: 17, CLAUSE: 4 | div(T45, T40, X41), SCOPE: 17, CLAUSE: 5\n\nT40 is ground\nT45 is ground\nX9 is free\nX41 is free\nuser_defined_=(T40, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(user_defined_=(T135, 0), ','(!_17, fail)) | div(T134, T135, X41), SCOPE: 17, CLAUSE: 4 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 5\n\nT134 is ground\nT135 is ground\nX9 is free\nX41 is free\nuser_defined_=(T135, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(user_defined_=(T135, 0), ','(!_17, fail)), SCOPE: 18, CLAUSE: 6 | ?_18 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 4 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 5\n\nT134 is ground\nT135 is ground\nX9 is free\nX41 is free\nuser_defined_=(T135, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ?_18 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 4 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 5\n\nT134 is ground\nT135 is ground\nX9 is free\nX41 is free\nuser_defined_=(T135, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: div(T134, T135, X41), SCOPE: 17, CLAUSE: 4 | div(T134, T135, X41), SCOPE: 17, CLAUSE: 5\n\nT134 is ground\nT135 is ground\nX9 is free\nX41 is free\nuser_defined_=(T135, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(user_defined_=(T141, 0), ','(!_17, user_defined_=(X236, 0))) | div(T141, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT141 is ground\nT142 is ground\nX9 is free\nX41 is free\nX236 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(user_defined_=(T141, 0), ','(!_17, user_defined_=(X236, 0))), SCOPE: 19, CLAUSE: 6 | ?_19 | div(T141, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT141 is ground\nT142 is ground\nX9 is free\nX41 is free\nX236 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(!_17, user_defined_=(X236, 0)) | ?_19 | div(0, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT142 is ground\nX9 is free\nX41 is free\nX236 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ?_19 | div(T141, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT141 is ground\nT142 is ground\nX9 is free\nX41 is free\nX239 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T141, 0) !=? user_defined_=(X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: user_defined_=(X236, 0)\n\nX236 is free", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: user_defined_=(X236, 0), SCOPE: 20, CLAUSE: 6\n\nX236 is free", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: div(T141, T142, X41), SCOPE: 17, CLAUSE: 5\n\nT141 is ground\nT142 is ground\nX9 is free\nX41 is free\nX239 is free\nuser_defined_=(T142, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T141, 0) !=? user_defined_=(X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(minus(T152, T153, X263), ','(div(X263, T153, X264), user_defined_=(X265, s(X264))))\n\nT152 is ground\nT153 is ground\nX9 is free\nX239 is free\nX265 is free\nX263 is free\nX264 is free\nuser_defined_=(T153, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T152, 0) !=? user_defined_=(X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: minus(T152, T153, X263)\n\nT152 is ground\nT153 is ground\nX9 is free\nX239 is free\nX263 is free\nuser_defined_=(T153, 0) !=? user_defined_=(X9, X9)\nuser_defined_=(T152, 0) !=? user_defined_=(X239, X239)", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(div(T156, T153, X264), user_defined_=(X265, s(X264)))\n\nT153 is ground\nT156 is ground\nX9 is free\nX265 is free\nX264 is free\nuser_defined_=(T153, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: div(T156, T153, X264)\n\nT153 is ground\nT156 is ground\nX9 is free\nX264 is free\nuser_defined_=(T153, 0) !=? user_defined_=(X9, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: user_defined_=(X265, s(T161))\n\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: user_defined_=(X265, s(T161)), SCOPE: 21, CLAUSE: 6\n\nX265 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: user_defined_=(T42, s(T127)), SCOPE: 22, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 185 [arrowhead = none ];
185 -> 3;

186 [label="ONLY EVAL with clause\ndiv(X4, X5, X6) :- ','(user_defined_=(X5, 0), ','(!_1, fail)).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T8,\nX5 -> T8,\nT3 -> T9,\nX6 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 186 [arrowhead = none ];
186 -> 5;

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

188 [label="EVAL with clause\nuser_defined_=(X9, X9).\nand substitutionT8 -> 0,\nX9 -> 0,\nT12 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 188 [arrowhead = none ];
188 -> 9;

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

190 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 190 [arrowhead = none ];
190 -> 13;

191 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 191 [arrowhead = none ];
191 -> 18;

192 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 192 [arrowhead = none ];
192 -> 16;

193 [label="ONLY EVAL with clause\ndiv(X16, X17, X18) :- ','(user_defined_=(X16, 0), ','(!_1, user_defined_=(X18, 0))).\nand substitutionT7 -> T20,\nX16 -> T20,\nT8 -> T21,\nX17 -> T21,\nT3 -> T23,\nX18 -> T23,\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 193 [arrowhead = none ];
193 -> 20;

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

195 [label="EVAL with clause\nuser_defined_=(X21, X21).\nand substitutionT20 -> 0,\nX21 -> 0,\nT26 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 195 [arrowhead = none ];
195 -> 24;

196 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 196 [arrowhead = none ];
196 -> 26;

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

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

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

200 [label="EVAL with clause\nuser_defined_=(X24, X24).\nand substitutionT23 -> 0,\nX24 -> 0,\nT29 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 200 [arrowhead = none ];
200 -> 33;

201 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 201 [arrowhead = none ];
201 -> 35;

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

203 [label="ONLY EVAL with clause\ndiv(X37, X38, X39) :- ','(minus(X37, X38, X40), ','(div(X40, X38, X41), user_defined_=(X39, s(X41)))).\nand substitutionT20 -> T39,\nX37 -> T39,\nT21 -> T40,\nX38 -> T40,\nT3 -> T42,\nX39 -> T42,\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 203 [arrowhead = none ];
203 -> 40;

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

205 [label="SPLIT 2\nnew knowledge:\nT39 is ground\nT40 is ground\nT45 is ground\nreplacements:X40 -> T45", fontsize=14, style = filled, fillcolor = violet];
40 -> 205 [arrowhead = none ];
205 -> 44;

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

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

208 [label="SPLIT 2\nnew knowledge:\nT45 is ground\nT40 is ground\nreplacements:X41 -> T127", fontsize=14, style = filled, fillcolor = violet];
44 -> 208 [arrowhead = none ];
208 -> 132;

209 [label="ONLY EVAL with clause\nminus(X58, X59, X60) :- ','(user_defined_=(X58, 0), ','(!_5, user_defined_=(X60, 0))).\nand substitutionT39 -> T52,\nX58 -> T52,\nT40 -> T53,\nX59 -> T53,\nX40 -> X61,\nX60 -> X61", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 209 [arrowhead = none ];
209 -> 48;

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

211 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T52, 0), user_defined_=(X21, X21))", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 211 [arrowhead = none ];
211 -> 52;

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

213 [label="ONLY EVAL with clause\nminus(X71, X72, X73) :- ','(user_defined_=(X72, 0), ','(!_5, user_defined_=(X73, X71))).\nand substitutionT52 -> T59,\nX71 -> T59,\nT53 -> T60,\nX72 -> T60,\nX40 -> X74,\nX73 -> X74", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 213 [arrowhead = none ];
213 -> 56;

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

215 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T60, 0), user_defined_=(X9, X9))", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 215 [arrowhead = none ];
215 -> 60;

216 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 216 [arrowhead = none ];
216 -> 62;

217 [label="ONLY EVAL with clause\nminus(X92, X93, X94) :- ','(user_defined_=(X92, s(X95)), ','(user_defined_=(X93, s(X96)), minus(X95, X96, X94))).\nand substitutionT59 -> T66,\nX92 -> T66,\nT60 -> T67,\nX93 -> T67,\nX40 -> X97,\nX94 -> X97", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 217 [arrowhead = none ];
217 -> 64;

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

219 [label="EVAL with clause\nuser_defined_=(X106, X106).\nand substitutionT66 -> s(T73),\nX106 -> s(T73),\nX95 -> T73,\nT72 -> s(T73)", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 219 [arrowhead = none ];
219 -> 68;

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

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

222 [label="EVAL with clause\nuser_defined_=(X114, X114).\nand substitutionT67 -> s(T80),\nX114 -> s(T80),\nX96 -> T80,\nT79 -> s(T80)", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 222 [arrowhead = none ];
222 -> 74;

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

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

225 [label="ONLY EVAL with clause\nminus(X127, X128, X129) :- ','(user_defined_=(X127, 0), ','(!_10, user_defined_=(X129, 0))).\nand substitutionT73 -> T87,\nX127 -> T87,\nT80 -> T88,\nX128 -> T88,\nX97 -> X130,\nX129 -> X130", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 225 [arrowhead = none ];
225 -> 81;

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

227 [label="EVAL with clause\nuser_defined_=(X133, X133).\nand substitutionT87 -> 0,\nX133 -> 0,\nT91 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 227 [arrowhead = none ];
227 -> 85;

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

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

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

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

232 [label="ONLY EVAL with clause\nuser_defined_=(X138, X138).\nand substitutionX130 -> 0,\nX138 -> 0,\nX139 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 232 [arrowhead = none ];
232 -> 94;

233 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 233 [arrowhead = none ];
233 -> 95;

234 [label="ONLY EVAL with clause\nminus(X148, X149, X150) :- ','(user_defined_=(X149, 0), ','(!_10, user_defined_=(X150, X148))).\nand substitutionT87 -> T96,\nX148 -> T96,\nT88 -> T97,\nX149 -> T97,\nX97 -> X151,\nX150 -> X151", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 234 [arrowhead = none ];
234 -> 99;

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

236 [label="EVAL with clause\nuser_defined_=(X154, X154).\nand substitutionT97 -> 0,\nX154 -> 0,\nT100 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 236 [arrowhead = none ];
236 -> 103;

237 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 237 [arrowhead = none ];
237 -> 106;

238 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 238 [arrowhead = none ];
238 -> 107;

239 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 239 [arrowhead = none ];
239 -> 114;

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

241 [label="ONLY EVAL with clause\nuser_defined_=(X159, X159).\nand substitutionX151 -> T103,\nX159 -> T103,\nT96 -> T103,\nX160 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 241 [arrowhead = none ];
241 -> 112;

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

243 [label="ONLY EVAL with clause\nminus(X177, X178, X179) :- ','(user_defined_=(X177, s(X180)), ','(user_defined_=(X178, s(X181)), minus(X180, X181, X179))).\nand substitutionT96 -> T108,\nX177 -> T108,\nT97 -> T109,\nX178 -> T109,\nX97 -> X182,\nX179 -> X182", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 243 [arrowhead = none ];
243 -> 116;

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

245 [label="EVAL with clause\nuser_defined_=(X191, X191).\nand substitutionT108 -> s(T115),\nX191 -> s(T115),\nX180 -> T115,\nT114 -> s(T115)", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 245 [arrowhead = none ];
245 -> 121;

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

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

248 [label="EVAL with clause\nuser_defined_=(X199, X199).\nand substitutionT109 -> s(T122),\nX199 -> s(T122),\nX181 -> T122,\nT121 -> s(T122)", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 248 [arrowhead = none ];
248 -> 127;

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

250 [label="INSTANCE with matching:\nT73 -> T115\nT80 -> T122\nX97 -> X182", fontsize=14, style = filled, fillcolor = lightgrey];
127 -> 250 [arrowhead = none , style=dashed];
250 -> 74[style=dashed];

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

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

253 [label="ONLY EVAL with clause\ndiv(X220, X221, X222) :- ','(user_defined_=(X221, 0), ','(!_17, fail)).\nand substitutionT45 -> T134,\nX220 -> T134,\nT40 -> T135,\nX221 -> T135,\nX41 -> X223,\nX222 -> X223", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 253 [arrowhead = none ];
253 -> 136;

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

255 [label="BACKTRACK\nfor clause: user_defined_=(X, X)\nwith clash: (user_defined_=(T135, 0), user_defined_=(X9, X9))", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 255 [arrowhead = none ];
255 -> 140;

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

257 [label="ONLY EVAL with clause\ndiv(X233, X234, X235) :- ','(user_defined_=(X233, 0), ','(!_17, user_defined_=(X235, 0))).\nand substitutionT134 -> T141,\nX233 -> T141,\nT135 -> T142,\nX234 -> T142,\nX41 -> X236,\nX235 -> X236", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 257 [arrowhead = none ];
257 -> 144;

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

259 [label="EVAL with clause\nuser_defined_=(X239, X239).\nand substitutionT141 -> 0,\nX239 -> 0,\nT145 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 259 [arrowhead = none ];
259 -> 148;

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

261 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 261 [arrowhead = none ];
261 -> 153;

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

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

264 [label="ONLY EVAL with clause\nuser_defined_=(X244, X244).\nand substitutionX236 -> 0,\nX244 -> 0,\nX245 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 264 [arrowhead = none ];
264 -> 158;

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

266 [label="ONLY EVAL with clause\ndiv(X260, X261, X262) :- ','(minus(X260, X261, X263), ','(div(X263, X261, X264), user_defined_=(X262, s(X264)))).\nand substitutionT141 -> T152,\nX260 -> T152,\nT142 -> T153,\nX261 -> T153,\nX41 -> X265,\nX262 -> X265", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 266 [arrowhead = none ];
266 -> 164;

267 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
164 -> 267 [arrowhead = none ];
267 -> 165;

268 [label="SPLIT 2\nnew knowledge:\nT152 is ground\nT153 is ground\nT156 is ground\nreplacements:X263 -> T156", fontsize=14, style = filled, fillcolor = violet];
164 -> 268 [arrowhead = none ];
268 -> 166;

269 [label="INSTANCE with matching:\nT39 -> T152\nT40 -> T153\nX40 -> X263\nX21 -> X239", fontsize=14, style = filled, fillcolor = lightgrey];
165 -> 269 [arrowhead = none , style=dashed];
269 -> 42[style=dashed];

270 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
166 -> 270 [arrowhead = none ];
270 -> 173;

271 [label="SPLIT 2\nnew knowledge:\nT156 is ground\nT153 is ground\nreplacements:X264 -> T161", fontsize=14, style = filled, fillcolor = violet];
166 -> 271 [arrowhead = none ];
271 -> 174;

272 [label="INSTANCE with matching:\nT45 -> T156\nT40 -> T153\nX41 -> X264", fontsize=14, style = filled, fillcolor = lightgrey];
173 -> 272 [arrowhead = none , style=dashed];
272 -> 131[style=dashed];

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

274 [label="ONLY EVAL with clause\nuser_defined_=(X286, X286).\nand substitutionX265 -> s(T166),\nX286 -> s(T166),\nT161 -> T166,\nX287 -> s(T166)", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 274 [arrowhead = none ];
274 -> 179;

275 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
179 -> 275 [arrowhead = none ];
275 -> 180;

276 [label="EVAL with clause\nuser_defined_=(X290, X290).\nand substitutionT42 -> s(T172),\nX290 -> s(T172),\nT127 -> T172,\nT171 -> s(T172)", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 276 [arrowhead = none ];
276 -> 182;

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

278 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 278 [arrowhead = none ];
278 -> 184;

}

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F2_IN(z0, z1) → c1(U1'(f40_in(z0, z1), z0, z1), F40_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c3(U2'(f74_in(z0, z1), s(z0), s(z1)), F74_IN(z0, z1))
F131_IN(z0, z1) → c6(U3'(f164_in(z0, z1), z0, z1), F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(U4'(f74_in(z0, z1), s(z0), s(z1)), F74_IN(z0, z1))
F40_IN(z0, z1) → c14(U5'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c15(U6'(f44_in(z0, z2), z1, z2, z0), F44_IN(z0, z2))
F44_IN(z0, z1) → c17(U7'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
U7'(f131_out1, z0, z1) → c18(U8'(f132_in, z0, z1), F132_IN)
F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(U10'(f166_in(z0, z2), z1, z2, z0), F166_IN(z0, z2))
F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
U11'(f131_out1, z0, z1) → c24(U12'(f174_in, z0, z1), F174_IN)

S tuples:

F2_IN(z0, z1) → c1(U1'(f40_in(z0, z1), z0, z1), F40_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c3(U2'(f74_in(z0, z1), s(z0), s(z1)), F74_IN(z0, z1))
F131_IN(z0, z1) → c6(U3'(f164_in(z0, z1), z0, z1), F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(U4'(f74_in(z0, z1), s(z0), s(z1)), F74_IN(z0, z1))
F40_IN(z0, z1) → c14(U5'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c15(U6'(f44_in(z0, z2), z1, z2, z0), F44_IN(z0, z2))
F44_IN(z0, z1) → c17(U7'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
U7'(f131_out1, z0, z1) → c18(U8'(f132_in, z0, z1), F132_IN)
F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(U10'(f166_in(z0, z2), z1, z2, z0), F166_IN(z0, z2))
F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
U11'(f131_out1, z0, z1) → c24(U12'(f174_in, z0, z1), F174_IN)

K tuples:none
Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F2_IN, F42_IN, F131_IN, F74_IN, F40_IN, U5', F44_IN, U7', F164_IN, U9', F166_IN, U11'

Compound Symbols:

c1, c3, c6, c10, c14, c15, c17, c18, c20, c21, c23, c24

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

Split RHS of tuples not part of any SCC

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F131_IN(z0, z1) → c6(U3'(f164_in(z0, z1), z0, z1), F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(U4'(f74_in(z0, z1), s(z0), s(z1)), F74_IN(z0, z1))
F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(U10'(f166_in(z0, z2), z1, z2, z0), F166_IN(z0, z2))
F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F2_IN(z0, z1) → c(U1'(f40_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c(F40_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(U2'(f74_in(z0, z1), s(z0), s(z1)))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(U6'(f44_in(z0, z2), z1, z2, z0))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
U7'(f131_out1, z0, z1) → c(U8'(f132_in, z0, z1))
U7'(f131_out1, z0, z1) → c(F132_IN)
U11'(f131_out1, z0, z1) → c(U12'(f174_in, z0, z1))
U11'(f131_out1, z0, z1) → c(F174_IN)

S tuples:

F131_IN(z0, z1) → c6(U3'(f164_in(z0, z1), z0, z1), F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(U4'(f74_in(z0, z1), s(z0), s(z1)), F74_IN(z0, z1))
F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(U10'(f166_in(z0, z2), z1, z2, z0), F166_IN(z0, z2))
F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F2_IN(z0, z1) → c(U1'(f40_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c(F40_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(U2'(f74_in(z0, z1), s(z0), s(z1)))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(U6'(f44_in(z0, z2), z1, z2, z0))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
U7'(f131_out1, z0, z1) → c(U8'(f132_in, z0, z1))
U7'(f131_out1, z0, z1) → c(F132_IN)
U11'(f131_out1, z0, z1) → c(U12'(f174_in, z0, z1))
U11'(f131_out1, z0, z1) → c(F174_IN)

K tuples:none
Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F131_IN, F74_IN, F164_IN, U9', F166_IN, F2_IN, F42_IN, F40_IN, U5', F44_IN, U7', U11'

Compound Symbols:

c6, c10, c20, c21, c23, c

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

Removed 10 trailing tuple parts

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F2_IN(z0, z1) → c(F40_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F2_IN(z0, z1) → c
F42_IN(s(z0), s(z1)) → c
U5'(f42_out1(z0), z1, z2) → c
U7'(f131_out1, z0, z1) → c
U11'(f131_out1, z0, z1) → c

S tuples:

F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F2_IN(z0, z1) → c(F40_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F2_IN(z0, z1) → c
F42_IN(s(z0), s(z1)) → c
U5'(f42_out1(z0), z1, z2) → c
U7'(f131_out1, z0, z1) → c
U11'(f131_out1, z0, z1) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F164_IN, F166_IN, F2_IN, F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', U7', U11'

Compound Symbols:

c20, c23, c, c6, c10, c21, c

(29) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(z0, z1) → c(F40_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F2_IN(z0, z1) → c
U5'(f42_out1(z0), z1, z2) → c
U7'(f131_out1, z0, z1) → c
U7'(f131_out1, z0, z1) → c
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
U5'(f42_out1(z0), z1, z2) → c
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
U7'(f131_out1, z0, z1) → c
U7'(f131_out1, z0, z1) → c

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F2_IN(z0, z1) → c(F40_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F2_IN(z0, z1) → c
F42_IN(s(z0), s(z1)) → c
U5'(f42_out1(z0), z1, z2) → c
U7'(f131_out1, z0, z1) → c
U11'(f131_out1, z0, z1) → c

S tuples:

F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1))
F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F42_IN(s(z0), s(z1)) → c
U11'(f131_out1, z0, z1) → c

K tuples:

F2_IN(z0, z1) → c(F40_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F2_IN(z0, z1) → c
U5'(f42_out1(z0), z1, z2) → c
U7'(f131_out1, z0, z1) → c

Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F164_IN, F166_IN, F2_IN, F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', U7', U11'

Compound Symbols:

c20, c23, c, c6, c10, c21, c

(31) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F164_IN(z0, z1) → c20(U9'(f42_in(z0, z1), z0, z1), F42_IN(z0, z1)) by

F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F2_IN(z0, z1) → c(F40_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F2_IN(z0, z1) → c
F42_IN(s(z0), s(z1)) → c
U5'(f42_out1(z0), z1, z2) → c
U7'(f131_out1, z0, z1) → c
U11'(f131_out1, z0, z1) → c
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))

S tuples:

F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F42_IN(s(z0), s(z1)) → c
U11'(f131_out1, z0, z1) → c
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))

K tuples:

F2_IN(z0, z1) → c(F40_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F2_IN(z0, z1) → c
U5'(f42_out1(z0), z1, z2) → c
U7'(f131_out1, z0, z1) → c

Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F166_IN, F2_IN, F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', U7', U11', F164_IN

Compound Symbols:

c23, c, c6, c10, c21, c, c20

(33) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 6 of 18 dangling nodes:

F2_IN(z0, z1) → c(F40_IN(z0, z1))
F40_IN(z0, z1) → c(F42_IN(z0, z1))
F44_IN(z0, z1) → c(U7'(f131_in(z0, z1), z0, z1))
F2_IN(z0, z1) → c
U7'(f131_out1, z0, z1) → c
U5'(f42_out1(z0), z1, z2) → c

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F42_IN(s(z0), s(z1)) → c
U11'(f131_out1, z0, z1) → c
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))

S tuples:

F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F42_IN(s(z0), s(z1)) → c
U11'(f131_out1, z0, z1) → c
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))

K tuples:

F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F166_IN, F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', U11', F164_IN

Compound Symbols:

c23, c, c6, c10, c21, c, c20

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

Split RHS of tuples not part of any SCC

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))

S tuples:

F166_IN(z0, z1) → c23(U11'(f131_in(z0, z1), z0, z1), F131_IN(z0, z1))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))

K tuples:

F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F166_IN, F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', F164_IN

Compound Symbols:

c23, c, c6, c10, c21, c20

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

Removed 1 trailing tuple parts

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))

S tuples:

F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))

K tuples:

F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', F164_IN, F166_IN

Compound Symbols:

c, c6, c10, c21, c20, c23

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

U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))

We considered the (Usable) Rules:

f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))

And the Tuples:

F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))

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

POL(0) = 0   
POL(F131_IN(x₁, x₂)) = [3] + [3]x₁   
POL(F164_IN(x₁, x₂)) = [3] + [3]x₁   
POL(F166_IN(x₁, x₂)) = [3] + [3]x₁   
POL(F40_IN(x₁, x₂)) = [3] + [3]x₁ + [2]x₂   
POL(F42_IN(x₁, x₂)) = 0   
POL(F44_IN(x₁, x₂)) = [3] + [3]x₁ + [2]x₂   
POL(F74_IN(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = x₁   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U5'(x₁, x₂, x₃)) = [3]x₁ + [2]x₃   
POL(U9'(x₁, x₂, x₃)) = [3]x₁   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c20(x₁, x₂)) = x₁ + x₂   
POL(c21(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(f42_in(x₁, x₂)) = [1] + x₁   
POL(f42_out1(x₁)) = [2] + x₁   
POL(f74_in(x₁, x₂)) = [3] + x₁   
POL(f74_out1(x₁)) = [2] + x₁   
POL(s(x₁)) = [2] + x₁   

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))

S tuples:

F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))

K tuples:

F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))

Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', F164_IN, F166_IN

Compound Symbols:

c, c6, c10, c21, c20, c23

(41) CdtKnowledgeProof (EQUIVALENT transformation)

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

F166_IN(z0, z1) → c23(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))

S tuples:

F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))

K tuples:

F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', F164_IN, F166_IN

Compound Symbols:

c, c6, c10, c21, c20, c23

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

F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))

We considered the (Usable) Rules:

f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))

And the Tuples:

F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))

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

POL(0) = 0   
POL(F131_IN(x₁, x₂)) = [1] + x₁ + x₂² + x₁·x₂ + x₁²   
POL(F164_IN(x₁, x₂)) = [1] + x₁ + x₂² + x₁·x₂ + x₁²   
POL(F166_IN(x₁, x₂)) = [1] + x₁ + x₂² + x₁·x₂ + x₁²   
POL(F40_IN(x₁, x₂)) = [1] + x₁ + x₂² + x₁·x₂ + x₁²   
POL(F42_IN(x₁, x₂)) = x₁   
POL(F44_IN(x₁, x₂)) = [1] + x₁ + x₂² + x₁·x₂ + x₁²   
POL(F74_IN(x₁, x₂)) = [1] + x₁   
POL(U2(x₁, x₂, x₃)) = x₁   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U5'(x₁, x₂, x₃)) = [1] + x₁ + x₃² + x₁·x₃ + x₁²   
POL(U9'(x₁, x₂, x₃)) = [1] + x₁ + x₂ + x₃² + x₁·x₃ + x₁²   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c20(x₁, x₂)) = x₁ + x₂   
POL(c21(x₁)) = x₁   
POL(c23(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(f42_in(x₁, x₂)) = x₁   
POL(f42_out1(x₁)) = x₁   
POL(f74_in(x₁, x₂)) = x₁   
POL(f74_out1(x₁)) = x₁   
POL(s(x₁)) = [1] + x₁   

(44) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0, z0) → f2_out1
f2_in(z0, z1) → U1(f40_in(z0, z1), z0, z1)
U1(f40_out1(z0), z1, z2) → f2_out1
f42_in(s(z0), s(z1)) → U2(f74_in(z0, z1), s(z0), s(z1))
U2(f74_out1(z0), s(z1), s(z2)) → f42_out1(z0)
f131_in(0, z0) → f131_out1
f131_in(z0, z1) → U3(f164_in(z0, z1), z0, z1)
U3(f164_out1(z0), z1, z2) → f131_out1
f74_in(0, z0) → f74_out1(0)
f74_in(z0, 0) → f74_out1(z0)
f74_in(s(z0), s(z1)) → U4(f74_in(z0, z1), s(z0), s(z1))
U4(f74_out1(z0), s(z1), s(z2)) → f74_out1(z0)
f132_in → f132_out1
f174_in → f174_out1
f40_in(z0, z1) → U5(f42_in(z0, z1), z0, z1)
U5(f42_out1(z0), z1, z2) → U6(f44_in(z0, z2), z1, z2, z0)
U6(f44_out1, z0, z1, z2) → f40_out1(z2)
f44_in(z0, z1) → U7(f131_in(z0, z1), z0, z1)
U7(f131_out1, z0, z1) → U8(f132_in, z0, z1)
U8(f132_out1, z0, z1) → f44_out1
f164_in(z0, z1) → U9(f42_in(z0, z1), z0, z1)
U9(f42_out1(z0), z1, z2) → U10(f166_in(z0, z2), z1, z2, z0)
U10(f166_out1, z0, z1, z2) → f164_out1(z2)
f166_in(z0, z1) → U11(f131_in(z0, z1), z0, z1)
U11(f131_out1, z0, z1) → U12(f174_in, z0, z1)
U12(f174_out1, z0, z1) → f166_out1

Tuples:

F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))

S tuples:none
K tuples:

F40_IN(z0, z1) → c(U5'(f42_in(z0, z1), z0, z1))
U5'(f42_out1(z0), z1, z2) → c(F44_IN(z0, z2))
F44_IN(z0, z1) → c(F131_IN(z0, z1))
U9'(f42_out1(z0), z1, z2) → c21(F166_IN(z0, z2))
F166_IN(z0, z1) → c23(F131_IN(z0, z1))
F131_IN(z0, z1) → c6(F164_IN(z0, z1))
F164_IN(s(z0), s(z1)) → c20(U9'(U2(f74_in(z0, z1), s(z0), s(z1)), s(z0), s(z1)), F42_IN(s(z0), s(z1)))
F42_IN(s(z0), s(z1)) → c(F74_IN(z0, z1))
F74_IN(s(z0), s(z1)) → c10(F74_IN(z0, z1))

Defined Rule Symbols:

f2_in, U1, f42_in, U2, f131_in, U3, f74_in, U4, f132_in, f174_in, f40_in, U5, U6, f44_in, U7, U8, f164_in, U9, U10, f166_in, U11, U12

Defined Pair Symbols:

F42_IN, F40_IN, U5', F44_IN, F131_IN, F74_IN, U9', F164_IN, F166_IN

Compound Symbols:

c, c6, c10, c21, c20, c23

(45) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(46) BOUNDS(O(1), O(1))