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

(0) Obligation:

Clauses:

tree(nil).
tree(node(L, X, R)) :- ','(tree(L), tree(R)).
s2t(s(X), node(T, Y, T)) :- s2t(X, T).
s2t(s(X), node(nil, Y, T)) :- s2t(X, T).
s2t(s(X), node(T, Y, nil)) :- s2t(X, T).
s2t(s(X), node(nil, Y, nil)).
s2t(0, nil).
goal(X) :- ','(s2t(X, T), tree(T)).

Query: goal(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: goal(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: goal(T1), SCOPE: 1, CLAUSE: 7\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(s2t(T3, X3), tree(X3))\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 2 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 3 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 4 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 3 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 4 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="B: ','(s2t(T8, X27), tree(node(X27, X28, X27)))\n\nT8 is ground\nX27 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="G: s2t(T8, X27)\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="J: tree(node(T10, X28, T10))\n\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: s2t(T8, X27), SCOPE: 3, CLAUSE: 2 | s2t(T8, X27), SCOPE: 3, CLAUSE: 3 | s2t(T8, X27), SCOPE: 3, CLAUSE: 4 | s2t(T8, X27), SCOPE: 3, CLAUSE: 5 | s2t(T8, X27), SCOPE: 3, CLAUSE: 6\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: s2t(T8, X27), SCOPE: 3, CLAUSE: 2\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: s2t(T8, X27), SCOPE: 3, CLAUSE: 3 | s2t(T8, X27), SCOPE: 3, CLAUSE: 4 | s2t(T8, X27), SCOPE: 3, CLAUSE: 5 | s2t(T8, X27), SCOPE: 3, CLAUSE: 6\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: s2t(T16, X62)\n\nT16 is ground\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: s2t(T8, X27), SCOPE: 3, CLAUSE: 3\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: s2t(T8, X27), SCOPE: 3, CLAUSE: 4 | s2t(T8, X27), SCOPE: 3, CLAUSE: 5 | s2t(T8, X27), SCOPE: 3, CLAUSE: 6\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: s2t(T22, X93)\n\nT22 is ground\nX93 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: s2t(T8, X27), SCOPE: 3, CLAUSE: 4\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: s2t(T8, X27), SCOPE: 3, CLAUSE: 5 | s2t(T8, X27), SCOPE: 3, CLAUSE: 6\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: s2t(T28, X122)\n\nT28 is ground\nX122 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: s2t(T8, X27), SCOPE: 3, CLAUSE: 5\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: s2t(T8, X27), SCOPE: 3, CLAUSE: 6\n\nT8 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: tree(node(T10, X28, T10)), SCOPE: 4, CLAUSE: 0 | tree(node(T10, X28, T10)), SCOPE: 4, CLAUSE: 1\n\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: tree(node(T10, X28, T10)), SCOPE: 4, CLAUSE: 1\n\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="K: ','(tree(T39), tree(T39))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: tree(T39)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="H: tree(T40)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: tree(T40), SCOPE: 5, CLAUSE: 0 | tree(T40), SCOPE: 5, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: tree(T40), SCOPE: 5, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: tree(T40), SCOPE: 5, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="I: ','(tree(T50), tree(T51))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: tree(T50)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: tree(T52)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 4 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="C: ','(s2t(T57, X189), tree(node(nil, X188, X189)))\n\nT57 is ground\nX188 is free\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: s2t(T57, X189)\n\nT57 is ground\nX189 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: tree(node(nil, X188, T59))\n\nX188 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 5 | ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="D: ','(s2t(T65, X223), tree(node(X223, X224, nil)))\n\nT65 is ground\nX223 is free\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: s2t(T65, X223)\n\nT65 is ground\nX223 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: tree(node(T67, X224, nil))\n\nX224 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 5\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ','(s2t(T3, X3), tree(X3)), SCOPE: 2, CLAUSE: 6\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: tree(node(nil, X249, nil))\n\nX249 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: tree(node(nil, X249, nil)), SCOPE: 6, CLAUSE: 0 | tree(node(nil, X249, nil)), SCOPE: 6, CLAUSE: 1\n\nX249 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: tree(node(nil, X249, nil)), SCOPE: 6, CLAUSE: 1\n\nX249 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="E: ','(tree(nil), tree(nil))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="F: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: tree(nil), SCOPE: 7, CLAUSE: 0 | tree(nil), SCOPE: 7, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: tree(nil), SCOPE: 7, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: tree(nil), SCOPE: 7, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: tree(nil)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 187 [arrowhead = none ];
187 -> 5;

188 [label="ONLY EVAL with clause\ngoal(X2) :- ','(s2t(X2, X3), tree(X3)).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 188 [arrowhead = none ];
188 -> 8;

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

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

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

192 [label="EVAL with clause\ns2t(s(X24), node(X25, X26, X25)) :- s2t(X24, X25).\nand substitutionX24 -> T8,\nT3 -> s(T8),\nX25 -> X27,\nX26 -> X28,\nX3 -> node(X27, X28, X27)", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 192 [arrowhead = none ];
192 -> 17;

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

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

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

196 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 196 [arrowhead = none ];
196 -> 25;

197 [label="SPLIT 2\nnew knowledge:\nT8 is ground\nreplacements:X27 -> T10", fontsize=14, style = filled, fillcolor = violet];
17 -> 197 [arrowhead = none ];
197 -> 26;

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

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

200 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 200 [arrowhead = none ];
200 -> 33;

201 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 201 [arrowhead = none ];
201 -> 35;

202 [label="EVAL with clause\ns2t(s(X59), node(X60, X61, X60)) :- s2t(X59, X60).\nand substitutionX59 -> T16,\nT8 -> s(T16),\nX60 -> X62,\nX61 -> X63,\nX27 -> node(X62, X63, X62)", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 202 [arrowhead = none ];
202 -> 45;

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

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

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

206 [label="INSTANCE with matching:\nT8 -> T16\nX27 -> X62", fontsize=14, style = filled, fillcolor = lightgrey];
45 -> 206 [arrowhead = none , style=dashed];
206 -> 25[style=dashed];

207 [label="EVAL with clause\ns2t(s(X89), node(nil, X90, X91)) :- s2t(X89, X91).\nand substitutionX89 -> T22,\nT8 -> s(T22),\nX90 -> X92,\nX91 -> X93,\nX27 -> node(nil, X92, X93)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 207 [arrowhead = none ];
207 -> 62;

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

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

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

211 [label="INSTANCE with matching:\nT8 -> T22\nX27 -> X93", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 211 [arrowhead = none , style=dashed];
211 -> 25[style=dashed];

212 [label="EVAL with clause\ns2t(s(X119), node(X120, X121, nil)) :- s2t(X119, X120).\nand substitutionX119 -> T28,\nT8 -> s(T28),\nX120 -> X122,\nX121 -> X123,\nX27 -> node(X122, X123, nil)", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 212 [arrowhead = none ];
212 -> 100;

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

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

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

216 [label="INSTANCE with matching:\nT8 -> T28\nX27 -> X122", fontsize=14, style = filled, fillcolor = lightgrey];
100 -> 216 [arrowhead = none , style=dashed];
216 -> 25[style=dashed];

217 [label="EVAL with clause\ns2t(s(X141), node(nil, X142, nil)).\nand substitutionX141 -> T34,\nT8 -> s(T34),\nX142 -> X143,\nX27 -> node(nil, X143, nil)", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 217 [arrowhead = none ];
217 -> 108;

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

219 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT8 -> 0,\nX27 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 219 [arrowhead = none ];
219 -> 117;

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

221 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 221 [arrowhead = none ];
221 -> 110;

222 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 222 [arrowhead = none ];
222 -> 119;

223 [label="BACKTRACK\nfor clause: tree(nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 223 [arrowhead = none ];
223 -> 121;

224 [label="ONLY EVAL with clause\ntree(node(X152, X153, X154)) :- ','(tree(X152), tree(X154)).\nand substitutionT10 -> T39,\nX152 -> T39,\nX28 -> X155,\nX153 -> X155,\nX154 -> T39,\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 224 [arrowhead = none ];
224 -> 123;

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

226 [label="SPLIT 2\nreplacements:T39 -> T40", fontsize=14, style = filled, fillcolor = violet];
123 -> 226 [arrowhead = none ];
226 -> 126;

227 [label="INSTANCE with matching:\nT40 -> T39", fontsize=14, style = filled, fillcolor = lightgrey];
125 -> 227 [arrowhead = none , style=dashed];
227 -> 126[style=dashed];

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

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

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

231 [label="EVAL with clause\ntree(nil).\nand substitutionT40 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 231 [arrowhead = none ];
231 -> 132;

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

233 [label="EVAL with clause\ntree(node(X162, X163, X164)) :- ','(tree(X162), tree(X164)).\nand substitutionX162 -> T50,\nX163 -> T48,\nX164 -> T51,\nT40 -> node(T50, T48, T51),\nT47 -> T50,\nT49 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 233 [arrowhead = none ];
233 -> 139;

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

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

236 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
139 -> 236 [arrowhead = none ];
236 -> 145;

237 [label="SPLIT 2\nreplacements:T51 -> T52", fontsize=14, style = filled, fillcolor = violet];
139 -> 237 [arrowhead = none ];
237 -> 146;

238 [label="INSTANCE with matching:\nT40 -> T50", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 238 [arrowhead = none , style=dashed];
238 -> 126[style=dashed];

239 [label="INSTANCE with matching:\nT40 -> T52", fontsize=14, style = filled, fillcolor = lightgrey];
146 -> 239 [arrowhead = none , style=dashed];
239 -> 126[style=dashed];

240 [label="EVAL with clause\ns2t(s(X185), node(nil, X186, X187)) :- s2t(X185, X187).\nand substitutionX185 -> T57,\nT3 -> s(T57),\nX186 -> X188,\nX187 -> X189,\nX3 -> node(nil, X188, X189)", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 240 [arrowhead = none ];
240 -> 160;

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

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

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

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

245 [label="SPLIT 2\nnew knowledge:\nT57 is ground\nreplacements:X189 -> T59", fontsize=14, style = filled, fillcolor = violet];
160 -> 245 [arrowhead = none ];
245 -> 163;

246 [label="INSTANCE with matching:\nT8 -> T57\nX27 -> X189", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 246 [arrowhead = none , style=dashed];
246 -> 25[style=dashed];

247 [label="INSTANCE with matching:\nT40 -> node(nil, X188, T59)", fontsize=14, style = filled, fillcolor = lightgrey];
163 -> 247 [arrowhead = none , style=dashed];
247 -> 126[style=dashed];

248 [label="EVAL with clause\ns2t(s(X220), node(X221, X222, nil)) :- s2t(X220, X221).\nand substitutionX220 -> T65,\nT3 -> s(T65),\nX221 -> X223,\nX222 -> X224,\nX3 -> node(X223, X224, nil)", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 248 [arrowhead = none ];
248 -> 166;

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

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

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

252 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
166 -> 252 [arrowhead = none ];
252 -> 168;

253 [label="SPLIT 2\nnew knowledge:\nT65 is ground\nreplacements:X223 -> T67", fontsize=14, style = filled, fillcolor = violet];
166 -> 253 [arrowhead = none ];
253 -> 169;

254 [label="INSTANCE with matching:\nT8 -> T65\nX27 -> X223", fontsize=14, style = filled, fillcolor = lightgrey];
168 -> 254 [arrowhead = none , style=dashed];
254 -> 25[style=dashed];

255 [label="INSTANCE with matching:\nT40 -> node(T67, X224, nil)", fontsize=14, style = filled, fillcolor = lightgrey];
169 -> 255 [arrowhead = none , style=dashed];
255 -> 126[style=dashed];

256 [label="EVAL with clause\ns2t(s(X247), node(nil, X248, nil)).\nand substitutionX247 -> T73,\nT3 -> s(T73),\nX248 -> X249,\nX3 -> node(nil, X249, nil)", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 256 [arrowhead = none ];
256 -> 172;

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

258 [label="EVAL with clause\ns2t(0, nil).\nand substitutionT3 -> 0,\nX3 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 258 [arrowhead = none ];
258 -> 185;

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

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

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

262 [label="ONLY EVAL with clause\ntree(node(X258, X259, X260)) :- ','(tree(X258), tree(X260)).\nand substitutionX258 -> nil,\nX249 -> X261,\nX259 -> X261,\nX260 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 262 [arrowhead = none ];
262 -> 176;

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

264 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
176 -> 264 [arrowhead = none ];
264 -> 178;

265 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
177 -> 265 [arrowhead = none , style=dashed];
265 -> 178[style=dashed];

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

267 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 267 [arrowhead = none ];
267 -> 180;

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

269 [label="ONLY EVAL with clause\ntree(nil).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 269 [arrowhead = none ];
269 -> 182;

270 [label="BACKTRACK\nfor clause: tree(node(L, X, R)) :- ','(tree(L), tree(R))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 270 [arrowhead = none ];
270 -> 184;

271 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 271 [arrowhead = none ];
271 -> 183;

272 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
185 -> 272 [arrowhead = none , style=dashed];
272 -> 178[style=dashed];

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X27, X28))
pB_in_gaa(T8, T10, X28) → U11_gaa(T8, T10, X28, s2tG_in_ga(T8, T10))
s2tG_in_ga(s(T16), node(X62, X63, X62)) → U6_ga(T16, X62, X63, s2tG_in_ga(T16, X62))
s2tG_in_ga(s(T22), node(nil, X92, X93)) → U7_ga(T22, X92, X93, s2tG_in_ga(T22, X93))
s2tG_in_ga(s(T28), node(X122, X123, nil)) → U8_ga(T28, X122, X123, s2tG_in_ga(T28, X122))
s2tG_in_ga(s(T34), node(nil, X143, nil)) → s2tG_out_ga(s(T34), node(nil, X143, nil))
s2tG_in_ga(0, nil) → s2tG_out_ga(0, nil)
U8_ga(T28, X122, X123, s2tG_out_ga(T28, X122)) → s2tG_out_ga(s(T28), node(X122, X123, nil))
U7_ga(T22, X92, X93, s2tG_out_ga(T22, X93)) → s2tG_out_ga(s(T22), node(nil, X92, X93))
U6_ga(T16, X62, X63, s2tG_out_ga(T16, X62)) → s2tG_out_ga(s(T16), node(X62, X63, X62))
U11_gaa(T8, T10, X28, s2tG_out_ga(T8, T10)) → U12_gaa(T8, T10, X28, treeJ_in_ga(T10, X28))
treeJ_in_ga(T39, X155) → U10_ga(T39, X155, pK_in_g(T39))
pK_in_g(T40) → U13_g(T40, treeH_in_g(T40))
treeH_in_g(nil) → treeH_out_g(nil)
treeH_in_g(node(T50, T48, T51)) → U9_g(T50, T48, T51, pI_in_gg(T50, T51))
pI_in_gg(T50, T52) → U15_gg(T50, T52, treeH_in_g(T50))
U15_gg(T50, T52, treeH_out_g(T50)) → U16_gg(T50, T52, treeH_in_g(T52))
U16_gg(T50, T52, treeH_out_g(T52)) → pI_out_gg(T50, T52)
U9_g(T50, T48, T51, pI_out_gg(T50, T51)) → treeH_out_g(node(T50, T48, T51))
U13_g(T40, treeH_out_g(T40)) → U14_g(T40, treeH_in_g(T40))
U14_g(T40, treeH_out_g(T40)) → pK_out_g(T40)
U10_ga(T39, X155, pK_out_g(T39)) → treeJ_out_ga(T39, X155)
U12_gaa(T8, T10, X28, treeJ_out_ga(T10, X28)) → pB_out_gaa(T8, T10, X28)
U1_g(T8, pB_out_gaa(T8, X27, X28)) → goalA_out_g(s(T8))
goalA_in_g(s(T57)) → U2_g(T57, pC_in_gaa(T57, X189, X188))
pC_in_gaa(T57, T59, X188) → U17_gaa(T57, T59, X188, s2tG_in_ga(T57, T59))
U17_gaa(T57, T59, X188, s2tG_out_ga(T57, T59)) → U18_gaa(T57, T59, X188, treeH_in_g(node(nil, X188, T59)))
U18_gaa(T57, T59, X188, treeH_out_g(node(nil, X188, T59))) → pC_out_gaa(T57, T59, X188)
U2_g(T57, pC_out_gaa(T57, X189, X188)) → goalA_out_g(s(T57))
goalA_in_g(s(T65)) → U3_g(T65, pD_in_gaa(T65, X223, X224))
pD_in_gaa(T65, T67, X224) → U19_gaa(T65, T67, X224, s2tG_in_ga(T65, T67))
U19_gaa(T65, T67, X224, s2tG_out_ga(T65, T67)) → U20_gaa(T65, T67, X224, treeH_in_g(node(T67, X224, nil)))
U20_gaa(T65, T67, X224, treeH_out_g(node(T67, X224, nil))) → pD_out_gaa(T65, T67, X224)
U3_g(T65, pD_out_gaa(T65, X223, X224)) → goalA_out_g(s(T65))
goalA_in_g(s(T73)) → U4_g(T73, pE_in_)
pE_in_ → U21_(treeF_in_)
treeF_in_ → treeF_out_
U21_(treeF_out_) → U22_(treeF_in_)
U22_(treeF_out_) → pE_out_
U4_g(T73, pE_out_) → goalA_out_g(s(T73))
goalA_in_g(0) → U5_g(treeF_in_)
U5_g(treeF_out_) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
s2tG_in_ga(x1, x2)  =  s2tG_in_ga(x1)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
U8_ga(x1, x2, x3, x4)  =  U8_ga(x1, x4)
s2tG_out_ga(x1, x2)  =  s2tG_out_ga(x1, x2)
node(x1, x2, x3)  =  node(x1, x3)
0  =  0
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x2, x4)
treeJ_in_ga(x1, x2)  =  treeJ_in_ga(x1)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pK_in_g(x1)  =  pK_in_g(x1)
U13_g(x1, x2)  =  U13_g(x1, x2)
treeH_in_g(x1)  =  treeH_in_g(x1)
nil  =  nil
treeH_out_g(x1)  =  treeH_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x3, x4)
pI_in_gg(x1, x2)  =  pI_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
pI_out_gg(x1, x2)  =  pI_out_gg(x1, x2)
U14_g(x1, x2)  =  U14_g(x1, x2)
pK_out_g(x1)  =  pK_out_g(x1)
treeJ_out_ga(x1, x2)  =  treeJ_out_ga(x1)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x4)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x2, x4)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x4)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2)
U4_g(x1, x2)  =  U4_g(x1, x2)
pE_in_  =  pE_in_
U21_(x1)  =  U21_(x1)
treeF_in_  =  treeF_in_
treeF_out_  =  treeF_out_
U22_(x1)  =  U22_(x1)
pE_out_  =  pE_out_
U5_g(x1)  =  U5_g(x1)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

GOALA_IN_G(s(T8)) → U1_G(T8, pB_in_gaa(T8, X27, X28))
GOALA_IN_G(s(T8)) → PB_IN_GAA(T8, X27, X28)
PB_IN_GAA(T8, T10, X28) → U11_GAA(T8, T10, X28, s2tG_in_ga(T8, T10))
PB_IN_GAA(T8, T10, X28) → S2TG_IN_GA(T8, T10)
S2TG_IN_GA(s(T16), node(X62, X63, X62)) → U6_GA(T16, X62, X63, s2tG_in_ga(T16, X62))
S2TG_IN_GA(s(T16), node(X62, X63, X62)) → S2TG_IN_GA(T16, X62)
S2TG_IN_GA(s(T22), node(nil, X92, X93)) → U7_GA(T22, X92, X93, s2tG_in_ga(T22, X93))
S2TG_IN_GA(s(T22), node(nil, X92, X93)) → S2TG_IN_GA(T22, X93)
S2TG_IN_GA(s(T28), node(X122, X123, nil)) → U8_GA(T28, X122, X123, s2tG_in_ga(T28, X122))
S2TG_IN_GA(s(T28), node(X122, X123, nil)) → S2TG_IN_GA(T28, X122)
U11_GAA(T8, T10, X28, s2tG_out_ga(T8, T10)) → U12_GAA(T8, T10, X28, treeJ_in_ga(T10, X28))
U11_GAA(T8, T10, X28, s2tG_out_ga(T8, T10)) → TREEJ_IN_GA(T10, X28)
TREEJ_IN_GA(T39, X155) → U10_GA(T39, X155, pK_in_g(T39))
TREEJ_IN_GA(T39, X155) → PK_IN_G(T39)
PK_IN_G(T40) → U13_G(T40, treeH_in_g(T40))
PK_IN_G(T40) → TREEH_IN_G(T40)
TREEH_IN_G(node(T50, T48, T51)) → U9_G(T50, T48, T51, pI_in_gg(T50, T51))
TREEH_IN_G(node(T50, T48, T51)) → PI_IN_GG(T50, T51)
PI_IN_GG(T50, T52) → U15_GG(T50, T52, treeH_in_g(T50))
PI_IN_GG(T50, T52) → TREEH_IN_G(T50)
U15_GG(T50, T52, treeH_out_g(T50)) → U16_GG(T50, T52, treeH_in_g(T52))
U15_GG(T50, T52, treeH_out_g(T50)) → TREEH_IN_G(T52)
U13_G(T40, treeH_out_g(T40)) → U14_G(T40, treeH_in_g(T40))
U13_G(T40, treeH_out_g(T40)) → TREEH_IN_G(T40)
GOALA_IN_G(s(T57)) → U2_G(T57, pC_in_gaa(T57, X189, X188))
GOALA_IN_G(s(T57)) → PC_IN_GAA(T57, X189, X188)
PC_IN_GAA(T57, T59, X188) → U17_GAA(T57, T59, X188, s2tG_in_ga(T57, T59))
PC_IN_GAA(T57, T59, X188) → S2TG_IN_GA(T57, T59)
U17_GAA(T57, T59, X188, s2tG_out_ga(T57, T59)) → U18_GAA(T57, T59, X188, treeH_in_g(node(nil, X188, T59)))
U17_GAA(T57, T59, X188, s2tG_out_ga(T57, T59)) → TREEH_IN_G(node(nil, X188, T59))
GOALA_IN_G(s(T65)) → U3_G(T65, pD_in_gaa(T65, X223, X224))
GOALA_IN_G(s(T65)) → PD_IN_GAA(T65, X223, X224)
PD_IN_GAA(T65, T67, X224) → U19_GAA(T65, T67, X224, s2tG_in_ga(T65, T67))
PD_IN_GAA(T65, T67, X224) → S2TG_IN_GA(T65, T67)
U19_GAA(T65, T67, X224, s2tG_out_ga(T65, T67)) → U20_GAA(T65, T67, X224, treeH_in_g(node(T67, X224, nil)))
U19_GAA(T65, T67, X224, s2tG_out_ga(T65, T67)) → TREEH_IN_G(node(T67, X224, nil))
GOALA_IN_G(s(T73)) → U4_G(T73, pE_in_)
GOALA_IN_G(s(T73)) → PE_IN_
PE_IN_ → U21_¹(treeF_in_)
PE_IN_ → TREEF_IN_
U21_¹(treeF_out_) → U22_¹(treeF_in_)
U21_¹(treeF_out_) → TREEF_IN_
GOALA_IN_G(0) → U5_G(treeF_in_)
GOALA_IN_G(0) → TREEF_IN_

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X27, X28))
pB_in_gaa(T8, T10, X28) → U11_gaa(T8, T10, X28, s2tG_in_ga(T8, T10))
s2tG_in_ga(s(T16), node(X62, X63, X62)) → U6_ga(T16, X62, X63, s2tG_in_ga(T16, X62))
s2tG_in_ga(s(T22), node(nil, X92, X93)) → U7_ga(T22, X92, X93, s2tG_in_ga(T22, X93))
s2tG_in_ga(s(T28), node(X122, X123, nil)) → U8_ga(T28, X122, X123, s2tG_in_ga(T28, X122))
s2tG_in_ga(s(T34), node(nil, X143, nil)) → s2tG_out_ga(s(T34), node(nil, X143, nil))
s2tG_in_ga(0, nil) → s2tG_out_ga(0, nil)
U8_ga(T28, X122, X123, s2tG_out_ga(T28, X122)) → s2tG_out_ga(s(T28), node(X122, X123, nil))
U7_ga(T22, X92, X93, s2tG_out_ga(T22, X93)) → s2tG_out_ga(s(T22), node(nil, X92, X93))
U6_ga(T16, X62, X63, s2tG_out_ga(T16, X62)) → s2tG_out_ga(s(T16), node(X62, X63, X62))
U11_gaa(T8, T10, X28, s2tG_out_ga(T8, T10)) → U12_gaa(T8, T10, X28, treeJ_in_ga(T10, X28))
treeJ_in_ga(T39, X155) → U10_ga(T39, X155, pK_in_g(T39))
pK_in_g(T40) → U13_g(T40, treeH_in_g(T40))
treeH_in_g(nil) → treeH_out_g(nil)
treeH_in_g(node(T50, T48, T51)) → U9_g(T50, T48, T51, pI_in_gg(T50, T51))
pI_in_gg(T50, T52) → U15_gg(T50, T52, treeH_in_g(T50))
U15_gg(T50, T52, treeH_out_g(T50)) → U16_gg(T50, T52, treeH_in_g(T52))
U16_gg(T50, T52, treeH_out_g(T52)) → pI_out_gg(T50, T52)
U9_g(T50, T48, T51, pI_out_gg(T50, T51)) → treeH_out_g(node(T50, T48, T51))
U13_g(T40, treeH_out_g(T40)) → U14_g(T40, treeH_in_g(T40))
U14_g(T40, treeH_out_g(T40)) → pK_out_g(T40)
U10_ga(T39, X155, pK_out_g(T39)) → treeJ_out_ga(T39, X155)
U12_gaa(T8, T10, X28, treeJ_out_ga(T10, X28)) → pB_out_gaa(T8, T10, X28)
U1_g(T8, pB_out_gaa(T8, X27, X28)) → goalA_out_g(s(T8))
goalA_in_g(s(T57)) → U2_g(T57, pC_in_gaa(T57, X189, X188))
pC_in_gaa(T57, T59, X188) → U17_gaa(T57, T59, X188, s2tG_in_ga(T57, T59))
U17_gaa(T57, T59, X188, s2tG_out_ga(T57, T59)) → U18_gaa(T57, T59, X188, treeH_in_g(node(nil, X188, T59)))
U18_gaa(T57, T59, X188, treeH_out_g(node(nil, X188, T59))) → pC_out_gaa(T57, T59, X188)
U2_g(T57, pC_out_gaa(T57, X189, X188)) → goalA_out_g(s(T57))
goalA_in_g(s(T65)) → U3_g(T65, pD_in_gaa(T65, X223, X224))
pD_in_gaa(T65, T67, X224) → U19_gaa(T65, T67, X224, s2tG_in_ga(T65, T67))
U19_gaa(T65, T67, X224, s2tG_out_ga(T65, T67)) → U20_gaa(T65, T67, X224, treeH_in_g(node(T67, X224, nil)))
U20_gaa(T65, T67, X224, treeH_out_g(node(T67, X224, nil))) → pD_out_gaa(T65, T67, X224)
U3_g(T65, pD_out_gaa(T65, X223, X224)) → goalA_out_g(s(T65))
goalA_in_g(s(T73)) → U4_g(T73, pE_in_)
pE_in_ → U21_(treeF_in_)
treeF_in_ → treeF_out_
U21_(treeF_out_) → U22_(treeF_in_)
U22_(treeF_out_) → pE_out_
U4_g(T73, pE_out_) → goalA_out_g(s(T73))
goalA_in_g(0) → U5_g(treeF_in_)
U5_g(treeF_out_) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
s2tG_in_ga(x1, x2)  =  s2tG_in_ga(x1)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
U8_ga(x1, x2, x3, x4)  =  U8_ga(x1, x4)
s2tG_out_ga(x1, x2)  =  s2tG_out_ga(x1, x2)
node(x1, x2, x3)  =  node(x1, x3)
0  =  0
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x2, x4)
treeJ_in_ga(x1, x2)  =  treeJ_in_ga(x1)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pK_in_g(x1)  =  pK_in_g(x1)
U13_g(x1, x2)  =  U13_g(x1, x2)
treeH_in_g(x1)  =  treeH_in_g(x1)
nil  =  nil
treeH_out_g(x1)  =  treeH_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x3, x4)
pI_in_gg(x1, x2)  =  pI_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
pI_out_gg(x1, x2)  =  pI_out_gg(x1, x2)
U14_g(x1, x2)  =  U14_g(x1, x2)
pK_out_g(x1)  =  pK_out_g(x1)
treeJ_out_ga(x1, x2)  =  treeJ_out_ga(x1)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x4)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x2, x4)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x4)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2)
U4_g(x1, x2)  =  U4_g(x1, x2)
pE_in_  =  pE_in_
U21_(x1)  =  U21_(x1)
treeF_in_  =  treeF_in_
treeF_out_  =  treeF_out_
U22_(x1)  =  U22_(x1)
pE_out_  =  pE_out_
U5_g(x1)  =  U5_g(x1)
GOALA_IN_G(x1)  =  GOALA_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U11_GAA(x1, x2, x3, x4)  =  U11_GAA(x1, x4)
S2TG_IN_GA(x1, x2)  =  S2TG_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)
U12_GAA(x1, x2, x3, x4)  =  U12_GAA(x1, x2, x4)
TREEJ_IN_GA(x1, x2)  =  TREEJ_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
PK_IN_G(x1)  =  PK_IN_G(x1)
U13_G(x1, x2)  =  U13_G(x1, x2)
TREEH_IN_G(x1)  =  TREEH_IN_G(x1)
U9_G(x1, x2, x3, x4)  =  U9_G(x1, x3, x4)
PI_IN_GG(x1, x2)  =  PI_IN_GG(x1, x2)
U15_GG(x1, x2, x3)  =  U15_GG(x1, x2, x3)
U16_GG(x1, x2, x3)  =  U16_GG(x1, x2, x3)
U14_G(x1, x2)  =  U14_G(x1, x2)
U2_G(x1, x2)  =  U2_G(x1, x2)
PC_IN_GAA(x1, x2, x3)  =  PC_IN_GAA(x1)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x4)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x2, x4)
U3_G(x1, x2)  =  U3_G(x1, x2)
PD_IN_GAA(x1, x2, x3)  =  PD_IN_GAA(x1)
U19_GAA(x1, x2, x3, x4)  =  U19_GAA(x1, x4)
U20_GAA(x1, x2, x3, x4)  =  U20_GAA(x1, x2, x4)
U4_G(x1, x2)  =  U4_G(x1, x2)
PE_IN_  =  PE_IN_
U21_¹(x1)  =  U21_¹(x1)
TREEF_IN_  =  TREEF_IN_
U22_¹(x1)  =  U22_¹(x1)
U5_G(x1)  =  U5_G(x1)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

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

GOALA_IN_G(s(T8)) → U1_G(T8, pB_in_gaa(T8, X27, X28))
GOALA_IN_G(s(T8)) → PB_IN_GAA(T8, X27, X28)
PB_IN_GAA(T8, T10, X28) → U11_GAA(T8, T10, X28, s2tG_in_ga(T8, T10))
PB_IN_GAA(T8, T10, X28) → S2TG_IN_GA(T8, T10)
S2TG_IN_GA(s(T16), node(X62, X63, X62)) → U6_GA(T16, X62, X63, s2tG_in_ga(T16, X62))
S2TG_IN_GA(s(T16), node(X62, X63, X62)) → S2TG_IN_GA(T16, X62)
S2TG_IN_GA(s(T22), node(nil, X92, X93)) → U7_GA(T22, X92, X93, s2tG_in_ga(T22, X93))
S2TG_IN_GA(s(T22), node(nil, X92, X93)) → S2TG_IN_GA(T22, X93)
S2TG_IN_GA(s(T28), node(X122, X123, nil)) → U8_GA(T28, X122, X123, s2tG_in_ga(T28, X122))
S2TG_IN_GA(s(T28), node(X122, X123, nil)) → S2TG_IN_GA(T28, X122)
U11_GAA(T8, T10, X28, s2tG_out_ga(T8, T10)) → U12_GAA(T8, T10, X28, treeJ_in_ga(T10, X28))
U11_GAA(T8, T10, X28, s2tG_out_ga(T8, T10)) → TREEJ_IN_GA(T10, X28)
TREEJ_IN_GA(T39, X155) → U10_GA(T39, X155, pK_in_g(T39))
TREEJ_IN_GA(T39, X155) → PK_IN_G(T39)
PK_IN_G(T40) → U13_G(T40, treeH_in_g(T40))
PK_IN_G(T40) → TREEH_IN_G(T40)
TREEH_IN_G(node(T50, T48, T51)) → U9_G(T50, T48, T51, pI_in_gg(T50, T51))
TREEH_IN_G(node(T50, T48, T51)) → PI_IN_GG(T50, T51)
PI_IN_GG(T50, T52) → U15_GG(T50, T52, treeH_in_g(T50))
PI_IN_GG(T50, T52) → TREEH_IN_G(T50)
U15_GG(T50, T52, treeH_out_g(T50)) → U16_GG(T50, T52, treeH_in_g(T52))
U15_GG(T50, T52, treeH_out_g(T50)) → TREEH_IN_G(T52)
U13_G(T40, treeH_out_g(T40)) → U14_G(T40, treeH_in_g(T40))
U13_G(T40, treeH_out_g(T40)) → TREEH_IN_G(T40)
GOALA_IN_G(s(T57)) → U2_G(T57, pC_in_gaa(T57, X189, X188))
GOALA_IN_G(s(T57)) → PC_IN_GAA(T57, X189, X188)
PC_IN_GAA(T57, T59, X188) → U17_GAA(T57, T59, X188, s2tG_in_ga(T57, T59))
PC_IN_GAA(T57, T59, X188) → S2TG_IN_GA(T57, T59)
U17_GAA(T57, T59, X188, s2tG_out_ga(T57, T59)) → U18_GAA(T57, T59, X188, treeH_in_g(node(nil, X188, T59)))
U17_GAA(T57, T59, X188, s2tG_out_ga(T57, T59)) → TREEH_IN_G(node(nil, X188, T59))
GOALA_IN_G(s(T65)) → U3_G(T65, pD_in_gaa(T65, X223, X224))
GOALA_IN_G(s(T65)) → PD_IN_GAA(T65, X223, X224)
PD_IN_GAA(T65, T67, X224) → U19_GAA(T65, T67, X224, s2tG_in_ga(T65, T67))
PD_IN_GAA(T65, T67, X224) → S2TG_IN_GA(T65, T67)
U19_GAA(T65, T67, X224, s2tG_out_ga(T65, T67)) → U20_GAA(T65, T67, X224, treeH_in_g(node(T67, X224, nil)))
U19_GAA(T65, T67, X224, s2tG_out_ga(T65, T67)) → TREEH_IN_G(node(T67, X224, nil))
GOALA_IN_G(s(T73)) → U4_G(T73, pE_in_)
GOALA_IN_G(s(T73)) → PE_IN_
PE_IN_ → U21_¹(treeF_in_)
PE_IN_ → TREEF_IN_
U21_¹(treeF_out_) → U22_¹(treeF_in_)
U21_¹(treeF_out_) → TREEF_IN_
GOALA_IN_G(0) → U5_G(treeF_in_)
GOALA_IN_G(0) → TREEF_IN_

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X27, X28))
pB_in_gaa(T8, T10, X28) → U11_gaa(T8, T10, X28, s2tG_in_ga(T8, T10))
s2tG_in_ga(s(T16), node(X62, X63, X62)) → U6_ga(T16, X62, X63, s2tG_in_ga(T16, X62))
s2tG_in_ga(s(T22), node(nil, X92, X93)) → U7_ga(T22, X92, X93, s2tG_in_ga(T22, X93))
s2tG_in_ga(s(T28), node(X122, X123, nil)) → U8_ga(T28, X122, X123, s2tG_in_ga(T28, X122))
s2tG_in_ga(s(T34), node(nil, X143, nil)) → s2tG_out_ga(s(T34), node(nil, X143, nil))
s2tG_in_ga(0, nil) → s2tG_out_ga(0, nil)
U8_ga(T28, X122, X123, s2tG_out_ga(T28, X122)) → s2tG_out_ga(s(T28), node(X122, X123, nil))
U7_ga(T22, X92, X93, s2tG_out_ga(T22, X93)) → s2tG_out_ga(s(T22), node(nil, X92, X93))
U6_ga(T16, X62, X63, s2tG_out_ga(T16, X62)) → s2tG_out_ga(s(T16), node(X62, X63, X62))
U11_gaa(T8, T10, X28, s2tG_out_ga(T8, T10)) → U12_gaa(T8, T10, X28, treeJ_in_ga(T10, X28))
treeJ_in_ga(T39, X155) → U10_ga(T39, X155, pK_in_g(T39))
pK_in_g(T40) → U13_g(T40, treeH_in_g(T40))
treeH_in_g(nil) → treeH_out_g(nil)
treeH_in_g(node(T50, T48, T51)) → U9_g(T50, T48, T51, pI_in_gg(T50, T51))
pI_in_gg(T50, T52) → U15_gg(T50, T52, treeH_in_g(T50))
U15_gg(T50, T52, treeH_out_g(T50)) → U16_gg(T50, T52, treeH_in_g(T52))
U16_gg(T50, T52, treeH_out_g(T52)) → pI_out_gg(T50, T52)
U9_g(T50, T48, T51, pI_out_gg(T50, T51)) → treeH_out_g(node(T50, T48, T51))
U13_g(T40, treeH_out_g(T40)) → U14_g(T40, treeH_in_g(T40))
U14_g(T40, treeH_out_g(T40)) → pK_out_g(T40)
U10_ga(T39, X155, pK_out_g(T39)) → treeJ_out_ga(T39, X155)
U12_gaa(T8, T10, X28, treeJ_out_ga(T10, X28)) → pB_out_gaa(T8, T10, X28)
U1_g(T8, pB_out_gaa(T8, X27, X28)) → goalA_out_g(s(T8))
goalA_in_g(s(T57)) → U2_g(T57, pC_in_gaa(T57, X189, X188))
pC_in_gaa(T57, T59, X188) → U17_gaa(T57, T59, X188, s2tG_in_ga(T57, T59))
U17_gaa(T57, T59, X188, s2tG_out_ga(T57, T59)) → U18_gaa(T57, T59, X188, treeH_in_g(node(nil, X188, T59)))
U18_gaa(T57, T59, X188, treeH_out_g(node(nil, X188, T59))) → pC_out_gaa(T57, T59, X188)
U2_g(T57, pC_out_gaa(T57, X189, X188)) → goalA_out_g(s(T57))
goalA_in_g(s(T65)) → U3_g(T65, pD_in_gaa(T65, X223, X224))
pD_in_gaa(T65, T67, X224) → U19_gaa(T65, T67, X224, s2tG_in_ga(T65, T67))
U19_gaa(T65, T67, X224, s2tG_out_ga(T65, T67)) → U20_gaa(T65, T67, X224, treeH_in_g(node(T67, X224, nil)))
U20_gaa(T65, T67, X224, treeH_out_g(node(T67, X224, nil))) → pD_out_gaa(T65, T67, X224)
U3_g(T65, pD_out_gaa(T65, X223, X224)) → goalA_out_g(s(T65))
goalA_in_g(s(T73)) → U4_g(T73, pE_in_)
pE_in_ → U21_(treeF_in_)
treeF_in_ → treeF_out_
U21_(treeF_out_) → U22_(treeF_in_)
U22_(treeF_out_) → pE_out_
U4_g(T73, pE_out_) → goalA_out_g(s(T73))
goalA_in_g(0) → U5_g(treeF_in_)
U5_g(treeF_out_) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
s2tG_in_ga(x1, x2)  =  s2tG_in_ga(x1)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
U8_ga(x1, x2, x3, x4)  =  U8_ga(x1, x4)
s2tG_out_ga(x1, x2)  =  s2tG_out_ga(x1, x2)
node(x1, x2, x3)  =  node(x1, x3)
0  =  0
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x2, x4)
treeJ_in_ga(x1, x2)  =  treeJ_in_ga(x1)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pK_in_g(x1)  =  pK_in_g(x1)
U13_g(x1, x2)  =  U13_g(x1, x2)
treeH_in_g(x1)  =  treeH_in_g(x1)
nil  =  nil
treeH_out_g(x1)  =  treeH_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x3, x4)
pI_in_gg(x1, x2)  =  pI_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
pI_out_gg(x1, x2)  =  pI_out_gg(x1, x2)
U14_g(x1, x2)  =  U14_g(x1, x2)
pK_out_g(x1)  =  pK_out_g(x1)
treeJ_out_ga(x1, x2)  =  treeJ_out_ga(x1)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x4)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x2, x4)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x4)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2)
U4_g(x1, x2)  =  U4_g(x1, x2)
pE_in_  =  pE_in_
U21_(x1)  =  U21_(x1)
treeF_in_  =  treeF_in_
treeF_out_  =  treeF_out_
U22_(x1)  =  U22_(x1)
pE_out_  =  pE_out_
U5_g(x1)  =  U5_g(x1)
GOALA_IN_G(x1)  =  GOALA_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U11_GAA(x1, x2, x3, x4)  =  U11_GAA(x1, x4)
S2TG_IN_GA(x1, x2)  =  S2TG_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)
U12_GAA(x1, x2, x3, x4)  =  U12_GAA(x1, x2, x4)
TREEJ_IN_GA(x1, x2)  =  TREEJ_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
PK_IN_G(x1)  =  PK_IN_G(x1)
U13_G(x1, x2)  =  U13_G(x1, x2)
TREEH_IN_G(x1)  =  TREEH_IN_G(x1)
U9_G(x1, x2, x3, x4)  =  U9_G(x1, x3, x4)
PI_IN_GG(x1, x2)  =  PI_IN_GG(x1, x2)
U15_GG(x1, x2, x3)  =  U15_GG(x1, x2, x3)
U16_GG(x1, x2, x3)  =  U16_GG(x1, x2, x3)
U14_G(x1, x2)  =  U14_G(x1, x2)
U2_G(x1, x2)  =  U2_G(x1, x2)
PC_IN_GAA(x1, x2, x3)  =  PC_IN_GAA(x1)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x4)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x2, x4)
U3_G(x1, x2)  =  U3_G(x1, x2)
PD_IN_GAA(x1, x2, x3)  =  PD_IN_GAA(x1)
U19_GAA(x1, x2, x3, x4)  =  U19_GAA(x1, x4)
U20_GAA(x1, x2, x3, x4)  =  U20_GAA(x1, x2, x4)
U4_G(x1, x2)  =  U4_G(x1, x2)
PE_IN_  =  PE_IN_
U21_¹(x1)  =  U21_¹(x1)
TREEF_IN_  =  TREEF_IN_
U22_¹(x1)  =  U22_¹(x1)
U5_G(x1)  =  U5_G(x1)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 37 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

