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

(0) Obligation:

Clauses:

m(X, 0, Z) :- ','(!, =(Z, X)).
m(0, Y, Z) :- ','(!, =(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(0), 0).
p(s(s(X)), s(Y)) :- p(s(X), Y).
=(X, X).

Query: m(g,g,a)

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

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

(2) Obligation:

Clauses:

m(X, 0, Z) :- ','(!, user_defined_=(Z, X)).
m(0, Y, Z) :- ','(!, user_defined_=(Z, 0)).
m(X, Y, Z) :- ','(p(X, A), ','(p(Y, B), m(A, B, Z))).
p(0, 0).
p(s(0), 0).
p(s(s(X)), s(Y)) :- p(s(X), Y).
user_defined_=(X, X).

Query: m(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];
3 [label="3: m(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: m(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(!_1, user_defined_=(T8, T6)) | m(T6, 0, T3), SCOPE: 1, CLAUSE: 1 | m(T6, 0, T3), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: m(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX3 is free\nX4 is free\nm(T1, T2, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: user_defined_=(T8, T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: user_defined_=(T8, T6), SCOPE: 2, CLAUSE: 6\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(!_1, user_defined_=(T16, 0)) | m(0, T14, T3), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nX3 is free\nX4 is free\nm(0, T14, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nm(T1, T2, T3) !=? m(X3, 0, X4)\nm(T1, T2, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: user_defined_=(T16, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: user_defined_=(T16, 0), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26)))\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 3 | ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 4 | ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 4 | ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(p(T24, X22), m(0, X22, T26)) | ','(p(s(0), X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 5\n\nT24 is ground\nX3 is free\nX4 is free\nX21 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(p(T23, X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 5\n\nT23 is ground\nT24 is ground\nX3 is free\nX4 is free\nX10 is free\nX11 is free\nX21 is free\nX22 is free\nm(T23, T24, T3) !=? m(X3, 0, X4)\nm(T23, T24, T3) !=? m(0, X10, X11)\np(T23, X21) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(p(T24, X22), m(0, X22, T26))\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(p(s(0), X21), ','(p(T24, X22), m(X21, X22, T26))), SCOPE: 4, CLAUSE: 5\n\nT24 is ground\nX3 is free\nX4 is free\nX21 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: p(T24, X22)\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: m(0, T27, T26)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: p(T24, X22), SCOPE: 5, CLAUSE: 3 | p(T24, X22), SCOPE: 5, CLAUSE: 4 | p(T24, X22), SCOPE: 5, CLAUSE: 5\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: p(T24, X22), SCOPE: 5, CLAUSE: 4 | p(T24, X22), SCOPE: 5, CLAUSE: 5\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: true | p(s(0), X22), SCOPE: 5, CLAUSE: 5\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: p(T24, X22), SCOPE: 5, CLAUSE: 5\n\nT24 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(0), T24, T3) !=? m(X3, 0, X4)\np(T24, X22) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: p(s(0), X22), SCOPE: 5, CLAUSE: 5\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: p(s(T30), X33)\n\nT30 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: p(s(T30), X33), SCOPE: 6, CLAUSE: 3 | p(s(T30), X33), SCOPE: 6, CLAUSE: 4 | p(s(T30), X33), SCOPE: 6, CLAUSE: 5\n\nT30 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: p(s(T30), X33), SCOPE: 6, CLAUSE: 4 | p(s(T30), X33), SCOPE: 6, CLAUSE: 5\n\nT30 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: true | p(s(0), X33), SCOPE: 6, CLAUSE: 5\n\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: p(s(T30), X33), SCOPE: 6, CLAUSE: 5\n\nT30 is ground\nX33 is free\np(s(T30), X33) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: p(s(0), X33), SCOPE: 6, CLAUSE: 5\n\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: p(s(T33), X44)\n\nT33 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: m(0, T27, T26), SCOPE: 7, CLAUSE: 0 | m(0, T27, T26), SCOPE: 7, CLAUSE: 1 | m(0, T27, T26), SCOPE: 7, CLAUSE: 2\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(!_7, user_defined_=(T38, 0)) | m(0, 0, T26), SCOPE: 7, CLAUSE: 1 | m(0, 0, T26), SCOPE: 7, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: m(0, T27, T26), SCOPE: 7, CLAUSE: 1 | m(0, T27, T26), SCOPE: 7, CLAUSE: 2\n\nT27 is ground\nX51 is free\nX52 is free\nm(0, T27, T26) !=? m(X51, 0, X52)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: user_defined_=(T38, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: user_defined_=(T38, 0), SCOPE: 8, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(!_7, user_defined_=(T49, 0)) | m(0, T47, T26), SCOPE: 7, CLAUSE: 2\n\nT47 is ground\nX51 is free\nX52 is free\nm(0, T47, T26) !=? m(X51, 0, X52)", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: user_defined_=(T49, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: user_defined_=(T49, 0), SCOPE: 9, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(p(s(T55), X75), ','(p(T24, X22), m(s(X75), X22, T26)))\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nX75 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: p(s(T55), X75)\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX75 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(p(T24, X22), m(s(T56), X22, T26))\n\nT24 is ground\nT55 is ground\nT56 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: p(T24, X22)\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: m(s(T56), T57, T26)\n\nT56 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: p(T24, X22), SCOPE: 10, CLAUSE: 3 | p(T24, X22), SCOPE: 10, CLAUSE: 4 | p(T24, X22), SCOPE: 10, CLAUSE: 5\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: p(T24, X22), SCOPE: 10, CLAUSE: 4 | p(T24, X22), SCOPE: 10, CLAUSE: 5\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: true | p(s(0), X22), SCOPE: 10, CLAUSE: 5\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: p(T24, X22), SCOPE: 10, CLAUSE: 5\n\nT24 is ground\nT55 is ground\nX3 is free\nX4 is free\nX22 is free\nm(s(s(T55)), T24, T3) !=? m(X3, 0, X4)\np(T24, X22) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: p(s(0), X22), SCOPE: 10, CLAUSE: 5\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: p(s(T60), X86)\n\nT60 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 111 [arrowhead = none ];
111 -> 4;

112 [label="EVAL with clause\nm(X3, 0, X4) :- ','(!_1, user_defined_=(X4, X3)).\nand substitutionT1 -> T6,\nX3 -> T6,\nT2 -> 0,\nT3 -> T8,\nX4 -> T8,\nT7 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 112 [arrowhead = none ];
112 -> 6;

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

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

115 [label="EVAL with clause\nm(0, X10, X11) :- ','(!_1, user_defined_=(X11, 0)).\nand substitutionT1 -> 0,\nT2 -> T14,\nX10 -> T14,\nT3 -> T16,\nX11 -> T16,\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 115 [arrowhead = none ];
115 -> 19;

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

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

118 [label="EVAL with clause\nuser_defined_=(X7, X7).\nand substitutionT8 -> T11,\nX7 -> T11,\nT6 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 118 [arrowhead = none ];
118 -> 13;

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

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

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

122 [label="ONLY EVAL with clause\nm(X18, X19, X20) :- ','(p(X18, X21), ','(p(X19, X22), m(X21, X22, X20))).\nand substitutionT1 -> T23,\nX18 -> T23,\nT2 -> T24,\nX19 -> T24,\nT3 -> T26,\nX20 -> T26,\nT25 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 122 [arrowhead = none ];
122 -> 26;

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

124 [label="EVAL with clause\nuser_defined_=(X14, X14).\nand substitutionT16 -> 0,\nX14 -> 0,\nT19 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 124 [arrowhead = none ];
124 -> 23;

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

126 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 126 [arrowhead = none ];
126 -> 25;

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

128 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T23, T24, T3), m(0, X10, X11))", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 128 [arrowhead = none ];
128 -> 28;

129 [label="EVAL with clause\np(s(0), 0).\nand substitutionT23 -> s(0),\nX21 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 129 [arrowhead = none ];
129 -> 36;

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

131 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 131 [arrowhead = none ];
131 -> 39;

132 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 132 [arrowhead = none ];
132 -> 40;

133 [label="EVAL with clause\np(s(s(X73)), s(X74)) :- p(s(X73), X74).\nand substitutionX73 -> T55,\nT23 -> s(s(T55)),\nX74 -> X75,\nX21 -> s(X75)", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 133 [arrowhead = none ];
133 -> 92;

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

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

136 [label="SPLIT 2\nnew knowledge:\nT24 is ground\nT27 is ground\nreplacements:X22 -> T27", fontsize=14, style = filled, fillcolor = violet];
39 -> 136 [arrowhead = none ];
136 -> 43;

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

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

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

140 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(0), T24, T3), m(X3, 0, X4))", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 140 [arrowhead = none ];
140 -> 47;

141 [label="EVAL with clause\np(s(0), 0).\nand substitutionT24 -> s(0),\nX22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 141 [arrowhead = none ];
141 -> 48;

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

143 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 143 [arrowhead = none ];
143 -> 51;

144 [label="EVAL with clause\np(s(s(X31)), s(X32)) :- p(s(X31), X32).\nand substitutionX31 -> T30,\nT24 -> s(s(T30)),\nX32 -> X33,\nX22 -> s(X33)", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 144 [arrowhead = none ];
144 -> 56;

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

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

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

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

149 [label="EVAL with clause\np(s(0), 0).\nand substitutionT30 -> 0,\nX33 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 149 [arrowhead = none ];
149 -> 60;

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

151 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 151 [arrowhead = none ];
151 -> 63;

152 [label="EVAL with clause\np(s(s(X42)), s(X43)) :- p(s(X42), X43).\nand substitutionX42 -> T33,\nT30 -> s(T33),\nX43 -> X44,\nX33 -> s(X44)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 152 [arrowhead = none ];
152 -> 65;

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

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

155 [label="INSTANCE with matching:\nT30 -> T33\nX33 -> X44", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 155 [arrowhead = none , style=dashed];
155 -> 56[style=dashed];

156 [label="EVAL with clause\nm(X51, 0, X52) :- ','(!_7, user_defined_=(X52, X51)).\nand substitutionX51 -> 0,\nT27 -> 0,\nT26 -> T38,\nX52 -> T38,\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 156 [arrowhead = none ];
156 -> 72;

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

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

159 [label="ONLY EVAL with clause\nm(0, X60, X61) :- ','(!_7, user_defined_=(X61, 0)).\nand substitutionT27 -> T47,\nX60 -> T47,\nT26 -> T49,\nX61 -> T49,\nT48 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 159 [arrowhead = none ];
159 -> 83;

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

161 [label="EVAL with clause\nuser_defined_=(X55, X55).\nand substitutionT38 -> 0,\nX55 -> 0,\nT41 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 161 [arrowhead = none ];
161 -> 77;

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

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

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

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

166 [label="EVAL with clause\nuser_defined_=(X64, X64).\nand substitutionT49 -> 0,\nX64 -> 0,\nT52 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 166 [arrowhead = none ];
166 -> 88;

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

168 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 168 [arrowhead = none ];
168 -> 90;

169 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
92 -> 169 [arrowhead = none ];
169 -> 94;

170 [label="SPLIT 2\nnew knowledge:\nT55 is ground\nT56 is ground\nreplacements:X75 -> T56", fontsize=14, style = filled, fillcolor = violet];
92 -> 170 [arrowhead = none ];
170 -> 95;

171 [label="INSTANCE with matching:\nT30 -> T55\nX33 -> X75", fontsize=14, style = filled, fillcolor = lightgrey];
94 -> 171 [arrowhead = none , style=dashed];
171 -> 56[style=dashed];

172 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
95 -> 172 [arrowhead = none ];
172 -> 96;

173 [label="SPLIT 2\nnew knowledge:\nT24 is ground\nT57 is ground\nreplacements:X22 -> T57", fontsize=14, style = filled, fillcolor = violet];
95 -> 173 [arrowhead = none ];
173 -> 97;

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

175 [label="INSTANCE with matching:\nT1 -> s(T56)\nT2 -> T57\nT3 -> T26", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 175 [arrowhead = none , style=dashed];
175 -> 3[style=dashed];

176 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(s(s(T55)), T24, T3), m(X3, 0, X4))", fontsize=14, style = filled, fillcolor = lightgreen];
98 -> 176 [arrowhead = none ];
176 -> 99;

177 [label="EVAL with clause\np(s(0), 0).\nand substitutionT24 -> s(0),\nX22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 177 [arrowhead = none ];
177 -> 100;

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

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

180 [label="EVAL with clause\np(s(s(X84)), s(X85)) :- p(s(X84), X85).\nand substitutionX84 -> T60,\nT24 -> s(s(T60)),\nX85 -> X86,\nX22 -> s(X86)", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 180 [arrowhead = none ];
180 -> 107;

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

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

183 [label="INSTANCE with matching:\nT30 -> T60\nX33 -> X86", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 183 [arrowhead = none , style=dashed];
183 -> 56[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f3_in(z0, 0) → f3_out1(z0)
f3_in(0, z0) → f3_out1(0)
f3_in(s(0), z0) → U1(f36_in(z0), s(0), z0)
f3_in(s(s(z0)), z1) → U2(f92_in(z0, z1), s(s(z0)), z1)
U1(f36_out1(z0, z1), s(0), z2) → f3_out1(z1)
U1(f36_out2(z0, z1, z2), s(0), z3) → f3_out1(z2)
U2(f92_out1(z0, z1, z2), s(s(z3)), z4) → f3_out1(z2)
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
f43_in(0) → f43_out1(0)
f43_in(z0) → f43_out1(0)
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))
f39_in(z0) → U6(f42_in(z0), z0)
U6(f42_out1(z0), z1) → U7(f43_in(z0), z1, z0)
U7(f43_out1(z0), z1, z2) → f39_out1(z2, z0)
f92_in(z0, z1) → U8(f56_in(z0), z0, z1)
U8(f56_out1(z0), z1, z2) → U9(f95_in(z2, z0), z1, z2, z0)
U9(f95_out1(z0, z1), z2, z3, z4) → f92_out1(z4, z0, z1)
f95_in(z0, z1) → U10(f96_in(z0), z0, z1)
U10(f96_out1(z0), z1, z2) → U11(f3_in(s(z2), z0), z1, z2, z0)
U11(f3_out1(z0), z1, z2, z3) → f95_out1(z3, z0)
f36_in(z0) → U12(f39_in(z0), f40_in(z0), z0)
U12(f39_out1(z0, z1), z2, z3) → f36_out1(z0, z1)
U12(z0, f40_out1(z1, z2, z3), z4) → f36_out2(z1, z2, z3)

Tuples:

F3_IN(s(0), z0) → c2(U1'(f36_in(z0), s(0), z0), F36_IN(z0))
F3_IN(s(s(z0)), z1) → c3(U2'(f92_in(z0, z1), s(s(z0)), z1), F92_IN(z0, z1))
F56_IN(s(z0)) → c8(U3'(f56_in(z0), s(z0)), F56_IN(z0))
F42_IN(s(s(z0))) → c11(U4'(f56_in(z0), s(s(z0))), F56_IN(z0))
F96_IN(s(s(z0))) → c16(U5'(f56_in(z0), s(s(z0))), F56_IN(z0))
F39_IN(z0) → c18(U6'(f42_in(z0), z0), F42_IN(z0))
U6'(f42_out1(z0), z1) → c19(U7'(f43_in(z0), z1, z0), F43_IN(z0))
F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(U9'(f95_in(z2, z0), z1, z2, z0), F95_IN(z2, z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
U10'(f96_out1(z0), z1, z2) → c25(U11'(f3_in(s(z2), z0), z1, z2, z0), F3_IN(s(z2), z0))
F36_IN(z0) → c27(U12'(f39_in(z0), f40_in(z0), z0), F39_IN(z0))

S tuples:

F3_IN(s(0), z0) → c2(U1'(f36_in(z0), s(0), z0), F36_IN(z0))
F3_IN(s(s(z0)), z1) → c3(U2'(f92_in(z0, z1), s(s(z0)), z1), F92_IN(z0, z1))
F56_IN(s(z0)) → c8(U3'(f56_in(z0), s(z0)), F56_IN(z0))
F42_IN(s(s(z0))) → c11(U4'(f56_in(z0), s(s(z0))), F56_IN(z0))
F96_IN(s(s(z0))) → c16(U5'(f56_in(z0), s(s(z0))), F56_IN(z0))
F39_IN(z0) → c18(U6'(f42_in(z0), z0), F42_IN(z0))
U6'(f42_out1(z0), z1) → c19(U7'(f43_in(z0), z1, z0), F43_IN(z0))
F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(U9'(f95_in(z2, z0), z1, z2, z0), F95_IN(z2, z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
U10'(f96_out1(z0), z1, z2) → c25(U11'(f3_in(s(z2), z0), z1, z2, z0), F3_IN(s(z2), z0))
F36_IN(z0) → c27(U12'(f39_in(z0), f40_in(z0), z0), F39_IN(z0))

K tuples:none
Defined Rule Symbols:

f3_in, U1, U2, f56_in, U3, f42_in, U4, f43_in, f96_in, U5, f39_in, U6, U7, f92_in, U8, U9, f95_in, U10, U11, f36_in, U12

Defined Pair Symbols:

F3_IN, F56_IN, F42_IN, F96_IN, F39_IN, U6', F92_IN, U8', F95_IN, U10', F36_IN

Compound Symbols:

c2, c3, c8, c11, c16, c18, c19, c21, c22, c24, c25, c27

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f3_in(z0, 0) → f3_out1(z0)
f3_in(0, z0) → f3_out1(0)
f3_in(s(0), z0) → U1(f36_in(z0), s(0), z0)
f3_in(s(s(z0)), z1) → U2(f92_in(z0, z1), s(s(z0)), z1)
U1(f36_out1(z0, z1), s(0), z2) → f3_out1(z1)
U1(f36_out2(z0, z1, z2), s(0), z3) → f3_out1(z2)
U2(f92_out1(z0, z1, z2), s(s(z3)), z4) → f3_out1(z2)
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
f43_in(0) → f43_out1(0)
f43_in(z0) → f43_out1(0)
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))
f39_in(z0) → U6(f42_in(z0), z0)
U6(f42_out1(z0), z1) → U7(f43_in(z0), z1, z0)
U7(f43_out1(z0), z1, z2) → f39_out1(z2, z0)
f92_in(z0, z1) → U8(f56_in(z0), z0, z1)
U8(f56_out1(z0), z1, z2) → U9(f95_in(z2, z0), z1, z2, z0)
U9(f95_out1(z0, z1), z2, z3, z4) → f92_out1(z4, z0, z1)
f95_in(z0, z1) → U10(f96_in(z0), z0, z1)
U10(f96_out1(z0), z1, z2) → U11(f3_in(s(z2), z0), z1, z2, z0)
U11(f3_out1(z0), z1, z2, z3) → f95_out1(z3, z0)
f36_in(z0) → U12(f39_in(z0), f40_in(z0), z0)
U12(f39_out1(z0, z1), z2, z3) → f36_out1(z0, z1)
U12(z0, f40_out1(z1, z2, z3), z4) → f36_out2(z1, z2, z3)

Tuples:

F3_IN(s(s(z0)), z1) → c3(U2'(f92_in(z0, z1), s(s(z0)), z1), F92_IN(z0, z1))
F56_IN(s(z0)) → c8(U3'(f56_in(z0), s(z0)), F56_IN(z0))
F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(U9'(f95_in(z2, z0), z1, z2, z0), F95_IN(z2, z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
U10'(f96_out1(z0), z1, z2) → c25(U11'(f3_in(s(z2), z0), z1, z2, z0), F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c(U1'(f36_in(z0), s(0), z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(U4'(f56_in(z0), s(s(z0))))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(U5'(f56_in(z0), s(s(z0))))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
U6'(f42_out1(z0), z1) → c(U7'(f43_in(z0), z1, z0))
U6'(f42_out1(z0), z1) → c(F43_IN(z0))
F36_IN(z0) → c(U12'(f39_in(z0), f40_in(z0), z0))
F36_IN(z0) → c(F39_IN(z0))

S tuples:

F3_IN(s(s(z0)), z1) → c3(U2'(f92_in(z0, z1), s(s(z0)), z1), F92_IN(z0, z1))
F56_IN(s(z0)) → c8(U3'(f56_in(z0), s(z0)), F56_IN(z0))
F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(U9'(f95_in(z2, z0), z1, z2, z0), F95_IN(z2, z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
U10'(f96_out1(z0), z1, z2) → c25(U11'(f3_in(s(z2), z0), z1, z2, z0), F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c(U1'(f36_in(z0), s(0), z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(U4'(f56_in(z0), s(s(z0))))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(U5'(f56_in(z0), s(s(z0))))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
U6'(f42_out1(z0), z1) → c(U7'(f43_in(z0), z1, z0))
U6'(f42_out1(z0), z1) → c(F43_IN(z0))
F36_IN(z0) → c(U12'(f39_in(z0), f40_in(z0), z0))
F36_IN(z0) → c(F39_IN(z0))

K tuples:none
Defined Rule Symbols:

f3_in, U1, U2, f56_in, U3, f42_in, U4, f43_in, f96_in, U5, f39_in, U6, U7, f92_in, U8, U9, f95_in, U10, U11, f36_in, U12

Defined Pair Symbols:

F3_IN, F56_IN, F92_IN, U8', F95_IN, U10', F42_IN, F96_IN, F39_IN, U6', F36_IN

Compound Symbols:

c3, c8, c21, c22, c24, c25, c

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

Removed 10 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f3_in(z0, 0) → f3_out1(z0)
f3_in(0, z0) → f3_out1(0)
f3_in(s(0), z0) → U1(f36_in(z0), s(0), z0)
f3_in(s(s(z0)), z1) → U2(f92_in(z0, z1), s(s(z0)), z1)
U1(f36_out1(z0, z1), s(0), z2) → f3_out1(z1)
U1(f36_out2(z0, z1, z2), s(0), z3) → f3_out1(z2)
U2(f92_out1(z0, z1, z2), s(s(z3)), z4) → f3_out1(z2)
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
f43_in(0) → f43_out1(0)
f43_in(z0) → f43_out1(0)
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))
f39_in(z0) → U6(f42_in(z0), z0)
U6(f42_out1(z0), z1) → U7(f43_in(z0), z1, z0)
U7(f43_out1(z0), z1, z2) → f39_out1(z2, z0)
f92_in(z0, z1) → U8(f56_in(z0), z0, z1)
U8(f56_out1(z0), z1, z2) → U9(f95_in(z2, z0), z1, z2, z0)
U9(f95_out1(z0, z1), z2, z3, z4) → f92_out1(z4, z0, z1)
f95_in(z0, z1) → U10(f96_in(z0), z0, z1)
U10(f96_out1(z0), z1, z2) → U11(f3_in(s(z2), z0), z1, z2, z0)
U11(f3_out1(z0), z1, z2, z3) → f95_out1(z3, z0)
f36_in(z0) → U12(f39_in(z0), f40_in(z0), z0)
U12(f39_out1(z0, z1), z2, z3) → f36_out1(z0, z1)
U12(z0, f40_out1(z1, z2, z3), z4) → f36_out2(z1, z2, z3)

Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

S tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

K tuples:none
Defined Rule Symbols:

f3_in, U1, U2, f56_in, U3, f42_in, U4, f43_in, f96_in, U5, f39_in, U6, U7, f92_in, U8, U9, f95_in, U10, U11, f36_in, U12

Defined Pair Symbols:

F92_IN, F95_IN, F3_IN, F42_IN, F96_IN, F39_IN, F36_IN, F56_IN, U8', U10', U6'

Compound Symbols:

c21, c24, c, c3, c8, c22, c25, c

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

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

F3_IN(s(0), z0) → c(F36_IN(z0))
F3_IN(s(0), z0) → c

We considered the (Usable) Rules:

f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))

And the Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

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

POL(0) = 0   
POL(F36_IN(x₁)) = [2]x₁   
POL(F39_IN(x₁)) = [2]x₁   
POL(F3_IN(x₁, x₂)) = [1] + [2]x₂   
POL(F42_IN(x₁)) = x₁   
POL(F56_IN(x₁)) = 0   
POL(F92_IN(x₁, x₂)) = [1] + [2]x₂   
POL(F95_IN(x₁, x₂)) = [1] + x₁   
POL(F96_IN(x₁)) = 0   
POL(U10'(x₁, x₂, x₃)) = [1] + [2]x₁   
POL(U3(x₁, x₂)) = 0   
POL(U4(x₁, x₂)) = 0   
POL(U5(x₁, x₂)) = 0   
POL(U6'(x₁, x₂)) = x₂   
POL(U8'(x₁, x₂, x₃)) = [1] + x₃   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c21(x₁, x₂)) = x₁ + x₂   
POL(c22(x₁)) = x₁   
POL(c24(x₁, x₂)) = x₁ + x₂   
POL(c25(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(f42_in(x₁)) = 0   
POL(f42_out1(x₁)) = 0   
POL(f56_in(x₁)) = 0   
POL(f56_out1(x₁)) = 0   
POL(f96_in(x₁)) = 0   
POL(f96_out1(x₁)) = x₁   
POL(s(x₁)) = 0   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f3_in(z0, 0) → f3_out1(z0)
f3_in(0, z0) → f3_out1(0)
f3_in(s(0), z0) → U1(f36_in(z0), s(0), z0)
f3_in(s(s(z0)), z1) → U2(f92_in(z0, z1), s(s(z0)), z1)
U1(f36_out1(z0, z1), s(0), z2) → f3_out1(z1)
U1(f36_out2(z0, z1, z2), s(0), z3) → f3_out1(z2)
U2(f92_out1(z0, z1, z2), s(s(z3)), z4) → f3_out1(z2)
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
f43_in(0) → f43_out1(0)
f43_in(z0) → f43_out1(0)
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))
f39_in(z0) → U6(f42_in(z0), z0)
U6(f42_out1(z0), z1) → U7(f43_in(z0), z1, z0)
U7(f43_out1(z0), z1, z2) → f39_out1(z2, z0)
f92_in(z0, z1) → U8(f56_in(z0), z0, z1)
U8(f56_out1(z0), z1, z2) → U9(f95_in(z2, z0), z1, z2, z0)
U9(f95_out1(z0, z1), z2, z3, z4) → f92_out1(z4, z0, z1)
f95_in(z0, z1) → U10(f96_in(z0), z0, z1)
U10(f96_out1(z0), z1, z2) → U11(f3_in(s(z2), z0), z1, z2, z0)
U11(f3_out1(z0), z1, z2, z3) → f95_out1(z3, z0)
f36_in(z0) → U12(f39_in(z0), f40_in(z0), z0)
U12(f39_out1(z0, z1), z2, z3) → f36_out1(z0, z1)
U12(z0, f40_out1(z1, z2, z3), z4) → f36_out2(z1, z2, z3)

Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

S tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

K tuples:

F3_IN(s(0), z0) → c(F36_IN(z0))
F3_IN(s(0), z0) → c

Defined Rule Symbols:

f3_in, U1, U2, f56_in, U3, f42_in, U4, f43_in, f96_in, U5, f39_in, U6, U7, f92_in, U8, U9, f95_in, U10, U11, f36_in, U12

Defined Pair Symbols:

F92_IN, F95_IN, F3_IN, F42_IN, F96_IN, F39_IN, F36_IN, F56_IN, U8', U10', U6'

Compound Symbols:

c21, c24, c, c3, c8, c22, c25, c

(11) CdtKnowledgeProof (EQUIVALENT transformation)

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

F36_IN(z0) → c(F39_IN(z0))
F36_IN(z0) → c
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
U6'(f42_out1(z0), z1) → c
U6'(f42_out1(z0), z1) → c
F42_IN(s(s(z0))) → c(F56_IN(z0))
F42_IN(s(s(z0))) → c

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f3_in(z0, 0) → f3_out1(z0)
f3_in(0, z0) → f3_out1(0)
f3_in(s(0), z0) → U1(f36_in(z0), s(0), z0)
f3_in(s(s(z0)), z1) → U2(f92_in(z0, z1), s(s(z0)), z1)
U1(f36_out1(z0, z1), s(0), z2) → f3_out1(z1)
U1(f36_out2(z0, z1, z2), s(0), z3) → f3_out1(z2)
U2(f92_out1(z0, z1, z2), s(s(z3)), z4) → f3_out1(z2)
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
f43_in(0) → f43_out1(0)
f43_in(z0) → f43_out1(0)
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))
f39_in(z0) → U6(f42_in(z0), z0)
U6(f42_out1(z0), z1) → U7(f43_in(z0), z1, z0)
U7(f43_out1(z0), z1, z2) → f39_out1(z2, z0)
f92_in(z0, z1) → U8(f56_in(z0), z0, z1)
U8(f56_out1(z0), z1, z2) → U9(f95_in(z2, z0), z1, z2, z0)
U9(f95_out1(z0, z1), z2, z3, z4) → f92_out1(z4, z0, z1)
f95_in(z0, z1) → U10(f96_in(z0), z0, z1)
U10(f96_out1(z0), z1, z2) → U11(f3_in(s(z2), z0), z1, z2, z0)
U11(f3_out1(z0), z1, z2, z3) → f95_out1(z3, z0)
f36_in(z0) → U12(f39_in(z0), f40_in(z0), z0)
U12(f39_out1(z0, z1), z2, z3) → f36_out1(z0, z1)
U12(z0, f40_out1(z1, z2, z3), z4) → f36_out2(z1, z2, z3)

Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

S tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F96_IN(s(s(z0))) → c

K tuples:

F3_IN(s(0), z0) → c(F36_IN(z0))
F3_IN(s(0), z0) → c
F36_IN(z0) → c(F39_IN(z0))
F36_IN(z0) → c
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
U6'(f42_out1(z0), z1) → c
F42_IN(s(s(z0))) → c(F56_IN(z0))
F42_IN(s(s(z0))) → c

Defined Rule Symbols:

f3_in, U1, U2, f56_in, U3, f42_in, U4, f43_in, f96_in, U5, f39_in, U6, U7, f92_in, U8, U9, f95_in, U10, U11, f36_in, U12

Defined Pair Symbols:

F92_IN, F95_IN, F3_IN, F42_IN, F96_IN, F39_IN, F36_IN, F56_IN, U8', U10', U6'

Compound Symbols:

c21, c24, c, c3, c8, c22, c25, c

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

F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))

We considered the (Usable) Rules:

f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))

And the Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

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

POL(0) = 0   
POL(F36_IN(x₁)) = [2]   
POL(F39_IN(x₁)) = [1]   
POL(F3_IN(x₁, x₂)) = x₁   
POL(F42_IN(x₁)) = [1]   
POL(F56_IN(x₁)) = 0   
POL(F92_IN(x₁, x₂)) = [2] + x₁   
POL(F95_IN(x₁, x₂)) = [2] + x₂   
POL(F96_IN(x₁)) = 0   
POL(U10'(x₁, x₂, x₃)) = [2] + x₃   
POL(U3(x₁, x₂)) = [2] + x₁   
POL(U4(x₁, x₂)) = 0   
POL(U5(x₁, x₂)) = 0   
POL(U6'(x₁, x₂)) = [1]   
POL(U8'(x₁, x₂, x₃)) = [2] + x₁   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c21(x₁, x₂)) = x₁ + x₂   
POL(c22(x₁)) = x₁   
POL(c24(x₁, x₂)) = x₁ + x₂   
POL(c25(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(f42_in(x₁)) = 0   
POL(f42_out1(x₁)) = 0   
POL(f56_in(x₁)) = x₁   
POL(f56_out1(x₁)) = x₁   
POL(f96_in(x₁)) = 0   
POL(f96_out1(x₁)) = 0   
POL(s(x₁)) = [2] + x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f3_in(z0, 0) → f3_out1(z0)
f3_in(0, z0) → f3_out1(0)
f3_in(s(0), z0) → U1(f36_in(z0), s(0), z0)
f3_in(s(s(z0)), z1) → U2(f92_in(z0, z1), s(s(z0)), z1)
U1(f36_out1(z0, z1), s(0), z2) → f3_out1(z1)
U1(f36_out2(z0, z1, z2), s(0), z3) → f3_out1(z2)
U2(f92_out1(z0, z1, z2), s(s(z3)), z4) → f3_out1(z2)
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
f43_in(0) → f43_out1(0)
f43_in(z0) → f43_out1(0)
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))
f39_in(z0) → U6(f42_in(z0), z0)
U6(f42_out1(z0), z1) → U7(f43_in(z0), z1, z0)
U7(f43_out1(z0), z1, z2) → f39_out1(z2, z0)
f92_in(z0, z1) → U8(f56_in(z0), z0, z1)
U8(f56_out1(z0), z1, z2) → U9(f95_in(z2, z0), z1, z2, z0)
U9(f95_out1(z0, z1), z2, z3, z4) → f92_out1(z4, z0, z1)
f95_in(z0, z1) → U10(f96_in(z0), z0, z1)
U10(f96_out1(z0), z1, z2) → U11(f3_in(s(z2), z0), z1, z2, z0)
U11(f3_out1(z0), z1, z2, z3) → f95_out1(z3, z0)
f36_in(z0) → U12(f39_in(z0), f40_in(z0), z0)
U12(f39_out1(z0, z1), z2, z3) → f36_out1(z0, z1)
U12(z0, f40_out1(z1, z2, z3), z4) → f36_out2(z1, z2, z3)

Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

S tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F96_IN(s(s(z0))) → c

K tuples:

F3_IN(s(0), z0) → c(F36_IN(z0))
F3_IN(s(0), z0) → c
F36_IN(z0) → c(F39_IN(z0))
F36_IN(z0) → c
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
U6'(f42_out1(z0), z1) → c
F42_IN(s(s(z0))) → c(F56_IN(z0))
F42_IN(s(s(z0))) → c
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))

Defined Rule Symbols:

f3_in, U1, U2, f56_in, U3, f42_in, U4, f43_in, f96_in, U5, f39_in, U6, U7, f92_in, U8, U9, f95_in, U10, U11, f36_in, U12

Defined Pair Symbols:

F92_IN, F95_IN, F3_IN, F42_IN, F96_IN, F39_IN, F36_IN, F56_IN, U8', U10', U6'

Compound Symbols:

c21, c24, c, c3, c8, c22, c25, c

(15) CdtKnowledgeProof (EQUIVALENT transformation)

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

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F96_IN(s(s(z0))) → c
F3_IN(s(0), z0) → c(F36_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F3_IN(s(0), z0) → c

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f3_in(z0, 0) → f3_out1(z0)
f3_in(0, z0) → f3_out1(0)
f3_in(s(0), z0) → U1(f36_in(z0), s(0), z0)
f3_in(s(s(z0)), z1) → U2(f92_in(z0, z1), s(s(z0)), z1)
U1(f36_out1(z0, z1), s(0), z2) → f3_out1(z1)
U1(f36_out2(z0, z1, z2), s(0), z3) → f3_out1(z2)
U2(f92_out1(z0, z1, z2), s(s(z3)), z4) → f3_out1(z2)
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
f43_in(0) → f43_out1(0)
f43_in(z0) → f43_out1(0)
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))
f39_in(z0) → U6(f42_in(z0), z0)
U6(f42_out1(z0), z1) → U7(f43_in(z0), z1, z0)
U7(f43_out1(z0), z1, z2) → f39_out1(z2, z0)
f92_in(z0, z1) → U8(f56_in(z0), z0, z1)
U8(f56_out1(z0), z1, z2) → U9(f95_in(z2, z0), z1, z2, z0)
U9(f95_out1(z0, z1), z2, z3, z4) → f92_out1(z4, z0, z1)
f95_in(z0, z1) → U10(f96_in(z0), z0, z1)
U10(f96_out1(z0), z1, z2) → U11(f3_in(s(z2), z0), z1, z2, z0)
U11(f3_out1(z0), z1, z2, z3) → f95_out1(z3, z0)
f36_in(z0) → U12(f39_in(z0), f40_in(z0), z0)
U12(f39_out1(z0, z1), z2, z3) → f36_out1(z0, z1)
U12(z0, f40_out1(z1, z2, z3), z4) → f36_out2(z1, z2, z3)

Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

S tuples:

F56_IN(s(z0)) → c8(F56_IN(z0))

K tuples:

F3_IN(s(0), z0) → c(F36_IN(z0))
F3_IN(s(0), z0) → c
F36_IN(z0) → c(F39_IN(z0))
F36_IN(z0) → c
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
U6'(f42_out1(z0), z1) → c
F42_IN(s(s(z0))) → c(F56_IN(z0))
F42_IN(s(s(z0))) → c
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F96_IN(s(s(z0))) → c

Defined Rule Symbols:

f3_in, U1, U2, f56_in, U3, f42_in, U4, f43_in, f96_in, U5, f39_in, U6, U7, f92_in, U8, U9, f95_in, U10, U11, f36_in, U12

Defined Pair Symbols:

F92_IN, F95_IN, F3_IN, F42_IN, F96_IN, F39_IN, F36_IN, F56_IN, U8', U10', U6'

Compound Symbols:

c21, c24, c, c3, c8, c22, c25, c

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

F56_IN(s(z0)) → c8(F56_IN(z0))

We considered the (Usable) Rules:

f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))

And the Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

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

POL(0) = 0   
POL(F36_IN(x₁)) = x₁ + x₁²   
POL(F39_IN(x₁)) = x₁ + x₁²   
POL(F3_IN(x₁, x₂)) = [1] + x₁ + x₂² + x₁·x₂   
POL(F42_IN(x₁)) = x₁   
POL(F56_IN(x₁)) = x₁   
POL(F92_IN(x₁, x₂)) = [1] + x₁ + x₂ + x₂² + x₁·x₂   
POL(F95_IN(x₁, x₂)) = [1] + x₁ + x₁·x₂ + x₁²   
POL(F96_IN(x₁)) = x₁   
POL(U10'(x₁, x₂, x₃)) = [1] + x₁·x₃ + x₁²   
POL(U3(x₁, x₂)) = [1] + x₁   
POL(U4(x₁, x₂)) = x₂   
POL(U5(x₁, x₂)) = [1] + x₁   
POL(U6'(x₁, x₂)) = 0   
POL(U8'(x₁, x₂, x₃)) = [1] + x₃² + x₁·x₃   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c21(x₁, x₂)) = x₁ + x₂   
POL(c22(x₁)) = x₁   
POL(c24(x₁, x₂)) = x₁ + x₂   
POL(c25(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c8(x₁)) = x₁   
POL(f42_in(x₁)) = x₁ + x₁²   
POL(f42_out1(x₁)) = 0   
POL(f56_in(x₁)) = [1] + x₁   
POL(f56_out1(x₁)) = [1] + x₁   
POL(f96_in(x₁)) = x₁   
POL(f96_out1(x₁)) = [1] + x₁   
POL(s(x₁)) = [1] + x₁   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f3_in(z0, 0) → f3_out1(z0)
f3_in(0, z0) → f3_out1(0)
f3_in(s(0), z0) → U1(f36_in(z0), s(0), z0)
f3_in(s(s(z0)), z1) → U2(f92_in(z0, z1), s(s(z0)), z1)
U1(f36_out1(z0, z1), s(0), z2) → f3_out1(z1)
U1(f36_out2(z0, z1, z2), s(0), z3) → f3_out1(z2)
U2(f92_out1(z0, z1, z2), s(s(z3)), z4) → f3_out1(z2)
f56_in(0) → f56_out1(0)
f56_in(s(z0)) → U3(f56_in(z0), s(z0))
U3(f56_out1(z0), s(z1)) → f56_out1(s(z0))
f42_in(s(0)) → f42_out1(0)
f42_in(s(s(z0))) → U4(f56_in(z0), s(s(z0)))
U4(f56_out1(z0), s(s(z1))) → f42_out1(s(z0))
f43_in(0) → f43_out1(0)
f43_in(z0) → f43_out1(0)
f96_in(s(0)) → f96_out1(0)
f96_in(s(s(z0))) → U5(f56_in(z0), s(s(z0)))
U5(f56_out1(z0), s(s(z1))) → f96_out1(s(z0))
f39_in(z0) → U6(f42_in(z0), z0)
U6(f42_out1(z0), z1) → U7(f43_in(z0), z1, z0)
U7(f43_out1(z0), z1, z2) → f39_out1(z2, z0)
f92_in(z0, z1) → U8(f56_in(z0), z0, z1)
U8(f56_out1(z0), z1, z2) → U9(f95_in(z2, z0), z1, z2, z0)
U9(f95_out1(z0, z1), z2, z3, z4) → f92_out1(z4, z0, z1)
f95_in(z0, z1) → U10(f96_in(z0), z0, z1)
U10(f96_out1(z0), z1, z2) → U11(f3_in(s(z2), z0), z1, z2, z0)
U11(f3_out1(z0), z1, z2, z3) → f95_out1(z3, z0)
f36_in(z0) → U12(f39_in(z0), f40_in(z0), z0)
U12(f39_out1(z0, z1), z2, z3) → f36_out1(z0, z1)
U12(z0, f40_out1(z1, z2, z3), z4) → f36_out2(z1, z2, z3)

Tuples:

F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F3_IN(s(0), z0) → c(F36_IN(z0))
F42_IN(s(s(z0))) → c(F56_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
F36_IN(z0) → c(F39_IN(z0))
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F56_IN(s(z0)) → c8(F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F3_IN(s(0), z0) → c
F42_IN(s(s(z0))) → c
F96_IN(s(s(z0))) → c
U6'(f42_out1(z0), z1) → c
F36_IN(z0) → c

S tuples:none
K tuples:

F3_IN(s(0), z0) → c(F36_IN(z0))
F3_IN(s(0), z0) → c
F36_IN(z0) → c(F39_IN(z0))
F36_IN(z0) → c
F39_IN(z0) → c(U6'(f42_in(z0), z0))
F39_IN(z0) → c(F42_IN(z0))
U6'(f42_out1(z0), z1) → c
F42_IN(s(s(z0))) → c(F56_IN(z0))
F42_IN(s(s(z0))) → c
F3_IN(s(s(z0)), z1) → c3(F92_IN(z0, z1))
F92_IN(z0, z1) → c21(U8'(f56_in(z0), z0, z1), F56_IN(z0))
U8'(f56_out1(z0), z1, z2) → c22(F95_IN(z2, z0))
F95_IN(z0, z1) → c24(U10'(f96_in(z0), z0, z1), F96_IN(z0))
F96_IN(s(s(z0))) → c(F56_IN(z0))
U10'(f96_out1(z0), z1, z2) → c25(F3_IN(s(z2), z0))
F96_IN(s(s(z0))) → c
F56_IN(s(z0)) → c8(F56_IN(z0))

Defined Rule Symbols:

f3_in, U1, U2, f56_in, U3, f42_in, U4, f43_in, f96_in, U5, f39_in, U6, U7, f92_in, U8, U9, f95_in, U10, U11, f36_in, U12

Defined Pair Symbols:

F92_IN, F95_IN, F3_IN, F42_IN, F96_IN, F39_IN, F36_IN, F56_IN, U8', U10', U6'

Compound Symbols:

c21, c24, c, c3, c8, c22, c25, c

(19) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(20) BOUNDS(O(1), O(1))

(21) 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: m(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: m(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(!_1, user_defined_=(T10, T8)) | m(T8, 0, T3), SCOPE: 1, CLAUSE: 1 | m(T8, 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: m(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX5 is free\nX6 is free\nm(T1, T2, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: user_defined_=(T10, T8)\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: user_defined_=(T10, T8), SCOPE: 2, CLAUSE: 6\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(!_1, user_defined_=(T20, 0)) | m(0, T18, T3), SCOPE: 1, CLAUSE: 2\n\nT18 is ground\nX5 is free\nX6 is free\nm(0, T18, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: m(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nm(T1, T2, T3) !=? m(X5, 0, X6)\nm(T1, T2, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: user_defined_=(T20, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: user_defined_=(T20, 0), SCOPE: 3, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(p(T31, X30), ','(p(T32, X31), m(X30, X31, T34)))\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX30 is free\nX31 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: p(T31, X30)\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX30 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(p(T32, X31), m(T35, X31, T34))\n\nT31 is ground\nT32 is ground\nT35 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX31 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: p(T31, X30), SCOPE: 4, CLAUSE: 3 | p(T31, X30), SCOPE: 4, CLAUSE: 4 | p(T31, X30), SCOPE: 4, CLAUSE: 5\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX30 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: p(T31, X30), SCOPE: 4, CLAUSE: 4 | p(T31, X30), SCOPE: 4, CLAUSE: 5\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX30 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true | p(s(0), X30), SCOPE: 4, CLAUSE: 5\n\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: p(T31, X30), SCOPE: 4, CLAUSE: 5\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX30 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)\np(T31, X30) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: p(s(0), X30), SCOPE: 4, CLAUSE: 5\n\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: p(s(T38), X42)\n\nT32 is ground\nT38 is ground\nX5 is free\nX6 is free\nX42 is free\nm(s(s(T38)), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: p(s(T38), X42), SCOPE: 5, CLAUSE: 3 | p(s(T38), X42), SCOPE: 5, CLAUSE: 4 | p(s(T38), X42), SCOPE: 5, CLAUSE: 5\n\nT32 is ground\nT38 is ground\nX5 is free\nX6 is free\nX42 is free\nm(s(s(T38)), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: p(s(T38), X42), SCOPE: 5, CLAUSE: 4 | p(s(T38), X42), SCOPE: 5, CLAUSE: 5\n\nT32 is ground\nT38 is ground\nX5 is free\nX6 is free\nX42 is free\nm(s(s(T38)), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: true | p(s(0), X42), SCOPE: 5, CLAUSE: 5\n\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: p(s(T38), X42), SCOPE: 5, CLAUSE: 5\n\nT32 is ground\nT38 is ground\nX5 is free\nX6 is free\nX42 is free\nm(s(s(T38)), T32, T3) !=? m(X5, 0, X6)\np(s(T38), X42) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: p(s(0), X42), SCOPE: 5, CLAUSE: 5\n\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: p(s(T41), X53)\n\nT32 is ground\nT41 is ground\nX5 is free\nX6 is free\nX53 is free\nm(s(s(s(T41))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: p(s(T41), X53), SCOPE: 6, CLAUSE: 3 | p(s(T41), X53), SCOPE: 6, CLAUSE: 4 | p(s(T41), X53), SCOPE: 6, CLAUSE: 5\n\nT32 is ground\nT41 is ground\nX5 is free\nX6 is free\nX53 is free\nm(s(s(s(T41))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: p(s(T41), X53), SCOPE: 6, CLAUSE: 4 | p(s(T41), X53), SCOPE: 6, CLAUSE: 5\n\nT32 is ground\nT41 is ground\nX5 is free\nX6 is free\nX53 is free\nm(s(s(s(T41))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: true | p(s(0), X53), SCOPE: 6, CLAUSE: 5\n\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: p(s(T41), X53), SCOPE: 6, CLAUSE: 5\n\nT32 is ground\nT41 is ground\nX5 is free\nX6 is free\nX53 is free\nm(s(s(s(T41))), T32, T3) !=? m(X5, 0, X6)\np(s(T41), X53) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: p(s(0), X53), SCOPE: 6, CLAUSE: 5\n\nX53 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: p(s(T44), X64)\n\nT32 is ground\nT44 is ground\nX5 is free\nX6 is free\nX64 is free\nm(s(s(s(s(T44)))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: p(s(T44), X64), SCOPE: 7, CLAUSE: 3 | p(s(T44), X64), SCOPE: 7, CLAUSE: 4 | p(s(T44), X64), SCOPE: 7, CLAUSE: 5\n\nT32 is ground\nT44 is ground\nX5 is free\nX6 is free\nX64 is free\nm(s(s(s(s(T44)))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: p(s(T44), X64), SCOPE: 7, CLAUSE: 4 | p(s(T44), X64), SCOPE: 7, CLAUSE: 5\n\nT32 is ground\nT44 is ground\nX5 is free\nX6 is free\nX64 is free\nm(s(s(s(s(T44)))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: true | p(s(0), X64), SCOPE: 7, CLAUSE: 5\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: p(s(T44), X64), SCOPE: 7, CLAUSE: 5\n\nT32 is ground\nT44 is ground\nX5 is free\nX6 is free\nX64 is free\nm(s(s(s(s(T44)))), T32, T3) !=? m(X5, 0, X6)\np(s(T44), X64) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: p(s(0), X64), SCOPE: 7, CLAUSE: 5\n\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: p(s(T47), X75)\n\nT32 is ground\nT47 is ground\nX5 is free\nX6 is free\nX75 is free\nm(s(s(s(s(s(T47))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: p(s(T47), X75), SCOPE: 8, CLAUSE: 3 | p(s(T47), X75), SCOPE: 8, CLAUSE: 4 | p(s(T47), X75), SCOPE: 8, CLAUSE: 5\n\nT32 is ground\nT47 is ground\nX5 is free\nX6 is free\nX75 is free\nm(s(s(s(s(s(T47))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: p(s(T47), X75), SCOPE: 8, CLAUSE: 4 | p(s(T47), X75), SCOPE: 8, CLAUSE: 5\n\nT32 is ground\nT47 is ground\nX5 is free\nX6 is free\nX75 is free\nm(s(s(s(s(s(T47))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: true | p(s(0), X75), SCOPE: 8, CLAUSE: 5\n\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: p(s(T47), X75), SCOPE: 8, CLAUSE: 5\n\nT32 is ground\nT47 is ground\nX5 is free\nX6 is free\nX75 is free\nm(s(s(s(s(s(T47))))), T32, T3) !=? m(X5, 0, X6)\np(s(T47), X75) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: p(s(0), X75), SCOPE: 8, CLAUSE: 5\n\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: p(s(T50), X86)\n\nT32 is ground\nT50 is ground\nX5 is free\nX6 is free\nX86 is free\nm(s(s(s(s(s(s(T50)))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: p(s(T50), X86), SCOPE: 9, CLAUSE: 3 | p(s(T50), X86), SCOPE: 9, CLAUSE: 4 | p(s(T50), X86), SCOPE: 9, CLAUSE: 5\n\nT32 is ground\nT50 is ground\nX5 is free\nX6 is free\nX86 is free\nm(s(s(s(s(s(s(T50)))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: p(s(T50), X86), SCOPE: 9, CLAUSE: 4 | p(s(T50), X86), SCOPE: 9, CLAUSE: 5\n\nT32 is ground\nT50 is ground\nX5 is free\nX6 is free\nX86 is free\nm(s(s(s(s(s(s(T50)))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: true | p(s(0), X86), SCOPE: 9, CLAUSE: 5\n\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: p(s(T50), X86), SCOPE: 9, CLAUSE: 5\n\nT32 is ground\nT50 is ground\nX5 is free\nX6 is free\nX86 is free\nm(s(s(s(s(s(s(T50)))))), T32, T3) !=? m(X5, 0, X6)\np(s(T50), X86) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: p(s(0), X86), SCOPE: 9, CLAUSE: 5\n\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: p(s(T53), X97)\n\nT32 is ground\nT53 is ground\nX5 is free\nX6 is free\nX97 is free\nm(s(s(s(s(s(s(s(T53))))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: p(s(T53), X97), SCOPE: 10, CLAUSE: 3 | p(s(T53), X97), SCOPE: 10, CLAUSE: 4 | p(s(T53), X97), SCOPE: 10, CLAUSE: 5\n\nT32 is ground\nT53 is ground\nX5 is free\nX6 is free\nX97 is free\nm(s(s(s(s(s(s(s(T53))))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: p(s(T53), X97), SCOPE: 10, CLAUSE: 4 | p(s(T53), X97), SCOPE: 10, CLAUSE: 5\n\nT32 is ground\nT53 is ground\nX5 is free\nX6 is free\nX97 is free\nm(s(s(s(s(s(s(s(T53))))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: true | p(s(0), X97), SCOPE: 10, CLAUSE: 5\n\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: p(s(T53), X97), SCOPE: 10, CLAUSE: 5\n\nT32 is ground\nT53 is ground\nX5 is free\nX6 is free\nX97 is free\nm(s(s(s(s(s(s(s(T53))))))), T32, T3) !=? m(X5, 0, X6)\np(s(T53), X97) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: p(s(0), X97), SCOPE: 10, CLAUSE: 5\n\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: p(s(T56), X108)\n\nT32 is ground\nT56 is ground\nX5 is free\nX6 is free\nX108 is free\nm(s(s(s(s(s(s(s(s(T56)))))))), T32, T3) !=? m(X5, 0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: p(s(T56), X108)\n\nT56 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: p(s(T56), X108), SCOPE: 11, CLAUSE: 3 | p(s(T56), X108), SCOPE: 11, CLAUSE: 4 | p(s(T56), X108), SCOPE: 11, CLAUSE: 5\n\nT56 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: p(s(T56), X108), SCOPE: 11, CLAUSE: 4 | p(s(T56), X108), SCOPE: 11, CLAUSE: 5\n\nT56 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: true | p(s(0), X108), SCOPE: 11, CLAUSE: 5\n\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: p(s(T56), X108), SCOPE: 11, CLAUSE: 5\n\nT56 is ground\nX108 is free\np(s(T56), X108) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: p(s(0), X108), SCOPE: 11, CLAUSE: 5\n\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: p(s(T60), X119)\n\nT60 is ground\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: p(T32, X31)\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX31 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: m(T35, T61, T34)\n\nT35 is ground\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: p(T32, X31), SCOPE: 12, CLAUSE: 3 | p(T32, X31), SCOPE: 12, CLAUSE: 4 | p(T32, X31), SCOPE: 12, CLAUSE: 5\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX31 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: p(T32, X31), SCOPE: 12, CLAUSE: 4 | p(T32, X31), SCOPE: 12, CLAUSE: 5\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX31 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: true | p(s(0), X31), SCOPE: 12, CLAUSE: 5\n\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: p(T32, X31), SCOPE: 12, CLAUSE: 5\n\nT31 is ground\nT32 is ground\nX5 is free\nX6 is free\nX14 is free\nX15 is free\nX31 is free\nm(T31, T32, T3) !=? m(X5, 0, X6)\nm(T31, T32, T3) !=? m(0, X14, X15)\np(T32, X31) !=? p(s(0), 0)", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: p(s(0), X31), SCOPE: 12, CLAUSE: 5\n\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: p(s(T64), X130)\n\nT31 is ground\nT64 is ground\nX14 is free\nX15 is free\nX130 is free\nm(T31, s(s(T64)), T3) !=? m(0, X14, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 177 [arrowhead = none ];
177 -> 2;

178 [label="EVAL with clause\nm(X5, 0, X6) :- ','(!_1, user_defined_=(X6, X5)).\nand substitutionT1 -> T8,\nX5 -> T8,\nT2 -> 0,\nT3 -> T10,\nX6 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 178 [arrowhead = none ];
178 -> 5;

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

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

181 [label="EVAL with clause\nm(0, X14, X15) :- ','(!_1, user_defined_=(X15, 0)).\nand substitutionT1 -> 0,\nT2 -> T18,\nX14 -> T18,\nT3 -> T20,\nX15 -> T20,\nT19 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 181 [arrowhead = none ];
181 -> 29;

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

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

184 [label="EVAL with clause\nuser_defined_=(X9, X9).\nand substitutionT10 -> T13,\nX9 -> T13,\nT8 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 184 [arrowhead = none ];
184 -> 14;

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

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

187 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 187 [arrowhead = none ];
187 -> 31;

188 [label="ONLY EVAL with clause\nm(X27, X28, X29) :- ','(p(X27, X30), ','(p(X28, X31), m(X30, X31, X29))).\nand substitutionT1 -> T31,\nX27 -> T31,\nT2 -> T32,\nX28 -> T32,\nT3 -> T34,\nX29 -> T34,\nT33 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 188 [arrowhead = none ];
188 -> 38;

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

190 [label="EVAL with clause\nuser_defined_=(X18, X18).\nand substitutionT20 -> 0,\nX18 -> 0,\nT23 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 190 [arrowhead = none ];
190 -> 33;

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

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

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

194 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT35 is ground\nreplacements:X30 -> T35", fontsize=14, style = filled, fillcolor = violet];
38 -> 194 [arrowhead = none ];
194 -> 44;

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

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

197 [label="SPLIT 2\nnew knowledge:\nT32 is ground\nT61 is ground\nreplacements:X31 -> T61", fontsize=14, style = filled, fillcolor = violet];
44 -> 197 [arrowhead = none ];
197 -> 168;

198 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T31, T32, T3), m(0, X14, X15))", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 198 [arrowhead = none ];
198 -> 49;

199 [label="EVAL with clause\np(s(0), 0).\nand substitutionT31 -> s(0),\nX30 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 199 [arrowhead = none ];
199 -> 52;

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

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

202 [label="EVAL with clause\np(s(s(X40)), s(X41)) :- p(s(X40), X41).\nand substitutionX40 -> T38,\nT31 -> s(s(T38)),\nX41 -> X42,\nX30 -> s(X42)", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 202 [arrowhead = none ];
202 -> 67;

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

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

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

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

207 [label="EVAL with clause\np(s(0), 0).\nand substitutionT38 -> 0,\nX42 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 207 [arrowhead = none ];
207 -> 76;

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

209 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 209 [arrowhead = none ];
209 -> 81;

210 [label="EVAL with clause\np(s(s(X51)), s(X52)) :- p(s(X51), X52).\nand substitutionX51 -> T41,\nT38 -> s(T41),\nX52 -> X53,\nX42 -> s(X53)", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 210 [arrowhead = none ];
210 -> 86;

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

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

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

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

215 [label="EVAL with clause\np(s(0), 0).\nand substitutionT41 -> 0,\nX53 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 215 [arrowhead = none ];
215 -> 106;

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

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

218 [label="EVAL with clause\np(s(s(X62)), s(X63)) :- p(s(X62), X63).\nand substitutionX62 -> T44,\nT41 -> s(T44),\nX63 -> X64,\nX53 -> s(X64)", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 218 [arrowhead = none ];
218 -> 112;

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

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

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

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

223 [label="EVAL with clause\np(s(0), 0).\nand substitutionT44 -> 0,\nX64 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 223 [arrowhead = none ];
223 -> 116;

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

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

226 [label="EVAL with clause\np(s(s(X73)), s(X74)) :- p(s(X73), X74).\nand substitutionX73 -> T47,\nT44 -> s(T47),\nX74 -> X75,\nX64 -> s(X75)", fontsize=14, style = filled, fillcolor = lightblue];
117 -> 226 [arrowhead = none ];
226 -> 120;

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

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

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

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

231 [label="EVAL with clause\np(s(0), 0).\nand substitutionT47 -> 0,\nX75 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 231 [arrowhead = none ];
231 -> 124;

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

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

234 [label="EVAL with clause\np(s(s(X84)), s(X85)) :- p(s(X84), X85).\nand substitutionX84 -> T50,\nT47 -> s(T50),\nX85 -> X86,\nX75 -> s(X86)", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 234 [arrowhead = none ];
234 -> 128;

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

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

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

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

239 [label="EVAL with clause\np(s(0), 0).\nand substitutionT50 -> 0,\nX86 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 239 [arrowhead = none ];
239 -> 132;

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

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

242 [label="EVAL with clause\np(s(s(X95)), s(X96)) :- p(s(X95), X96).\nand substitutionX95 -> T53,\nT50 -> s(T53),\nX96 -> X97,\nX86 -> s(X97)", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 242 [arrowhead = none ];
242 -> 136;

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

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

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

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

247 [label="EVAL with clause\np(s(0), 0).\nand substitutionT53 -> 0,\nX97 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 247 [arrowhead = none ];
247 -> 140;

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

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

250 [label="EVAL with clause\np(s(s(X106)), s(X107)) :- p(s(X106), X107).\nand substitutionX106 -> T56,\nT53 -> s(T56),\nX107 -> X108,\nX97 -> s(X108)", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 250 [arrowhead = none ];
250 -> 144;

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

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

253 [label="GENERALIZATION\nT57 <-- s(s(s(s(s(s(s(T56)))))))\n\nNew Knowledge:\nT57 is ground", fontsize=14, style = filled, fillcolor = violet];
144 -> 253 [arrowhead = none ];
253 -> 146;

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

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

256 [label="EVAL with clause\np(s(0), 0).\nand substitutionT56 -> 0,\nX108 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 256 [arrowhead = none ];
256 -> 149;

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

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

259 [label="EVAL with clause\np(s(s(X117)), s(X118)) :- p(s(X117), X118).\nand substitutionX117 -> T60,\nT56 -> s(T60),\nX118 -> X119,\nX108 -> s(X119)", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 259 [arrowhead = none ];
259 -> 165;

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

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

262 [label="INSTANCE with matching:\nT56 -> T60\nX108 -> X119", fontsize=14, style = filled, fillcolor = lightgrey];
165 -> 262 [arrowhead = none , style=dashed];
262 -> 146[style=dashed];

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

264 [label="INSTANCE with matching:\nT1 -> T35\nT2 -> T61\nT3 -> T34", fontsize=14, style = filled, fillcolor = lightgrey];
168 -> 264 [arrowhead = none , style=dashed];
264 -> 1[style=dashed];

265 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (m(T31, T32, T3), m(X5, 0, X6))", fontsize=14, style = filled, fillcolor = lightgreen];
169 -> 265 [arrowhead = none ];
265 -> 170;

266 [label="EVAL with clause\np(s(0), 0).\nand substitutionT32 -> s(0),\nX31 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 266 [arrowhead = none ];
266 -> 171;

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

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

269 [label="EVAL with clause\np(s(s(X128)), s(X129)) :- p(s(X128), X129).\nand substitutionX128 -> T64,\nT32 -> s(s(T64)),\nX129 -> X130,\nX31 -> s(X130)", 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="BACKTRACK\nfor clause: p(s(s(X)), s(Y)) :- p(s(X), Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 271 [arrowhead = none ];
271 -> 174;

272 [label="INSTANCE with matching:\nT56 -> T64\nX108 -> X130", fontsize=14, style = filled, fillcolor = lightgrey];
175 -> 272 [arrowhead = none , style=dashed];
272 -> 146[style=dashed];

}

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(z0)
f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f38_in(z0, z1), z0, z1)
U1(f38_out1(z0, z1, z2), z3, z4) → f1_out1(z2)
f146_in(0) → f146_out1(0)
f146_in(s(z0)) → U2(f146_in(z0), s(z0))
U2(f146_out1(z0), s(z1)) → f146_out1(s(z0))
f41_in(s(0)) → f41_out1(0)
f41_in(s(s(0))) → f41_out1(s(0))
f41_in(s(s(s(0)))) → f41_out1(s(s(0)))
f41_in(s(s(s(s(0))))) → f41_out1(s(s(s(0))))
f41_in(s(s(s(s(s(0)))))) → f41_out1(s(s(s(s(0)))))
f41_in(s(s(s(s(s(s(0))))))) → f41_out1(s(s(s(s(s(0))))))
f41_in(s(s(s(s(s(s(s(0)))))))) → f41_out1(s(s(s(s(s(s(0)))))))
f41_in(s(s(s(s(s(s(s(s(z0))))))))) → U3(f146_in(z0), s(s(s(s(s(s(s(s(z0)))))))))
U3(f146_out1(z0), s(s(s(s(s(s(s(s(z1))))))))) → f41_out1(s(s(s(s(s(s(s(z0))))))))
f167_in(s(0)) → f167_out1(0)
f167_in(s(s(z0))) → U4(f146_in(z0), s(s(z0)))
U4(f146_out1(z0), s(s(z1))) → f167_out1(s(z0))
f38_in(z0, z1) → U5(f41_in(z0), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f44_in(z2, z0), z1, z2, z0)
U6(f44_out1(z0, z1), z2, z3, z4) → f38_out1(z4, z0, z1)
f44_in(z0, z1) → U7(f167_in(z0), z0, z1)
U7(f167_out1(z0), z1, z2) → U8(f1_in(z2, z0), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f44_out1(z3, z0)

Tuples:

F1_IN(z0, z1) → c2(U1'(f38_in(z0, z1), z0, z1), F38_IN(z0, z1))
F146_IN(s(z0)) → c5(U2'(f146_in(z0), s(z0)), F146_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c14(U3'(f146_in(z0), s(s(s(s(s(s(s(s(z0))))))))), F146_IN(z0))
F167_IN(s(s(z0))) → c17(U4'(f146_in(z0), s(s(z0))), F146_IN(z0))
F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(U6'(f44_in(z2, z0), z1, z2, z0), F44_IN(z2, z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
U7'(f167_out1(z0), z1, z2) → c23(U8'(f1_in(z2, z0), z1, z2, z0), F1_IN(z2, z0))

S tuples:

F1_IN(z0, z1) → c2(U1'(f38_in(z0, z1), z0, z1), F38_IN(z0, z1))
F146_IN(s(z0)) → c5(U2'(f146_in(z0), s(z0)), F146_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c14(U3'(f146_in(z0), s(s(s(s(s(s(s(s(z0))))))))), F146_IN(z0))
F167_IN(s(s(z0))) → c17(U4'(f146_in(z0), s(s(z0))), F146_IN(z0))
F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(U6'(f44_in(z2, z0), z1, z2, z0), F44_IN(z2, z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
U7'(f167_out1(z0), z1, z2) → c23(U8'(f1_in(z2, z0), z1, z2, z0), F1_IN(z2, z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f146_in, U2, f41_in, U3, f167_in, U4, f38_in, U5, U6, f44_in, U7, U8

Defined Pair Symbols:

F1_IN, F146_IN, F41_IN, F167_IN, F38_IN, U5', F44_IN, U7'

Compound Symbols:

c2, c5, c14, c17, c19, c20, c22, c23

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

Split RHS of tuples not part of any SCC

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(z0)
f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f38_in(z0, z1), z0, z1)
U1(f38_out1(z0, z1, z2), z3, z4) → f1_out1(z2)
f146_in(0) → f146_out1(0)
f146_in(s(z0)) → U2(f146_in(z0), s(z0))
U2(f146_out1(z0), s(z1)) → f146_out1(s(z0))
f41_in(s(0)) → f41_out1(0)
f41_in(s(s(0))) → f41_out1(s(0))
f41_in(s(s(s(0)))) → f41_out1(s(s(0)))
f41_in(s(s(s(s(0))))) → f41_out1(s(s(s(0))))
f41_in(s(s(s(s(s(0)))))) → f41_out1(s(s(s(s(0)))))
f41_in(s(s(s(s(s(s(0))))))) → f41_out1(s(s(s(s(s(0))))))
f41_in(s(s(s(s(s(s(s(0)))))))) → f41_out1(s(s(s(s(s(s(0)))))))
f41_in(s(s(s(s(s(s(s(s(z0))))))))) → U3(f146_in(z0), s(s(s(s(s(s(s(s(z0)))))))))
U3(f146_out1(z0), s(s(s(s(s(s(s(s(z1))))))))) → f41_out1(s(s(s(s(s(s(s(z0))))))))
f167_in(s(0)) → f167_out1(0)
f167_in(s(s(z0))) → U4(f146_in(z0), s(s(z0)))
U4(f146_out1(z0), s(s(z1))) → f167_out1(s(z0))
f38_in(z0, z1) → U5(f41_in(z0), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f44_in(z2, z0), z1, z2, z0)
U6(f44_out1(z0, z1), z2, z3, z4) → f38_out1(z4, z0, z1)
f44_in(z0, z1) → U7(f167_in(z0), z0, z1)
U7(f167_out1(z0), z1, z2) → U8(f1_in(z2, z0), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f44_out1(z3, z0)

Tuples:

F1_IN(z0, z1) → c2(U1'(f38_in(z0, z1), z0, z1), F38_IN(z0, z1))
F146_IN(s(z0)) → c5(U2'(f146_in(z0), s(z0)), F146_IN(z0))
F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(U6'(f44_in(z2, z0), z1, z2, z0), F44_IN(z2, z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
U7'(f167_out1(z0), z1, z2) → c23(U8'(f1_in(z2, z0), z1, z2, z0), F1_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(U3'(f146_in(z0), s(s(s(s(s(s(s(s(z0))))))))))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
F167_IN(s(s(z0))) → c(U4'(f146_in(z0), s(s(z0))))
F167_IN(s(s(z0))) → c(F146_IN(z0))

S tuples:

F1_IN(z0, z1) → c2(U1'(f38_in(z0, z1), z0, z1), F38_IN(z0, z1))
F146_IN(s(z0)) → c5(U2'(f146_in(z0), s(z0)), F146_IN(z0))
F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(U6'(f44_in(z2, z0), z1, z2, z0), F44_IN(z2, z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
U7'(f167_out1(z0), z1, z2) → c23(U8'(f1_in(z2, z0), z1, z2, z0), F1_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(U3'(f146_in(z0), s(s(s(s(s(s(s(s(z0))))))))))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
F167_IN(s(s(z0))) → c(U4'(f146_in(z0), s(s(z0))))
F167_IN(s(s(z0))) → c(F146_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f146_in, U2, f41_in, U3, f167_in, U4, f38_in, U5, U6, f44_in, U7, U8

Defined Pair Symbols:

F1_IN, F146_IN, F38_IN, U5', F44_IN, U7', F41_IN, F167_IN

Compound Symbols:

c2, c5, c19, c20, c22, c23, c

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

Removed 6 trailing tuple parts

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(z0)
f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f38_in(z0, z1), z0, z1)
U1(f38_out1(z0, z1, z2), z3, z4) → f1_out1(z2)
f146_in(0) → f146_out1(0)
f146_in(s(z0)) → U2(f146_in(z0), s(z0))
U2(f146_out1(z0), s(z1)) → f146_out1(s(z0))
f41_in(s(0)) → f41_out1(0)
f41_in(s(s(0))) → f41_out1(s(0))
f41_in(s(s(s(0)))) → f41_out1(s(s(0)))
f41_in(s(s(s(s(0))))) → f41_out1(s(s(s(0))))
f41_in(s(s(s(s(s(0)))))) → f41_out1(s(s(s(s(0)))))
f41_in(s(s(s(s(s(s(0))))))) → f41_out1(s(s(s(s(s(0))))))
f41_in(s(s(s(s(s(s(s(0)))))))) → f41_out1(s(s(s(s(s(s(0)))))))
f41_in(s(s(s(s(s(s(s(s(z0))))))))) → U3(f146_in(z0), s(s(s(s(s(s(s(s(z0)))))))))
U3(f146_out1(z0), s(s(s(s(s(s(s(s(z1))))))))) → f41_out1(s(s(s(s(s(s(s(z0))))))))
f167_in(s(0)) → f167_out1(0)
f167_in(s(s(z0))) → U4(f146_in(z0), s(s(z0)))
U4(f146_out1(z0), s(s(z1))) → f167_out1(s(z0))
f38_in(z0, z1) → U5(f41_in(z0), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f44_in(z2, z0), z1, z2, z0)
U6(f44_out1(z0, z1), z2, z3, z4) → f38_out1(z4, z0, z1)
f44_in(z0, z1) → U7(f167_in(z0), z0, z1)
U7(f167_out1(z0), z1, z2) → U8(f1_in(z2, z0), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f44_out1(z3, z0)

Tuples:

F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
F167_IN(s(s(z0))) → c(F146_IN(z0))
F1_IN(z0, z1) → c2(F38_IN(z0, z1))
F146_IN(s(z0)) → c5(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
U7'(f167_out1(z0), z1, z2) → c23(F1_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F167_IN(s(s(z0))) → c

S tuples:

F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
F167_IN(s(s(z0))) → c(F146_IN(z0))
F1_IN(z0, z1) → c2(F38_IN(z0, z1))
F146_IN(s(z0)) → c5(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
U7'(f167_out1(z0), z1, z2) → c23(F1_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F167_IN(s(s(z0))) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f146_in, U2, f41_in, U3, f167_in, U4, f38_in, U5, U6, f44_in, U7, U8

Defined Pair Symbols:

F38_IN, F44_IN, F41_IN, F167_IN, F1_IN, F146_IN, U5', U7'

Compound Symbols:

c19, c22, c, c2, c5, c20, c23, c

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

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

F1_IN(z0, z1) → c2(F38_IN(z0, z1))

We considered the (Usable) Rules:

f167_in(s(0)) → f167_out1(0)
f167_in(s(s(z0))) → U4(f146_in(z0), s(s(z0)))
f146_in(0) → f146_out1(0)
f146_in(s(z0)) → U2(f146_in(z0), s(z0))
U4(f146_out1(z0), s(s(z1))) → f167_out1(s(z0))
U2(f146_out1(z0), s(z1)) → f146_out1(s(z0))
f41_in(s(0)) → f41_out1(0)
f41_in(s(s(0))) → f41_out1(s(0))
f41_in(s(s(s(0)))) → f41_out1(s(s(0)))
f41_in(s(s(s(s(0))))) → f41_out1(s(s(s(0))))
f41_in(s(s(s(s(s(0)))))) → f41_out1(s(s(s(s(0)))))
f41_in(s(s(s(s(s(s(0))))))) → f41_out1(s(s(s(s(s(0))))))
f41_in(s(s(s(s(s(s(s(0)))))))) → f41_out1(s(s(s(s(s(s(0)))))))
f41_in(s(s(s(s(s(s(s(s(z0))))))))) → U3(f146_in(z0), s(s(s(s(s(s(s(s(z0)))))))))
U3(f146_out1(z0), s(s(s(s(s(s(s(s(z1))))))))) → f41_out1(s(s(s(s(s(s(s(z0))))))))

And the Tuples:

F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
F167_IN(s(s(z0))) → c(F146_IN(z0))
F1_IN(z0, z1) → c2(F38_IN(z0, z1))
F146_IN(s(z0)) → c5(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
U7'(f167_out1(z0), z1, z2) → c23(F1_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F167_IN(s(s(z0))) → c

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

POL(0) = 0   
POL(F146_IN(x₁)) = 0   
POL(F167_IN(x₁)) = 0   
POL(F1_IN(x₁, x₂)) = [1] + x₂   
POL(F38_IN(x₁, x₂)) = x₂   
POL(F41_IN(x₁)) = 0   
POL(F44_IN(x₁, x₂)) = x₁   
POL(U2(x₁, x₂)) = [1] + x₁   
POL(U3(x₁, x₂)) = 0   
POL(U4(x₁, x₂)) = [2] + x₁   
POL(U5'(x₁, x₂, x₃)) = x₃   
POL(U7'(x₁, x₂, x₃)) = x₁   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c19(x₁, x₂)) = x₁ + x₂   
POL(c2(x₁)) = x₁   
POL(c20(x₁)) = x₁   
POL(c22(x₁, x₂)) = x₁ + x₂   
POL(c23(x₁)) = x₁   
POL(c5(x₁)) = x₁   
POL(f146_in(x₁)) = x₁   
POL(f146_out1(x₁)) = x₁   
POL(f167_in(x₁)) = x₁   
POL(f167_out1(x₁)) = [1] + x₁   
POL(f41_in(x₁)) = 0   
POL(f41_out1(x₁)) = 0   
POL(s(x₁)) = [1] + x₁   

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(z0)
f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f38_in(z0, z1), z0, z1)
U1(f38_out1(z0, z1, z2), z3, z4) → f1_out1(z2)
f146_in(0) → f146_out1(0)
f146_in(s(z0)) → U2(f146_in(z0), s(z0))
U2(f146_out1(z0), s(z1)) → f146_out1(s(z0))
f41_in(s(0)) → f41_out1(0)
f41_in(s(s(0))) → f41_out1(s(0))
f41_in(s(s(s(0)))) → f41_out1(s(s(0)))
f41_in(s(s(s(s(0))))) → f41_out1(s(s(s(0))))
f41_in(s(s(s(s(s(0)))))) → f41_out1(s(s(s(s(0)))))
f41_in(s(s(s(s(s(s(0))))))) → f41_out1(s(s(s(s(s(0))))))
f41_in(s(s(s(s(s(s(s(0)))))))) → f41_out1(s(s(s(s(s(s(0)))))))
f41_in(s(s(s(s(s(s(s(s(z0))))))))) → U3(f146_in(z0), s(s(s(s(s(s(s(s(z0)))))))))
U3(f146_out1(z0), s(s(s(s(s(s(s(s(z1))))))))) → f41_out1(s(s(s(s(s(s(s(z0))))))))
f167_in(s(0)) → f167_out1(0)
f167_in(s(s(z0))) → U4(f146_in(z0), s(s(z0)))
U4(f146_out1(z0), s(s(z1))) → f167_out1(s(z0))
f38_in(z0, z1) → U5(f41_in(z0), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f44_in(z2, z0), z1, z2, z0)
U6(f44_out1(z0, z1), z2, z3, z4) → f38_out1(z4, z0, z1)
f44_in(z0, z1) → U7(f167_in(z0), z0, z1)
U7(f167_out1(z0), z1, z2) → U8(f1_in(z2, z0), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f44_out1(z3, z0)

Tuples:

F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
F167_IN(s(s(z0))) → c(F146_IN(z0))
F1_IN(z0, z1) → c2(F38_IN(z0, z1))
F146_IN(s(z0)) → c5(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
U7'(f167_out1(z0), z1, z2) → c23(F1_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F167_IN(s(s(z0))) → c

S tuples:

F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
F167_IN(s(s(z0))) → c(F146_IN(z0))
F146_IN(s(z0)) → c5(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
U7'(f167_out1(z0), z1, z2) → c23(F1_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F167_IN(s(s(z0))) → c

K tuples:

F1_IN(z0, z1) → c2(F38_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f146_in, U2, f41_in, U3, f167_in, U4, f38_in, U5, U6, f44_in, U7, U8

Defined Pair Symbols:

F38_IN, F44_IN, F41_IN, F167_IN, F1_IN, F146_IN, U5', U7'

Compound Symbols:

c19, c22, c, c2, c5, c20, c23, c

(29) CdtKnowledgeProof (EQUIVALENT transformation)

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

F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
F167_IN(s(s(z0))) → c(F146_IN(z0))
U7'(f167_out1(z0), z1, z2) → c23(F1_IN(z2, z0))
F167_IN(s(s(z0))) → c
F1_IN(z0, z1) → c2(F38_IN(z0, z1))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, 0) → f1_out1(z0)
f1_in(0, z0) → f1_out1(0)
f1_in(z0, z1) → U1(f38_in(z0, z1), z0, z1)
U1(f38_out1(z0, z1, z2), z3, z4) → f1_out1(z2)
f146_in(0) → f146_out1(0)
f146_in(s(z0)) → U2(f146_in(z0), s(z0))
U2(f146_out1(z0), s(z1)) → f146_out1(s(z0))
f41_in(s(0)) → f41_out1(0)
f41_in(s(s(0))) → f41_out1(s(0))
f41_in(s(s(s(0)))) → f41_out1(s(s(0)))
f41_in(s(s(s(s(0))))) → f41_out1(s(s(s(0))))
f41_in(s(s(s(s(s(0)))))) → f41_out1(s(s(s(s(0)))))
f41_in(s(s(s(s(s(s(0))))))) → f41_out1(s(s(s(s(s(0))))))
f41_in(s(s(s(s(s(s(s(0)))))))) → f41_out1(s(s(s(s(s(s(0)))))))
f41_in(s(s(s(s(s(s(s(s(z0))))))))) → U3(f146_in(z0), s(s(s(s(s(s(s(s(z0)))))))))
U3(f146_out1(z0), s(s(s(s(s(s(s(s(z1))))))))) → f41_out1(s(s(s(s(s(s(s(z0))))))))
f167_in(s(0)) → f167_out1(0)
f167_in(s(s(z0))) → U4(f146_in(z0), s(s(z0)))
U4(f146_out1(z0), s(s(z1))) → f167_out1(s(z0))
f38_in(z0, z1) → U5(f41_in(z0), z0, z1)
U5(f41_out1(z0), z1, z2) → U6(f44_in(z2, z0), z1, z2, z0)
U6(f44_out1(z0, z1), z2, z3, z4) → f38_out1(z4, z0, z1)
f44_in(z0, z1) → U7(f167_in(z0), z0, z1)
U7(f167_out1(z0), z1, z2) → U8(f1_in(z2, z0), z1, z2, z0)
U8(f1_out1(z0), z1, z2, z3) → f44_out1(z3, z0)

Tuples:

F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
F167_IN(s(s(z0))) → c(F146_IN(z0))
F1_IN(z0, z1) → c2(F38_IN(z0, z1))
F146_IN(s(z0)) → c5(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
U7'(f167_out1(z0), z1, z2) → c23(F1_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F167_IN(s(s(z0))) → c

S tuples:

F146_IN(s(z0)) → c5(F146_IN(z0))

K tuples:

F1_IN(z0, z1) → c2(F38_IN(z0, z1))
F38_IN(z0, z1) → c19(U5'(f41_in(z0), z0, z1), F41_IN(z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c(F146_IN(z0))
U5'(f41_out1(z0), z1, z2) → c20(F44_IN(z2, z0))
F41_IN(s(s(s(s(s(s(s(s(z0))))))))) → c
F44_IN(z0, z1) → c22(U7'(f167_in(z0), z0, z1), F167_IN(z0))
F167_IN(s(s(z0))) → c(F146_IN(z0))
U7'(f167_out1(z0), z1, z2) → c23(F1_IN(z2, z0))
F167_IN(s(s(z0))) → c

Defined Rule Symbols:

f1_in, U1, f146_in, U2, f41_in, U3, f167_in, U4, f38_in, U5, U6, f44_in, U7, U8

Defined Pair Symbols:

F38_IN, F44_IN, F41_IN, F167_IN, F1_IN, F146_IN, U5', U7'

Compound Symbols:

c19, c22, c, c2, c5, c20, c23, c