Left Termination of the query pattern
delete(a,a,g)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(a,a,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: delete(T1, T2, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: delmin(T49, T47, T48)\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: delmin(T49, T47, T48), SCOPE: 2, CLAUSE: 5 | delmin(T49, T47, T48), SCOPE: 2, CLAUSE: 6\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: delmin(T49, T47, T48), SCOPE: 2, CLAUSE: 5\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: delmin(T49, T47, T48), SCOPE: 2, CLAUSE: 6\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: delmin(T82, T79, T80)\n\nT79 is ground\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(less(T112, T108), delete(T112, T113, T111))\n\nT108 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: less(T112, T108)\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: delete(T116, T117, T111)\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: less(T112, T108), SCOPE: 3, CLAUSE: 7 | less(T112, T108), SCOPE: 3, CLAUSE: 8\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: less(T112, T108), SCOPE: 3, CLAUSE: 7\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: less(T112, T108), SCOPE: 3, CLAUSE: 8\n\nT108 is ground", 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];
103 [label="103: less(T131, T130)\n\nT130 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 0 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 1 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 2 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 3 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 0\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 1 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 2 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 3 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 1\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 2 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 3 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 2\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 3 | delete(T116, T117, T111), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: delmin(T183, T181, T182)\n\nT181 is ground\nT182 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 3\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: delete(T116, T117, T111), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(less(T208, T209), delete(T208, T213, T212))\n\nT208 is ground\nT209 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: less(T208, T209)\n\nT208 is ground\nT209 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: delete(T208, T213, T212)\n\nT208 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: less(T208, T209), SCOPE: 5, CLAUSE: 7 | less(T208, T209), SCOPE: 5, CLAUSE: 8\n\nT208 is ground\nT209 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: less(T208, T209), SCOPE: 5, CLAUSE: 7\n\nT208 is ground\nT209 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: less(T208, T209), SCOPE: 5, CLAUSE: 8\n\nT208 is ground\nT209 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: less(T227, T228)\n\nT227 is ground\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(less(T246, T245), delete(T245, T250, T249))\n\nT245 is ground\nT246 is ground\nT249 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: less(T246, T245)\n\nT245 is ground\nT246 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: delete(T245, T250, T249)\n\nT245 is ground\nT249 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(less(T270, T274), delete(T274, T275, T273))\n\nT270 is ground\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: less(T270, T274)\n\nT270 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: delete(T278, T279, T273)\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: less(T270, T274), SCOPE: 6, CLAUSE: 7 | less(T270, T274), SCOPE: 6, CLAUSE: 8\n\nT270 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: less(T270, T274), SCOPE: 6, CLAUSE: 7\n\nT270 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: less(T270, T274), SCOPE: 6, CLAUSE: 8\n\nT270 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: less(T291, T293)\n\nT291 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 228 [arrowhead = none ];
228 -> 5;

229 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
5 -> 229 [arrowhead = none ];
229 -> 8;

230 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
5 -> 230 [arrowhead = none ];
230 -> 9;

231 [label="EVAL with clause\ndelete(X12, tree(X12, void, X13), X13).\nand substitutionT1 -> T12,\nX12 -> T12,\nX13 -> T13,\nT2 -> tree(T12, void, T13),\nT3 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 231 [arrowhead = none ];
231 -> 15;

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

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

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

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

236 [label="EVAL with clause\ndelete(X22, tree(X22, X23, void), X23).\nand substitutionT1 -> T22,\nX22 -> T22,\nX23 -> T23,\nT2 -> tree(T22, T23, void),\nT3 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 236 [arrowhead = none ];
236 -> 26;

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

238 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
22 -> 238 [arrowhead = none ];
238 -> 31;

239 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
22 -> 239 [arrowhead = none ];
239 -> 32;

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

241 [label="EVAL with clause\ndelete(X44, tree(X44, X45, X46), tree(X47, X45, X48)) :- delmin(X46, X47, X48).\nand substitutionT1 -> T44,\nX44 -> T44,\nX45 -> T45,\nX46 -> T49,\nT2 -> tree(T44, T45, T49),\nX47 -> T47,\nX48 -> T48,\nT3 -> tree(T47, T45, T48),\nT46 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 241 [arrowhead = none ];
241 -> 51;

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

243 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 243 [arrowhead = none ];
243 -> 80;

244 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 244 [arrowhead = none ];
244 -> 81;

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

246 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 246 [arrowhead = none ];
246 -> 59;

247 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 247 [arrowhead = none ];
247 -> 61;

248 [label="EVAL with clause\ndelmin(tree(X61, void, X62), X61, X62).\nand substitutionX61 -> T62,\nX62 -> T63,\nT49 -> tree(T62, void, T63),\nT47 -> T62,\nT48 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 248 [arrowhead = none ];
248 -> 69;

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

250 [label="EVAL with clause\ndelmin(tree(X75, X76, X77), X78, tree(X75, X79, X80)) :- delmin(X76, X78, X79).\nand substitutionX75 -> T76,\nX76 -> T82,\nX77 -> T78,\nT49 -> tree(T76, T82, T78),\nT47 -> T79,\nX78 -> T79,\nX79 -> T80,\nX80 -> T81,\nT48 -> tree(T76, T80, T81),\nT77 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 250 [arrowhead = none ];
250 -> 74;

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

252 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 252 [arrowhead = none ];
252 -> 71;

253 [label="INSTANCE with matching:\nT49 -> T82\nT47 -> T79\nT48 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 253 [arrowhead = none , style=dashed];
253 -> 51[style=dashed];

254 [label="EVAL with clause\ndelete(X105, tree(X106, X107, X108), tree(X106, X109, X108)) :- ','(less(X105, X106), delete(X105, X107, X109)).\nand substitutionT1 -> T112,\nX105 -> T112,\nX106 -> T108,\nX107 -> T113,\nX108 -> T110,\nT2 -> tree(T108, T113, T110),\nX109 -> T111,\nT3 -> tree(T108, T111, T110),\nT107 -> T112,\nT109 -> T113", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 254 [arrowhead = none ];
254 -> 84;

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

256 [label="EVAL with clause\ndelete(X259, tree(X260, X261, X262), tree(X260, X261, X263)) :- ','(less(X260, X259), delete(X259, X262, X263)).\nand substitutionT1 -> T274,\nX259 -> T274,\nX260 -> T270,\nX261 -> T271,\nX262 -> T275,\nT2 -> tree(T270, T271, T275),\nX263 -> T273,\nT3 -> tree(T270, T271, T273),\nT269 -> T274,\nT272 -> T275", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 256 [arrowhead = none ];
256 -> 214;

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

258 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
84 -> 258 [arrowhead = none ];
258 -> 88;

259 [label="SPLIT 2\nnew knowledge:\nT116 is ground\nT108 is ground\nreplacements:T112 -> T116,\nT113 -> T117", fontsize=14, style = filled, fillcolor = violet];
84 -> 259 [arrowhead = none ];
259 -> 89;

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

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

262 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
94 -> 262 [arrowhead = none ];
262 -> 95;

263 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
94 -> 263 [arrowhead = none ];
263 -> 96;

264 [label="EVAL with clause\nless(0, s(X118)).\nand substitutionT112 -> 0,\nX118 -> T124,\nT108 -> s(T124)", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 264 [arrowhead = none ];
264 -> 98;

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

266 [label="EVAL with clause\nless(s(X123), s(X124)) :- less(X123, X124).\nand substitutionX123 -> T131,\nT112 -> s(T131),\nX124 -> T130,\nT108 -> s(T130),\nT129 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 266 [arrowhead = none ];
266 -> 103;

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

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

269 [label="INSTANCE with matching:\nT112 -> T131\nT108 -> T130", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 269 [arrowhead = none , style=dashed];
269 -> 88[style=dashed];

270 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
105 -> 270 [arrowhead = none ];
270 -> 109;

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

272 [label="EVAL with clause\ndelete(X139, tree(X139, void, X140), X140).\nand substitutionT116 -> T146,\nX139 -> T146,\nX140 -> T147,\nT117 -> tree(T146, void, T147),\nT111 -> T147", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 272 [arrowhead = none ];
272 -> 114;

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

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

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

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

277 [label="EVAL with clause\ndelete(X149, tree(X149, X150, void), X150).\nand substitutionT116 -> T156,\nX149 -> T156,\nX150 -> T157,\nT117 -> tree(T156, T157, void),\nT111 -> T157", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 277 [arrowhead = none ];
277 -> 123;

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

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

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

281 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 281 [arrowhead = none ];
281 -> 125;

282 [label="EVAL with clause\ndelete(X171, tree(X171, X172, X173), tree(X174, X172, X175)) :- delmin(X173, X174, X175).\nand substitutionT116 -> T178,\nX171 -> T178,\nX172 -> T179,\nX173 -> T183,\nT117 -> tree(T178, T179, T183),\nX174 -> T181,\nX175 -> T182,\nT111 -> tree(T181, T179, T182),\nT180 -> T183", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 282 [arrowhead = none ];
282 -> 136;

283 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 283 [arrowhead = none ];
283 -> 138;

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

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

286 [label="INSTANCE with matching:\nT49 -> T183\nT47 -> T181\nT48 -> T182", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 286 [arrowhead = none , style=dashed];
286 -> 51[style=dashed];

287 [label="EVAL with clause\ndelete(X200, tree(X201, X202, X203), tree(X201, X204, X203)) :- ','(less(X200, X201), delete(X200, X202, X204)).\nand substitutionT116 -> T208,\nX200 -> T208,\nX201 -> T209,\nX202 -> T213,\nX203 -> T211,\nT117 -> tree(T209, T213, T211),\nX204 -> T212,\nT111 -> tree(T209, T212, T211),\nT210 -> T213", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 287 [arrowhead = none ];
287 -> 156;

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

289 [label="EVAL with clause\ndelete(X236, tree(X237, X238, X239), tree(X237, X238, X240)) :- ','(less(X237, X236), delete(X236, X239, X240)).\nand substitutionT116 -> T245,\nX236 -> T245,\nX237 -> T246,\nX238 -> T247,\nX239 -> T250,\nT117 -> tree(T246, T247, T250),\nX240 -> T249,\nT111 -> tree(T246, T247, T249),\nT248 -> T250", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 289 [arrowhead = none ];
289 -> 199;

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

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

292 [label="SPLIT 2\nnew knowledge:\nT208 is ground\nT209 is ground", fontsize=14, style = filled, fillcolor = violet];
156 -> 292 [arrowhead = none ];
292 -> 161;

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

294 [label="INSTANCE with matching:\nT116 -> T208\nT117 -> T213\nT111 -> T212", fontsize=14, style = filled, fillcolor = lightgrey];
161 -> 294 [arrowhead = none , style=dashed];
294 -> 89[style=dashed];

295 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
165 -> 295 [arrowhead = none ];
295 -> 166;

296 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
165 -> 296 [arrowhead = none ];
296 -> 167;

297 [label="EVAL with clause\nless(0, s(X213)).\nand substitutionT208 -> 0,\nX213 -> T222,\nT209 -> s(T222)", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 297 [arrowhead = none ];
297 -> 170;

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

299 [label="EVAL with clause\nless(s(X218), s(X219)) :- less(X218, X219).\nand substitutionX218 -> T227,\nT208 -> s(T227),\nX219 -> T228,\nT209 -> s(T228)", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 299 [arrowhead = none ];
299 -> 180;

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

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

302 [label="INSTANCE with matching:\nT208 -> T227\nT209 -> T228", fontsize=14, style = filled, fillcolor = lightgrey];
180 -> 302 [arrowhead = none , style=dashed];
302 -> 160[style=dashed];

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

304 [label="SPLIT 2\nnew knowledge:\nT246 is ground\nT245 is ground", fontsize=14, style = filled, fillcolor = violet];
199 -> 304 [arrowhead = none ];
304 -> 205;

305 [label="INSTANCE with matching:\nT208 -> T246\nT209 -> T245", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 305 [arrowhead = none , style=dashed];
305 -> 160[style=dashed];

306 [label="INSTANCE with matching:\nT116 -> T245\nT117 -> T250\nT111 -> T249", fontsize=14, style = filled, fillcolor = lightgrey];
205 -> 306 [arrowhead = none , style=dashed];
306 -> 89[style=dashed];

307 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
214 -> 307 [arrowhead = none ];
307 -> 218;

308 [label="SPLIT 2\nnew knowledge:\nT270 is ground\nreplacements:T274 -> T278,\nT275 -> T279", fontsize=14, style = filled, fillcolor = violet];
214 -> 308 [arrowhead = none ];
308 -> 219;

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

310 [label="INSTANCE with matching:\nT1 -> T278\nT2 -> T279\nT3 -> T273", fontsize=14, style = filled, fillcolor = lightgrey];
219 -> 310 [arrowhead = none , style=dashed];
310 -> 3[style=dashed];

311 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
220 -> 311 [arrowhead = none ];
311 -> 221;

312 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
220 -> 312 [arrowhead = none ];
312 -> 222;

313 [label="EVAL with clause\nless(0, s(X272)).\nand substitutionT270 -> 0,\nX272 -> T286,\nT274 -> s(T286)", fontsize=14, style = filled, fillcolor = lightblue];
221 -> 313 [arrowhead = none ];
313 -> 223;

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

315 [label="EVAL with clause\nless(s(X277), s(X278)) :- less(X277, X278).\nand substitutionX277 -> T291,\nT270 -> s(T291),\nX278 -> T293,\nT274 -> s(T293),\nT292 -> T293", fontsize=14, style = filled, fillcolor = lightblue];
222 -> 315 [arrowhead = none ];
315 -> 226;

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

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

318 [label="INSTANCE with matching:\nT270 -> T291\nT274 -> T293", fontsize=14, style = filled, fillcolor = lightgrey];
226 -> 318 [arrowhead = none , style=dashed];
318 -> 218[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f3_in(T13) → f3_out1
f3_in(tree(T47, T45, T48)) → U1(f51_in(T47, T48), tree(T47, T45, T48))
U1(f51_out1, tree(T47, T45, T48)) → f3_out1
f3_in(tree(T108, T111, T110)) → U2(f84_in(T108, T111), tree(T108, T111, T110))
U2(f84_out1(T112), tree(T108, T111, T110)) → f3_out1
f3_in(tree(T270, T271, T273)) → U3(f214_in(T270, T273), tree(T270, T271, T273))
U3(f214_out1, tree(T270, T271, T273)) → f3_out1
f51_in(T62, T63) → f51_out1
f51_in(T79, tree(T76, T80, T81)) → U4(f51_in(T79, T80), T79, tree(T76, T80, T81))
U4(f51_out1, T79, tree(T76, T80, T81)) → f51_out1
f88_in(s(T124)) → f88_out1(0)
f88_in(s(T130)) → U5(f88_in(T130), s(T130))
U5(f88_out1(T131), s(T130)) → f88_out1(s(T131))
f89_in(T146, T147) → f89_out1
f89_in(T178, tree(T181, T179, T182)) → U6(f51_in(T181, T182), T178, tree(T181, T179, T182))
U6(f51_out1, T178, tree(T181, T179, T182)) → f89_out1
f89_in(T208, tree(T209, T212, T211)) → U7(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
U7(f156_out1, T208, tree(T209, T212, T211)) → f89_out1
f89_in(T245, tree(T246, T247, T249)) → U8(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
U8(f199_out1, T245, tree(T246, T247, T249)) → f89_out1
f160_in(0, s(T222)) → f160_out1
f160_in(s(T227), s(T228)) → U9(f160_in(T227, T228), s(T227), s(T228))
U9(f160_out1, s(T227), s(T228)) → f160_out1
f218_in(0) → f218_out1
f218_in(s(T291)) → U10(f218_in(T291), s(T291))
U10(f218_out1, s(T291)) → f218_out1
f84_in(T108, T111) → U11(f88_in(T108), T108, T111)
U11(f88_out1(T116), T108, T111) → U12(f89_in(T116, T111), T108, T111, T116)
U12(f89_out1, T108, T111, T116) → f84_out1(T116)
f156_in(T208, T209, T212) → U13(f160_in(T208, T209), T208, T209, T212)
U13(f160_out1, T208, T209, T212) → U14(f89_in(T208, T212), T208, T209, T212)
U14(f89_out1, T208, T209, T212) → f156_out1
f199_in(T246, T245, T249) → U15(f160_in(T246, T245), T246, T245, T249)
U15(f160_out1, T246, T245, T249) → U16(f89_in(T245, T249), T246, T245, T249)
U16(f89_out1, T246, T245, T249) → f199_out1
f214_in(T270, T273) → U17(f218_in(T270), T270, T273)
U17(f218_out1, T270, T273) → U18(f3_in(T273), T270, T273)
U18(f3_out1, T270, T273) → f214_out1

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F3_IN(tree(T47, T45, T48)) → U1¹(f51_in(T47, T48), tree(T47, T45, T48))
F3_IN(tree(T47, T45, T48)) → F51_IN(T47, T48)
F3_IN(tree(T108, T111, T110)) → U2¹(f84_in(T108, T111), tree(T108, T111, T110))
F3_IN(tree(T108, T111, T110)) → F84_IN(T108, T111)
F3_IN(tree(T270, T271, T273)) → U3¹(f214_in(T270, T273), tree(T270, T271, T273))
F3_IN(tree(T270, T271, T273)) → F214_IN(T270, T273)
F51_IN(T79, tree(T76, T80, T81)) → U4¹(f51_in(T79, T80), T79, tree(T76, T80, T81))
F51_IN(T79, tree(T76, T80, T81)) → F51_IN(T79, T80)
F88_IN(s(T130)) → U5¹(f88_in(T130), s(T130))
F88_IN(s(T130)) → F88_IN(T130)
F89_IN(T178, tree(T181, T179, T182)) → U6¹(f51_in(T181, T182), T178, tree(T181, T179, T182))
F89_IN(T178, tree(T181, T179, T182)) → F51_IN(T181, T182)
F89_IN(T208, tree(T209, T212, T211)) → U7¹(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
F89_IN(T208, tree(T209, T212, T211)) → F156_IN(T208, T209, T212)
F89_IN(T245, tree(T246, T247, T249)) → U8¹(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
F89_IN(T245, tree(T246, T247, T249)) → F199_IN(T246, T245, T249)
F160_IN(s(T227), s(T228)) → U9¹(f160_in(T227, T228), s(T227), s(T228))
F160_IN(s(T227), s(T228)) → F160_IN(T227, T228)
F218_IN(s(T291)) → U10¹(f218_in(T291), s(T291))
F218_IN(s(T291)) → F218_IN(T291)
F84_IN(T108, T111) → U11¹(f88_in(T108), T108, T111)
F84_IN(T108, T111) → F88_IN(T108)
U11¹(f88_out1(T116), T108, T111) → U12¹(f89_in(T116, T111), T108, T111, T116)
U11¹(f88_out1(T116), T108, T111) → F89_IN(T116, T111)
F156_IN(T208, T209, T212) → U13¹(f160_in(T208, T209), T208, T209, T212)
F156_IN(T208, T209, T212) → F160_IN(T208, T209)
U13¹(f160_out1, T208, T209, T212) → U14¹(f89_in(T208, T212), T208, T209, T212)
U13¹(f160_out1, T208, T209, T212) → F89_IN(T208, T212)
F199_IN(T246, T245, T249) → U15¹(f160_in(T246, T245), T246, T245, T249)
F199_IN(T246, T245, T249) → F160_IN(T246, T245)
U15¹(f160_out1, T246, T245, T249) → U16¹(f89_in(T245, T249), T246, T245, T249)
U15¹(f160_out1, T246, T245, T249) → F89_IN(T245, T249)
F214_IN(T270, T273) → U17¹(f218_in(T270), T270, T273)
F214_IN(T270, T273) → F218_IN(T270)
U17¹(f218_out1, T270, T273) → U18¹(f3_in(T273), T270, T273)
U17¹(f218_out1, T270, T273) → F3_IN(T273)

The TRS R consists of the following rules:

f3_in(T13) → f3_out1
f3_in(tree(T47, T45, T48)) → U1(f51_in(T47, T48), tree(T47, T45, T48))
U1(f51_out1, tree(T47, T45, T48)) → f3_out1
f3_in(tree(T108, T111, T110)) → U2(f84_in(T108, T111), tree(T108, T111, T110))
U2(f84_out1(T112), tree(T108, T111, T110)) → f3_out1
f3_in(tree(T270, T271, T273)) → U3(f214_in(T270, T273), tree(T270, T271, T273))
U3(f214_out1, tree(T270, T271, T273)) → f3_out1
f51_in(T62, T63) → f51_out1
f51_in(T79, tree(T76, T80, T81)) → U4(f51_in(T79, T80), T79, tree(T76, T80, T81))
U4(f51_out1, T79, tree(T76, T80, T81)) → f51_out1
f88_in(s(T124)) → f88_out1(0)
f88_in(s(T130)) → U5(f88_in(T130), s(T130))
U5(f88_out1(T131), s(T130)) → f88_out1(s(T131))
f89_in(T146, T147) → f89_out1
f89_in(T178, tree(T181, T179, T182)) → U6(f51_in(T181, T182), T178, tree(T181, T179, T182))
U6(f51_out1, T178, tree(T181, T179, T182)) → f89_out1
f89_in(T208, tree(T209, T212, T211)) → U7(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
U7(f156_out1, T208, tree(T209, T212, T211)) → f89_out1
f89_in(T245, tree(T246, T247, T249)) → U8(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
U8(f199_out1, T245, tree(T246, T247, T249)) → f89_out1
f160_in(0, s(T222)) → f160_out1
f160_in(s(T227), s(T228)) → U9(f160_in(T227, T228), s(T227), s(T228))
U9(f160_out1, s(T227), s(T228)) → f160_out1
f218_in(0) → f218_out1
f218_in(s(T291)) → U10(f218_in(T291), s(T291))
U10(f218_out1, s(T291)) → f218_out1
f84_in(T108, T111) → U11(f88_in(T108), T108, T111)
U11(f88_out1(T116), T108, T111) → U12(f89_in(T116, T111), T108, T111, T116)
U12(f89_out1, T108, T111, T116) → f84_out1(T116)
f156_in(T208, T209, T212) → U13(f160_in(T208, T209), T208, T209, T212)
U13(f160_out1, T208, T209, T212) → U14(f89_in(T208, T212), T208, T209, T212)
U14(f89_out1, T208, T209, T212) → f156_out1
f199_in(T246, T245, T249) → U15(f160_in(T246, T245), T246, T245, T249)
U15(f160_out1, T246, T245, T249) → U16(f89_in(T245, T249), T246, T245, T249)
U16(f89_out1, T246, T245, T249) → f199_out1
f214_in(T270, T273) → U17(f218_in(T270), T270, T273)
U17(f218_out1, T270, T273) → U18(f3_in(T273), T270, T273)
U18(f3_out1, T270, T273) → f214_out1

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 6 SCCs with 23 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F218_IN(s(T291)) → F218_IN(T291)

The TRS R consists of the following rules:

f3_in(T13) → f3_out1
f3_in(tree(T47, T45, T48)) → U1(f51_in(T47, T48), tree(T47, T45, T48))
U1(f51_out1, tree(T47, T45, T48)) → f3_out1
f3_in(tree(T108, T111, T110)) → U2(f84_in(T108, T111), tree(T108, T111, T110))
U2(f84_out1(T112), tree(T108, T111, T110)) → f3_out1
f3_in(tree(T270, T271, T273)) → U3(f214_in(T270, T273), tree(T270, T271, T273))
U3(f214_out1, tree(T270, T271, T273)) → f3_out1
f51_in(T62, T63) → f51_out1
f51_in(T79, tree(T76, T80, T81)) → U4(f51_in(T79, T80), T79, tree(T76, T80, T81))
U4(f51_out1, T79, tree(T76, T80, T81)) → f51_out1
f88_in(s(T124)) → f88_out1(0)
f88_in(s(T130)) → U5(f88_in(T130), s(T130))
U5(f88_out1(T131), s(T130)) → f88_out1(s(T131))
f89_in(T146, T147) → f89_out1
f89_in(T178, tree(T181, T179, T182)) → U6(f51_in(T181, T182), T178, tree(T181, T179, T182))
U6(f51_out1, T178, tree(T181, T179, T182)) → f89_out1
f89_in(T208, tree(T209, T212, T211)) → U7(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
U7(f156_out1, T208, tree(T209, T212, T211)) → f89_out1
f89_in(T245, tree(T246, T247, T249)) → U8(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
U8(f199_out1, T245, tree(T246, T247, T249)) → f89_out1
f160_in(0, s(T222)) → f160_out1
f160_in(s(T227), s(T228)) → U9(f160_in(T227, T228), s(T227), s(T228))
U9(f160_out1, s(T227), s(T228)) → f160_out1
f218_in(0) → f218_out1
f218_in(s(T291)) → U10(f218_in(T291), s(T291))
U10(f218_out1, s(T291)) → f218_out1
f84_in(T108, T111) → U11(f88_in(T108), T108, T111)
U11(f88_out1(T116), T108, T111) → U12(f89_in(T116, T111), T108, T111, T116)
U12(f89_out1, T108, T111, T116) → f84_out1(T116)
f156_in(T208, T209, T212) → U13(f160_in(T208, T209), T208, T209, T212)
U13(f160_out1, T208, T209, T212) → U14(f89_in(T208, T212), T208, T209, T212)
U14(f89_out1, T208, T209, T212) → f156_out1
f199_in(T246, T245, T249) → U15(f160_in(T246, T245), T246, T245, T249)
U15(f160_out1, T246, T245, T249) → U16(f89_in(T245, T249), T246, T245, T249)
U16(f89_out1, T246, T245, T249) → f199_out1
f214_in(T270, T273) → U17(f218_in(T270), T270, T273)
U17(f218_out1, T270, T273) → U18(f3_in(T273), T270, T273)
U18(f3_out1, T270, T273) → f214_out1

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(8) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F218_IN(s(T291)) → F218_IN(T291)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• F218_IN(s(T291)) → F218_IN(T291)
  The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F160_IN(s(T227), s(T228)) → F160_IN(T227, T228)

The TRS R consists of the following rules:

f3_in(T13) → f3_out1
f3_in(tree(T47, T45, T48)) → U1(f51_in(T47, T48), tree(T47, T45, T48))
U1(f51_out1, tree(T47, T45, T48)) → f3_out1
f3_in(tree(T108, T111, T110)) → U2(f84_in(T108, T111), tree(T108, T111, T110))
U2(f84_out1(T112), tree(T108, T111, T110)) → f3_out1
f3_in(tree(T270, T271, T273)) → U3(f214_in(T270, T273), tree(T270, T271, T273))
U3(f214_out1, tree(T270, T271, T273)) → f3_out1
f51_in(T62, T63) → f51_out1
f51_in(T79, tree(T76, T80, T81)) → U4(f51_in(T79, T80), T79, tree(T76, T80, T81))
U4(f51_out1, T79, tree(T76, T80, T81)) → f51_out1
f88_in(s(T124)) → f88_out1(0)
f88_in(s(T130)) → U5(f88_in(T130), s(T130))
U5(f88_out1(T131), s(T130)) → f88_out1(s(T131))
f89_in(T146, T147) → f89_out1
f89_in(T178, tree(T181, T179, T182)) → U6(f51_in(T181, T182), T178, tree(T181, T179, T182))
U6(f51_out1, T178, tree(T181, T179, T182)) → f89_out1
f89_in(T208, tree(T209, T212, T211)) → U7(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
U7(f156_out1, T208, tree(T209, T212, T211)) → f89_out1
f89_in(T245, tree(T246, T247, T249)) → U8(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
U8(f199_out1, T245, tree(T246, T247, T249)) → f89_out1
f160_in(0, s(T222)) → f160_out1
f160_in(s(T227), s(T228)) → U9(f160_in(T227, T228), s(T227), s(T228))
U9(f160_out1, s(T227), s(T228)) → f160_out1
f218_in(0) → f218_out1
f218_in(s(T291)) → U10(f218_in(T291), s(T291))
U10(f218_out1, s(T291)) → f218_out1
f84_in(T108, T111) → U11(f88_in(T108), T108, T111)
U11(f88_out1(T116), T108, T111) → U12(f89_in(T116, T111), T108, T111, T116)
U12(f89_out1, T108, T111, T116) → f84_out1(T116)
f156_in(T208, T209, T212) → U13(f160_in(T208, T209), T208, T209, T212)
U13(f160_out1, T208, T209, T212) → U14(f89_in(T208, T212), T208, T209, T212)
U14(f89_out1, T208, T209, T212) → f156_out1
f199_in(T246, T245, T249) → U15(f160_in(T246, T245), T246, T245, T249)
U15(f160_out1, T246, T245, T249) → U16(f89_in(T245, T249), T246, T245, T249)
U16(f89_out1, T246, T245, T249) → f199_out1
f214_in(T270, T273) → U17(f218_in(T270), T270, T273)
U17(f218_out1, T270, T273) → U18(f3_in(T273), T270, T273)
U18(f3_out1, T270, T273) → f214_out1

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(13) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F160_IN(s(T227), s(T228)) → F160_IN(T227, T228)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• F160_IN(s(T227), s(T228)) → F160_IN(T227, T228)
  The graph contains the following edges 1 > 1, 2 > 2

(16) YES

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F88_IN(s(T130)) → F88_IN(T130)

The TRS R consists of the following rules:

f3_in(T13) → f3_out1
f3_in(tree(T47, T45, T48)) → U1(f51_in(T47, T48), tree(T47, T45, T48))
U1(f51_out1, tree(T47, T45, T48)) → f3_out1
f3_in(tree(T108, T111, T110)) → U2(f84_in(T108, T111), tree(T108, T111, T110))
U2(f84_out1(T112), tree(T108, T111, T110)) → f3_out1
f3_in(tree(T270, T271, T273)) → U3(f214_in(T270, T273), tree(T270, T271, T273))
U3(f214_out1, tree(T270, T271, T273)) → f3_out1
f51_in(T62, T63) → f51_out1
f51_in(T79, tree(T76, T80, T81)) → U4(f51_in(T79, T80), T79, tree(T76, T80, T81))
U4(f51_out1, T79, tree(T76, T80, T81)) → f51_out1
f88_in(s(T124)) → f88_out1(0)
f88_in(s(T130)) → U5(f88_in(T130), s(T130))
U5(f88_out1(T131), s(T130)) → f88_out1(s(T131))
f89_in(T146, T147) → f89_out1
f89_in(T178, tree(T181, T179, T182)) → U6(f51_in(T181, T182), T178, tree(T181, T179, T182))
U6(f51_out1, T178, tree(T181, T179, T182)) → f89_out1
f89_in(T208, tree(T209, T212, T211)) → U7(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
U7(f156_out1, T208, tree(T209, T212, T211)) → f89_out1
f89_in(T245, tree(T246, T247, T249)) → U8(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
U8(f199_out1, T245, tree(T246, T247, T249)) → f89_out1
f160_in(0, s(T222)) → f160_out1
f160_in(s(T227), s(T228)) → U9(f160_in(T227, T228), s(T227), s(T228))
U9(f160_out1, s(T227), s(T228)) → f160_out1
f218_in(0) → f218_out1
f218_in(s(T291)) → U10(f218_in(T291), s(T291))
U10(f218_out1, s(T291)) → f218_out1
f84_in(T108, T111) → U11(f88_in(T108), T108, T111)
U11(f88_out1(T116), T108, T111) → U12(f89_in(T116, T111), T108, T111, T116)
U12(f89_out1, T108, T111, T116) → f84_out1(T116)
f156_in(T208, T209, T212) → U13(f160_in(T208, T209), T208, T209, T212)
U13(f160_out1, T208, T209, T212) → U14(f89_in(T208, T212), T208, T209, T212)
U14(f89_out1, T208, T209, T212) → f156_out1
f199_in(T246, T245, T249) → U15(f160_in(T246, T245), T246, T245, T249)
U15(f160_out1, T246, T245, T249) → U16(f89_in(T245, T249), T246, T245, T249)
U16(f89_out1, T246, T245, T249) → f199_out1
f214_in(T270, T273) → U17(f218_in(T270), T270, T273)
U17(f218_out1, T270, T273) → U18(f3_in(T273), T270, T273)
U18(f3_out1, T270, T273) → f214_out1

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F88_IN(s(T130)) → F88_IN(T130)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(20) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• F88_IN(s(T130)) → F88_IN(T130)
  The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F51_IN(T79, tree(T76, T80, T81)) → F51_IN(T79, T80)

The TRS R consists of the following rules:

f3_in(T13) → f3_out1
f3_in(tree(T47, T45, T48)) → U1(f51_in(T47, T48), tree(T47, T45, T48))
U1(f51_out1, tree(T47, T45, T48)) → f3_out1
f3_in(tree(T108, T111, T110)) → U2(f84_in(T108, T111), tree(T108, T111, T110))
U2(f84_out1(T112), tree(T108, T111, T110)) → f3_out1
f3_in(tree(T270, T271, T273)) → U3(f214_in(T270, T273), tree(T270, T271, T273))
U3(f214_out1, tree(T270, T271, T273)) → f3_out1
f51_in(T62, T63) → f51_out1
f51_in(T79, tree(T76, T80, T81)) → U4(f51_in(T79, T80), T79, tree(T76, T80, T81))
U4(f51_out1, T79, tree(T76, T80, T81)) → f51_out1
f88_in(s(T124)) → f88_out1(0)
f88_in(s(T130)) → U5(f88_in(T130), s(T130))
U5(f88_out1(T131), s(T130)) → f88_out1(s(T131))
f89_in(T146, T147) → f89_out1
f89_in(T178, tree(T181, T179, T182)) → U6(f51_in(T181, T182), T178, tree(T181, T179, T182))
U6(f51_out1, T178, tree(T181, T179, T182)) → f89_out1
f89_in(T208, tree(T209, T212, T211)) → U7(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
U7(f156_out1, T208, tree(T209, T212, T211)) → f89_out1
f89_in(T245, tree(T246, T247, T249)) → U8(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
U8(f199_out1, T245, tree(T246, T247, T249)) → f89_out1
f160_in(0, s(T222)) → f160_out1
f160_in(s(T227), s(T228)) → U9(f160_in(T227, T228), s(T227), s(T228))
U9(f160_out1, s(T227), s(T228)) → f160_out1
f218_in(0) → f218_out1
f218_in(s(T291)) → U10(f218_in(T291), s(T291))
U10(f218_out1, s(T291)) → f218_out1
f84_in(T108, T111) → U11(f88_in(T108), T108, T111)
U11(f88_out1(T116), T108, T111) → U12(f89_in(T116, T111), T108, T111, T116)
U12(f89_out1, T108, T111, T116) → f84_out1(T116)
f156_in(T208, T209, T212) → U13(f160_in(T208, T209), T208, T209, T212)
U13(f160_out1, T208, T209, T212) → U14(f89_in(T208, T212), T208, T209, T212)
U14(f89_out1, T208, T209, T212) → f156_out1
f199_in(T246, T245, T249) → U15(f160_in(T246, T245), T246, T245, T249)
U15(f160_out1, T246, T245, T249) → U16(f89_in(T245, T249), T246, T245, T249)
U16(f89_out1, T246, T245, T249) → f199_out1
f214_in(T270, T273) → U17(f218_in(T270), T270, T273)
U17(f218_out1, T270, T273) → U18(f3_in(T273), T270, T273)
U18(f3_out1, T270, T273) → f214_out1

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F51_IN(T79, tree(T76, T80, T81)) → F51_IN(T79, T80)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• F51_IN(T79, tree(T76, T80, T81)) → F51_IN(T79, T80)
  The graph contains the following edges 1 >= 1, 2 > 2

(26) YES

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F89_IN(T208, tree(T209, T212, T211)) → F156_IN(T208, T209, T212)
F156_IN(T208, T209, T212) → U13¹(f160_in(T208, T209), T208, T209, T212)
U13¹(f160_out1, T208, T209, T212) → F89_IN(T208, T212)
F89_IN(T245, tree(T246, T247, T249)) → F199_IN(T246, T245, T249)
F199_IN(T246, T245, T249) → U15¹(f160_in(T246, T245), T246, T245, T249)
U15¹(f160_out1, T246, T245, T249) → F89_IN(T245, T249)

The TRS R consists of the following rules:

f3_in(T13) → f3_out1
f3_in(tree(T47, T45, T48)) → U1(f51_in(T47, T48), tree(T47, T45, T48))
U1(f51_out1, tree(T47, T45, T48)) → f3_out1
f3_in(tree(T108, T111, T110)) → U2(f84_in(T108, T111), tree(T108, T111, T110))
U2(f84_out1(T112), tree(T108, T111, T110)) → f3_out1
f3_in(tree(T270, T271, T273)) → U3(f214_in(T270, T273), tree(T270, T271, T273))
U3(f214_out1, tree(T270, T271, T273)) → f3_out1
f51_in(T62, T63) → f51_out1
f51_in(T79, tree(T76, T80, T81)) → U4(f51_in(T79, T80), T79, tree(T76, T80, T81))
U4(f51_out1, T79, tree(T76, T80, T81)) → f51_out1
f88_in(s(T124)) → f88_out1(0)
f88_in(s(T130)) → U5(f88_in(T130), s(T130))
U5(f88_out1(T131), s(T130)) → f88_out1(s(T131))
f89_in(T146, T147) → f89_out1
f89_in(T178, tree(T181, T179, T182)) → U6(f51_in(T181, T182), T178, tree(T181, T179, T182))
U6(f51_out1, T178, tree(T181, T179, T182)) → f89_out1
f89_in(T208, tree(T209, T212, T211)) → U7(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
U7(f156_out1, T208, tree(T209, T212, T211)) → f89_out1
f89_in(T245, tree(T246, T247, T249)) → U8(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
U8(f199_out1, T245, tree(T246, T247, T249)) → f89_out1
f160_in(0, s(T222)) → f160_out1
f160_in(s(T227), s(T228)) → U9(f160_in(T227, T228), s(T227), s(T228))
U9(f160_out1, s(T227), s(T228)) → f160_out1
f218_in(0) → f218_out1
f218_in(s(T291)) → U10(f218_in(T291), s(T291))
U10(f218_out1, s(T291)) → f218_out1
f84_in(T108, T111) → U11(f88_in(T108), T108, T111)
U11(f88_out1(T116), T108, T111) → U12(f89_in(T116, T111), T108, T111, T116)
U12(f89_out1, T108, T111, T116) → f84_out1(T116)
f156_in(T208, T209, T212) → U13(f160_in(T208, T209), T208, T209, T212)
U13(f160_out1, T208, T209, T212) → U14(f89_in(T208, T212), T208, T209, T212)
U14(f89_out1, T208, T209, T212) → f156_out1
f199_in(T246, T245, T249) → U15(f160_in(T246, T245), T246, T245, T249)
U15(f160_out1, T246, T245, T249) → U16(f89_in(T245, T249), T246, T245, T249)
U16(f89_out1, T246, T245, T249) → f199_out1
f214_in(T270, T273) → U17(f218_in(T270), T270, T273)
U17(f218_out1, T270, T273) → U18(f3_in(T273), T270, T273)
U18(f3_out1, T270, T273) → f214_out1

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• F156_IN(T208, T209, T212) → U13¹(f160_in(T208, T209), T208, T209, T212)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

• U13¹(f160_out1, T208, T209, T212) → F89_IN(T208, T212)
  The graph contains the following edges 2 >= 1, 4 >= 2

• U15¹(f160_out1, T246, T245, T249) → F89_IN(T245, T249)
  The graph contains the following edges 3 >= 1, 4 >= 2

• F89_IN(T208, tree(T209, T212, T211)) → F156_IN(T208, T209, T212)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

• F89_IN(T245, tree(T246, T247, T249)) → F199_IN(T246, T245, T249)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• F199_IN(T246, T245, T249) → U15¹(f160_in(T246, T245), T246, T245, T249)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

(29) YES

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F3_IN(tree(T270, T271, T273)) → F214_IN(T270, T273)
F214_IN(T270, T273) → U17¹(f218_in(T270), T270, T273)
U17¹(f218_out1, T270, T273) → F3_IN(T273)

The TRS R consists of the following rules:

f3_in(T13) → f3_out1
f3_in(tree(T47, T45, T48)) → U1(f51_in(T47, T48), tree(T47, T45, T48))
U1(f51_out1, tree(T47, T45, T48)) → f3_out1
f3_in(tree(T108, T111, T110)) → U2(f84_in(T108, T111), tree(T108, T111, T110))
U2(f84_out1(T112), tree(T108, T111, T110)) → f3_out1
f3_in(tree(T270, T271, T273)) → U3(f214_in(T270, T273), tree(T270, T271, T273))
U3(f214_out1, tree(T270, T271, T273)) → f3_out1
f51_in(T62, T63) → f51_out1
f51_in(T79, tree(T76, T80, T81)) → U4(f51_in(T79, T80), T79, tree(T76, T80, T81))
U4(f51_out1, T79, tree(T76, T80, T81)) → f51_out1
f88_in(s(T124)) → f88_out1(0)
f88_in(s(T130)) → U5(f88_in(T130), s(T130))
U5(f88_out1(T131), s(T130)) → f88_out1(s(T131))
f89_in(T146, T147) → f89_out1
f89_in(T178, tree(T181, T179, T182)) → U6(f51_in(T181, T182), T178, tree(T181, T179, T182))
U6(f51_out1, T178, tree(T181, T179, T182)) → f89_out1
f89_in(T208, tree(T209, T212, T211)) → U7(f156_in(T208, T209, T212), T208, tree(T209, T212, T211))
U7(f156_out1, T208, tree(T209, T212, T211)) → f89_out1
f89_in(T245, tree(T246, T247, T249)) → U8(f199_in(T246, T245, T249), T245, tree(T246, T247, T249))
U8(f199_out1, T245, tree(T246, T247, T249)) → f89_out1
f160_in(0, s(T222)) → f160_out1
f160_in(s(T227), s(T228)) → U9(f160_in(T227, T228), s(T227), s(T228))
U9(f160_out1, s(T227), s(T228)) → f160_out1
f218_in(0) → f218_out1
f218_in(s(T291)) → U10(f218_in(T291), s(T291))
U10(f218_out1, s(T291)) → f218_out1
f84_in(T108, T111) → U11(f88_in(T108), T108, T111)
U11(f88_out1(T116), T108, T111) → U12(f89_in(T116, T111), T108, T111, T116)
U12(f89_out1, T108, T111, T116) → f84_out1(T116)
f156_in(T208, T209, T212) → U13(f160_in(T208, T209), T208, T209, T212)
U13(f160_out1, T208, T209, T212) → U14(f89_in(T208, T212), T208, T209, T212)
U14(f89_out1, T208, T209, T212) → f156_out1
f199_in(T246, T245, T249) → U15(f160_in(T246, T245), T246, T245, T249)
U15(f160_out1, T246, T245, T249) → U16(f89_in(T245, T249), T246, T245, T249)
U16(f89_out1, T246, T245, T249) → f199_out1
f214_in(T270, T273) → U17(f218_in(T270), T270, T273)
U17(f218_out1, T270, T273) → U18(f3_in(T273), T270, T273)
U18(f3_out1, T270, T273) → f214_out1

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(31) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• F214_IN(T270, T273) → U17¹(f218_in(T270), T270, T273)
  The graph contains the following edges 1 >= 2, 2 >= 3

• U17¹(f218_out1, T270, T273) → F3_IN(T273)
  The graph contains the following edges 3 >= 1

• F3_IN(tree(T270, T271, T273)) → F214_IN(T270, T273)
  The graph contains the following edges 1 > 1, 1 > 2

(32) YES