TREEH_IN_G(node(T50, T48, T51)) → PI_IN_GG(T50, T51)
PI_IN_GG(T50, T52) → U15_GG(T50, T52, treeH_in_g(T50))
U15_GG(T50, T52, treeH_out_g(T50)) → TREEH_IN_G(T52)
PI_IN_GG(T50, T52) → TREEH_IN_G(T50)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X27, X28))
pB_in_gaa(T8, T10, X28) → U11_gaa(T8, T10, X28, s2tG_in_ga(T8, T10))
s2tG_in_ga(s(T16), node(X62, X63, X62)) → U6_ga(T16, X62, X63, s2tG_in_ga(T16, X62))
s2tG_in_ga(s(T22), node(nil, X92, X93)) → U7_ga(T22, X92, X93, s2tG_in_ga(T22, X93))
s2tG_in_ga(s(T28), node(X122, X123, nil)) → U8_ga(T28, X122, X123, s2tG_in_ga(T28, X122))
s2tG_in_ga(s(T34), node(nil, X143, nil)) → s2tG_out_ga(s(T34), node(nil, X143, nil))
s2tG_in_ga(0, nil) → s2tG_out_ga(0, nil)
U8_ga(T28, X122, X123, s2tG_out_ga(T28, X122)) → s2tG_out_ga(s(T28), node(X122, X123, nil))
U7_ga(T22, X92, X93, s2tG_out_ga(T22, X93)) → s2tG_out_ga(s(T22), node(nil, X92, X93))
U6_ga(T16, X62, X63, s2tG_out_ga(T16, X62)) → s2tG_out_ga(s(T16), node(X62, X63, X62))
U11_gaa(T8, T10, X28, s2tG_out_ga(T8, T10)) → U12_gaa(T8, T10, X28, treeJ_in_ga(T10, X28))
treeJ_in_ga(T39, X155) → U10_ga(T39, X155, pK_in_g(T39))
pK_in_g(T40) → U13_g(T40, treeH_in_g(T40))
treeH_in_g(nil) → treeH_out_g(nil)
treeH_in_g(node(T50, T48, T51)) → U9_g(T50, T48, T51, pI_in_gg(T50, T51))
pI_in_gg(T50, T52) → U15_gg(T50, T52, treeH_in_g(T50))
U15_gg(T50, T52, treeH_out_g(T50)) → U16_gg(T50, T52, treeH_in_g(T52))
U16_gg(T50, T52, treeH_out_g(T52)) → pI_out_gg(T50, T52)
U9_g(T50, T48, T51, pI_out_gg(T50, T51)) → treeH_out_g(node(T50, T48, T51))
U13_g(T40, treeH_out_g(T40)) → U14_g(T40, treeH_in_g(T40))
U14_g(T40, treeH_out_g(T40)) → pK_out_g(T40)
U10_ga(T39, X155, pK_out_g(T39)) → treeJ_out_ga(T39, X155)
U12_gaa(T8, T10, X28, treeJ_out_ga(T10, X28)) → pB_out_gaa(T8, T10, X28)
U1_g(T8, pB_out_gaa(T8, X27, X28)) → goalA_out_g(s(T8))
goalA_in_g(s(T57)) → U2_g(T57, pC_in_gaa(T57, X189, X188))
pC_in_gaa(T57, T59, X188) → U17_gaa(T57, T59, X188, s2tG_in_ga(T57, T59))
U17_gaa(T57, T59, X188, s2tG_out_ga(T57, T59)) → U18_gaa(T57, T59, X188, treeH_in_g(node(nil, X188, T59)))
U18_gaa(T57, T59, X188, treeH_out_g(node(nil, X188, T59))) → pC_out_gaa(T57, T59, X188)
U2_g(T57, pC_out_gaa(T57, X189, X188)) → goalA_out_g(s(T57))
goalA_in_g(s(T65)) → U3_g(T65, pD_in_gaa(T65, X223, X224))
pD_in_gaa(T65, T67, X224) → U19_gaa(T65, T67, X224, s2tG_in_ga(T65, T67))
U19_gaa(T65, T67, X224, s2tG_out_ga(T65, T67)) → U20_gaa(T65, T67, X224, treeH_in_g(node(T67, X224, nil)))
U20_gaa(T65, T67, X224, treeH_out_g(node(T67, X224, nil))) → pD_out_gaa(T65, T67, X224)
U3_g(T65, pD_out_gaa(T65, X223, X224)) → goalA_out_g(s(T65))
goalA_in_g(s(T73)) → U4_g(T73, pE_in_)
pE_in_ → U21_(treeF_in_)
treeF_in_ → treeF_out_
U21_(treeF_out_) → U22_(treeF_in_)
U22_(treeF_out_) → pE_out_
U4_g(T73, pE_out_) → goalA_out_g(s(T73))
goalA_in_g(0) → U5_g(treeF_in_)
U5_g(treeF_out_) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
s2tG_in_ga(x1, x2)  =  s2tG_in_ga(x1)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
U8_ga(x1, x2, x3, x4)  =  U8_ga(x1, x4)
s2tG_out_ga(x1, x2)  =  s2tG_out_ga(x1, x2)
node(x1, x2, x3)  =  node(x1, x3)
0  =  0
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x2, x4)
treeJ_in_ga(x1, x2)  =  treeJ_in_ga(x1)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pK_in_g(x1)  =  pK_in_g(x1)
U13_g(x1, x2)  =  U13_g(x1, x2)
treeH_in_g(x1)  =  treeH_in_g(x1)
nil  =  nil
treeH_out_g(x1)  =  treeH_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x3, x4)
pI_in_gg(x1, x2)  =  pI_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
pI_out_gg(x1, x2)  =  pI_out_gg(x1, x2)
U14_g(x1, x2)  =  U14_g(x1, x2)
pK_out_g(x1)  =  pK_out_g(x1)
treeJ_out_ga(x1, x2)  =  treeJ_out_ga(x1)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x4)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x2, x4)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x4)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2)
U4_g(x1, x2)  =  U4_g(x1, x2)
pE_in_  =  pE_in_
U21_(x1)  =  U21_(x1)
treeF_in_  =  treeF_in_
treeF_out_  =  treeF_out_
U22_(x1)  =  U22_(x1)
pE_out_  =  pE_out_
U5_g(x1)  =  U5_g(x1)
TREEH_IN_G(x1)  =  TREEH_IN_G(x1)
PI_IN_GG(x1, x2)  =  PI_IN_GG(x1, x2)
U15_GG(x1, x2, x3)  =  U15_GG(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

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

TREEH_IN_G(node(T50, T48, T51)) → PI_IN_GG(T50, T51)
PI_IN_GG(T50, T52) → U15_GG(T50, T52, treeH_in_g(T50))
U15_GG(T50, T52, treeH_out_g(T50)) → TREEH_IN_G(T52)
PI_IN_GG(T50, T52) → TREEH_IN_G(T50)

The TRS R consists of the following rules:

treeH_in_g(nil) → treeH_out_g(nil)
treeH_in_g(node(T50, T48, T51)) → U9_g(T50, T48, T51, pI_in_gg(T50, T51))
U9_g(T50, T48, T51, pI_out_gg(T50, T51)) → treeH_out_g(node(T50, T48, T51))
pI_in_gg(T50, T52) → U15_gg(T50, T52, treeH_in_g(T50))
U15_gg(T50, T52, treeH_out_g(T50)) → U16_gg(T50, T52, treeH_in_g(T52))
U16_gg(T50, T52, treeH_out_g(T52)) → pI_out_gg(T50, T52)

The argument filtering Pi contains the following mapping:
node(x1, x2, x3)  =  node(x1, x3)
treeH_in_g(x1)  =  treeH_in_g(x1)
nil  =  nil
treeH_out_g(x1)  =  treeH_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x3, x4)
pI_in_gg(x1, x2)  =  pI_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
pI_out_gg(x1, x2)  =  pI_out_gg(x1, x2)
TREEH_IN_G(x1)  =  TREEH_IN_G(x1)
PI_IN_GG(x1, x2)  =  PI_IN_GG(x1, x2)
U15_GG(x1, x2, x3)  =  U15_GG(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

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

TREEH_IN_G(node(T50, T51)) → PI_IN_GG(T50, T51)
PI_IN_GG(T50, T52) → U15_GG(T50, T52, treeH_in_g(T50))
U15_GG(T50, T52, treeH_out_g(T50)) → TREEH_IN_G(T52)
PI_IN_GG(T50, T52) → TREEH_IN_G(T50)

The TRS R consists of the following rules:

treeH_in_g(nil) → treeH_out_g(nil)
treeH_in_g(node(T50, T51)) → U9_g(T50, T51, pI_in_gg(T50, T51))
U9_g(T50, T51, pI_out_gg(T50, T51)) → treeH_out_g(node(T50, T51))
pI_in_gg(T50, T52) → U15_gg(T50, T52, treeH_in_g(T50))
U15_gg(T50, T52, treeH_out_g(T50)) → U16_gg(T50, T52, treeH_in_g(T52))
U16_gg(T50, T52, treeH_out_g(T52)) → pI_out_gg(T50, T52)

The set Q consists of the following terms:

treeH_in_g(x0)
U9_g(x0, x1, x2)
pI_in_gg(x0, x1)
U15_gg(x0, x1, x2)
U16_gg(x0, x1, x2)

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

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

• PI_IN_GG(T50, T52) → TREEH_IN_G(T50)
  The graph contains the following edges 1 >= 1

• PI_IN_GG(T50, T52) → U15_GG(T50, T52, treeH_in_g(T50))
  The graph contains the following edges 1 >= 1, 2 >= 2

• U15_GG(T50, T52, treeH_out_g(T50)) → TREEH_IN_G(T52)
  The graph contains the following edges 2 >= 1

• TREEH_IN_G(node(T50, T51)) → PI_IN_GG(T50, T51)
  The graph contains the following edges 1 > 1, 1 > 2

(13) YES

(14) Obligation:

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

S2TG_IN_GA(s(T22), node(nil, X92, X93)) → S2TG_IN_GA(T22, X93)
S2TG_IN_GA(s(T16), node(X62, X63, X62)) → S2TG_IN_GA(T16, X62)
S2TG_IN_GA(s(T28), node(X122, X123, nil)) → S2TG_IN_GA(T28, X122)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X27, X28))
pB_in_gaa(T8, T10, X28) → U11_gaa(T8, T10, X28, s2tG_in_ga(T8, T10))
s2tG_in_ga(s(T16), node(X62, X63, X62)) → U6_ga(T16, X62, X63, s2tG_in_ga(T16, X62))
s2tG_in_ga(s(T22), node(nil, X92, X93)) → U7_ga(T22, X92, X93, s2tG_in_ga(T22, X93))
s2tG_in_ga(s(T28), node(X122, X123, nil)) → U8_ga(T28, X122, X123, s2tG_in_ga(T28, X122))
s2tG_in_ga(s(T34), node(nil, X143, nil)) → s2tG_out_ga(s(T34), node(nil, X143, nil))
s2tG_in_ga(0, nil) → s2tG_out_ga(0, nil)
U8_ga(T28, X122, X123, s2tG_out_ga(T28, X122)) → s2tG_out_ga(s(T28), node(X122, X123, nil))
U7_ga(T22, X92, X93, s2tG_out_ga(T22, X93)) → s2tG_out_ga(s(T22), node(nil, X92, X93))
U6_ga(T16, X62, X63, s2tG_out_ga(T16, X62)) → s2tG_out_ga(s(T16), node(X62, X63, X62))
U11_gaa(T8, T10, X28, s2tG_out_ga(T8, T10)) → U12_gaa(T8, T10, X28, treeJ_in_ga(T10, X28))
treeJ_in_ga(T39, X155) → U10_ga(T39, X155, pK_in_g(T39))
pK_in_g(T40) → U13_g(T40, treeH_in_g(T40))
treeH_in_g(nil) → treeH_out_g(nil)
treeH_in_g(node(T50, T48, T51)) → U9_g(T50, T48, T51, pI_in_gg(T50, T51))
pI_in_gg(T50, T52) → U15_gg(T50, T52, treeH_in_g(T50))
U15_gg(T50, T52, treeH_out_g(T50)) → U16_gg(T50, T52, treeH_in_g(T52))
U16_gg(T50, T52, treeH_out_g(T52)) → pI_out_gg(T50, T52)
U9_g(T50, T48, T51, pI_out_gg(T50, T51)) → treeH_out_g(node(T50, T48, T51))
U13_g(T40, treeH_out_g(T40)) → U14_g(T40, treeH_in_g(T40))
U14_g(T40, treeH_out_g(T40)) → pK_out_g(T40)
U10_ga(T39, X155, pK_out_g(T39)) → treeJ_out_ga(T39, X155)
U12_gaa(T8, T10, X28, treeJ_out_ga(T10, X28)) → pB_out_gaa(T8, T10, X28)
U1_g(T8, pB_out_gaa(T8, X27, X28)) → goalA_out_g(s(T8))
goalA_in_g(s(T57)) → U2_g(T57, pC_in_gaa(T57, X189, X188))
pC_in_gaa(T57, T59, X188) → U17_gaa(T57, T59, X188, s2tG_in_ga(T57, T59))
U17_gaa(T57, T59, X188, s2tG_out_ga(T57, T59)) → U18_gaa(T57, T59, X188, treeH_in_g(node(nil, X188, T59)))
U18_gaa(T57, T59, X188, treeH_out_g(node(nil, X188, T59))) → pC_out_gaa(T57, T59, X188)
U2_g(T57, pC_out_gaa(T57, X189, X188)) → goalA_out_g(s(T57))
goalA_in_g(s(T65)) → U3_g(T65, pD_in_gaa(T65, X223, X224))
pD_in_gaa(T65, T67, X224) → U19_gaa(T65, T67, X224, s2tG_in_ga(T65, T67))
U19_gaa(T65, T67, X224, s2tG_out_ga(T65, T67)) → U20_gaa(T65, T67, X224, treeH_in_g(node(T67, X224, nil)))
U20_gaa(T65, T67, X224, treeH_out_g(node(T67, X224, nil))) → pD_out_gaa(T65, T67, X224)
U3_g(T65, pD_out_gaa(T65, X223, X224)) → goalA_out_g(s(T65))
goalA_in_g(s(T73)) → U4_g(T73, pE_in_)
pE_in_ → U21_(treeF_in_)
treeF_in_ → treeF_out_
U21_(treeF_out_) → U22_(treeF_in_)
U22_(treeF_out_) → pE_out_
U4_g(T73, pE_out_) → goalA_out_g(s(T73))
goalA_in_g(0) → U5_g(treeF_in_)
U5_g(treeF_out_) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
s2tG_in_ga(x1, x2)  =  s2tG_in_ga(x1)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
U8_ga(x1, x2, x3, x4)  =  U8_ga(x1, x4)
s2tG_out_ga(x1, x2)  =  s2tG_out_ga(x1, x2)
node(x1, x2, x3)  =  node(x1, x3)
0  =  0
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x2, x4)
treeJ_in_ga(x1, x2)  =  treeJ_in_ga(x1)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pK_in_g(x1)  =  pK_in_g(x1)
U13_g(x1, x2)  =  U13_g(x1, x2)
treeH_in_g(x1)  =  treeH_in_g(x1)
nil  =  nil
treeH_out_g(x1)  =  treeH_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x3, x4)
pI_in_gg(x1, x2)  =  pI_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
pI_out_gg(x1, x2)  =  pI_out_gg(x1, x2)
U14_g(x1, x2)  =  U14_g(x1, x2)
pK_out_g(x1)  =  pK_out_g(x1)
treeJ_out_ga(x1, x2)  =  treeJ_out_ga(x1)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x4)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x2, x4)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
U3_g(x1, x2)  =  U3_g(x1, x2)
pD_in_gaa(x1, x2, x3)  =  pD_in_gaa(x1)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x4)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x2, x4)
pD_out_gaa(x1, x2, x3)  =  pD_out_gaa(x1, x2)
U4_g(x1, x2)  =  U4_g(x1, x2)
pE_in_  =  pE_in_
U21_(x1)  =  U21_(x1)
treeF_in_  =  treeF_in_
treeF_out_  =  treeF_out_
U22_(x1)  =  U22_(x1)
pE_out_  =  pE_out_
U5_g(x1)  =  U5_g(x1)
S2TG_IN_GA(x1, x2)  =  S2TG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

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

S2TG_IN_GA(s(T22), node(nil, X92, X93)) → S2TG_IN_GA(T22, X93)
S2TG_IN_GA(s(T16), node(X62, X63, X62)) → S2TG_IN_GA(T16, X62)
S2TG_IN_GA(s(T28), node(X122, X123, nil)) → S2TG_IN_GA(T28, X122)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
node(x1, x2, x3)  =  node(x1, x3)
nil  =  nil
S2TG_IN_GA(x1, x2)  =  S2TG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

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

S2TG_IN_GA(s(T22)) → S2TG_IN_GA(T22)

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

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

• S2TG_IN_GA(s(T22)) → S2TG_IN_GA(T22)
  The graph contains the following edges 1 > 1

(20) YES