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

(0) Obligation:

Clauses:

ordered([]) :- !.
ordered(.(X1, [])) :- !.
ordered(Xs) :- ','(head(Xs, X), ','(tail(Xs, Ys), ','(head(Ys, Y), ','(tail(Ys, Zs), ','(less(X, s(Y)), ordered(.(Y, Zs))))))).
head([], X2).
head(.(X, X3), X).
tail([], []).
tail(.(X4, Xs), Xs).
less(0, Y) :- ','(!, eq(Y, s(X5))).
less(X, Y) :- ','(p(X, Px), ','(p(Y, Py), less(Px, Py))).
p(0, 0).
p(s(X), X).
eq(X, X).

Query: ordered(g)

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

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: ordered(T1), SCOPE: 1, CLAUSE: 0 | ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: !_1 | ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nordered(T1) !=? ordered([])", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: !_1 | ordered(.(T4, [])), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX8 is free\nordered(T1) !=? ordered([])\nordered(T1) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(head(T7, X19), ','(tail(T7, X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(X19, s(X21)), ordered(.(X21, X22)))))))\n\nT7 is ground\nX8 is free\nX19 is free\nX20 is free\nX21 is free\nX22 is free\nordered(T7) !=? ordered([])\nordered(T7) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(head(T7, X19), ','(tail(T7, X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(X19, s(X21)), ordered(.(X21, X22))))))), SCOPE: 2, CLAUSE: 3 | ','(head(T7, X19), ','(tail(T7, X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(X19, s(X21)), ordered(.(X21, X22))))))), SCOPE: 2, CLAUSE: 4\n\nT7 is ground\nX8 is free\nX19 is free\nX20 is free\nX21 is free\nX22 is free\nordered(T7) !=? ordered([])\nordered(T7) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(head(T7, X19), ','(tail(T7, X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(X19, s(X21)), ordered(.(X21, X22))))))), SCOPE: 2, CLAUSE: 4\n\nT7 is ground\nX8 is free\nX19 is free\nX20 is free\nX21 is free\nX22 is free\nordered(T7) !=? ordered([])\nordered(T7) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(tail(.(T12, T13), X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(T12, s(X21)), ordered(.(X21, X22))))))\n\nT12 is ground\nT13 is ground\nX8 is free\nX20 is free\nX21 is free\nX22 is free\nordered(.(T12, T13)) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(tail(.(T12, T13), X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(T12, s(X21)), ordered(.(X21, X22)))))), SCOPE: 3, CLAUSE: 5 | ','(tail(.(T12, T13), X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(T12, s(X21)), ordered(.(X21, X22)))))), SCOPE: 3, CLAUSE: 6\n\nT12 is ground\nT13 is ground\nX8 is free\nX20 is free\nX21 is free\nX22 is free\nordered(.(T12, T13)) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(tail(.(T12, T13), X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(T12, s(X21)), ordered(.(X21, X22)))))), SCOPE: 3, CLAUSE: 6\n\nT12 is ground\nT13 is ground\nX8 is free\nX20 is free\nX21 is free\nX22 is free\nordered(.(T12, T13)) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(head(T19, X21), ','(tail(T19, X22), ','(less(T18, s(X21)), ordered(.(X21, X22)))))\n\nT18 is ground\nT19 is ground\nX8 is free\nX21 is free\nX22 is free\nordered(.(T18, T19)) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(head(T19, X21), ','(tail(T19, X22), ','(less(T18, s(X21)), ordered(.(X21, X22))))), SCOPE: 4, CLAUSE: 3 | ','(head(T19, X21), ','(tail(T19, X22), ','(less(T18, s(X21)), ordered(.(X21, X22))))), SCOPE: 4, CLAUSE: 4\n\nT18 is ground\nT19 is ground\nX8 is free\nX21 is free\nX22 is free\nordered(.(T18, T19)) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(head(T19, X21), ','(tail(T19, X22), ','(less(T18, s(X21)), ordered(.(X21, X22))))), SCOPE: 4, CLAUSE: 4\n\nT18 is ground\nT19 is ground\nX8 is free\nX21 is free\nX22 is free\nordered(.(T18, T19)) !=? ordered(.(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(tail(.(T24, T25), X22), ','(less(T18, s(T24)), ordered(.(T24, X22))))\n\nT18 is ground\nT24 is ground\nT25 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(tail(.(T24, T25), X22), ','(less(T18, s(T24)), ordered(.(T24, X22)))), SCOPE: 5, CLAUSE: 5 | ','(tail(.(T24, T25), X22), ','(less(T18, s(T24)), ordered(.(T24, X22)))), SCOPE: 5, CLAUSE: 6\n\nT18 is ground\nT24 is ground\nT25 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(tail(.(T24, T25), X22), ','(less(T18, s(T24)), ordered(.(T24, X22)))), SCOPE: 5, CLAUSE: 6\n\nT18 is ground\nT24 is ground\nT25 is ground\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(less(T18, s(T32)), ordered(.(T32, T33)))\n\nT18 is ground\nT32 is ground\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: less(T18, s(T32))\n\nT18 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ordered(.(T32, T33))\n\nT32 is ground\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: less(T18, s(T32)), SCOPE: 6, CLAUSE: 7 | less(T18, s(T32)), SCOPE: 6, CLAUSE: 8\n\nT18 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(!_6, eq(s(T38), s(X75))) | less(0, s(T38)), SCOPE: 6, CLAUSE: 8\n\nT38 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: less(T18, s(T32)), SCOPE: 6, CLAUSE: 8\n\nT18 is ground\nT32 is ground\nX74 is free\nless(T18, s(T32)) !=? less(0, X74)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: eq(s(T38), s(X75))\n\nT38 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: eq(s(T38), s(X75)), SCOPE: 7, CLAUSE: 11\n\nT38 is ground\nX75 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(p(T46, X90), ','(p(s(T47), X91), less(X90, X91)))\n\nT46 is ground\nT47 is ground\nX74 is free\nX90 is free\nX91 is free\nless(T46, s(T47)) !=? less(0, X74)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(p(T46, X90), ','(p(s(T47), X91), less(X90, X91))), SCOPE: 8, CLAUSE: 9 | ','(p(T46, X90), ','(p(s(T47), X91), less(X90, X91))), SCOPE: 8, CLAUSE: 10\n\nT46 is ground\nT47 is ground\nX74 is free\nX90 is free\nX91 is free\nless(T46, s(T47)) !=? less(0, X74)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(p(T46, X90), ','(p(s(T47), X91), less(X90, X91))), SCOPE: 8, CLAUSE: 10\n\nT46 is ground\nT47 is ground\nX74 is free\nX90 is free\nX91 is free\nless(T46, s(T47)) !=? less(0, X74)", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(p(s(T47), X91), less(T50, X91))\n\nT47 is ground\nT50 is ground\nX91 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(p(s(T47), X91), less(T50, X91)), SCOPE: 9, CLAUSE: 9 | ','(p(s(T47), X91), less(T50, X91)), SCOPE: 9, CLAUSE: 10\n\nT47 is ground\nT50 is ground\nX91 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(p(s(T47), X91), less(T50, X91)), SCOPE: 9, CLAUSE: 10\n\nT47 is ground\nT50 is ground\nX91 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: less(T50, T54)\n\nT50 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: less(T50, T54), SCOPE: 10, CLAUSE: 7 | less(T50, T54), SCOPE: 10, CLAUSE: 8\n\nT50 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(!_10, eq(T58, s(X112))) | less(0, T58), SCOPE: 10, CLAUSE: 8\n\nT58 is ground\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: less(T50, T54), SCOPE: 10, CLAUSE: 8\n\nT50 is ground\nT54 is ground\nX111 is free\nless(T50, T54) !=? less(0, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: eq(T58, s(X112))\n\nT58 is ground\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: eq(T58, s(X112)), SCOPE: 11, CLAUSE: 11\n\nT58 is ground\nX112 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(p(T69, X127), ','(p(T70, X128), less(X127, X128)))\n\nT69 is ground\nT70 is ground\nX111 is free\nX127 is free\nX128 is free\nless(T69, T70) !=? less(0, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(p(T69, X127), ','(p(T70, X128), less(X127, X128))), SCOPE: 12, CLAUSE: 9 | ','(p(T69, X127), ','(p(T70, X128), less(X127, X128))), SCOPE: 12, CLAUSE: 10\n\nT69 is ground\nT70 is ground\nX111 is free\nX127 is free\nX128 is free\nless(T69, T70) !=? less(0, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(p(T69, X127), ','(p(T70, X128), less(X127, X128))), SCOPE: 12, CLAUSE: 10\n\nT69 is ground\nT70 is ground\nX111 is free\nX127 is free\nX128 is free\nless(T69, T70) !=? less(0, X111)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(p(T70, X128), less(T73, X128))\n\nT70 is ground\nT73 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(p(T70, X128), less(T73, X128)), SCOPE: 13, CLAUSE: 9 | ','(p(T70, X128), less(T73, X128)), SCOPE: 13, CLAUSE: 10\n\nT70 is ground\nT73 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: less(T73, 0) | ','(p(0, X128), less(T73, X128)), SCOPE: 13, CLAUSE: 10\n\nT73 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: ','(p(T70, X128), less(T73, X128)), SCOPE: 13, CLAUSE: 10\n\nT70 is ground\nT73 is ground\nX128 is free\np(T70, X128) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: less(T73, 0)\n\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(p(0, X128), less(T73, X128)), SCOPE: 13, CLAUSE: 10\n\nT73 is ground\nX128 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: less(T73, 0), SCOPE: 14, CLAUSE: 7 | less(T73, 0), SCOPE: 14, CLAUSE: 8\n\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(!_14, eq(0, s(X146))) | less(0, 0), SCOPE: 14, CLAUSE: 8\n\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: less(T73, 0), SCOPE: 14, CLAUSE: 8\n\nT73 is ground\nX145 is free\nless(T73, 0) !=? less(0, X145)", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: eq(0, s(X146))\n\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: eq(0, s(X146)), SCOPE: 15, CLAUSE: 11\n\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(p(T76, X159), ','(p(0, X160), less(X159, X160)))\n\nT76 is ground\nX145 is free\nX159 is free\nX160 is free\nless(T76, 0) !=? less(0, X145)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(p(T76, X159), ','(p(0, X160), less(X159, X160))), SCOPE: 16, CLAUSE: 9 | ','(p(T76, X159), ','(p(0, X160), less(X159, X160))), SCOPE: 16, CLAUSE: 10\n\nT76 is ground\nX145 is free\nX159 is free\nX160 is free\nless(T76, 0) !=? less(0, X145)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(p(T76, X159), ','(p(0, X160), less(X159, X160))), SCOPE: 16, CLAUSE: 10\n\nT76 is ground\nX145 is free\nX159 is free\nX160 is free\nless(T76, 0) !=? less(0, X145)", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(p(0, X160), less(T79, X160))\n\nT79 is ground\nX160 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(p(0, X160), less(T79, X160)), SCOPE: 17, CLAUSE: 9 | ','(p(0, X160), less(T79, X160)), SCOPE: 17, CLAUSE: 10\n\nT79 is ground\nX160 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: less(T79, 0) | ','(p(0, X160), less(T79, X160)), SCOPE: 17, CLAUSE: 10\n\nT79 is ground\nX160 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: less(T79, 0)\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(p(0, X160), less(T79, X160)), SCOPE: 17, CLAUSE: 10\n\nT79 is ground\nX160 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: less(T73, T82)\n\nT73 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 159 [arrowhead = none ];
159 -> 3;

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

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

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

163 [label="EVAL with clause\nordered(.(X8, [])) :- !_1.\nand substitutionX8 -> T4,\nT1 -> .(T4, [])", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 163 [arrowhead = none ];
163 -> 14;

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

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

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

167 [label="ONLY EVAL with clause\nordered(X18) :- ','(head(X18, X19), ','(tail(X18, X20), ','(head(X20, X21), ','(tail(X20, X22), ','(less(X19, s(X21)), ordered(.(X21, X22))))))).\nand substitutionT1 -> T7,\nX18 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 167 [arrowhead = none ];
167 -> 23;

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

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

170 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(T7), ordered([]))", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 170 [arrowhead = none ];
170 -> 26;

171 [label="EVAL with clause\nhead(.(X32, X33), X32).\nand substitutionX32 -> T12,\nX33 -> T13,\nT7 -> .(T12, T13),\nX19 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 171 [arrowhead = none ];
171 -> 31;

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

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

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

175 [label="ONLY EVAL with clause\ntail(.(X44, X45), X45).\nand substitutionT12 -> T18,\nX44 -> T18,\nT13 -> T19,\nX45 -> T19,\nX20 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 175 [arrowhead = none ];
175 -> 39;

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

177 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(.(T18, T19)), ordered(.(X8, [])))", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 177 [arrowhead = none ];
177 -> 44;

178 [label="EVAL with clause\nhead(.(X55, X56), X55).\nand substitutionX55 -> T24,\nX56 -> T25,\nT19 -> .(T24, T25),\nX21 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 178 [arrowhead = none ];
178 -> 46;

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

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

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

182 [label="ONLY EVAL with clause\ntail(.(X65, X66), X66).\nand substitutionT24 -> T32,\nX65 -> T32,\nT25 -> T33,\nX66 -> T33,\nX22 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 182 [arrowhead = none ];
182 -> 50;

183 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
50 -> 183 [arrowhead = none ];
183 -> 53;

184 [label="SPLIT 2\nnew knowledge:\nT18 is ground\nT32 is ground", fontsize=14, style = filled, fillcolor = violet];
50 -> 184 [arrowhead = none ];
184 -> 54;

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

186 [label="INSTANCE with matching:\nT1 -> .(T32, T33)", fontsize=14, style = filled, fillcolor = lightgrey];
54 -> 186 [arrowhead = none , style=dashed];
186 -> 2[style=dashed];

187 [label="EVAL with clause\nless(0, X74) :- ','(!_6, eq(X74, s(X75))).\nand substitutionT18 -> 0,\nT32 -> T38,\nX74 -> s(T38)", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 187 [arrowhead = none ];
187 -> 59;

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

189 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 189 [arrowhead = none ];
189 -> 63;

190 [label="ONLY EVAL with clause\nless(X88, X89) :- ','(p(X88, X90), ','(p(X89, X91), less(X90, X91))).\nand substitutionT18 -> T46,\nX88 -> T46,\nT32 -> T47,\nX89 -> s(T47)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 190 [arrowhead = none ];
190 -> 70;

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

192 [label="ONLY EVAL with clause\neq(X78, X78).\nand substitutionT38 -> T41,\nX78 -> s(T41),\nX75 -> T41", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 192 [arrowhead = none ];
192 -> 67;

193 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 193 [arrowhead = none ];
193 -> 68;

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

195 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T46, s(T47)), less(0, X74))", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 195 [arrowhead = none ];
195 -> 74;

196 [label="EVAL with clause\np(s(X97), X97).\nand substitutionX97 -> T50,\nT46 -> s(T50),\nX90 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 196 [arrowhead = none ];
196 -> 79;

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

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

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

200 [label="ONLY EVAL with clause\np(s(X105), X105).\nand substitutionT47 -> T54,\nX105 -> T54,\nX91 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 200 [arrowhead = none ];
200 -> 85;

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

202 [label="EVAL with clause\nless(0, X111) :- ','(!_10, eq(X111, s(X112))).\nand substitutionT50 -> 0,\nT54 -> T58,\nX111 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
87 -> 202 [arrowhead = none ];
202 -> 91;

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

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

205 [label="ONLY EVAL with clause\nless(X125, X126) :- ','(p(X125, X127), ','(p(X126, X128), less(X127, X128))).\nand substitutionT50 -> T69,\nX125 -> T69,\nT54 -> T70,\nX126 -> T70", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 205 [arrowhead = none ];
205 -> 104;

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

207 [label="EVAL with clause\neq(X115, X115).\nand substitutionT58 -> s(T64),\nX115 -> s(T64),\nX112 -> T64,\nT63 -> s(T64)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 207 [arrowhead = none ];
207 -> 98;

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

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

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

211 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T69, T70), less(0, X111))", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 211 [arrowhead = none ];
211 -> 108;

212 [label="EVAL with clause\np(s(X134), X134).\nand substitutionX134 -> T73,\nT69 -> s(T73),\nX127 -> T73", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 212 [arrowhead = none ];
212 -> 112;

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

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

215 [label="EVAL with clause\np(0, 0).\nand substitutionT70 -> 0,\nX128 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 215 [arrowhead = none ];
215 -> 115;

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

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

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

219 [label="EVAL with clause\np(s(X180), X180).\nand substitutionX180 -> T82,\nT70 -> s(T82),\nX128 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 219 [arrowhead = none ];
219 -> 157;

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

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

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

223 [label="EVAL with clause\nless(0, X145) :- ','(!_14, eq(X145, s(X146))).\nand substitutionT73 -> 0,\nX145 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 223 [arrowhead = none ];
223 -> 128;

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

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

226 [label="ONLY EVAL with clause\nless(X157, X158) :- ','(p(X157, X159), ','(p(X158, X160), less(X159, X160))).\nand substitutionT73 -> T76,\nX157 -> T76,\nX158 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 226 [arrowhead = none ];
226 -> 136;

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

228 [label="BACKTRACK\nfor clause: eq(X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
131 -> 228 [arrowhead = none ];
228 -> 132;

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

230 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T76, 0), less(0, X145))", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 230 [arrowhead = none ];
230 -> 140;

231 [label="EVAL with clause\np(s(X166), X166).\nand substitutionX166 -> T79,\nT76 -> s(T79),\nX159 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 231 [arrowhead = none ];
231 -> 142;

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

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

234 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX160 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 234 [arrowhead = none ];
234 -> 148;

235 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
148 -> 235 [arrowhead = none ];
235 -> 149;

236 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
148 -> 236 [arrowhead = none ];
236 -> 150;

237 [label="INSTANCE with matching:\nT73 -> T79", fontsize=14, style = filled, fillcolor = lightgrey];
149 -> 237 [arrowhead = none , style=dashed];
237 -> 119[style=dashed];

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

239 [label="INSTANCE with matching:\nT50 -> T73\nT54 -> T82", fontsize=14, style = filled, fillcolor = lightgrey];
157 -> 239 [arrowhead = none , style=dashed];
239 -> 85[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f50_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f50_out1, .(z0, .(z1, z2))) → f2_out1
f85_in(0, s(z0)) → f85_out1
f85_in(s(z0), 0) → U2(f115_in(z0), s(z0), 0)
f85_in(s(z0), s(z1)) → U3(f85_in(z0, z1), s(z0), s(z1))
U2(f115_out1, s(z0), 0) → f85_out1
U2(f115_out2(z0), s(z1), 0) → f85_out1
U3(f85_out1, s(z0), s(z1)) → f85_out1
f119_in(s(z0)) → U4(f148_in(z0), s(z0))
U4(f148_out1, s(z0)) → f119_out1
U4(f148_out2(z0), s(z1)) → f119_out1
f53_in(0, z0) → f53_out1
f53_in(s(z0), z1) → U5(f85_in(z0, z1), s(z0), z1)
U5(f85_out1, s(z0), z1) → f53_out1
f50_in(z0, z1, z2) → U6(f53_in(z0, z1), z0, z1, z2)
U6(f53_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f50_out1
f115_in(z0) → U8(f119_in(z0), f120_in(z0), z0)
U8(f119_out1, z0, z1) → f115_out1
U8(z0, f120_out1(z1), z2) → f115_out2(z1)
f148_in(z0) → U9(f119_in(z0), f150_in(z0), z0)
U9(f119_out1, z0, z1) → f148_out1
U9(z0, f150_out1(z1), z2) → f148_out2(z1)

Tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f50_in(z0, z1, z2), .(z0, .(z1, z2))), F50_IN(z0, z1, z2))
F85_IN(s(z0), 0) → c5(U2'(f115_in(z0), s(z0), 0), F115_IN(z0))
F85_IN(s(z0), s(z1)) → c6(U3'(f85_in(z0, z1), s(z0), s(z1)), F85_IN(z0, z1))
F119_IN(s(z0)) → c10(U4'(f148_in(z0), s(z0)), F148_IN(z0))
F53_IN(s(z0), z1) → c14(U5'(f85_in(z0, z1), s(z0), z1), F85_IN(z0, z1))
F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
U6'(f53_out1, z0, z1, z2) → c17(U7'(f2_in(.(z1, z2)), z0, z1, z2), F2_IN(.(z1, z2)))
F115_IN(z0) → c19(U8'(f119_in(z0), f120_in(z0), z0), F119_IN(z0))
F148_IN(z0) → c22(U9'(f119_in(z0), f150_in(z0), z0), F119_IN(z0))

S tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f50_in(z0, z1, z2), .(z0, .(z1, z2))), F50_IN(z0, z1, z2))
F85_IN(s(z0), 0) → c5(U2'(f115_in(z0), s(z0), 0), F115_IN(z0))
F85_IN(s(z0), s(z1)) → c6(U3'(f85_in(z0, z1), s(z0), s(z1)), F85_IN(z0, z1))
F119_IN(s(z0)) → c10(U4'(f148_in(z0), s(z0)), F148_IN(z0))
F53_IN(s(z0), z1) → c14(U5'(f85_in(z0, z1), s(z0), z1), F85_IN(z0, z1))
F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
U6'(f53_out1, z0, z1, z2) → c17(U7'(f2_in(.(z1, z2)), z0, z1, z2), F2_IN(.(z1, z2)))
F115_IN(z0) → c19(U8'(f119_in(z0), f120_in(z0), z0), F119_IN(z0))
F148_IN(z0) → c22(U9'(f119_in(z0), f150_in(z0), z0), F119_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f85_in, U2, U3, f119_in, U4, f53_in, U5, f50_in, U6, U7, f115_in, U8, f148_in, U9

Defined Pair Symbols:

F2_IN, F85_IN, F119_IN, F53_IN, F50_IN, U6', F115_IN, F148_IN

Compound Symbols:

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

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

Split RHS of tuples not part of any SCC

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f50_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f50_out1, .(z0, .(z1, z2))) → f2_out1
f85_in(0, s(z0)) → f85_out1
f85_in(s(z0), 0) → U2(f115_in(z0), s(z0), 0)
f85_in(s(z0), s(z1)) → U3(f85_in(z0, z1), s(z0), s(z1))
U2(f115_out1, s(z0), 0) → f85_out1
U2(f115_out2(z0), s(z1), 0) → f85_out1
U3(f85_out1, s(z0), s(z1)) → f85_out1
f119_in(s(z0)) → U4(f148_in(z0), s(z0))
U4(f148_out1, s(z0)) → f119_out1
U4(f148_out2(z0), s(z1)) → f119_out1
f53_in(0, z0) → f53_out1
f53_in(s(z0), z1) → U5(f85_in(z0, z1), s(z0), z1)
U5(f85_out1, s(z0), z1) → f53_out1
f50_in(z0, z1, z2) → U6(f53_in(z0, z1), z0, z1, z2)
U6(f53_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f50_out1
f115_in(z0) → U8(f119_in(z0), f120_in(z0), z0)
U8(f119_out1, z0, z1) → f115_out1
U8(z0, f120_out1(z1), z2) → f115_out2(z1)
f148_in(z0) → U9(f119_in(z0), f150_in(z0), z0)
U9(f119_out1, z0, z1) → f148_out1
U9(z0, f150_out1(z1), z2) → f148_out2(z1)

Tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f50_in(z0, z1, z2), .(z0, .(z1, z2))), F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(U3'(f85_in(z0, z1), s(z0), s(z1)), F85_IN(z0, z1))
F119_IN(s(z0)) → c10(U4'(f148_in(z0), s(z0)), F148_IN(z0))
F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
U6'(f53_out1, z0, z1, z2) → c17(U7'(f2_in(.(z1, z2)), z0, z1, z2), F2_IN(.(z1, z2)))
F148_IN(z0) → c22(U9'(f119_in(z0), f150_in(z0), z0), F119_IN(z0))
F85_IN(s(z0), 0) → c(U2'(f115_in(z0), s(z0), 0))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(U5'(f85_in(z0, z1), s(z0), z1))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(U8'(f119_in(z0), f120_in(z0), z0))
F115_IN(z0) → c(F119_IN(z0))

S tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f50_in(z0, z1, z2), .(z0, .(z1, z2))), F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(U3'(f85_in(z0, z1), s(z0), s(z1)), F85_IN(z0, z1))
F119_IN(s(z0)) → c10(U4'(f148_in(z0), s(z0)), F148_IN(z0))
F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
U6'(f53_out1, z0, z1, z2) → c17(U7'(f2_in(.(z1, z2)), z0, z1, z2), F2_IN(.(z1, z2)))
F148_IN(z0) → c22(U9'(f119_in(z0), f150_in(z0), z0), F119_IN(z0))
F85_IN(s(z0), 0) → c(U2'(f115_in(z0), s(z0), 0))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(U5'(f85_in(z0, z1), s(z0), z1))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(U8'(f119_in(z0), f120_in(z0), z0))
F115_IN(z0) → c(F119_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f85_in, U2, U3, f119_in, U4, f53_in, U5, f50_in, U6, U7, f115_in, U8, f148_in, U9

Defined Pair Symbols:

F2_IN, F85_IN, F119_IN, F50_IN, U6', F148_IN, F53_IN, F115_IN

Compound Symbols:

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

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

Removed 8 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f50_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f50_out1, .(z0, .(z1, z2))) → f2_out1
f85_in(0, s(z0)) → f85_out1
f85_in(s(z0), 0) → U2(f115_in(z0), s(z0), 0)
f85_in(s(z0), s(z1)) → U3(f85_in(z0, z1), s(z0), s(z1))
U2(f115_out1, s(z0), 0) → f85_out1
U2(f115_out2(z0), s(z1), 0) → f85_out1
U3(f85_out1, s(z0), s(z1)) → f85_out1
f119_in(s(z0)) → U4(f148_in(z0), s(z0))
U4(f148_out1, s(z0)) → f119_out1
U4(f148_out2(z0), s(z1)) → f119_out1
f53_in(0, z0) → f53_out1
f53_in(s(z0), z1) → U5(f85_in(z0, z1), s(z0), z1)
U5(f85_out1, s(z0), z1) → f53_out1
f50_in(z0, z1, z2) → U6(f53_in(z0, z1), z0, z1, z2)
U6(f53_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f50_out1
f115_in(z0) → U8(f119_in(z0), f120_in(z0), z0)
U8(f119_out1, z0, z1) → f115_out1
U8(z0, f120_out1(z1), z2) → f115_out2(z1)
f148_in(z0) → U9(f119_in(z0), f150_in(z0), z0)
U9(f119_out1, z0, z1) → f148_out1
U9(z0, f150_out1(z1), z2) → f148_out2(z1)

Tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F148_IN(z0) → c22(F119_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

S tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F148_IN(z0) → c22(F119_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f85_in, U2, U3, f119_in, U4, f53_in, U5, f50_in, U6, U7, f115_in, U8, f148_in, U9

Defined Pair Symbols:

F50_IN, F85_IN, F53_IN, F115_IN, F2_IN, F119_IN, U6', F148_IN

Compound Symbols:

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

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

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

F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

We considered the (Usable) Rules:

f53_in(0, z0) → f53_out1
f53_in(s(z0), z1) → U5(f85_in(z0, z1), s(z0), z1)
f85_in(0, s(z0)) → f85_out1
f85_in(s(z0), 0) → U2(f115_in(z0), s(z0), 0)
f85_in(s(z0), s(z1)) → U3(f85_in(z0, z1), s(z0), s(z1))
U5(f85_out1, s(z0), z1) → f53_out1
U3(f85_out1, s(z0), s(z1)) → f85_out1
f115_in(z0) → U8(f119_in(z0), f120_in(z0), z0)
U2(f115_out1, s(z0), 0) → f85_out1
U2(f115_out2(z0), s(z1), 0) → f85_out1
f119_in(s(z0)) → U4(f148_in(z0), s(z0))
U8(f119_out1, z0, z1) → f115_out1
f148_in(z0) → U9(f119_in(z0), f150_in(z0), z0)
U4(f148_out1, s(z0)) → f119_out1
U4(f148_out2(z0), s(z1)) → f119_out1
U9(f119_out1, z0, z1) → f148_out1

And the Tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F148_IN(z0) → c22(F119_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

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

POL(.(x₁, x₂)) = [1] + x₁ + x₂   
POL(0) = 0   
POL(F115_IN(x₁)) = [3] + x₁   
POL(F119_IN(x₁)) = x₁   
POL(F148_IN(x₁)) = x₁   
POL(F2_IN(x₁)) = x₁   
POL(F50_IN(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃   
POL(F53_IN(x₁, x₂)) = [1] + x₁   
POL(F85_IN(x₁, x₂)) = [2] + x₁   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂)) = [3]x₂   
POL(U5(x₁, x₂, x₃)) = 0   
POL(U6'(x₁, x₂, x₃, x₄)) = [1] + x₃ + x₄   
POL(U8(x₁, x₂, x₃)) = 0   
POL(U9(x₁, x₂, x₃)) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(f115_in(x₁)) = 0   
POL(f115_out1) = 0   
POL(f115_out2(x₁)) = 0   
POL(f119_in(x₁)) = [2] + [3]x₁   
POL(f119_out1) = 0   
POL(f120_in(x₁)) = 0   
POL(f148_in(x₁)) = 0   
POL(f148_out1) = 0   
POL(f148_out2(x₁)) = 0   
POL(f150_in(x₁)) = 0   
POL(f53_in(x₁, x₂)) = 0   
POL(f53_out1) = 0   
POL(f85_in(x₁, x₂)) = 0   
POL(f85_out1) = 0   
POL(s(x₁)) = [2] + x₁   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f50_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f50_out1, .(z0, .(z1, z2))) → f2_out1
f85_in(0, s(z0)) → f85_out1
f85_in(s(z0), 0) → U2(f115_in(z0), s(z0), 0)
f85_in(s(z0), s(z1)) → U3(f85_in(z0, z1), s(z0), s(z1))
U2(f115_out1, s(z0), 0) → f85_out1
U2(f115_out2(z0), s(z1), 0) → f85_out1
U3(f85_out1, s(z0), s(z1)) → f85_out1
f119_in(s(z0)) → U4(f148_in(z0), s(z0))
U4(f148_out1, s(z0)) → f119_out1
U4(f148_out2(z0), s(z1)) → f119_out1
f53_in(0, z0) → f53_out1
f53_in(s(z0), z1) → U5(f85_in(z0, z1), s(z0), z1)
U5(f85_out1, s(z0), z1) → f53_out1
f50_in(z0, z1, z2) → U6(f53_in(z0, z1), z0, z1, z2)
U6(f53_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f50_out1
f115_in(z0) → U8(f119_in(z0), f120_in(z0), z0)
U8(f119_out1, z0, z1) → f115_out1
U8(z0, f120_out1(z1), z2) → f115_out2(z1)
f148_in(z0) → U9(f119_in(z0), f150_in(z0), z0)
U9(f119_out1, z0, z1) → f148_out1
U9(z0, f150_out1(z1), z2) → f148_out2(z1)

Tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F148_IN(z0) → c22(F119_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

S tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F148_IN(z0) → c22(F119_IN(z0))

K tuples:

F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

Defined Rule Symbols:

f2_in, U1, f85_in, U2, U3, f119_in, U4, f53_in, U5, f50_in, U6, U7, f115_in, U8, f148_in, U9

Defined Pair Symbols:

F50_IN, F85_IN, F53_IN, F115_IN, F2_IN, F119_IN, U6', F148_IN

Compound Symbols:

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

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F148_IN(z0) → c22(F119_IN(z0))
F119_IN(s(z0)) → c10(F148_IN(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f50_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f50_out1, .(z0, .(z1, z2))) → f2_out1
f85_in(0, s(z0)) → f85_out1
f85_in(s(z0), 0) → U2(f115_in(z0), s(z0), 0)
f85_in(s(z0), s(z1)) → U3(f85_in(z0, z1), s(z0), s(z1))
U2(f115_out1, s(z0), 0) → f85_out1
U2(f115_out2(z0), s(z1), 0) → f85_out1
U3(f85_out1, s(z0), s(z1)) → f85_out1
f119_in(s(z0)) → U4(f148_in(z0), s(z0))
U4(f148_out1, s(z0)) → f119_out1
U4(f148_out2(z0), s(z1)) → f119_out1
f53_in(0, z0) → f53_out1
f53_in(s(z0), z1) → U5(f85_in(z0, z1), s(z0), z1)
U5(f85_out1, s(z0), z1) → f53_out1
f50_in(z0, z1, z2) → U6(f53_in(z0, z1), z0, z1, z2)
U6(f53_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f50_out1
f115_in(z0) → U8(f119_in(z0), f120_in(z0), z0)
U8(f119_out1, z0, z1) → f115_out1
U8(z0, f120_out1(z1), z2) → f115_out2(z1)
f148_in(z0) → U9(f119_in(z0), f150_in(z0), z0)
U9(f119_out1, z0, z1) → f148_out1
U9(z0, f150_out1(z1), z2) → f148_out2(z1)

Tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F148_IN(z0) → c22(F119_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

S tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))

K tuples:

F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c
F148_IN(z0) → c22(F119_IN(z0))

Defined Rule Symbols:

f2_in, U1, f85_in, U2, U3, f119_in, U4, f53_in, U5, f50_in, U6, U7, f115_in, U8, f148_in, U9

Defined Pair Symbols:

F50_IN, F85_IN, F53_IN, F115_IN, F2_IN, F119_IN, U6', F148_IN

Compound Symbols:

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

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

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

F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))

We considered the (Usable) Rules:

f53_in(0, z0) → f53_out1
f53_in(s(z0), z1) → U5(f85_in(z0, z1), s(z0), z1)
f85_in(0, s(z0)) → f85_out1
f85_in(s(z0), 0) → U2(f115_in(z0), s(z0), 0)
f85_in(s(z0), s(z1)) → U3(f85_in(z0, z1), s(z0), s(z1))
U5(f85_out1, s(z0), z1) → f53_out1
U3(f85_out1, s(z0), s(z1)) → f85_out1
f115_in(z0) → U8(f119_in(z0), f120_in(z0), z0)
U2(f115_out1, s(z0), 0) → f85_out1
U2(f115_out2(z0), s(z1), 0) → f85_out1
f119_in(s(z0)) → U4(f148_in(z0), s(z0))
U8(f119_out1, z0, z1) → f115_out1
f148_in(z0) → U9(f119_in(z0), f150_in(z0), z0)
U4(f148_out1, s(z0)) → f119_out1
U4(f148_out2(z0), s(z1)) → f119_out1
U9(f119_out1, z0, z1) → f148_out1

And the Tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F148_IN(z0) → c22(F119_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

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

POL(.(x₁, x₂)) = [1] + x₂   
POL(0) = 0   
POL(F115_IN(x₁)) = 0   
POL(F119_IN(x₁)) = 0   
POL(F148_IN(x₁)) = 0   
POL(F2_IN(x₁)) = x₁   
POL(F50_IN(x₁, x₂, x₃)) = [1] + x₃   
POL(F53_IN(x₁, x₂)) = 0   
POL(F85_IN(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂)) = 0   
POL(U5(x₁, x₂, x₃)) = 0   
POL(U6'(x₁, x₂, x₃, x₄)) = [1] + x₄   
POL(U8(x₁, x₂, x₃)) = 0   
POL(U9(x₁, x₂, x₃)) = x₁   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(f115_in(x₁)) = [3] + x₁   
POL(f115_out1) = 0   
POL(f115_out2(x₁)) = 0   
POL(f119_in(x₁)) = [1] + x₁   
POL(f119_out1) = 0   
POL(f120_in(x₁)) = 0   
POL(f148_in(x₁)) = [1] + [2]x₁   
POL(f148_out1) = 0   
POL(f148_out2(x₁)) = 0   
POL(f150_in(x₁)) = 0   
POL(f53_in(x₁, x₂)) = 0   
POL(f53_out1) = 0   
POL(f85_in(x₁, x₂)) = 0   
POL(f85_out1) = 0   
POL(s(x₁)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z1, z2))) → U1(f50_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f50_out1, .(z0, .(z1, z2))) → f2_out1
f85_in(0, s(z0)) → f85_out1
f85_in(s(z0), 0) → U2(f115_in(z0), s(z0), 0)
f85_in(s(z0), s(z1)) → U3(f85_in(z0, z1), s(z0), s(z1))
U2(f115_out1, s(z0), 0) → f85_out1
U2(f115_out2(z0), s(z1), 0) → f85_out1
U3(f85_out1, s(z0), s(z1)) → f85_out1
f119_in(s(z0)) → U4(f148_in(z0), s(z0))
U4(f148_out1, s(z0)) → f119_out1
U4(f148_out2(z0), s(z1)) → f119_out1
f53_in(0, z0) → f53_out1
f53_in(s(z0), z1) → U5(f85_in(z0, z1), s(z0), z1)
U5(f85_out1, s(z0), z1) → f53_out1
f50_in(z0, z1, z2) → U6(f53_in(z0, z1), z0, z1, z2)
U6(f53_out1, z0, z1, z2) → U7(f2_in(.(z1, z2)), z0, z1, z2)
U7(f2_out1, z0, z1, z2) → f50_out1
f115_in(z0) → U8(f119_in(z0), f120_in(z0), z0)
U8(f119_out1, z0, z1) → f115_out1
U8(z0, f120_out1(z1), z2) → f115_out2(z1)
f148_in(z0) → U9(f119_in(z0), f150_in(z0), z0)
U9(f119_out1, z0, z1) → f148_out1
U9(z0, f150_out1(z1), z2) → f148_out2(z1)

Tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))
F148_IN(z0) → c22(F119_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c

S tuples:

F50_IN(z0, z1, z2) → c16(U6'(f53_in(z0, z1), z0, z1, z2), F53_IN(z0, z1))
U6'(f53_out1, z0, z1, z2) → c17(F2_IN(.(z1, z2)))

K tuples:

F85_IN(s(z0), 0) → c(F115_IN(z0))
F53_IN(s(z0), z1) → c(F85_IN(z0, z1))
F115_IN(z0) → c(F119_IN(z0))
F85_IN(s(z0), s(z1)) → c6(F85_IN(z0, z1))
F119_IN(s(z0)) → c10(F148_IN(z0))
F85_IN(s(z0), 0) → c
F53_IN(s(z0), z1) → c
F115_IN(z0) → c
F148_IN(z0) → c22(F119_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c2(F50_IN(z0, z1, z2))

Defined Rule Symbols:

f2_in, U1, f85_in, U2, U3, f119_in, U4, f53_in, U5, f50_in, U6, U7, f115_in, U8, f148_in, U9

Defined Pair Symbols:

F50_IN, F85_IN, F53_IN, F115_IN, F2_IN, F119_IN, U6', F148_IN

Compound Symbols:

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

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

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: ordered(T1), SCOPE: 1, CLAUSE: 0 | ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: !_1 | ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nordered(T1) !=? ordered([])", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: !_1 | ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX7 is free\nordered(T1) !=? ordered([])\nordered(T1) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(head(T5, X10), ','(tail(T5, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13)))))))\n\nT5 is ground\nX7 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nordered(T5) !=? ordered([])\nordered(T5) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(head(T5, X10), ','(tail(T5, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13))))))), SCOPE: 2, CLAUSE: 3 | ','(head(T5, X10), ','(tail(T5, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13))))))), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX7 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nordered(T5) !=? ordered([])\nordered(T5) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(head(T5, X10), ','(tail(T5, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13))))))), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX7 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nordered(T5) !=? ordered([])\nordered(T5) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(tail(.(T10, T11), X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(T10, s(X12)), ordered(.(X12, X13))))))\n\nT10 is ground\nT11 is ground\nX7 is free\nX11 is free\nX12 is free\nX13 is free\nordered(.(T10, T11)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(tail(.(T10, T11), X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(T10, s(X12)), ordered(.(X12, X13)))))), SCOPE: 3, CLAUSE: 5 | ','(tail(.(T10, T11), X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(T10, s(X12)), ordered(.(X12, X13)))))), SCOPE: 3, CLAUSE: 6\n\nT10 is ground\nT11 is ground\nX7 is free\nX11 is free\nX12 is free\nX13 is free\nordered(.(T10, T11)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(tail(.(T10, T11), X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(T10, s(X12)), ordered(.(X12, X13)))))), SCOPE: 3, CLAUSE: 6\n\nT10 is ground\nT11 is ground\nX7 is free\nX11 is free\nX12 is free\nX13 is free\nordered(.(T10, T11)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(head(T17, X12), ','(tail(T17, X13), ','(less(T16, s(X12)), ordered(.(X12, X13)))))\n\nT16 is ground\nT17 is ground\nX7 is free\nX12 is free\nX13 is free\nordered(.(T16, T17)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(head(T17, X12), ','(tail(T17, X13), ','(less(T16, s(X12)), ordered(.(X12, X13))))), SCOPE: 4, CLAUSE: 3 | ','(head(T17, X12), ','(tail(T17, X13), ','(less(T16, s(X12)), ordered(.(X12, X13))))), SCOPE: 4, CLAUSE: 4\n\nT16 is ground\nT17 is ground\nX7 is free\nX12 is free\nX13 is free\nordered(.(T16, T17)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(head(T17, X12), ','(tail(T17, X13), ','(less(T16, s(X12)), ordered(.(X12, X13))))), SCOPE: 4, CLAUSE: 4\n\nT16 is ground\nT17 is ground\nX7 is free\nX12 is free\nX13 is free\nordered(.(T16, T17)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(tail(.(T22, T23), X13), ','(less(T16, s(T22)), ordered(.(T22, X13))))\n\nT16 is ground\nT22 is ground\nT23 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(tail(.(T22, T23), X13), ','(less(T16, s(T22)), ordered(.(T22, X13)))), SCOPE: 5, CLAUSE: 5 | ','(tail(.(T22, T23), X13), ','(less(T16, s(T22)), ordered(.(T22, X13)))), SCOPE: 5, CLAUSE: 6\n\nT16 is ground\nT22 is ground\nT23 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(tail(.(T22, T23), X13), ','(less(T16, s(T22)), ordered(.(T22, X13)))), SCOPE: 5, CLAUSE: 6\n\nT16 is ground\nT22 is ground\nT23 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(less(T16, s(T30)), ordered(.(T30, T31)))\n\nT16 is ground\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: less(T16, s(T30))\n\nT16 is ground\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ordered(.(T30, T31))\n\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: less(T16, s(T30)), SCOPE: 6, CLAUSE: 7 | less(T16, s(T30)), SCOPE: 6, CLAUSE: 8\n\nT16 is ground\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(!_6, eq(s(T36), s(X63))) | less(0, s(T36)), SCOPE: 6, CLAUSE: 8\n\nT36 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: less(T16, s(T30)), SCOPE: 6, CLAUSE: 8\n\nT16 is ground\nT30 is ground\nX62 is free\nless(T16, s(T30)) !=? less(0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: eq(s(T36), s(X63))\n\nT36 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: eq(s(T36), s(X63)), SCOPE: 7, CLAUSE: 11\n\nT36 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(p(T44, X78), ','(p(s(T45), X79), less(X78, X79)))\n\nT44 is ground\nT45 is ground\nX62 is free\nX78 is free\nX79 is free\nless(T44, s(T45)) !=? less(0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(p(T44, X78), ','(p(s(T45), X79), less(X78, X79))), SCOPE: 8, CLAUSE: 9 | ','(p(T44, X78), ','(p(s(T45), X79), less(X78, X79))), SCOPE: 8, CLAUSE: 10\n\nT44 is ground\nT45 is ground\nX62 is free\nX78 is free\nX79 is free\nless(T44, s(T45)) !=? less(0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ','(p(T44, X78), ','(p(s(T45), X79), less(X78, X79))), SCOPE: 8, CLAUSE: 10\n\nT44 is ground\nT45 is ground\nX62 is free\nX78 is free\nX79 is free\nless(T44, s(T45)) !=? less(0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(p(s(T45), X79), less(T48, X79))\n\nT45 is ground\nT48 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(p(s(T45), X79), less(T48, X79)), SCOPE: 9, CLAUSE: 9 | ','(p(s(T45), X79), less(T48, X79)), SCOPE: 9, CLAUSE: 10\n\nT45 is ground\nT48 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(p(s(T45), X79), less(T48, X79)), SCOPE: 9, CLAUSE: 10\n\nT45 is ground\nT48 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: less(T48, T52)\n\nT48 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: less(T48, T52), SCOPE: 10, CLAUSE: 7 | less(T48, T52), SCOPE: 10, CLAUSE: 8\n\nT48 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(!_10, eq(T56, s(X100))) | less(0, T56), SCOPE: 10, CLAUSE: 8\n\nT56 is ground\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: less(T48, T52), SCOPE: 10, CLAUSE: 8\n\nT48 is ground\nT52 is ground\nX99 is free\nless(T48, T52) !=? less(0, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: eq(T56, s(X100))\n\nT56 is ground\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: eq(T56, s(X100)), SCOPE: 11, CLAUSE: 11\n\nT56 is ground\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(p(T67, X115), ','(p(T68, X116), less(X115, X116)))\n\nT67 is ground\nT68 is ground\nX99 is free\nX115 is free\nX116 is free\nless(T67, T68) !=? less(0, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(p(T67, X115), ','(p(T68, X116), less(X115, X116))), SCOPE: 12, CLAUSE: 9 | ','(p(T67, X115), ','(p(T68, X116), less(X115, X116))), SCOPE: 12, CLAUSE: 10\n\nT67 is ground\nT68 is ground\nX99 is free\nX115 is free\nX116 is free\nless(T67, T68) !=? less(0, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(p(T67, X115), ','(p(T68, X116), less(X115, X116))), SCOPE: 12, CLAUSE: 10\n\nT67 is ground\nT68 is ground\nX99 is free\nX115 is free\nX116 is free\nless(T67, T68) !=? less(0, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(p(T68, X116), less(T71, X116))\n\nT68 is ground\nT71 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(p(T68, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 9 | ','(p(T68, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 10\n\nT68 is ground\nT71 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: less(T71, 0) | ','(p(0, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 10\n\nT71 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(p(T68, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 10\n\nT68 is ground\nT71 is ground\nX116 is free\np(T68, X116) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: less(T71, 0)\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(p(0, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 10\n\nT71 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: less(T71, 0), SCOPE: 14, CLAUSE: 7 | less(T71, 0), SCOPE: 14, CLAUSE: 8\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(!_14, eq(0, s(X134))) | less(0, 0), SCOPE: 14, CLAUSE: 8\n\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: less(T71, 0), SCOPE: 14, CLAUSE: 8\n\nT71 is ground\nX133 is free\nless(T71, 0) !=? less(0, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: eq(0, s(X134))\n\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: eq(0, s(X134)), SCOPE: 15, CLAUSE: 11\n\nX134 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(p(T74, X147), ','(p(0, X148), less(X147, X148)))\n\nT74 is ground\nX133 is free\nX147 is free\nX148 is free\nless(T74, 0) !=? less(0, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(p(T74, X147), ','(p(0, X148), less(X147, X148))), SCOPE: 16, CLAUSE: 9 | ','(p(T74, X147), ','(p(0, X148), less(X147, X148))), SCOPE: 16, CLAUSE: 10\n\nT74 is ground\nX133 is free\nX147 is free\nX148 is free\nless(T74, 0) !=? less(0, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(p(T74, X147), ','(p(0, X148), less(X147, X148))), SCOPE: 16, CLAUSE: 10\n\nT74 is ground\nX133 is free\nX147 is free\nX148 is free\nless(T74, 0) !=? less(0, X133)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(p(0, X148), less(T77, X148))\n\nT77 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(p(0, X148), less(T77, X148)), SCOPE: 17, CLAUSE: 9 | ','(p(0, X148), less(T77, X148)), SCOPE: 17, CLAUSE: 10\n\nT77 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: less(T77, 0) | ','(p(0, X148), less(T77, X148)), SCOPE: 17, CLAUSE: 10\n\nT77 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: less(T77, 0)\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(p(0, X148), less(T77, X148)), SCOPE: 17, CLAUSE: 10\n\nT77 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: less(T71, T80)\n\nT71 is ground\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 157 [arrowhead = none ];
157 -> 4;

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

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

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

161 [label="EVAL with clause\nordered(.(X7, [])) :- !_1.\nand substitutionX7 -> T3,\nT1 -> .(T3, [])", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 161 [arrowhead = none ];
161 -> 13;

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

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

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

165 [label="ONLY EVAL with clause\nordered(X9) :- ','(head(X9, X10), ','(tail(X9, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13))))))).\nand substitutionT1 -> T5,\nX9 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 165 [arrowhead = none ];
165 -> 21;

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

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

168 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(T5), ordered([]))", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 168 [arrowhead = none ];
168 -> 24;

169 [label="EVAL with clause\nhead(.(X20, X21), X20).\nand substitutionX20 -> T10,\nX21 -> T11,\nT5 -> .(T10, T11),\nX10 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 169 [arrowhead = none ];
169 -> 27;

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

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

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

173 [label="ONLY EVAL with clause\ntail(.(X32, X33), X33).\nand substitutionT10 -> T16,\nX32 -> T16,\nT11 -> T17,\nX33 -> T17,\nX11 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 173 [arrowhead = none ];
173 -> 33;

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

175 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(.(T16, T17)), ordered(.(X7, [])))", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 175 [arrowhead = none ];
175 -> 37;

176 [label="EVAL with clause\nhead(.(X43, X44), X43).\nand substitutionX43 -> T22,\nX44 -> T23,\nT17 -> .(T22, T23),\nX12 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 176 [arrowhead = none ];
176 -> 38;

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

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

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

180 [label="ONLY EVAL with clause\ntail(.(X53, X54), X54).\nand substitutionT22 -> T30,\nX53 -> T30,\nT23 -> T31,\nX54 -> T31,\nX13 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 180 [arrowhead = none ];
180 -> 45;

181 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
45 -> 181 [arrowhead = none ];
181 -> 51;

182 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nT30 is ground", fontsize=14, style = filled, fillcolor = violet];
45 -> 182 [arrowhead = none ];
182 -> 52;

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

184 [label="INSTANCE with matching:\nT1 -> .(T30, T31)", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 184 [arrowhead = none , style=dashed];
184 -> 1[style=dashed];

185 [label="EVAL with clause\nless(0, X62) :- ','(!_6, eq(X62, s(X63))).\nand substitutionT16 -> 0,\nT30 -> T36,\nX62 -> s(T36)", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 185 [arrowhead = none ];
185 -> 57;

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

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

188 [label="ONLY EVAL with clause\nless(X76, X77) :- ','(p(X76, X78), ','(p(X77, X79), less(X78, X79))).\nand substitutionT16 -> T44,\nX76 -> T44,\nT30 -> T45,\nX77 -> s(T45)", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 188 [arrowhead = none ];
188 -> 69;

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

190 [label="ONLY EVAL with clause\neq(X66, X66).\nand substitutionT36 -> T39,\nX66 -> s(T39),\nX63 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 190 [arrowhead = none ];
190 -> 65;

191 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 191 [arrowhead = none ];
191 -> 66;

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

193 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T44, s(T45)), less(0, X62))", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 193 [arrowhead = none ];
193 -> 72;

194 [label="EVAL with clause\np(s(X85), X85).\nand substitutionX85 -> T48,\nT44 -> s(T48),\nX78 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 194 [arrowhead = none ];
194 -> 75;

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

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

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

198 [label="ONLY EVAL with clause\np(s(X93), X93).\nand substitutionT45 -> T52,\nX93 -> T52,\nX79 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 198 [arrowhead = none ];
198 -> 83;

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

200 [label="EVAL with clause\nless(0, X99) :- ','(!_10, eq(X99, s(X100))).\nand substitutionT48 -> 0,\nT52 -> T56,\nX99 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 200 [arrowhead = none ];
200 -> 86;

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

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

203 [label="ONLY EVAL with clause\nless(X113, X114) :- ','(p(X113, X115), ','(p(X114, X116), less(X115, X116))).\nand substitutionT48 -> T67,\nX113 -> T67,\nT52 -> T68,\nX114 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 203 [arrowhead = none ];
203 -> 101;

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

205 [label="EVAL with clause\neq(X103, X103).\nand substitutionT56 -> s(T62),\nX103 -> s(T62),\nX100 -> T62,\nT61 -> s(T62)", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 205 [arrowhead = none ];
205 -> 93;

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

207 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 207 [arrowhead = none ];
207 -> 97;

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

209 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T67, T68), less(0, X99))", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 209 [arrowhead = none ];
209 -> 103;

210 [label="EVAL with clause\np(s(X122), X122).\nand substitutionX122 -> T71,\nT67 -> s(T71),\nX115 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 210 [arrowhead = none ];
210 -> 105;

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

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

213 [label="EVAL with clause\np(0, 0).\nand substitutionT68 -> 0,\nX116 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 213 [arrowhead = none ];
213 -> 110;

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

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

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

217 [label="EVAL with clause\np(s(X168), X168).\nand substitutionX168 -> T80,\nT68 -> s(T80),\nX116 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 217 [arrowhead = none ];
217 -> 155;

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

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

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

221 [label="EVAL with clause\nless(0, X133) :- ','(!_14, eq(X133, s(X134))).\nand substitutionT71 -> 0,\nX133 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 221 [arrowhead = none ];
221 -> 122;

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

223 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 223 [arrowhead = none ];
223 -> 125;

224 [label="ONLY EVAL with clause\nless(X145, X146) :- ','(p(X145, X147), ','(p(X146, X148), less(X147, X148))).\nand substitutionT71 -> T74,\nX145 -> T74,\nX146 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 224 [arrowhead = none ];
224 -> 133;

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

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

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

228 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T74, 0), less(0, X133))", fontsize=14, style = filled, fillcolor = lightgreen];
134 -> 228 [arrowhead = none ];
228 -> 135;

229 [label="EVAL with clause\np(s(X154), X154).\nand substitutionX154 -> T77,\nT74 -> s(T77),\nX147 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 229 [arrowhead = none ];
229 -> 138;

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

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

232 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX148 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 232 [arrowhead = none ];
232 -> 144;

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

234 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
144 -> 234 [arrowhead = none ];
234 -> 147;

235 [label="INSTANCE with matching:\nT71 -> T77", fontsize=14, style = filled, fillcolor = lightgrey];
146 -> 235 [arrowhead = none , style=dashed];
235 -> 116[style=dashed];

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

237 [label="INSTANCE with matching:\nT48 -> T71\nT52 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
155 -> 237 [arrowhead = none , style=dashed];
237 -> 83[style=dashed];

}

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f45_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f45_out1, .(z0, .(z1, z2))) → f1_out1
f83_in(0, s(z0)) → f83_out1
f83_in(s(z0), 0) → U2(f110_in(z0), s(z0), 0)
f83_in(s(z0), s(z1)) → U3(f83_in(z0, z1), s(z0), s(z1))
U2(f110_out1, s(z0), 0) → f83_out1
U2(f110_out2(z0), s(z1), 0) → f83_out1
U3(f83_out1, s(z0), s(z1)) → f83_out1
f116_in(s(z0)) → U4(f144_in(z0), s(z0))
U4(f144_out1, s(z0)) → f116_out1
U4(f144_out2(z0), s(z1)) → f116_out1
f51_in(0, z0) → f51_out1
f51_in(s(z0), z1) → U5(f83_in(z0, z1), s(z0), z1)
U5(f83_out1, s(z0), z1) → f51_out1
f45_in(z0, z1, z2) → U6(f51_in(z0, z1), z0, z1, z2)
U6(f51_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f45_out1
f110_in(z0) → U8(f116_in(z0), f117_in(z0), z0)
U8(f116_out1, z0, z1) → f110_out1
U8(z0, f117_out1(z1), z2) → f110_out2(z1)
f144_in(z0) → U9(f116_in(z0), f147_in(z0), z0)
U9(f116_out1, z0, z1) → f144_out1
U9(z0, f147_out1(z1), z2) → f144_out2(z1)

Tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f45_in(z0, z1, z2), .(z0, .(z1, z2))), F45_IN(z0, z1, z2))
F83_IN(s(z0), 0) → c5(U2'(f110_in(z0), s(z0), 0), F110_IN(z0))
F83_IN(s(z0), s(z1)) → c6(U3'(f83_in(z0, z1), s(z0), s(z1)), F83_IN(z0, z1))
F116_IN(s(z0)) → c10(U4'(f144_in(z0), s(z0)), F144_IN(z0))
F51_IN(s(z0), z1) → c14(U5'(f83_in(z0, z1), s(z0), z1), F83_IN(z0, z1))
F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
U6'(f51_out1, z0, z1, z2) → c17(U7'(f1_in(.(z1, z2)), z0, z1, z2), F1_IN(.(z1, z2)))
F110_IN(z0) → c19(U8'(f116_in(z0), f117_in(z0), z0), F116_IN(z0))
F144_IN(z0) → c22(U9'(f116_in(z0), f147_in(z0), z0), F116_IN(z0))

S tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f45_in(z0, z1, z2), .(z0, .(z1, z2))), F45_IN(z0, z1, z2))
F83_IN(s(z0), 0) → c5(U2'(f110_in(z0), s(z0), 0), F110_IN(z0))
F83_IN(s(z0), s(z1)) → c6(U3'(f83_in(z0, z1), s(z0), s(z1)), F83_IN(z0, z1))
F116_IN(s(z0)) → c10(U4'(f144_in(z0), s(z0)), F144_IN(z0))
F51_IN(s(z0), z1) → c14(U5'(f83_in(z0, z1), s(z0), z1), F83_IN(z0, z1))
F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
U6'(f51_out1, z0, z1, z2) → c17(U7'(f1_in(.(z1, z2)), z0, z1, z2), F1_IN(.(z1, z2)))
F110_IN(z0) → c19(U8'(f116_in(z0), f117_in(z0), z0), F116_IN(z0))
F144_IN(z0) → c22(U9'(f116_in(z0), f147_in(z0), z0), F116_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f83_in, U2, U3, f116_in, U4, f51_in, U5, f45_in, U6, U7, f110_in, U8, f144_in, U9

Defined Pair Symbols:

F1_IN, F83_IN, F116_IN, F51_IN, F45_IN, U6', F110_IN, F144_IN

Compound Symbols:

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

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

Split RHS of tuples not part of any SCC

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f45_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f45_out1, .(z0, .(z1, z2))) → f1_out1
f83_in(0, s(z0)) → f83_out1
f83_in(s(z0), 0) → U2(f110_in(z0), s(z0), 0)
f83_in(s(z0), s(z1)) → U3(f83_in(z0, z1), s(z0), s(z1))
U2(f110_out1, s(z0), 0) → f83_out1
U2(f110_out2(z0), s(z1), 0) → f83_out1
U3(f83_out1, s(z0), s(z1)) → f83_out1
f116_in(s(z0)) → U4(f144_in(z0), s(z0))
U4(f144_out1, s(z0)) → f116_out1
U4(f144_out2(z0), s(z1)) → f116_out1
f51_in(0, z0) → f51_out1
f51_in(s(z0), z1) → U5(f83_in(z0, z1), s(z0), z1)
U5(f83_out1, s(z0), z1) → f51_out1
f45_in(z0, z1, z2) → U6(f51_in(z0, z1), z0, z1, z2)
U6(f51_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f45_out1
f110_in(z0) → U8(f116_in(z0), f117_in(z0), z0)
U8(f116_out1, z0, z1) → f110_out1
U8(z0, f117_out1(z1), z2) → f110_out2(z1)
f144_in(z0) → U9(f116_in(z0), f147_in(z0), z0)
U9(f116_out1, z0, z1) → f144_out1
U9(z0, f147_out1(z1), z2) → f144_out2(z1)

Tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f45_in(z0, z1, z2), .(z0, .(z1, z2))), F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(U3'(f83_in(z0, z1), s(z0), s(z1)), F83_IN(z0, z1))
F116_IN(s(z0)) → c10(U4'(f144_in(z0), s(z0)), F144_IN(z0))
F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
U6'(f51_out1, z0, z1, z2) → c17(U7'(f1_in(.(z1, z2)), z0, z1, z2), F1_IN(.(z1, z2)))
F144_IN(z0) → c22(U9'(f116_in(z0), f147_in(z0), z0), F116_IN(z0))
F83_IN(s(z0), 0) → c(U2'(f110_in(z0), s(z0), 0))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(U5'(f83_in(z0, z1), s(z0), z1))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(U8'(f116_in(z0), f117_in(z0), z0))
F110_IN(z0) → c(F116_IN(z0))

S tuples:

F1_IN(.(z0, .(z1, z2))) → c2(U1'(f45_in(z0, z1, z2), .(z0, .(z1, z2))), F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(U3'(f83_in(z0, z1), s(z0), s(z1)), F83_IN(z0, z1))
F116_IN(s(z0)) → c10(U4'(f144_in(z0), s(z0)), F144_IN(z0))
F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
U6'(f51_out1, z0, z1, z2) → c17(U7'(f1_in(.(z1, z2)), z0, z1, z2), F1_IN(.(z1, z2)))
F144_IN(z0) → c22(U9'(f116_in(z0), f147_in(z0), z0), F116_IN(z0))
F83_IN(s(z0), 0) → c(U2'(f110_in(z0), s(z0), 0))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(U5'(f83_in(z0, z1), s(z0), z1))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(U8'(f116_in(z0), f117_in(z0), z0))
F110_IN(z0) → c(F116_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f83_in, U2, U3, f116_in, U4, f51_in, U5, f45_in, U6, U7, f110_in, U8, f144_in, U9

Defined Pair Symbols:

F1_IN, F83_IN, F116_IN, F45_IN, U6', F144_IN, F51_IN, F110_IN

Compound Symbols:

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

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

Removed 8 trailing tuple parts

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f45_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f45_out1, .(z0, .(z1, z2))) → f1_out1
f83_in(0, s(z0)) → f83_out1
f83_in(s(z0), 0) → U2(f110_in(z0), s(z0), 0)
f83_in(s(z0), s(z1)) → U3(f83_in(z0, z1), s(z0), s(z1))
U2(f110_out1, s(z0), 0) → f83_out1
U2(f110_out2(z0), s(z1), 0) → f83_out1
U3(f83_out1, s(z0), s(z1)) → f83_out1
f116_in(s(z0)) → U4(f144_in(z0), s(z0))
U4(f144_out1, s(z0)) → f116_out1
U4(f144_out2(z0), s(z1)) → f116_out1
f51_in(0, z0) → f51_out1
f51_in(s(z0), z1) → U5(f83_in(z0, z1), s(z0), z1)
U5(f83_out1, s(z0), z1) → f51_out1
f45_in(z0, z1, z2) → U6(f51_in(z0, z1), z0, z1, z2)
U6(f51_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f45_out1
f110_in(z0) → U8(f116_in(z0), f117_in(z0), z0)
U8(f116_out1, z0, z1) → f110_out1
U8(z0, f117_out1(z1), z2) → f110_out2(z1)
f144_in(z0) → U9(f116_in(z0), f147_in(z0), z0)
U9(f116_out1, z0, z1) → f144_out1
U9(z0, f147_out1(z1), z2) → f144_out2(z1)

Tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F144_IN(z0) → c22(F116_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

S tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F144_IN(z0) → c22(F116_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f83_in, U2, U3, f116_in, U4, f51_in, U5, f45_in, U6, U7, f110_in, U8, f144_in, U9

Defined Pair Symbols:

F45_IN, F83_IN, F51_IN, F110_IN, F1_IN, F116_IN, U6', F144_IN

Compound Symbols:

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

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

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

F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

We considered the (Usable) Rules:

f51_in(0, z0) → f51_out1
f51_in(s(z0), z1) → U5(f83_in(z0, z1), s(z0), z1)
f83_in(0, s(z0)) → f83_out1
f83_in(s(z0), 0) → U2(f110_in(z0), s(z0), 0)
f83_in(s(z0), s(z1)) → U3(f83_in(z0, z1), s(z0), s(z1))
U5(f83_out1, s(z0), z1) → f51_out1
U3(f83_out1, s(z0), s(z1)) → f83_out1
f110_in(z0) → U8(f116_in(z0), f117_in(z0), z0)
U2(f110_out1, s(z0), 0) → f83_out1
U2(f110_out2(z0), s(z1), 0) → f83_out1
f116_in(s(z0)) → U4(f144_in(z0), s(z0))
U8(f116_out1, z0, z1) → f110_out1
f144_in(z0) → U9(f116_in(z0), f147_in(z0), z0)
U4(f144_out1, s(z0)) → f116_out1
U4(f144_out2(z0), s(z1)) → f116_out1
U9(f116_out1, z0, z1) → f144_out1

And the Tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F144_IN(z0) → c22(F116_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

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

POL(.(x₁, x₂)) = [1] + x₁ + x₂   
POL(0) = 0   
POL(F110_IN(x₁)) = [3] + x₁   
POL(F116_IN(x₁)) = x₁   
POL(F144_IN(x₁)) = x₁   
POL(F1_IN(x₁)) = x₁   
POL(F45_IN(x₁, x₂, x₃)) = [2] + x₁ + x₂ + x₃   
POL(F51_IN(x₁, x₂)) = [1] + x₁   
POL(F83_IN(x₁, x₂)) = [2] + x₁   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂)) = [3]x₂   
POL(U5(x₁, x₂, x₃)) = 0   
POL(U6'(x₁, x₂, x₃, x₄)) = [1] + x₃ + x₄   
POL(U8(x₁, x₂, x₃)) = 0   
POL(U9(x₁, x₂, x₃)) = 0   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(f110_in(x₁)) = 0   
POL(f110_out1) = 0   
POL(f110_out2(x₁)) = 0   
POL(f116_in(x₁)) = [2] + [3]x₁   
POL(f116_out1) = 0   
POL(f117_in(x₁)) = 0   
POL(f144_in(x₁)) = 0   
POL(f144_out1) = 0   
POL(f144_out2(x₁)) = 0   
POL(f147_in(x₁)) = 0   
POL(f51_in(x₁, x₂)) = 0   
POL(f51_out1) = 0   
POL(f83_in(x₁, x₂)) = 0   
POL(f83_out1) = 0   
POL(s(x₁)) = [2] + x₁   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f45_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f45_out1, .(z0, .(z1, z2))) → f1_out1
f83_in(0, s(z0)) → f83_out1
f83_in(s(z0), 0) → U2(f110_in(z0), s(z0), 0)
f83_in(s(z0), s(z1)) → U3(f83_in(z0, z1), s(z0), s(z1))
U2(f110_out1, s(z0), 0) → f83_out1
U2(f110_out2(z0), s(z1), 0) → f83_out1
U3(f83_out1, s(z0), s(z1)) → f83_out1
f116_in(s(z0)) → U4(f144_in(z0), s(z0))
U4(f144_out1, s(z0)) → f116_out1
U4(f144_out2(z0), s(z1)) → f116_out1
f51_in(0, z0) → f51_out1
f51_in(s(z0), z1) → U5(f83_in(z0, z1), s(z0), z1)
U5(f83_out1, s(z0), z1) → f51_out1
f45_in(z0, z1, z2) → U6(f51_in(z0, z1), z0, z1, z2)
U6(f51_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f45_out1
f110_in(z0) → U8(f116_in(z0), f117_in(z0), z0)
U8(f116_out1, z0, z1) → f110_out1
U8(z0, f117_out1(z1), z2) → f110_out2(z1)
f144_in(z0) → U9(f116_in(z0), f147_in(z0), z0)
U9(f116_out1, z0, z1) → f144_out1
U9(z0, f147_out1(z1), z2) → f144_out2(z1)

Tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F144_IN(z0) → c22(F116_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

S tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F144_IN(z0) → c22(F116_IN(z0))

K tuples:

F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

Defined Rule Symbols:

f1_in, U1, f83_in, U2, U3, f116_in, U4, f51_in, U5, f45_in, U6, U7, f110_in, U8, f144_in, U9

Defined Pair Symbols:

F45_IN, F83_IN, F51_IN, F110_IN, F1_IN, F116_IN, U6', F144_IN

Compound Symbols:

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

(21) CdtKnowledgeProof (EQUIVALENT transformation)

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

F144_IN(z0) → c22(F116_IN(z0))
F116_IN(s(z0)) → c10(F144_IN(z0))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f45_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f45_out1, .(z0, .(z1, z2))) → f1_out1
f83_in(0, s(z0)) → f83_out1
f83_in(s(z0), 0) → U2(f110_in(z0), s(z0), 0)
f83_in(s(z0), s(z1)) → U3(f83_in(z0, z1), s(z0), s(z1))
U2(f110_out1, s(z0), 0) → f83_out1
U2(f110_out2(z0), s(z1), 0) → f83_out1
U3(f83_out1, s(z0), s(z1)) → f83_out1
f116_in(s(z0)) → U4(f144_in(z0), s(z0))
U4(f144_out1, s(z0)) → f116_out1
U4(f144_out2(z0), s(z1)) → f116_out1
f51_in(0, z0) → f51_out1
f51_in(s(z0), z1) → U5(f83_in(z0, z1), s(z0), z1)
U5(f83_out1, s(z0), z1) → f51_out1
f45_in(z0, z1, z2) → U6(f51_in(z0, z1), z0, z1, z2)
U6(f51_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f45_out1
f110_in(z0) → U8(f116_in(z0), f117_in(z0), z0)
U8(f116_out1, z0, z1) → f110_out1
U8(z0, f117_out1(z1), z2) → f110_out2(z1)
f144_in(z0) → U9(f116_in(z0), f147_in(z0), z0)
U9(f116_out1, z0, z1) → f144_out1
U9(z0, f147_out1(z1), z2) → f144_out2(z1)

Tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F144_IN(z0) → c22(F116_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

S tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))

K tuples:

F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c
F144_IN(z0) → c22(F116_IN(z0))

Defined Rule Symbols:

f1_in, U1, f83_in, U2, U3, f116_in, U4, f51_in, U5, f45_in, U6, U7, f110_in, U8, f144_in, U9

Defined Pair Symbols:

F45_IN, F83_IN, F51_IN, F110_IN, F1_IN, F116_IN, U6', F144_IN

Compound Symbols:

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

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

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

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

We considered the (Usable) Rules:

f51_in(0, z0) → f51_out1
f51_in(s(z0), z1) → U5(f83_in(z0, z1), s(z0), z1)
f83_in(0, s(z0)) → f83_out1
f83_in(s(z0), 0) → U2(f110_in(z0), s(z0), 0)
f83_in(s(z0), s(z1)) → U3(f83_in(z0, z1), s(z0), s(z1))
U5(f83_out1, s(z0), z1) → f51_out1
U3(f83_out1, s(z0), s(z1)) → f83_out1
f110_in(z0) → U8(f116_in(z0), f117_in(z0), z0)
U2(f110_out1, s(z0), 0) → f83_out1
U2(f110_out2(z0), s(z1), 0) → f83_out1
f116_in(s(z0)) → U4(f144_in(z0), s(z0))
U8(f116_out1, z0, z1) → f110_out1
f144_in(z0) → U9(f116_in(z0), f147_in(z0), z0)
U4(f144_out1, s(z0)) → f116_out1
U4(f144_out2(z0), s(z1)) → f116_out1
U9(f116_out1, z0, z1) → f144_out1

And the Tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F144_IN(z0) → c22(F116_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

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

POL(.(x₁, x₂)) = [1] + x₂   
POL(0) = 0   
POL(F110_IN(x₁)) = 0   
POL(F116_IN(x₁)) = 0   
POL(F144_IN(x₁)) = 0   
POL(F1_IN(x₁)) = x₁   
POL(F45_IN(x₁, x₂, x₃)) = [1] + x₃   
POL(F51_IN(x₁, x₂)) = 0   
POL(F83_IN(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂)) = 0   
POL(U5(x₁, x₂, x₃)) = 0   
POL(U6'(x₁, x₂, x₃, x₄)) = [1] + x₄   
POL(U8(x₁, x₂, x₃)) = 0   
POL(U9(x₁, x₂, x₃)) = x₁   
POL(c) = 0   
POL(c(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c16(x₁, x₂)) = x₁ + x₂   
POL(c17(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c22(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(f110_in(x₁)) = [3] + x₁   
POL(f110_out1) = 0   
POL(f110_out2(x₁)) = 0   
POL(f116_in(x₁)) = [1] + x₁   
POL(f116_out1) = 0   
POL(f117_in(x₁)) = 0   
POL(f144_in(x₁)) = [1] + [2]x₁   
POL(f144_out1) = 0   
POL(f144_out2(x₁)) = 0   
POL(f147_in(x₁)) = 0   
POL(f51_in(x₁, x₂)) = 0   
POL(f51_out1) = 0   
POL(f83_in(x₁, x₂)) = 0   
POL(f83_out1) = 0   
POL(s(x₁)) = 0   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z1, z2))) → U1(f45_in(z0, z1, z2), .(z0, .(z1, z2)))
U1(f45_out1, .(z0, .(z1, z2))) → f1_out1
f83_in(0, s(z0)) → f83_out1
f83_in(s(z0), 0) → U2(f110_in(z0), s(z0), 0)
f83_in(s(z0), s(z1)) → U3(f83_in(z0, z1), s(z0), s(z1))
U2(f110_out1, s(z0), 0) → f83_out1
U2(f110_out2(z0), s(z1), 0) → f83_out1
U3(f83_out1, s(z0), s(z1)) → f83_out1
f116_in(s(z0)) → U4(f144_in(z0), s(z0))
U4(f144_out1, s(z0)) → f116_out1
U4(f144_out2(z0), s(z1)) → f116_out1
f51_in(0, z0) → f51_out1
f51_in(s(z0), z1) → U5(f83_in(z0, z1), s(z0), z1)
U5(f83_out1, s(z0), z1) → f51_out1
f45_in(z0, z1, z2) → U6(f51_in(z0, z1), z0, z1, z2)
U6(f51_out1, z0, z1, z2) → U7(f1_in(.(z1, z2)), z0, z1, z2)
U7(f1_out1, z0, z1, z2) → f45_out1
f110_in(z0) → U8(f116_in(z0), f117_in(z0), z0)
U8(f116_out1, z0, z1) → f110_out1
U8(z0, f117_out1(z1), z2) → f110_out2(z1)
f144_in(z0) → U9(f116_in(z0), f147_in(z0), z0)
U9(f116_out1, z0, z1) → f144_out1
U9(z0, f147_out1(z1), z2) → f144_out2(z1)

Tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F144_IN(z0) → c22(F116_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c

S tuples:

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))

K tuples:

F83_IN(s(z0), 0) → c(F110_IN(z0))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
F110_IN(z0) → c(F116_IN(z0))
F83_IN(s(z0), s(z1)) → c6(F83_IN(z0, z1))
F116_IN(s(z0)) → c10(F144_IN(z0))
F83_IN(s(z0), 0) → c
F51_IN(s(z0), z1) → c
F110_IN(z0) → c
F144_IN(z0) → c22(F116_IN(z0))
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))

Defined Rule Symbols:

f1_in, U1, f83_in, U2, U3, f116_in, U4, f51_in, U5, f45_in, U6, U7, f110_in, U8, f144_in, U9

Defined Pair Symbols:

F45_IN, F83_IN, F51_IN, F110_IN, F1_IN, F116_IN, U6', F144_IN

Compound Symbols:

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

(25) CdtKnowledgeProof (EQUIVALENT transformation)

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

F45_IN(z0, z1, z2) → c16(U6'(f51_in(z0, z1), z0, z1, z2), F51_IN(z0, z1))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F51_IN(s(z0), z1) → c(F83_IN(z0, z1))
U6'(f51_out1, z0, z1, z2) → c17(F1_IN(.(z1, z2)))
F51_IN(s(z0), z1) → c
F1_IN(.(z0, .(z1, z2))) → c2(F45_IN(z0, z1, z2))

Now S is empty

(26) BOUNDS(O(1), O(1))