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

(0) Obligation:

Clauses:

insert(X, void, tree(X, void, void)).
insert(X, tree(X, Left, Right), tree(X, Left, Right)).
insert(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), insert(X, Left, Left1)).
insert(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), insert(X, Right, Right1)).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Query: insert(a,a,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: insert(T1, T2, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\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];
34 [label="34: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(less(T49, T45), insert(T49, T50, T48))\n\nT45 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: less(T49, T45)\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: insert(T53, T54, T48)\n\nT48 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: less(T49, T45), SCOPE: 2, CLAUSE: 4 | less(T49, T45), SCOPE: 2, CLAUSE: 5\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: less(T49, T45), SCOPE: 2, CLAUSE: 4\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: less(T49, T45), SCOPE: 2, CLAUSE: 5\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: less(T68, T67)\n\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: insert(T53, T54, T48), SCOPE: 3, CLAUSE: 0 | insert(T53, T54, T48), SCOPE: 3, CLAUSE: 1 | insert(T53, T54, T48), SCOPE: 3, CLAUSE: 2 | insert(T53, T54, T48), SCOPE: 3, CLAUSE: 3\n\nT48 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: insert(T53, T54, T48), SCOPE: 3, CLAUSE: 0\n\nT48 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: insert(T53, T54, T48), SCOPE: 3, CLAUSE: 1 | insert(T53, T54, T48), SCOPE: 3, CLAUSE: 2 | insert(T53, T54, T48), SCOPE: 3, CLAUSE: 3\n\nT48 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: insert(T53, T54, T48), SCOPE: 3, CLAUSE: 1\n\nT48 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: insert(T53, T54, T48), SCOPE: 3, CLAUSE: 2 | insert(T53, T54, T48), SCOPE: 3, CLAUSE: 3\n\nT48 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: 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];
120 [label="120: insert(T53, T54, T48), SCOPE: 3, CLAUSE: 2\n\nT48 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: insert(T53, T54, T48), SCOPE: 3, CLAUSE: 3\n\nT48 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(less(T113, T114), insert(T113, T118, T117))\n\nT113 is ground\nT114 is ground\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: less(T113, T114)\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: insert(T113, T118, T117)\n\nT113 is ground\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: less(T113, T114), SCOPE: 4, CLAUSE: 4 | less(T113, T114), SCOPE: 4, CLAUSE: 5\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: less(T113, T114), SCOPE: 4, CLAUSE: 4\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: less(T113, T114), SCOPE: 4, CLAUSE: 5\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: less(T132, T133)\n\nT132 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(less(T149, T148), insert(T148, T153, T152))\n\nT148 is ground\nT149 is ground\nT152 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: less(T149, T148)\n\nT148 is ground\nT149 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: insert(T148, T153, T152)\n\nT148 is ground\nT152 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(less(T171, T175), insert(T175, T176, T174))\n\nT171 is ground\nT174 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: less(T171, T175)\n\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: insert(T179, T180, T174)\n\nT174 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: less(T171, T175), SCOPE: 5, CLAUSE: 4 | less(T171, T175), SCOPE: 5, CLAUSE: 5\n\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: less(T171, T175), SCOPE: 5, CLAUSE: 4\n\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: less(T171, T175), SCOPE: 5, CLAUSE: 5\n\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: less(T192, T194)\n\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 203 [arrowhead = none ];
203 -> 6;

204 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 204 [arrowhead = none ];
204 -> 7;

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

206 [label="EVAL with clause\ninsert(X6, void, tree(X6, void, void)).\nand substitutionT1 -> T8,\nX6 -> T8,\nT2 -> void,\nT3 -> tree(T8, void, void)", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 206 [arrowhead = none ];
206 -> 11;

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

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

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

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

211 [label="EVAL with clause\ninsert(X19, tree(X19, X20, X21), tree(X19, X20, X21)).\nand substitutionT1 -> T21,\nX19 -> T21,\nX20 -> T22,\nX21 -> T23,\nT2 -> tree(T21, T22, T23),\nT3 -> tree(T21, T22, T23)", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 211 [arrowhead = none ];
211 -> 26;

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

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

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

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

216 [label="EVAL with clause\ninsert(X42, tree(X43, X44, X45), tree(X43, X46, X45)) :- ','(less(X42, X43), insert(X42, X44, X46)).\nand substitutionT1 -> T49,\nX42 -> T49,\nX43 -> T45,\nX44 -> T50,\nX45 -> T47,\nT2 -> tree(T45, T50, T47),\nX46 -> T48,\nT3 -> tree(T45, T48, T47),\nT44 -> T49,\nT46 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 216 [arrowhead = none ];
216 -> 49;

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

218 [label="EVAL with clause\ninsert(X161, tree(X162, X163, X164), tree(X162, X163, X165)) :- ','(less(X162, X161), insert(X161, X164, X165)).\nand substitutionT1 -> T175,\nX161 -> T175,\nX162 -> T171,\nX163 -> T172,\nX164 -> T176,\nT2 -> tree(T171, T172, T176),\nX165 -> T174,\nT3 -> tree(T171, T172, T174),\nT170 -> T175,\nT173 -> T176", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 218 [arrowhead = none ];
218 -> 185;

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

220 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
49 -> 220 [arrowhead = none ];
220 -> 54;

221 [label="SPLIT 2\nnew knowledge:\nT53 is ground\nT45 is ground\nreplacements:T49 -> T53,\nT50 -> T54", fontsize=14, style = filled, fillcolor = violet];
49 -> 221 [arrowhead = none ];
221 -> 56;

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

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

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
71 -> 224 [arrowhead = none ];
224 -> 73;

225 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
71 -> 225 [arrowhead = none ];
225 -> 74;

226 [label="EVAL with clause\nless(0, s(X55)).\nand substitutionT49 -> 0,\nX55 -> T61,\nT45 -> s(T61)", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 226 [arrowhead = none ];
226 -> 80;

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

228 [label="EVAL with clause\nless(s(X60), s(X61)) :- less(X60, X61).\nand substitutionX60 -> T68,\nT49 -> s(T68),\nX61 -> T67,\nT45 -> s(T67),\nT66 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 228 [arrowhead = none ];
228 -> 89;

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

230 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 230 [arrowhead = none ];
230 -> 83;

231 [label="INSTANCE with matching:\nT49 -> T68\nT45 -> T67", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 231 [arrowhead = none , style=dashed];
231 -> 54[style=dashed];

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

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

234 [label="EVAL with clause\ninsert(X70, void, tree(X70, void, void)).\nand substitutionT53 -> T77,\nX70 -> T77,\nT54 -> void,\nT48 -> tree(T77, void, void)", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 234 [arrowhead = none ];
234 -> 101;

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

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

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

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

239 [label="EVAL with clause\ninsert(X83, tree(X83, X84, X85), tree(X83, X84, X85)).\nand substitutionT53 -> T90,\nX83 -> T90,\nX84 -> T91,\nX85 -> T92,\nT54 -> tree(T90, T91, T92),\nT48 -> tree(T90, T91, T92)", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 239 [arrowhead = none ];
239 -> 113;

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

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

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

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

244 [label="EVAL with clause\ninsert(X106, tree(X107, X108, X109), tree(X107, X110, X109)) :- ','(less(X106, X107), insert(X106, X108, X110)).\nand substitutionT53 -> T113,\nX106 -> T113,\nX107 -> T114,\nX108 -> T118,\nX109 -> T116,\nT54 -> tree(T114, T118, T116),\nX110 -> T117,\nT48 -> tree(T114, T117, T116),\nT115 -> T118", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 244 [arrowhead = none ];
244 -> 125;

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

246 [label="EVAL with clause\ninsert(X140, tree(X141, X142, X143), tree(X141, X142, X144)) :- ','(less(X141, X140), insert(X140, X143, X144)).\nand substitutionT53 -> T148,\nX140 -> T148,\nX141 -> T149,\nX142 -> T150,\nX143 -> T153,\nT54 -> tree(T149, T150, T153),\nX144 -> T152,\nT48 -> tree(T149, T150, T152),\nT151 -> T153", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 246 [arrowhead = none ];
246 -> 167;

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

248 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
125 -> 248 [arrowhead = none ];
248 -> 141;

249 [label="SPLIT 2\nnew knowledge:\nT113 is ground\nT114 is ground", fontsize=14, style = filled, fillcolor = violet];
125 -> 249 [arrowhead = none ];
249 -> 142;

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

251 [label="INSTANCE with matching:\nT53 -> T113\nT54 -> T118\nT48 -> T117", fontsize=14, style = filled, fillcolor = lightgrey];
142 -> 251 [arrowhead = none , style=dashed];
251 -> 56[style=dashed];

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

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

254 [label="EVAL with clause\nless(0, s(X119)).\nand substitutionT113 -> 0,\nX119 -> T127,\nT114 -> s(T127)", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 254 [arrowhead = none ];
254 -> 149;

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

256 [label="EVAL with clause\nless(s(X124), s(X125)) :- less(X124, X125).\nand substitutionX124 -> T132,\nT113 -> s(T132),\nX125 -> T133,\nT114 -> s(T133)", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 256 [arrowhead = none ];
256 -> 154;

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

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

259 [label="INSTANCE with matching:\nT113 -> T132\nT114 -> T133", fontsize=14, style = filled, fillcolor = lightgrey];
154 -> 259 [arrowhead = none , style=dashed];
259 -> 141[style=dashed];

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

261 [label="SPLIT 2\nnew knowledge:\nT149 is ground\nT148 is ground", fontsize=14, style = filled, fillcolor = violet];
167 -> 261 [arrowhead = none ];
261 -> 170;

262 [label="INSTANCE with matching:\nT113 -> T149\nT114 -> T148", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 262 [arrowhead = none , style=dashed];
262 -> 141[style=dashed];

263 [label="INSTANCE with matching:\nT53 -> T148\nT54 -> T153\nT48 -> T152", fontsize=14, style = filled, fillcolor = lightgrey];
170 -> 263 [arrowhead = none , style=dashed];
263 -> 56[style=dashed];

264 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
185 -> 264 [arrowhead = none ];
264 -> 189;

265 [label="SPLIT 2\nnew knowledge:\nT171 is ground\nreplacements:T175 -> T179,\nT176 -> T180", fontsize=14, style = filled, fillcolor = violet];
185 -> 265 [arrowhead = none ];
265 -> 190;

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

267 [label="INSTANCE with matching:\nT1 -> T179\nT2 -> T180\nT3 -> T174", fontsize=14, style = filled, fillcolor = lightgrey];
190 -> 267 [arrowhead = none , style=dashed];
267 -> 1[style=dashed];

268 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
193 -> 268 [arrowhead = none ];
268 -> 195;

269 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
193 -> 269 [arrowhead = none ];
269 -> 196;

270 [label="EVAL with clause\nless(0, s(X174)).\nand substitutionT171 -> 0,\nX174 -> T187,\nT175 -> s(T187)", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 270 [arrowhead = none ];
270 -> 197;

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

272 [label="EVAL with clause\nless(s(X179), s(X180)) :- less(X179, X180).\nand substitutionX179 -> T192,\nT171 -> s(T192),\nX180 -> T194,\nT175 -> s(T194),\nT193 -> T194", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 272 [arrowhead = none ];
272 -> 201;

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

274 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 274 [arrowhead = none ];
274 -> 199;

275 [label="INSTANCE with matching:\nT171 -> T192\nT175 -> T194", fontsize=14, style = filled, fillcolor = lightgrey];
201 -> 275 [arrowhead = none , style=dashed];
275 -> 189[style=dashed];

}

(2) Obligation:

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

f1_in(tree(T8, void, void)) → f1_out1(T8, void)
f1_in(tree(T21, T22, T23)) → f1_out1(T21, tree(T21, T22, T23))
f1_in(tree(T45, T48, T47)) → U1(f49_in(T45, T48), tree(T45, T48, T47))
U1(f49_out1(T49, T50), tree(T45, T48, T47)) → f1_out1(T49, tree(T45, T50, T47))
f1_in(tree(T171, T172, T174)) → U2(f185_in(T171, T174), tree(T171, T172, T174))
U2(f185_out1(T175, T176), tree(T171, T172, T174)) → f1_out1(T175, tree(T171, T172, T176))
f54_in(s(T61)) → f54_out1(0)
f54_in(s(T67)) → U3(f54_in(T67), s(T67))
U3(f54_out1(T68), s(T67)) → f54_out1(s(T68))
f56_in(T77, tree(T77, void, void)) → f56_out1(void)
f56_in(T90, tree(T90, T91, T92)) → f56_out1(tree(T90, T91, T92))
f56_in(T113, tree(T114, T117, T116)) → U4(f125_in(T113, T114, T117), T113, tree(T114, T117, T116))
U4(f125_out1(T118), T113, tree(T114, T117, T116)) → f56_out1(tree(T114, T118, T116))
f56_in(T148, tree(T149, T150, T152)) → U5(f167_in(T149, T148, T152), T148, tree(T149, T150, T152))
U5(f167_out1(T153), T148, tree(T149, T150, T152)) → f56_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f189_in(0) → f189_out1
f189_in(s(T192)) → U7(f189_in(T192), s(T192))
U7(f189_out1, s(T192)) → f189_out1
f49_in(T45, T48) → U8(f54_in(T45), T45, T48)
U8(f54_out1(T53), T45, T48) → U9(f56_in(T53, T48), T45, T48, T53)
U9(f56_out1(T54), T45, T48, T53) → f49_out1(T53, T54)
f125_in(T113, T114, T117) → U10(f141_in(T113, T114), T113, T114, T117)
U10(f141_out1, T113, T114, T117) → U11(f56_in(T113, T117), T113, T114, T117)
U11(f56_out1(T118), T113, T114, T117) → f125_out1(T118)
f167_in(T149, T148, T152) → U12(f141_in(T149, T148), T149, T148, T152)
U12(f141_out1, T149, T148, T152) → U13(f56_in(T148, T152), T149, T148, T152)
U13(f56_out1(T153), T149, T148, T152) → f167_out1(T153)
f185_in(T171, T174) → U14(f189_in(T171), T171, T174)
U14(f189_out1, T171, T174) → U15(f1_in(T174), T171, T174)
U15(f1_out1(T179, T180), T171, T174) → f185_out1(T179, T180)

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:

F1_IN(tree(T45, T48, T47)) → U1¹(f49_in(T45, T48), tree(T45, T48, T47))
F1_IN(tree(T45, T48, T47)) → F49_IN(T45, T48)
F1_IN(tree(T171, T172, T174)) → U2¹(f185_in(T171, T174), tree(T171, T172, T174))
F1_IN(tree(T171, T172, T174)) → F185_IN(T171, T174)
F54_IN(s(T67)) → U3¹(f54_in(T67), s(T67))
F54_IN(s(T67)) → F54_IN(T67)
F56_IN(T113, tree(T114, T117, T116)) → U4¹(f125_in(T113, T114, T117), T113, tree(T114, T117, T116))
F56_IN(T113, tree(T114, T117, T116)) → F125_IN(T113, T114, T117)
F56_IN(T148, tree(T149, T150, T152)) → U5¹(f167_in(T149, T148, T152), T148, tree(T149, T150, T152))
F56_IN(T148, tree(T149, T150, T152)) → F167_IN(T149, T148, T152)
F141_IN(s(T132), s(T133)) → U6¹(f141_in(T132, T133), s(T132), s(T133))
F141_IN(s(T132), s(T133)) → F141_IN(T132, T133)
F189_IN(s(T192)) → U7¹(f189_in(T192), s(T192))
F189_IN(s(T192)) → F189_IN(T192)
F49_IN(T45, T48) → U8¹(f54_in(T45), T45, T48)
F49_IN(T45, T48) → F54_IN(T45)
U8¹(f54_out1(T53), T45, T48) → U9¹(f56_in(T53, T48), T45, T48, T53)
U8¹(f54_out1(T53), T45, T48) → F56_IN(T53, T48)
F125_IN(T113, T114, T117) → U10¹(f141_in(T113, T114), T113, T114, T117)
F125_IN(T113, T114, T117) → F141_IN(T113, T114)
U10¹(f141_out1, T113, T114, T117) → U11¹(f56_in(T113, T117), T113, T114, T117)
U10¹(f141_out1, T113, T114, T117) → F56_IN(T113, T117)
F167_IN(T149, T148, T152) → U12¹(f141_in(T149, T148), T149, T148, T152)
F167_IN(T149, T148, T152) → F141_IN(T149, T148)
U12¹(f141_out1, T149, T148, T152) → U13¹(f56_in(T148, T152), T149, T148, T152)
U12¹(f141_out1, T149, T148, T152) → F56_IN(T148, T152)
F185_IN(T171, T174) → U14¹(f189_in(T171), T171, T174)
F185_IN(T171, T174) → F189_IN(T171)
U14¹(f189_out1, T171, T174) → U15¹(f1_in(T174), T171, T174)
U14¹(f189_out1, T171, T174) → F1_IN(T174)

The TRS R consists of the following rules:

f1_in(tree(T8, void, void)) → f1_out1(T8, void)
f1_in(tree(T21, T22, T23)) → f1_out1(T21, tree(T21, T22, T23))
f1_in(tree(T45, T48, T47)) → U1(f49_in(T45, T48), tree(T45, T48, T47))
U1(f49_out1(T49, T50), tree(T45, T48, T47)) → f1_out1(T49, tree(T45, T50, T47))
f1_in(tree(T171, T172, T174)) → U2(f185_in(T171, T174), tree(T171, T172, T174))
U2(f185_out1(T175, T176), tree(T171, T172, T174)) → f1_out1(T175, tree(T171, T172, T176))
f54_in(s(T61)) → f54_out1(0)
f54_in(s(T67)) → U3(f54_in(T67), s(T67))
U3(f54_out1(T68), s(T67)) → f54_out1(s(T68))
f56_in(T77, tree(T77, void, void)) → f56_out1(void)
f56_in(T90, tree(T90, T91, T92)) → f56_out1(tree(T90, T91, T92))
f56_in(T113, tree(T114, T117, T116)) → U4(f125_in(T113, T114, T117), T113, tree(T114, T117, T116))
U4(f125_out1(T118), T113, tree(T114, T117, T116)) → f56_out1(tree(T114, T118, T116))
f56_in(T148, tree(T149, T150, T152)) → U5(f167_in(T149, T148, T152), T148, tree(T149, T150, T152))
U5(f167_out1(T153), T148, tree(T149, T150, T152)) → f56_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f189_in(0) → f189_out1
f189_in(s(T192)) → U7(f189_in(T192), s(T192))
U7(f189_out1, s(T192)) → f189_out1
f49_in(T45, T48) → U8(f54_in(T45), T45, T48)
U8(f54_out1(T53), T45, T48) → U9(f56_in(T53, T48), T45, T48, T53)
U9(f56_out1(T54), T45, T48, T53) → f49_out1(T53, T54)
f125_in(T113, T114, T117) → U10(f141_in(T113, T114), T113, T114, T117)
U10(f141_out1, T113, T114, T117) → U11(f56_in(T113, T117), T113, T114, T117)
U11(f56_out1(T118), T113, T114, T117) → f125_out1(T118)
f167_in(T149, T148, T152) → U12(f141_in(T149, T148), T149, T148, T152)
U12(f141_out1, T149, T148, T152) → U13(f56_in(T148, T152), T149, T148, T152)
U13(f56_out1(T153), T149, T148, T152) → f167_out1(T153)
f185_in(T171, T174) → U14(f189_in(T171), T171, T174)
U14(f189_out1, T171, T174) → U15(f1_in(T174), T171, T174)
U15(f1_out1(T179, T180), T171, T174) → f185_out1(T179, T180)

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 5 SCCs with 18 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

F189_IN(s(T192)) → F189_IN(T192)

The TRS R consists of the following rules:

f1_in(tree(T8, void, void)) → f1_out1(T8, void)
f1_in(tree(T21, T22, T23)) → f1_out1(T21, tree(T21, T22, T23))
f1_in(tree(T45, T48, T47)) → U1(f49_in(T45, T48), tree(T45, T48, T47))
U1(f49_out1(T49, T50), tree(T45, T48, T47)) → f1_out1(T49, tree(T45, T50, T47))
f1_in(tree(T171, T172, T174)) → U2(f185_in(T171, T174), tree(T171, T172, T174))
U2(f185_out1(T175, T176), tree(T171, T172, T174)) → f1_out1(T175, tree(T171, T172, T176))
f54_in(s(T61)) → f54_out1(0)
f54_in(s(T67)) → U3(f54_in(T67), s(T67))
U3(f54_out1(T68), s(T67)) → f54_out1(s(T68))
f56_in(T77, tree(T77, void, void)) → f56_out1(void)
f56_in(T90, tree(T90, T91, T92)) → f56_out1(tree(T90, T91, T92))
f56_in(T113, tree(T114, T117, T116)) → U4(f125_in(T113, T114, T117), T113, tree(T114, T117, T116))
U4(f125_out1(T118), T113, tree(T114, T117, T116)) → f56_out1(tree(T114, T118, T116))
f56_in(T148, tree(T149, T150, T152)) → U5(f167_in(T149, T148, T152), T148, tree(T149, T150, T152))
U5(f167_out1(T153), T148, tree(T149, T150, T152)) → f56_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f189_in(0) → f189_out1
f189_in(s(T192)) → U7(f189_in(T192), s(T192))
U7(f189_out1, s(T192)) → f189_out1
f49_in(T45, T48) → U8(f54_in(T45), T45, T48)
U8(f54_out1(T53), T45, T48) → U9(f56_in(T53, T48), T45, T48, T53)
U9(f56_out1(T54), T45, T48, T53) → f49_out1(T53, T54)
f125_in(T113, T114, T117) → U10(f141_in(T113, T114), T113, T114, T117)
U10(f141_out1, T113, T114, T117) → U11(f56_in(T113, T117), T113, T114, T117)
U11(f56_out1(T118), T113, T114, T117) → f125_out1(T118)
f167_in(T149, T148, T152) → U12(f141_in(T149, T148), T149, T148, T152)
U12(f141_out1, T149, T148, T152) → U13(f56_in(T148, T152), T149, T148, T152)
U13(f56_out1(T153), T149, T148, T152) → f167_out1(T153)
f185_in(T171, T174) → U14(f189_in(T171), T171, T174)
U14(f189_out1, T171, T174) → U15(f1_in(T174), T171, T174)
U15(f1_out1(T179, T180), T171, T174) → f185_out1(T179, T180)

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:

F189_IN(s(T192)) → F189_IN(T192)

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:

• F189_IN(s(T192)) → F189_IN(T192)
  The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

F141_IN(s(T132), s(T133)) → F141_IN(T132, T133)

The TRS R consists of the following rules:

f1_in(tree(T8, void, void)) → f1_out1(T8, void)
f1_in(tree(T21, T22, T23)) → f1_out1(T21, tree(T21, T22, T23))
f1_in(tree(T45, T48, T47)) → U1(f49_in(T45, T48), tree(T45, T48, T47))
U1(f49_out1(T49, T50), tree(T45, T48, T47)) → f1_out1(T49, tree(T45, T50, T47))
f1_in(tree(T171, T172, T174)) → U2(f185_in(T171, T174), tree(T171, T172, T174))
U2(f185_out1(T175, T176), tree(T171, T172, T174)) → f1_out1(T175, tree(T171, T172, T176))
f54_in(s(T61)) → f54_out1(0)
f54_in(s(T67)) → U3(f54_in(T67), s(T67))
U3(f54_out1(T68), s(T67)) → f54_out1(s(T68))
f56_in(T77, tree(T77, void, void)) → f56_out1(void)
f56_in(T90, tree(T90, T91, T92)) → f56_out1(tree(T90, T91, T92))
f56_in(T113, tree(T114, T117, T116)) → U4(f125_in(T113, T114, T117), T113, tree(T114, T117, T116))
U4(f125_out1(T118), T113, tree(T114, T117, T116)) → f56_out1(tree(T114, T118, T116))
f56_in(T148, tree(T149, T150, T152)) → U5(f167_in(T149, T148, T152), T148, tree(T149, T150, T152))
U5(f167_out1(T153), T148, tree(T149, T150, T152)) → f56_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f189_in(0) → f189_out1
f189_in(s(T192)) → U7(f189_in(T192), s(T192))
U7(f189_out1, s(T192)) → f189_out1
f49_in(T45, T48) → U8(f54_in(T45), T45, T48)
U8(f54_out1(T53), T45, T48) → U9(f56_in(T53, T48), T45, T48, T53)
U9(f56_out1(T54), T45, T48, T53) → f49_out1(T53, T54)
f125_in(T113, T114, T117) → U10(f141_in(T113, T114), T113, T114, T117)
U10(f141_out1, T113, T114, T117) → U11(f56_in(T113, T117), T113, T114, T117)
U11(f56_out1(T118), T113, T114, T117) → f125_out1(T118)
f167_in(T149, T148, T152) → U12(f141_in(T149, T148), T149, T148, T152)
U12(f141_out1, T149, T148, T152) → U13(f56_in(T148, T152), T149, T148, T152)
U13(f56_out1(T153), T149, T148, T152) → f167_out1(T153)
f185_in(T171, T174) → U14(f189_in(T171), T171, T174)
U14(f189_out1, T171, T174) → U15(f1_in(T174), T171, T174)
U15(f1_out1(T179, T180), T171, T174) → f185_out1(T179, T180)

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:

F141_IN(s(T132), s(T133)) → F141_IN(T132, T133)

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:

• F141_IN(s(T132), s(T133)) → F141_IN(T132, T133)
  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:

F56_IN(T113, tree(T114, T117, T116)) → F125_IN(T113, T114, T117)
F125_IN(T113, T114, T117) → U10¹(f141_in(T113, T114), T113, T114, T117)
U10¹(f141_out1, T113, T114, T117) → F56_IN(T113, T117)
F56_IN(T148, tree(T149, T150, T152)) → F167_IN(T149, T148, T152)
F167_IN(T149, T148, T152) → U12¹(f141_in(T149, T148), T149, T148, T152)
U12¹(f141_out1, T149, T148, T152) → F56_IN(T148, T152)

The TRS R consists of the following rules:

f1_in(tree(T8, void, void)) → f1_out1(T8, void)
f1_in(tree(T21, T22, T23)) → f1_out1(T21, tree(T21, T22, T23))
f1_in(tree(T45, T48, T47)) → U1(f49_in(T45, T48), tree(T45, T48, T47))
U1(f49_out1(T49, T50), tree(T45, T48, T47)) → f1_out1(T49, tree(T45, T50, T47))
f1_in(tree(T171, T172, T174)) → U2(f185_in(T171, T174), tree(T171, T172, T174))
U2(f185_out1(T175, T176), tree(T171, T172, T174)) → f1_out1(T175, tree(T171, T172, T176))
f54_in(s(T61)) → f54_out1(0)
f54_in(s(T67)) → U3(f54_in(T67), s(T67))
U3(f54_out1(T68), s(T67)) → f54_out1(s(T68))
f56_in(T77, tree(T77, void, void)) → f56_out1(void)
f56_in(T90, tree(T90, T91, T92)) → f56_out1(tree(T90, T91, T92))
f56_in(T113, tree(T114, T117, T116)) → U4(f125_in(T113, T114, T117), T113, tree(T114, T117, T116))
U4(f125_out1(T118), T113, tree(T114, T117, T116)) → f56_out1(tree(T114, T118, T116))
f56_in(T148, tree(T149, T150, T152)) → U5(f167_in(T149, T148, T152), T148, tree(T149, T150, T152))
U5(f167_out1(T153), T148, tree(T149, T150, T152)) → f56_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f189_in(0) → f189_out1
f189_in(s(T192)) → U7(f189_in(T192), s(T192))
U7(f189_out1, s(T192)) → f189_out1
f49_in(T45, T48) → U8(f54_in(T45), T45, T48)
U8(f54_out1(T53), T45, T48) → U9(f56_in(T53, T48), T45, T48, T53)
U9(f56_out1(T54), T45, T48, T53) → f49_out1(T53, T54)
f125_in(T113, T114, T117) → U10(f141_in(T113, T114), T113, T114, T117)
U10(f141_out1, T113, T114, T117) → U11(f56_in(T113, T117), T113, T114, T117)
U11(f56_out1(T118), T113, T114, T117) → f125_out1(T118)
f167_in(T149, T148, T152) → U12(f141_in(T149, T148), T149, T148, T152)
U12(f141_out1, T149, T148, T152) → U13(f56_in(T148, T152), T149, T148, T152)
U13(f56_out1(T153), T149, T148, T152) → f167_out1(T153)
f185_in(T171, T174) → U14(f189_in(T171), T171, T174)
U14(f189_out1, T171, T174) → U15(f1_in(T174), T171, T174)
U15(f1_out1(T179, T180), T171, T174) → f185_out1(T179, T180)

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

(18) 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:

• F125_IN(T113, T114, T117) → U10¹(f141_in(T113, T114), T113, T114, T117)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

• U10¹(f141_out1, T113, T114, T117) → F56_IN(T113, T117)
  The graph contains the following edges 2 >= 1, 4 >= 2

• U12¹(f141_out1, T149, T148, T152) → F56_IN(T148, T152)
  The graph contains the following edges 3 >= 1, 4 >= 2

• F56_IN(T113, tree(T114, T117, T116)) → F125_IN(T113, T114, T117)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

• F56_IN(T148, tree(T149, T150, T152)) → F167_IN(T149, T148, T152)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• F167_IN(T149, T148, T152) → U12¹(f141_in(T149, T148), T149, T148, T152)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

(19) YES

(20) Obligation:

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

F54_IN(s(T67)) → F54_IN(T67)

The TRS R consists of the following rules:

f1_in(tree(T8, void, void)) → f1_out1(T8, void)
f1_in(tree(T21, T22, T23)) → f1_out1(T21, tree(T21, T22, T23))
f1_in(tree(T45, T48, T47)) → U1(f49_in(T45, T48), tree(T45, T48, T47))
U1(f49_out1(T49, T50), tree(T45, T48, T47)) → f1_out1(T49, tree(T45, T50, T47))
f1_in(tree(T171, T172, T174)) → U2(f185_in(T171, T174), tree(T171, T172, T174))
U2(f185_out1(T175, T176), tree(T171, T172, T174)) → f1_out1(T175, tree(T171, T172, T176))
f54_in(s(T61)) → f54_out1(0)
f54_in(s(T67)) → U3(f54_in(T67), s(T67))
U3(f54_out1(T68), s(T67)) → f54_out1(s(T68))
f56_in(T77, tree(T77, void, void)) → f56_out1(void)
f56_in(T90, tree(T90, T91, T92)) → f56_out1(tree(T90, T91, T92))
f56_in(T113, tree(T114, T117, T116)) → U4(f125_in(T113, T114, T117), T113, tree(T114, T117, T116))
U4(f125_out1(T118), T113, tree(T114, T117, T116)) → f56_out1(tree(T114, T118, T116))
f56_in(T148, tree(T149, T150, T152)) → U5(f167_in(T149, T148, T152), T148, tree(T149, T150, T152))
U5(f167_out1(T153), T148, tree(T149, T150, T152)) → f56_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f189_in(0) → f189_out1
f189_in(s(T192)) → U7(f189_in(T192), s(T192))
U7(f189_out1, s(T192)) → f189_out1
f49_in(T45, T48) → U8(f54_in(T45), T45, T48)
U8(f54_out1(T53), T45, T48) → U9(f56_in(T53, T48), T45, T48, T53)
U9(f56_out1(T54), T45, T48, T53) → f49_out1(T53, T54)
f125_in(T113, T114, T117) → U10(f141_in(T113, T114), T113, T114, T117)
U10(f141_out1, T113, T114, T117) → U11(f56_in(T113, T117), T113, T114, T117)
U11(f56_out1(T118), T113, T114, T117) → f125_out1(T118)
f167_in(T149, T148, T152) → U12(f141_in(T149, T148), T149, T148, T152)
U12(f141_out1, T149, T148, T152) → U13(f56_in(T148, T152), T149, T148, T152)
U13(f56_out1(T153), T149, T148, T152) → f167_out1(T153)
f185_in(T171, T174) → U14(f189_in(T171), T171, T174)
U14(f189_out1, T171, T174) → U15(f1_in(T174), T171, T174)
U15(f1_out1(T179, T180), T171, T174) → f185_out1(T179, T180)

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

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

(22) Obligation:

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

F54_IN(s(T67)) → F54_IN(T67)

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

(23) 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:

• F54_IN(s(T67)) → F54_IN(T67)
  The graph contains the following edges 1 > 1

(24) YES

(25) Obligation:

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

F1_IN(tree(T171, T172, T174)) → F185_IN(T171, T174)
F185_IN(T171, T174) → U14¹(f189_in(T171), T171, T174)
U14¹(f189_out1, T171, T174) → F1_IN(T174)

The TRS R consists of the following rules:

f1_in(tree(T8, void, void)) → f1_out1(T8, void)
f1_in(tree(T21, T22, T23)) → f1_out1(T21, tree(T21, T22, T23))
f1_in(tree(T45, T48, T47)) → U1(f49_in(T45, T48), tree(T45, T48, T47))
U1(f49_out1(T49, T50), tree(T45, T48, T47)) → f1_out1(T49, tree(T45, T50, T47))
f1_in(tree(T171, T172, T174)) → U2(f185_in(T171, T174), tree(T171, T172, T174))
U2(f185_out1(T175, T176), tree(T171, T172, T174)) → f1_out1(T175, tree(T171, T172, T176))
f54_in(s(T61)) → f54_out1(0)
f54_in(s(T67)) → U3(f54_in(T67), s(T67))
U3(f54_out1(T68), s(T67)) → f54_out1(s(T68))
f56_in(T77, tree(T77, void, void)) → f56_out1(void)
f56_in(T90, tree(T90, T91, T92)) → f56_out1(tree(T90, T91, T92))
f56_in(T113, tree(T114, T117, T116)) → U4(f125_in(T113, T114, T117), T113, tree(T114, T117, T116))
U4(f125_out1(T118), T113, tree(T114, T117, T116)) → f56_out1(tree(T114, T118, T116))
f56_in(T148, tree(T149, T150, T152)) → U5(f167_in(T149, T148, T152), T148, tree(T149, T150, T152))
U5(f167_out1(T153), T148, tree(T149, T150, T152)) → f56_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f189_in(0) → f189_out1
f189_in(s(T192)) → U7(f189_in(T192), s(T192))
U7(f189_out1, s(T192)) → f189_out1
f49_in(T45, T48) → U8(f54_in(T45), T45, T48)
U8(f54_out1(T53), T45, T48) → U9(f56_in(T53, T48), T45, T48, T53)
U9(f56_out1(T54), T45, T48, T53) → f49_out1(T53, T54)
f125_in(T113, T114, T117) → U10(f141_in(T113, T114), T113, T114, T117)
U10(f141_out1, T113, T114, T117) → U11(f56_in(T113, T117), T113, T114, T117)
U11(f56_out1(T118), T113, T114, T117) → f125_out1(T118)
f167_in(T149, T148, T152) → U12(f141_in(T149, T148), T149, T148, T152)
U12(f141_out1, T149, T148, T152) → U13(f56_in(T148, T152), T149, T148, T152)
U13(f56_out1(T153), T149, T148, T152) → f167_out1(T153)
f185_in(T171, T174) → U14(f189_in(T171), T171, T174)
U14(f189_out1, T171, T174) → U15(f1_in(T174), T171, T174)
U15(f1_out1(T179, T180), T171, T174) → f185_out1(T179, T180)

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

(26) 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:

• F185_IN(T171, T174) → U14¹(f189_in(T171), T171, T174)
  The graph contains the following edges 1 >= 2, 2 >= 3

• U14¹(f189_out1, T171, T174) → F1_IN(T174)
  The graph contains the following edges 3 >= 1

• F1_IN(tree(T171, T172, T174)) → F185_IN(T171, T174)
  The graph contains the following edges 1 > 1, 1 > 2

(27) YES