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

(0) Obligation:

Clauses:

goal(X) :- ','(s2l(X, Xs), conf(Xs)).
conf(X) :- ','(del2(X, Z), ','(del(U, Y, Z), conf(Y))).
del2(X, Y) :- ','(del(U, X, Z), del(V, Z, Y)).
del(X1, [], X2) :- ','(!, failure(a)).
del(H, X, T) :- ','(head(X, H), tail(X, T)).
del(X, Y, .(H, T2)) :- ','(head(Y, H), ','(tail(Y, T1), del(X, T1, T2))).
s2l(0, L) :- ','(!, eq(L, [])).
s2l(X, .(X3, Xs)) :- ','(p(X, P), s2l(P, Xs)).
head([], X4).
head(.(H, X5), H).
tail([], []).
tail(.(X6, Xs), Xs).
p(0, 0).
p(s(X), X).
failure(b).
eq(X, X).

Query: goal(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: goal(T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: goal(T3), SCOPE: 1, CLAUSE: 0\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(s2l(T5, X9), conf(X9))\n\nT5 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(s2l(T5, X9), conf(X9)), SCOPE: 2, CLAUSE: 6 | ','(s2l(T5, X9), conf(X9)), SCOPE: 2, CLAUSE: 7\n\nT5 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(','(!_2, eq(X15, [])), conf(X15)) | ','(s2l(0, X9), conf(X9)), SCOPE: 2, CLAUSE: 7\n\nX9 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(s2l(T5, X9), conf(X9)), SCOPE: 2, CLAUSE: 7\n\nT5 is ground\nX9 is free\nX14 is free\ns2l(T5, X9) !=? s2l(0, X14)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(eq(X15, []), conf(X15))\n\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(eq(X15, []), conf(X15)), SCOPE: 3, CLAUSE: 15\n\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: conf([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: conf([]), SCOPE: 4, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="B: ','(del2([], X47), ','(del(X48, X49, X47), conf(X49)))\n\nX47 is free\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="I: del2([], X47)\n\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="M: ','(del(X48, X49, T6), conf(X49))\n\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: del2([], X47), SCOPE: 5, CLAUSE: 2\n\nX47 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="J: ','(del(X77, [], X78), del(X79, X78, X80))\n\nX80 is free\nX77 is free\nX78 is free\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="E: del(X77, [], X78)\n\nX77 is free\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="D: del(X79, T8, X80)\n\nX80 is free\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: del(X77, [], X78), SCOPE: 6, CLAUSE: 3 | del(X77, [], X78), SCOPE: 6, CLAUSE: 4 | del(X77, [], X78), SCOPE: 6, CLAUSE: 5\n\nX77 is free\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(!_6, failure(a)) | del(X77, [], X78), SCOPE: 6, CLAUSE: 4 | del(X77, [], X78), SCOPE: 6, CLAUSE: 5\n\nX77 is free\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: failure(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: failure(a), SCOPE: 7, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: del(X79, T8, X80), SCOPE: 8, CLAUSE: 3 | del(X79, T8, X80), SCOPE: 8, CLAUSE: 4 | del(X79, T8, X80), SCOPE: 8, CLAUSE: 5\n\nX80 is free\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(!_8, failure(a)) | del(X79, T8, X80), SCOPE: 8, CLAUSE: 4 | del(X79, T8, X80), SCOPE: 8, CLAUSE: 5\n\nX80 is free\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: del(X79, T8, X80), SCOPE: 8, CLAUSE: 4 | del(X79, T8, X80), SCOPE: 8, CLAUSE: 5\n\nX80 is free\nX79 is free\nX113 is free\nX114 is free\ndel(X79, T8, X80) !=? del(X113, [], X114)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: failure(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: failure(a), SCOPE: 9, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: del(X79, T8, X80), SCOPE: 8, CLAUSE: 4\n\nX80 is free\nX79 is free\nX113 is free\nX114 is free\ndel(X79, T8, X80) !=? del(X113, [], X114)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: del(X79, T8, X80), SCOPE: 8, CLAUSE: 5\n\nX80 is free\nX79 is free\nX113 is free\nX114 is free\ndel(X79, T8, X80) !=? del(X113, [], X114)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ','(head(T16, X140), tail(T16, X141))\n\nX140 is free\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(head(T16, X140), tail(T16, X141)), SCOPE: 10, CLAUSE: 8 | ','(head(T16, X140), tail(T16, X141)), SCOPE: 10, CLAUSE: 9\n\nX140 is free\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(head(T16, X140), tail(T16, X141)), SCOPE: 10, CLAUSE: 8\n\nX140 is free\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(head(T16, X140), tail(T16, X141)), SCOPE: 10, CLAUSE: 9\n\nX140 is free\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: tail([], X141)\n\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: tail([], X141), SCOPE: 11, CLAUSE: 10 | tail([], X141), SCOPE: 11, CLAUSE: 11\n\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: tail([], X141), SCOPE: 11, CLAUSE: 10\n\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: tail([], X141), SCOPE: 11, CLAUSE: 11\n\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: tail(.(T23, T24), X141)\n\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: tail(.(T23, T24), X141), SCOPE: 12, CLAUSE: 10 | tail(.(T23, T24), X141), SCOPE: 12, CLAUSE: 11\n\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: tail(.(T23, T24), X141), SCOPE: 12, CLAUSE: 11\n\nX141 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(head(T35, X191), ','(tail(T35, X189), del(X190, X189, X192)))\n\nX190 is free\nX191 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(head(T35, X191), ','(tail(T35, X189), del(X190, X189, X192))), SCOPE: 13, CLAUSE: 8 | ','(head(T35, X191), ','(tail(T35, X189), del(X190, X189, X192))), SCOPE: 13, CLAUSE: 9\n\nX190 is free\nX191 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(head(T35, X191), ','(tail(T35, X189), del(X190, X189, X192))), SCOPE: 13, CLAUSE: 8\n\nX190 is free\nX191 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: ','(head(T35, X191), ','(tail(T35, X189), del(X190, X189, X192))), SCOPE: 13, CLAUSE: 9\n\nX190 is free\nX191 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(tail([], X189), del(X190, X189, X192))\n\nX190 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(tail([], X189), del(X190, X189, X192)), SCOPE: 14, CLAUSE: 10 | ','(tail([], X189), del(X190, X189, X192)), SCOPE: 14, CLAUSE: 11\n\nX190 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: ','(tail([], X189), del(X190, X189, X192)), SCOPE: 14, CLAUSE: 10\n\nX190 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ','(tail([], X189), del(X190, X189, X192)), SCOPE: 14, CLAUSE: 11\n\nX190 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: del(X190, [], X192)\n\nX190 is free\nX192 is free", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(tail(.(T42, T43), X189), del(X190, X189, X192))\n\nX190 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(tail(.(T42, T43), X189), del(X190, X189, X192)), SCOPE: 15, CLAUSE: 10 | ','(tail(.(T42, T43), X189), del(X190, X189, X192)), SCOPE: 15, CLAUSE: 11\n\nX190 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(tail(.(T42, T43), X189), del(X190, X189, X192)), SCOPE: 15, CLAUSE: 11\n\nX190 is free\nX192 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: del(X190, T51, X192)\n\nX190 is free\nX192 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="N: del(X48, X49, T6)\n\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="F: conf(T54)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: del(X48, X49, T6), SCOPE: 16, CLAUSE: 3 | del(X48, X49, T6), SCOPE: 16, CLAUSE: 4 | del(X48, X49, T6), SCOPE: 16, CLAUSE: 5\n\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(!_16, failure(a)) | del(X48, X49, T6), SCOPE: 16, CLAUSE: 4 | del(X48, X49, T6), SCOPE: 16, CLAUSE: 5\n\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: failure(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: failure(a), SCOPE: 17, CLAUSE: 14\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: conf(T54), SCOPE: 18, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="G: ','(del2(T65, X280), ','(del(X281, X282, X280), conf(X282)))\n\nX280 is free\nX281 is free\nX282 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="K: del2(T65, X280)\n\nX280 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(del(X281, X282, T67), conf(X282))\n\nX281 is free\nX282 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: del2(T65, X280), SCOPE: 19, CLAUSE: 2\n\nX280 is free", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="L: ','(del(X310, T73, X311), del(X312, X311, X313))\n\nX313 is free\nX310 is free\nX311 is free\nX312 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: del(X310, T73, X311)\n\nX310 is free\nX311 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: del(X312, T75, X313)\n\nX313 is free\nX312 is free", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: ','(','(p(T79, X345), s2l(X345, X347)), conf(.(X346, X347)))\n\nT79 is ground\nX9 is free\nX14 is free\nX346 is free\nX347 is free\nX345 is free\ns2l(T79, X9) !=? s2l(0, X14)", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: ','(','(p(T79, X345), s2l(X345, X347)), conf(.(X346, X347))), SCOPE: 20, CLAUSE: 12 | ','(','(p(T79, X345), s2l(X345, X347)), conf(.(X346, X347))), SCOPE: 20, CLAUSE: 13\n\nT79 is ground\nX9 is free\nX14 is free\nX346 is free\nX347 is free\nX345 is free\ns2l(T79, X9) !=? s2l(0, X14)", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(','(p(T79, X345), s2l(X345, X347)), conf(.(X346, X347))), SCOPE: 20, CLAUSE: 13\n\nT79 is ground\nX9 is free\nX14 is free\nX346 is free\nX347 is free\nX345 is free\ns2l(T79, X9) !=? s2l(0, X14)", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="C: ','(s2l(T82, X347), conf(.(X346, X347)))\n\nT82 is ground\nX346 is free\nX347 is free", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="H: s2l(T82, X347)\n\nT82 is ground\nX347 is free", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: conf(.(X346, T83))\n\nX346 is free", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: s2l(T82, X347), SCOPE: 21, CLAUSE: 6 | s2l(T82, X347), SCOPE: 21, CLAUSE: 7\n\nT82 is ground\nX347 is free", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: ','(!_21, eq(X362, [])) | s2l(0, X347), SCOPE: 21, CLAUSE: 7\n\nX347 is free\nX362 is free", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: s2l(T82, X347), SCOPE: 21, CLAUSE: 7\n\nT82 is ground\nX347 is free\nX361 is free\ns2l(T82, X347) !=? s2l(0, X361)", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: eq(X362, [])\n\nX362 is free", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: eq(X362, []), SCOPE: 22, CLAUSE: 15\n\nX362 is free", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: ','(p(T86, X385), s2l(X385, X387))\n\nT86 is ground\nX347 is free\nX361 is free\nX387 is free\nX385 is free\ns2l(T86, X347) !=? s2l(0, X361)", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: ','(p(T86, X385), s2l(X385, X387)), SCOPE: 23, CLAUSE: 12 | ','(p(T86, X385), s2l(X385, X387)), SCOPE: 23, CLAUSE: 13\n\nT86 is ground\nX347 is free\nX361 is free\nX387 is free\nX385 is free\ns2l(T86, X347) !=? s2l(0, X361)", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: ','(p(T86, X385), s2l(X385, X387)), SCOPE: 23, CLAUSE: 13\n\nT86 is ground\nX347 is free\nX361 is free\nX387 is free\nX385 is free\ns2l(T86, X347) !=? s2l(0, X361)", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: s2l(T89, X387)\n\nT89 is ground\nX387 is free", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 263 [arrowhead = none ];
263 -> 5;

264 [label="ONLY EVAL with clause\ngoal(X8) :- ','(s2l(X8, X9), conf(X9)).\nand substitutionT3 -> T5,\nX8 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 264 [arrowhead = none ];
264 -> 7;

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

266 [label="EVAL with clause\ns2l(0, X14) :- ','(!_2, eq(X14, [])).\nand substitutionT5 -> 0,\nX9 -> X15,\nX14 -> X15", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 266 [arrowhead = none ];
266 -> 12;

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

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

269 [label="ONLY EVAL with clause\ns2l(X342, .(X343, X344)) :- ','(p(X342, X345), s2l(X345, X344)).\nand substitutionT5 -> T79,\nX342 -> T79,\nX343 -> X346,\nX344 -> X347,\nX9 -> .(X346, X347)", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 269 [arrowhead = none ];
269 -> 219;

270 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 270 [arrowhead = none ];
270 -> 18;

271 [label="ONLY EVAL with clause\neq(X29, X29).\nand substitutionX15 -> [],\nX29 -> [],\nX30 -> []", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 271 [arrowhead = none ];
271 -> 22;

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

273 [label="ONLY EVAL with clause\nconf(X46) :- ','(del2(X46, X47), ','(del(X48, X49, X47), conf(X49))).\nand substitutionX46 -> []", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 273 [arrowhead = none ];
273 -> 31;

274 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
31 -> 274 [arrowhead = none ];
274 -> 35;

275 [label="SPLIT 2\nreplacements:X47 -> T6", fontsize=14, style = filled, fillcolor = violet];
31 -> 275 [arrowhead = none ];
275 -> 36;

276 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 276 [arrowhead = none ];
276 -> 40;

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

278 [label="SPLIT 2\nreplacements:X48 -> T53,\nX49 -> T54", fontsize=14, style = filled, fillcolor = violet];
36 -> 278 [arrowhead = none ];
278 -> 161;

279 [label="ONLY EVAL with clause\ndel2(X75, X76) :- ','(del(X77, X75, X78), del(X79, X78, X76)).\nand substitutionX75 -> [],\nX47 -> X80,\nX76 -> X80", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 279 [arrowhead = none ];
279 -> 44;

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

281 [label="SPLIT 2\nreplacements:X77 -> T7,\nX78 -> T8", fontsize=14, style = filled, fillcolor = violet];
44 -> 281 [arrowhead = none ];
281 -> 47;

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

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

284 [label="ONLY EVAL with clause\ndel(X97, [], X98) :- ','(!_6, failure(a)).\nand substitutionX77 -> X99,\nX97 -> X99,\nX78 -> X100,\nX98 -> X100", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 284 [arrowhead = none ];
284 -> 54;

285 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 285 [arrowhead = none ];
285 -> 56;

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

287 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 287 [arrowhead = none ];
287 -> 58;

288 [label="EVAL with clause\ndel(X113, [], X114) :- ','(!_8, failure(a)).\nand substitutionX79 -> X115,\nX113 -> X115,\nT8 -> [],\nX80 -> X116,\nX114 -> X116", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 288 [arrowhead = none ];
288 -> 65;

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

290 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 290 [arrowhead = none ];
290 -> 67;

291 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 291 [arrowhead = none ];
291 -> 75;

292 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 292 [arrowhead = none ];
292 -> 76;

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

294 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 294 [arrowhead = none ];
294 -> 69;

295 [label="ONLY EVAL with clause\ndel(X137, X138, X139) :- ','(head(X138, X137), tail(X138, X139)).\nand substitutionX79 -> X140,\nX137 -> X140,\nT8 -> T16,\nX138 -> T16,\nX80 -> X141,\nX139 -> X141,\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 295 [arrowhead = none ];
295 -> 80;

296 [label="ONLY EVAL with clause\ndel(X185, X186, .(X187, X188)) :- ','(head(X186, X187), ','(tail(X186, X189), del(X185, X189, X188))).\nand substitutionX79 -> X190,\nX185 -> X190,\nT8 -> T35,\nX186 -> T35,\nX187 -> X191,\nX188 -> X192,\nX80 -> .(X191, X192),\nT34 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 296 [arrowhead = none ];
296 -> 119;

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

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

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

300 [label="EVAL with clause\nhead([], X150).\nand substitutionT16 -> [],\nX140 -> X151,\nX150 -> X151", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 300 [arrowhead = none ];
300 -> 91;

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

302 [label="EVAL with clause\nhead(.(X158, X159), X158).\nand substitutionX158 -> T23,\nX159 -> T24,\nT16 -> .(T23, T24),\nX140 -> T23,\nT21 -> T23,\nT22 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 302 [arrowhead = none ];
302 -> 107;

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

304 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 304 [arrowhead = none ];
304 -> 93;

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

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

307 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX141 -> []", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 307 [arrowhead = none ];
307 -> 96;

308 [label="BACKTRACK\nfor clause: tail(.(X6, Xs), Xs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 308 [arrowhead = none ];
308 -> 100;

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

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

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

312 [label="ONLY EVAL with clause\ntail(.(X164, X165), X165).\nand substitutionT23 -> T29,\nX164 -> T29,\nT24 -> T30,\nX165 -> T30,\nX141 -> T30", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 312 [arrowhead = none ];
312 -> 115;

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

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

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

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

317 [label="EVAL with clause\nhead([], X205).\nand substitutionT35 -> [],\nX191 -> X206,\nX205 -> X206", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 317 [arrowhead = none ];
317 -> 126;

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

319 [label="EVAL with clause\nhead(.(X229, X230), X229).\nand substitutionX229 -> T42,\nX230 -> T43,\nT35 -> .(T42, T43),\nX191 -> T42,\nT40 -> T42,\nT41 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 319 [arrowhead = none ];
319 -> 144;

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

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

322 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
130 -> 322 [arrowhead = none ];
322 -> 134;

323 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
130 -> 323 [arrowhead = none ];
323 -> 136;

324 [label="ONLY EVAL with clause\ntail([], []).\nand substitutionX189 -> []", fontsize=14, style = filled, fillcolor = lightblue];
134 -> 324 [arrowhead = none ];
324 -> 138;

325 [label="BACKTRACK\nfor clause: tail(.(X6, Xs), Xs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 325 [arrowhead = none ];
325 -> 142;

326 [label="INSTANCE with matching:\nX77 -> X190\nX78 -> X192", fontsize=14, style = filled, fillcolor = lightgrey];
138 -> 326 [arrowhead = none , style=dashed];
326 -> 46[style=dashed];

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

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

329 [label="ONLY EVAL with clause\ntail(.(X243, X244), X244).\nand substitutionT42 -> T49,\nX243 -> T49,\nT43 -> T51,\nX244 -> T51,\nX189 -> T51,\nT50 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 329 [arrowhead = none ];
329 -> 153;

330 [label="INSTANCE with matching:\nX79 -> X190\nT8 -> T51\nX80 -> X192", fontsize=14, style = filled, fillcolor = lightgrey];
153 -> 330 [arrowhead = none , style=dashed];
330 -> 47[style=dashed];

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

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

333 [label="ONLY EVAL with clause\ndel(X261, [], X262) :- ','(!_16, failure(a)).\nand substitutionX48 -> X263,\nX261 -> X263,\nX49 -> [],\nT6 -> T58,\nX262 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 333 [arrowhead = none ];
333 -> 170;

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

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

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

337 [label="ONLY EVAL with clause\nconf(X279) :- ','(del2(X279, X280), ','(del(X281, X282, X280), conf(X282))).\nand substitutionT54 -> T65,\nX279 -> T65,\nT64 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 337 [arrowhead = none ];
337 -> 192;

338 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
192 -> 338 [arrowhead = none ];
338 -> 198;

339 [label="SPLIT 2\nreplacements:X280 -> T67", fontsize=14, style = filled, fillcolor = violet];
192 -> 339 [arrowhead = none ];
339 -> 199;

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

341 [label="INSTANCE with matching:\nX48 -> X281\nX49 -> X282\nT6 -> T67", fontsize=14, style = filled, fillcolor = lightgrey];
199 -> 341 [arrowhead = none , style=dashed];
341 -> 36[style=dashed];

342 [label="ONLY EVAL with clause\ndel2(X308, X309) :- ','(del(X310, X308, X311), del(X312, X311, X309)).\nand substitutionT65 -> T73,\nX308 -> T73,\nX280 -> X313,\nX309 -> X313,\nT72 -> T73", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 342 [arrowhead = none ];
342 -> 204;

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

344 [label="SPLIT 2\nreplacements:X310 -> T74,\nX311 -> T75", fontsize=14, style = filled, fillcolor = violet];
204 -> 344 [arrowhead = none ];
344 -> 207;

345 [label="INSTANCE with matching:\nX79 -> X310\nT8 -> T73\nX80 -> X311", fontsize=14, style = filled, fillcolor = lightgrey];
206 -> 345 [arrowhead = none , style=dashed];
345 -> 47[style=dashed];

346 [label="INSTANCE with matching:\nX79 -> X312\nT8 -> T75\nX80 -> X313", fontsize=14, style = filled, fillcolor = lightgrey];
207 -> 346 [arrowhead = none , style=dashed];
346 -> 47[style=dashed];

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

348 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2l(T79, X9), s2l(0, X14))", fontsize=14, style = filled, fillcolor = lightgreen];
220 -> 348 [arrowhead = none ];
348 -> 221;

349 [label="EVAL with clause\np(s(X352), X352).\nand substitutionX352 -> T82,\nT79 -> s(T82),\nX345 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
221 -> 349 [arrowhead = none ];
349 -> 222;

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

351 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
222 -> 351 [arrowhead = none ];
351 -> 227;

352 [label="SPLIT 2\nnew knowledge:\nT82 is ground\nreplacements:X347 -> T83", fontsize=14, style = filled, fillcolor = violet];
222 -> 352 [arrowhead = none ];
352 -> 228;

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

354 [label="INSTANCE with matching:\nT54 -> .(X346, T83)", fontsize=14, style = filled, fillcolor = lightgrey];
228 -> 354 [arrowhead = none , style=dashed];
354 -> 161[style=dashed];

355 [label="EVAL with clause\ns2l(0, X361) :- ','(!_21, eq(X361, [])).\nand substitutionT82 -> 0,\nX347 -> X362,\nX361 -> X362", fontsize=14, style = filled, fillcolor = lightblue];
232 -> 355 [arrowhead = none ];
355 -> 234;

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

357 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
234 -> 357 [arrowhead = none ];
357 -> 236;

358 [label="ONLY EVAL with clause\ns2l(X382, .(X383, X384)) :- ','(p(X382, X385), s2l(X385, X384)).\nand substitutionT82 -> T86,\nX382 -> T86,\nX383 -> X386,\nX384 -> X387,\nX347 -> .(X386, X387)", fontsize=14, style = filled, fillcolor = lightblue];
235 -> 358 [arrowhead = none ];
358 -> 254;

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

360 [label="ONLY EVAL with clause\neq(X367, X367).\nand substitutionX362 -> [],\nX367 -> [],\nX368 -> []", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 360 [arrowhead = none ];
360 -> 245;

361 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
245 -> 361 [arrowhead = none ];
361 -> 246;

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

363 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2l(T86, X347), s2l(0, X361))", fontsize=14, style = filled, fillcolor = lightgreen];
255 -> 363 [arrowhead = none ];
363 -> 257;

364 [label="EVAL with clause\np(s(X392), X392).\nand substitutionX392 -> T89,\nT86 -> s(T89),\nX385 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
257 -> 364 [arrowhead = none ];
364 -> 261;

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

366 [label="INSTANCE with matching:\nT82 -> T89\nX347 -> X387", fontsize=14, style = filled, fillcolor = lightgrey];
261 -> 366 [arrowhead = none , style=dashed];
366 -> 227[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
R is empty.
Pi is empty.

(3) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(4) YES