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

(0) Obligation:

Clauses:

goal(X) :- ','(s2t(X, T), tree(T)).
tree(nil) :- !.
tree(X) :- ','(left(T, L), ','(right(T, R), ','(tree(L), tree(R)))).
s2t(0, L) :- ','(!, eq(L, nil)).
s2t(X, node(T, X1, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X2, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(T, X3, nil)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X4, nil)).
left(nil, nil).
left(node(L, X5, X6), L).
right(nil, nil).
right(node(X7, X8, R), R).
p(0, 0).
p(s(X), X).
eq(X, X).

Query: goal(g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: goal(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: goal(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(s2t(T4, X15), tree(X15))\n\nT4 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: s2t(T4, X15)\n\nT4 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: tree(T5)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: s2t(T4, X15), SCOPE: 2, CLAUSE: 3 | s2t(T4, X15), SCOPE: 2, CLAUSE: 4 | s2t(T4, X15), SCOPE: 2, CLAUSE: 5 | s2t(T4, X15), SCOPE: 2, CLAUSE: 6 | s2t(T4, X15), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(!_2, eq(X25, nil)) | s2t(0, X15), SCOPE: 2, CLAUSE: 4 | s2t(0, X15), SCOPE: 2, CLAUSE: 5 | s2t(0, X15), SCOPE: 2, CLAUSE: 6 | s2t(0, X15), SCOPE: 2, CLAUSE: 7\n\nX15 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: s2t(T4, X15), SCOPE: 2, CLAUSE: 4 | s2t(T4, X15), SCOPE: 2, CLAUSE: 5 | s2t(T4, X15), SCOPE: 2, CLAUSE: 6 | s2t(T4, X15), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX15 is free\nX24 is free\ns2t(T4, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: eq(X25, nil)\n\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: eq(X25, nil), SCOPE: 3, CLAUSE: 14\n\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: s2t(T4, X15), SCOPE: 2, CLAUSE: 4\n\nT4 is ground\nX15 is free\nX24 is free\ns2t(T4, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: s2t(T4, X15), SCOPE: 2, CLAUSE: 5 | s2t(T4, X15), SCOPE: 2, CLAUSE: 6 | s2t(T4, X15), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX15 is free\nX24 is free\ns2t(T4, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(p(T10, X61), s2t(X61, X62))\n\nT10 is ground\nX15 is free\nX24 is free\nX62 is free\nX61 is free\ns2t(T10, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(p(T10, X61), s2t(X61, X62)), SCOPE: 4, CLAUSE: 12 | ','(p(T10, X61), s2t(X61, X62)), SCOPE: 4, CLAUSE: 13\n\nT10 is ground\nX15 is free\nX24 is free\nX62 is free\nX61 is free\ns2t(T10, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(p(T10, X61), s2t(X61, X62)), SCOPE: 4, CLAUSE: 13\n\nT10 is ground\nX15 is free\nX24 is free\nX62 is free\nX61 is free\ns2t(T10, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: s2t(T13, X62)\n\nT13 is ground\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: s2t(T4, X15), SCOPE: 2, CLAUSE: 5\n\nT4 is ground\nX15 is free\nX24 is free\ns2t(T4, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: s2t(T4, X15), SCOPE: 2, CLAUSE: 6 | s2t(T4, X15), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX15 is free\nX24 is free\ns2t(T4, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(p(T18, X100), s2t(X100, X102))\n\nT18 is ground\nX15 is free\nX24 is free\nX102 is free\nX100 is free\ns2t(T18, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(p(T18, X100), s2t(X100, X102)), SCOPE: 5, CLAUSE: 12 | ','(p(T18, X100), s2t(X100, X102)), SCOPE: 5, CLAUSE: 13\n\nT18 is ground\nX15 is free\nX24 is free\nX102 is free\nX100 is free\ns2t(T18, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(p(T18, X100), s2t(X100, X102)), SCOPE: 5, CLAUSE: 13\n\nT18 is ground\nX15 is free\nX24 is free\nX102 is free\nX100 is free\ns2t(T18, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: s2t(T21, X102)\n\nT21 is ground\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: s2t(T4, X15), SCOPE: 2, CLAUSE: 6\n\nT4 is ground\nX15 is free\nX24 is free\ns2t(T4, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: s2t(T4, X15), SCOPE: 2, CLAUSE: 7\n\nT4 is ground\nX15 is free\nX24 is free\ns2t(T4, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(p(T26, X139), s2t(X139, X140))\n\nT26 is ground\nX15 is free\nX24 is free\nX140 is free\nX139 is free\ns2t(T26, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(p(T26, X139), s2t(X139, X140)), SCOPE: 6, CLAUSE: 12 | ','(p(T26, X139), s2t(X139, X140)), SCOPE: 6, CLAUSE: 13\n\nT26 is ground\nX15 is free\nX24 is free\nX140 is free\nX139 is free\ns2t(T26, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(p(T26, X139), s2t(X139, X140)), SCOPE: 6, CLAUSE: 13\n\nT26 is ground\nX15 is free\nX24 is free\nX140 is free\nX139 is free\ns2t(T26, X15) !=? s2t(0, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: s2t(T29, X140)\n\nT29 is ground\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: tree(T5), SCOPE: 7, CLAUSE: 1 | tree(T5), SCOPE: 7, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: !_7 | tree(T5), SCOPE: 7, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: tree(T5), SCOPE: 7, CLAUSE: 2\n\ntree(T5) !=? tree(nil)", 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];
117 [label="117: ','(left(X164, X165), ','(right(X164, X166), ','(tree(X165), tree(X166))))\n\nX164 is free\nX165 is free\nX166 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(left(X164, X165), ','(right(X164, X166), ','(tree(X165), tree(X166)))), SCOPE: 8, CLAUSE: 8 | ','(left(X164, X165), ','(right(X164, X166), ','(tree(X165), tree(X166)))), SCOPE: 8, CLAUSE: 9\n\nX164 is free\nX165 is free\nX166 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ','(left(X164, X165), ','(right(X164, X166), ','(tree(X165), tree(X166)))), SCOPE: 8, CLAUSE: 8\n\nX164 is free\nX165 is free\nX166 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(left(X164, X165), ','(right(X164, X166), ','(tree(X165), tree(X166)))), SCOPE: 8, CLAUSE: 9\n\nX164 is free\nX165 is free\nX166 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: ','(right(nil, X166), ','(tree(nil), tree(X166)))\n\nX166 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(right(nil, X166), ','(tree(nil), tree(X166))), SCOPE: 9, CLAUSE: 10 | ','(right(nil, X166), ','(tree(nil), tree(X166))), SCOPE: 9, CLAUSE: 11\n\nX166 is free", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: ','(right(nil, X166), ','(tree(nil), tree(X166))), SCOPE: 9, CLAUSE: 10\n\nX166 is free", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: ','(right(nil, X166), ','(tree(nil), tree(X166))), SCOPE: 9, CLAUSE: 11\n\nX166 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: tree(nil), SCOPE: 10, CLAUSE: 1 | tree(nil), SCOPE: 10, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: !_10 | tree(nil), SCOPE: 10, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(right(node(X185, X186, X187), X166), ','(tree(X185), tree(X166)))\n\nX166 is free\nX185 is free\nX186 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(right(node(X185, X186, X187), X166), ','(tree(X185), tree(X166))), SCOPE: 11, CLAUSE: 10 | ','(right(node(X185, X186, X187), X166), ','(tree(X185), tree(X166))), SCOPE: 11, CLAUSE: 11\n\nX166 is free\nX185 is free\nX186 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(right(node(X185, X186, X187), X166), ','(tree(X185), tree(X166))), SCOPE: 11, CLAUSE: 11\n\nX166 is free\nX185 is free\nX186 is free\nX187 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(tree(X203), tree(X205))\n\nX203 is free\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: tree(X203)\n\nX203 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: tree(X205)\n\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: tree(X205), SCOPE: 12, CLAUSE: 1 | tree(X205), SCOPE: 12, CLAUSE: 2\n\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: !_12 | tree(X205), SCOPE: 12, CLAUSE: 2\n\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 175 [arrowhead = none ];
175 -> 6;

176 [label="ONLY EVAL with clause\ngoal(X14) :- ','(s2t(X14, X15), tree(X15)).\nand substitutionT1 -> T4,\nX14 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 176 [arrowhead = none ];
176 -> 9;

177 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
9 -> 177 [arrowhead = none ];
177 -> 18;

178 [label="SPLIT 2\nnew knowledge:\nT4 is ground\nreplacements:X15 -> T5", fontsize=14, style = filled, fillcolor = violet];
9 -> 178 [arrowhead = none ];
178 -> 20;

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

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

181 [label="EVAL with clause\ns2t(0, X24) :- ','(!_2, eq(X24, nil)).\nand substitutionT4 -> 0,\nX15 -> X25,\nX24 -> X25", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 181 [arrowhead = none ];
181 -> 33;

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

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

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

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

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

187 [label="ONLY EVAL with clause\neq(X30, X30).\nand substitutionX25 -> nil,\nX30 -> nil,\nX31 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 187 [arrowhead = none ];
187 -> 37;

188 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 188 [arrowhead = none ];
188 -> 38;

189 [label="ONLY EVAL with clause\ns2t(X58, node(X59, X60, X59)) :- ','(p(X58, X61), s2t(X61, X59)).\nand substitutionT4 -> T10,\nX58 -> T10,\nX59 -> X62,\nX60 -> X63,\nX15 -> node(X62, X63, X62)", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 189 [arrowhead = none ];
189 -> 48;

190 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 190 [arrowhead = none ];
190 -> 67;

191 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 191 [arrowhead = none ];
191 -> 68;

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

193 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T10, X15), s2t(0, X24))", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 193 [arrowhead = none ];
193 -> 51;

194 [label="EVAL with clause\np(s(X68), X68).\nand substitutionX68 -> T13,\nT10 -> s(T13),\nX61 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 194 [arrowhead = none ];
194 -> 53;

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

196 [label="INSTANCE with matching:\nT4 -> T13\nX15 -> X62", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 196 [arrowhead = none , style=dashed];
196 -> 18[style=dashed];

197 [label="ONLY EVAL with clause\ns2t(X97, node(nil, X98, X99)) :- ','(p(X97, X100), s2t(X100, X99)).\nand substitutionT4 -> T18,\nX97 -> T18,\nX98 -> X101,\nX99 -> X102,\nX15 -> node(nil, X101, X102)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 197 [arrowhead = none ];
197 -> 73;

198 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 198 [arrowhead = none ];
198 -> 90;

199 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
68 -> 199 [arrowhead = none ];
199 -> 91;

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

201 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T18, X15), s2t(0, X24))", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 201 [arrowhead = none ];
201 -> 75;

202 [label="EVAL with clause\np(s(X107), X107).\nand substitutionX107 -> T21,\nT18 -> s(T21),\nX100 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 202 [arrowhead = none ];
202 -> 76;

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

204 [label="INSTANCE with matching:\nT4 -> T21\nX15 -> X102", fontsize=14, style = filled, fillcolor = lightgrey];
76 -> 204 [arrowhead = none , style=dashed];
204 -> 18[style=dashed];

205 [label="ONLY EVAL with clause\ns2t(X136, node(X137, X138, nil)) :- ','(p(X136, X139), s2t(X139, X137)).\nand substitutionT4 -> T26,\nX136 -> T26,\nX137 -> X140,\nX138 -> X141,\nX15 -> node(X140, X141, nil)", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 205 [arrowhead = none ];
205 -> 96;

206 [label="ONLY EVAL with clause\ns2t(X155, node(nil, X156, nil)).\nand substitutionT4 -> T32,\nX155 -> T32,\nX156 -> X157,\nX15 -> node(nil, X157, nil)", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 206 [arrowhead = none ];
206 -> 106;

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

208 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2t(T26, X15), s2t(0, X24))", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 208 [arrowhead = none ];
208 -> 98;

209 [label="EVAL with clause\np(s(X146), X146).\nand substitutionX146 -> T29,\nT26 -> s(T29),\nX139 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 209 [arrowhead = none ];
209 -> 100;

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

211 [label="INSTANCE with matching:\nT4 -> T29\nX15 -> X140", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 211 [arrowhead = none , style=dashed];
211 -> 18[style=dashed];

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

213 [label="EVAL with clause\ntree(nil) :- !_7.\nand substitutionT5 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 213 [arrowhead = none ];
213 -> 111;

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

215 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 215 [arrowhead = none ];
215 -> 115;

216 [label="ONLY EVAL with clause\ntree(X163) :- ','(left(X164, X165), ','(right(X164, X166), ','(tree(X165), tree(X166)))).\nand substitutionT5 -> T35,\nX163 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 216 [arrowhead = none ];
216 -> 117;

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

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

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

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

221 [label="ONLY EVAL with clause\nleft(nil, nil).\nand substitutionX164 -> nil,\nX165 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 221 [arrowhead = none ];
221 -> 125;

222 [label="ONLY EVAL with clause\nleft(node(X182, X183, X184), X182).\nand substitutionX182 -> X185,\nX183 -> X186,\nX184 -> X187,\nX164 -> node(X185, X186, X187),\nX165 -> X185", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 222 [arrowhead = none ];
222 -> 147;

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

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

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

226 [label="ONLY EVAL with clause\nright(nil, nil).\nand substitutionX166 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 226 [arrowhead = none ];
226 -> 133;

227 [label="BACKTRACK\nfor clause: right(node(X7, X8, R), R)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
131 -> 227 [arrowhead = none ];
227 -> 144;

228 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
133 -> 228 [arrowhead = none ];
228 -> 136;

229 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
133 -> 229 [arrowhead = none ];
229 -> 137;

230 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 230 [arrowhead = none , style=dashed];
230 -> 137[style=dashed];

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

232 [label="ONLY EVAL with clause\ntree(nil) :- !_10.\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 232 [arrowhead = none ];
232 -> 139;

233 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 233 [arrowhead = none ];
233 -> 140;

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

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

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

237 [label="ONLY EVAL with clause\nright(node(X200, X201, X202), X202).\nand substitutionX185 -> X203,\nX200 -> X203,\nX186 -> X204,\nX201 -> X204,\nX187 -> X205,\nX202 -> X205,\nX166 -> X205", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 237 [arrowhead = none ];
237 -> 160;

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

239 [label="SPLIT 2\nreplacements:X203 -> T36", fontsize=14, style = filled, fillcolor = violet];
160 -> 239 [arrowhead = none ];
239 -> 165;

240 [label="INSTANCE with matching:\nX205 -> X203", fontsize=14, style = filled, fillcolor = lightgrey];
164 -> 240 [arrowhead = none , style=dashed];
240 -> 165[style=dashed];

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

242 [label="ONLY EVAL with clause\ntree(nil) :- !_12.\nand substitutionX205 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 242 [arrowhead = none ];
242 -> 171;

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

244 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 244 [arrowhead = none ];
244 -> 174;

}

(2) Obligation:

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

f3_in(T4) → U1(f9_in(T4), T4)
U1(f9_out1, T4) → f3_out1
f18_in(0) → f18_out1
f18_in(s(T13)) → U2(f18_in(T13), s(T13))
U2(f18_out1, s(T13)) → f18_out1
f18_in(s(T21)) → U3(f18_in(T21), s(T21))
U3(f18_out1, s(T21)) → f18_out1
f18_in(s(T29)) → U4(f18_in(T29), s(T29))
U4(f18_out1, s(T29)) → f18_out1
f18_in(T32) → f18_out1
f137_in → f137_out1
f165_in → f165_out1
f20_in → f20_out1
f20_in → U5(f133_in)
U5(f133_out1) → f20_out1
f20_in → U6(f160_in)
U6(f160_out1) → f20_out1
f9_in(T4) → U7(f18_in(T4), T4)
U7(f18_out1, T4) → U8(f20_in, T4)
U8(f20_out1, T4) → f9_out1
f133_in → U9(f137_in)
U9(f137_out1) → U10(f137_in)
U10(f137_out1) → f133_out1
f160_in → U11(f165_in)
U11(f165_out1) → U12(f165_in)
U12(f165_out1) → f160_out1

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
f3_in(x1)  =  f3_in(x1)
U1(x1, x2)  =  U1(x1, x2)
f9_in(x1)  =  f9_in(x1)
f9_out1  =  f9_out1
f3_out1  =  f3_out1
f18_in(x1)  =  f18_in(x1)
0  =  0
f18_out1  =  f18_out1
s(x1)  =  s(x1)
U2(x1, x2)  =  U2(x1, x2)
U3(x1, x2)  =  U3(x1, x2)
U4(x1, x2)  =  U4(x1, x2)
f137_in  =  f137_in
f137_out1  =  f137_out1
f165_in  =  f165_in
f165_out1  =  f165_out1
f20_in  =  f20_in
f20_out1  =  f20_out1
U5(x1)  =  U5(x1)
f133_in  =  f133_in
f133_out1  =  f133_out1
U6(x1)  =  x1
f160_in  =  f160_in
f160_out1  =  f160_out1
U7(x1, x2)  =  U7(x1, x2)
U8(x1, x2)  =  U8(x1, x2)
U9(x1)  =  U9(x1)
U10(x1)  =  x1
U11(x1)  =  U11(x1)
U12(x1)  =  x1

Recursive path order with status [RPO].
Quasi-Precedence:

f3_in1 > U1₂ > f3_out1
f3_in1 > f9_in1 > [f18_in1, s₁] > U2₂ > f18_out1
f3_in1 > f9_in1 > [f18_in1, s₁] > U3₂
f3_in1 > f9_in1 > [f18_in1, s₁] > U4₂ > f18_out1
f3_in1 > f9_in1 > [f20_in, U7₂] > U5₁ > [f20_out1, f133_out1, f160_out1]
f3_in1 > f9_in1 > [f20_in, U7₂] > f133_in > [f137_in, U9₁] > f137_out1 > [f20_out1, f133_out1, f160_out1]
f3_in1 > f9_in1 > [f20_in, U7₂] > f160_in > U11₁ > f165_in > f165_out1 > [f20_out1, f133_out1, f160_out1]
f3_in1 > f9_in1 > [f20_in, U7₂] > U8₂ > f9_out1 > f3_out1
0 > f18_out1

Status:

f3_in1: multiset
U1₂: [2,1]
f9_in1: [1]
f9_out1: multiset
f3_out1: multiset
f18_in1: multiset
0: multiset
f18_out1: multiset
s₁: multiset
U2₂: multiset
U3₂: multiset
U4₂: multiset
f137_in: multiset
f137_out1: multiset
f165_in: multiset
f165_out1: multiset
f20_in: multiset
f20_out1: multiset
U5₁: multiset
f133_in: multiset
f133_out1: multiset
f160_in: multiset
f160_out1: multiset
U7₂: [1,2]
U8₂: multiset
U9₁: multiset
U11₁: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f3_in(T4) → U1(f9_in(T4), T4)
U1(f9_out1, T4) → f3_out1
f18_in(0) → f18_out1
f18_in(s(T13)) → U2(f18_in(T13), s(T13))
U2(f18_out1, s(T13)) → f18_out1
f18_in(s(T21)) → U3(f18_in(T21), s(T21))
U3(f18_out1, s(T21)) → f18_out1
f18_in(s(T29)) → U4(f18_in(T29), s(T29))
U4(f18_out1, s(T29)) → f18_out1
f18_in(T32) → f18_out1
f137_in → f137_out1
f165_in → f165_out1
f20_in → f20_out1
f20_in → U5(f133_in)
U5(f133_out1) → f20_out1
f20_in → U6(f160_in)
f9_in(T4) → U7(f18_in(T4), T4)
U7(f18_out1, T4) → U8(f20_in, T4)
U8(f20_out1, T4) → f9_out1
f133_in → U9(f137_in)
U9(f137_out1) → U10(f137_in)
U10(f137_out1) → f133_out1
f160_in → U11(f165_in)
U11(f165_out1) → U12(f165_in)
U12(f165_out1) → f160_out1

(4) Obligation:

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

U6(f160_out1) → f20_out1

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U6(x₁)) = 2·x₁   
POL(f160_out1) = 2   
POL(f20_out1) = 2   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

U6(f160_out1) → f20_out1

(6) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(7) RisEmptyProof (EQUIVALENT transformation)

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

(8) YES