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

(0) Obligation:

Clauses:

palindrome(Xs) :- reverse(Xs, Xs).
reverse(X1s, X2s) :- reverse3(X1s, [], X2s).
reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys).
reverse3([], Xs, Xs).

Query: palindrome(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: palindrome(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: palindrome(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: reverse(T3, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: reverse(T3, T3), SCOPE: 2, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: reverse3(T8, [], T8)\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: reverse3(T8, [], T8), SCOPE: 3, CLAUSE: 2 | reverse3(T8, [], T8), SCOPE: 3, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: reverse3(T8, [], T8), SCOPE: 3, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: reverse3(T8, [], T8), SCOPE: 3, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: reverse3(T20, .(T19, []), .(T19, T20))\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: reverse3(T20, .(T19, []), .(T19, T20)), SCOPE: 4, CLAUSE: 2 | reverse3(T20, .(T19, []), .(T19, T20)), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: reverse3(T20, .(T19, []), .(T19, T20)), SCOPE: 4, CLAUSE: 2\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: reverse3(T20, .(T19, []), .(T19, T20)), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: reverse3(T37, .(T36, .(T38, [])), .(T38, .(T36, T37)))\n\nT36 is ground\nT37 is ground\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: reverse3(T37, .(T36, .(T38, [])), .(T38, .(T36, T37))), SCOPE: 5, CLAUSE: 2 | reverse3(T37, .(T36, .(T38, [])), .(T38, .(T36, T37))), SCOPE: 5, CLAUSE: 3\n\nT36 is ground\nT37 is ground\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: reverse3(T37, .(T36, .(T38, [])), .(T38, .(T36, T37))), SCOPE: 5, CLAUSE: 2\n\nT36 is ground\nT37 is ground\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: reverse3(T37, .(T36, .(T38, [])), .(T38, .(T36, T37))), SCOPE: 5, CLAUSE: 3\n\nT36 is ground\nT37 is ground\nT38 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: reverse3(T60, .(T59, .(T61, .(T62, []))), .(T62, .(T61, .(T59, T60))))\n\nT59 is ground\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: reverse3(T60, .(T59, .(T61, .(T62, []))), .(T62, .(T61, .(T59, T60)))), SCOPE: 6, CLAUSE: 2 | reverse3(T60, .(T59, .(T61, .(T62, []))), .(T62, .(T61, .(T59, T60)))), SCOPE: 6, CLAUSE: 3\n\nT59 is ground\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: reverse3(T60, .(T59, .(T61, .(T62, []))), .(T62, .(T61, .(T59, T60)))), SCOPE: 6, CLAUSE: 2\n\nT59 is ground\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: reverse3(T60, .(T59, .(T61, .(T62, []))), .(T62, .(T61, .(T59, T60)))), SCOPE: 6, CLAUSE: 3\n\nT59 is ground\nT60 is ground\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: reverse3(T89, .(T88, .(T90, .(T91, .(T92, [])))), .(T92, .(T91, .(T90, .(T88, T89)))))\n\nT88 is ground\nT89 is ground\nT90 is ground\nT91 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: reverse3(T89, .(T88, .(T90, .(T91, .(T92, [])))), .(T92, .(T91, .(T90, .(T88, T89))))), SCOPE: 7, CLAUSE: 2 | reverse3(T89, .(T88, .(T90, .(T91, .(T92, [])))), .(T92, .(T91, .(T90, .(T88, T89))))), SCOPE: 7, CLAUSE: 3\n\nT88 is ground\nT89 is ground\nT90 is ground\nT91 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: reverse3(T89, .(T88, .(T90, .(T91, .(T92, [])))), .(T92, .(T91, .(T90, .(T88, T89))))), SCOPE: 7, CLAUSE: 2\n\nT88 is ground\nT89 is ground\nT90 is ground\nT91 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: reverse3(T89, .(T88, .(T90, .(T91, .(T92, [])))), .(T92, .(T91, .(T90, .(T88, T89))))), SCOPE: 7, CLAUSE: 3\n\nT88 is ground\nT89 is ground\nT90 is ground\nT91 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: reverse3(T124, .(T123, .(T125, .(T126, .(T127, .(T128, []))))), .(T128, .(T127, .(T126, .(T125, .(T123, T124))))))\n\nT123 is ground\nT124 is ground\nT125 is ground\nT126 is ground\nT127 is ground\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: reverse3(T124, .(T123, .(T125, .(T126, .(T127, .(T128, []))))), .(T128, .(T127, .(T126, .(T125, .(T123, T124)))))), SCOPE: 8, CLAUSE: 2 | reverse3(T124, .(T123, .(T125, .(T126, .(T127, .(T128, []))))), .(T128, .(T127, .(T126, .(T125, .(T123, T124)))))), SCOPE: 8, CLAUSE: 3\n\nT123 is ground\nT124 is ground\nT125 is ground\nT126 is ground\nT127 is ground\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: reverse3(T124, .(T123, .(T125, .(T126, .(T127, .(T128, []))))), .(T128, .(T127, .(T126, .(T125, .(T123, T124)))))), SCOPE: 8, CLAUSE: 2\n\nT123 is ground\nT124 is ground\nT125 is ground\nT126 is ground\nT127 is ground\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: reverse3(T124, .(T123, .(T125, .(T126, .(T127, .(T128, []))))), .(T128, .(T127, .(T126, .(T125, .(T123, T124)))))), SCOPE: 8, CLAUSE: 3\n\nT123 is ground\nT124 is ground\nT125 is ground\nT126 is ground\nT127 is ground\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: reverse3(T165, .(T164, .(T166, .(T167, .(T168, .(T169, .(T170, [])))))), .(T170, .(T169, .(T168, .(T167, .(T166, .(T164, T165)))))))\n\nT164 is ground\nT165 is ground\nT166 is ground\nT167 is ground\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: reverse3(T165, .(T164, .(T166, .(T167, .(T168, .(T169, .(T170, [])))))), .(T170, .(T169, .(T168, .(T167, .(T166, .(T164, T165))))))), SCOPE: 9, CLAUSE: 2 | reverse3(T165, .(T164, .(T166, .(T167, .(T168, .(T169, .(T170, [])))))), .(T170, .(T169, .(T168, .(T167, .(T166, .(T164, T165))))))), SCOPE: 9, CLAUSE: 3\n\nT164 is ground\nT165 is ground\nT166 is ground\nT167 is ground\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: reverse3(T165, .(T164, .(T166, .(T167, .(T168, .(T169, .(T170, [])))))), .(T170, .(T169, .(T168, .(T167, .(T166, .(T164, T165))))))), SCOPE: 9, CLAUSE: 2\n\nT164 is ground\nT165 is ground\nT166 is ground\nT167 is ground\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: reverse3(T165, .(T164, .(T166, .(T167, .(T168, .(T169, .(T170, [])))))), .(T170, .(T169, .(T168, .(T167, .(T166, .(T164, T165))))))), SCOPE: 9, CLAUSE: 3\n\nT164 is ground\nT165 is ground\nT166 is ground\nT167 is ground\nT168 is ground\nT169 is ground\nT170 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: reverse3(T212, .(T211, .(T213, .(T214, .(T215, .(T216, .(T217, .(T218, []))))))), .(T218, .(T217, .(T216, .(T215, .(T214, .(T213, .(T211, T212))))))))\n\nT211 is ground\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground\nT217 is ground\nT218 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: reverse3(T212, .(T211, .(T213, .(T214, .(T215, .(T216, .(T217, .(T218, []))))))), .(T218, .(T217, .(T216, .(T215, .(T214, .(T213, .(T211, T212)))))))), SCOPE: 10, CLAUSE: 2 | reverse3(T212, .(T211, .(T213, .(T214, .(T215, .(T216, .(T217, .(T218, []))))))), .(T218, .(T217, .(T216, .(T215, .(T214, .(T213, .(T211, T212)))))))), SCOPE: 10, CLAUSE: 3\n\nT211 is ground\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground\nT217 is ground\nT218 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: reverse3(T212, .(T211, .(T213, .(T214, .(T215, .(T216, .(T217, .(T218, []))))))), .(T218, .(T217, .(T216, .(T215, .(T214, .(T213, .(T211, T212)))))))), SCOPE: 10, CLAUSE: 2\n\nT211 is ground\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground\nT217 is ground\nT218 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: reverse3(T212, .(T211, .(T213, .(T214, .(T215, .(T216, .(T217, .(T218, []))))))), .(T218, .(T217, .(T216, .(T215, .(T214, .(T213, .(T211, T212)))))))), SCOPE: 10, CLAUSE: 3\n\nT211 is ground\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground\nT217 is ground\nT218 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: reverse3(T265, .(T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, [])))))))), .(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))\n\nT264 is ground\nT265 is ground\nT266 is ground\nT267 is ground\nT268 is ground\nT269 is ground\nT270 is ground\nT271 is ground\nT272 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="B: reverse3(T265, .(T264, T283), .(T272, T284))\n\nT264 is ground\nT265 is ground\nT272 is ground\nT283 is ground\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: reverse3(T265, .(T264, T283), .(T272, T284)), SCOPE: 11, CLAUSE: 2 | reverse3(T265, .(T264, T283), .(T272, T284)), SCOPE: 11, CLAUSE: 3\n\nT264 is ground\nT265 is ground\nT272 is ground\nT283 is ground\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: reverse3(T265, .(T264, T283), .(T272, T284)), SCOPE: 11, CLAUSE: 2\n\nT264 is ground\nT265 is ground\nT272 is ground\nT283 is ground\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: reverse3(T265, .(T264, T283), .(T272, T284)), SCOPE: 11, CLAUSE: 3\n\nT264 is ground\nT265 is ground\nT272 is ground\nT283 is ground\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: reverse3(T316, .(T315, .(T317, T318)), .(T319, T320))\n\nT315 is ground\nT316 is ground\nT317 is ground\nT318 is ground\nT319 is ground\nT320 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \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];
190 [label="190: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 235 [arrowhead = none ];
235 -> 4;

236 [label="ONLY EVAL with clause\npalindrome(X2) :- reverse(X2, X2).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 236 [arrowhead = none ];
236 -> 11;

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

238 [label="ONLY EVAL with clause\nreverse(X11, X12) :- reverse3(X11, [], X12).\nand substitutionT3 -> T8,\nX11 -> T8,\nX12 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 238 [arrowhead = none ];
238 -> 13;

239 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 239 [arrowhead = none ];
239 -> 15;

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

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

242 [label="EVAL with clause\nreverse3(.(X33, X34), X35, X36) :- reverse3(X34, .(X33, X35), X36).\nand substitutionX33 -> T19,\nX34 -> T20,\nT8 -> .(T19, T20),\nX35 -> [],\nX36 -> .(T19, T20)", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 242 [arrowhead = none ];
242 -> 27;

243 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 243 [arrowhead = none ];
243 -> 28;

244 [label="EVAL with clause\nreverse3([], X263, X263).\nand substitutionT8 -> [],\nX263 -> []", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 244 [arrowhead = none ];
244 -> 232;

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

246 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
27 -> 246 [arrowhead = none ];
246 -> 31;

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

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

249 [label="EVAL with clause\nreverse3(.(X57, X58), X59, X60) :- reverse3(X58, .(X57, X59), X60).\nand substitutionX57 -> T36,\nX58 -> T37,\nT20 -> .(T36, T37),\nT19 -> T38,\nX59 -> .(T38, []),\nX60 -> .(T38, .(T36, T37))", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 249 [arrowhead = none ];
249 -> 48;

250 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 250 [arrowhead = none ];
250 -> 49;

251 [label="EVAL with clause\nreverse3([], X260, X260).\nand substitutionT20 -> [],\nT19 -> T417,\nX260 -> .(T417, [])", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 251 [arrowhead = none ];
251 -> 229;

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

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

254 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 254 [arrowhead = none ];
254 -> 63;

255 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 255 [arrowhead = none ];
255 -> 64;

256 [label="EVAL with clause\nreverse3(.(X81, X82), X83, X84) :- reverse3(X82, .(X81, X83), X84).\nand substitutionX81 -> T59,\nX82 -> T60,\nT37 -> .(T59, T60),\nT36 -> T61,\nT38 -> T62,\nX83 -> .(T61, .(T62, [])),\nX84 -> .(T62, .(T61, .(T59, T60)))", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 256 [arrowhead = none ];
256 -> 67;

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

258 [label="EVAL with clause\nreverse3([], X257, X257).\nand substitutionT37 -> [],\nT36 -> T414,\nT38 -> T414,\nX257 -> .(T414, .(T414, [])),\nT413 -> T414", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 258 [arrowhead = none ];
258 -> 226;

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

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

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

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

263 [label="EVAL with clause\nreverse3(.(X105, X106), X107, X108) :- reverse3(X106, .(X105, X107), X108).\nand substitutionX105 -> T88,\nX106 -> T89,\nT60 -> .(T88, T89),\nT59 -> T90,\nT61 -> T91,\nT62 -> T92,\nX107 -> .(T90, .(T91, .(T92, []))),\nX108 -> .(T92, .(T91, .(T90, .(T88, T89))))", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 263 [arrowhead = none ];
263 -> 84;

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

265 [label="EVAL with clause\nreverse3([], X254, X254).\nand substitutionT60 -> [],\nT59 -> T408,\nT61 -> T407,\nT62 -> T408,\nX254 -> .(T408, .(T407, .(T408, []))),\nT406 -> T408", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 265 [arrowhead = none ];
265 -> 223;

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

267 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
84 -> 267 [arrowhead = none ];
267 -> 90;

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

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

270 [label="EVAL with clause\nreverse3(.(X129, X130), X131, X132) :- reverse3(X130, .(X129, X131), X132).\nand substitutionX129 -> T123,\nX130 -> T124,\nT89 -> .(T123, T124),\nT88 -> T125,\nT90 -> T126,\nT91 -> T127,\nT92 -> T128,\nX131 -> .(T125, .(T126, .(T127, .(T128, [])))),\nX132 -> .(T128, .(T127, .(T126, .(T125, .(T123, T124)))))", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 270 [arrowhead = none ];
270 -> 98;

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

272 [label="EVAL with clause\nreverse3([], X251, X251).\nand substitutionT89 -> [],\nT88 -> T399,\nT90 -> T398,\nT91 -> T398,\nT92 -> T399,\nX251 -> .(T399, .(T398, .(T398, .(T399, [])))),\nT396 -> T399,\nT397 -> T398", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 272 [arrowhead = none ];
272 -> 202;

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

274 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
98 -> 274 [arrowhead = none ];
274 -> 104;

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

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

277 [label="EVAL with clause\nreverse3(.(X153, X154), X155, X156) :- reverse3(X154, .(X153, X155), X156).\nand substitutionX153 -> T164,\nX154 -> T165,\nT124 -> .(T164, T165),\nT123 -> T166,\nT125 -> T167,\nT126 -> T168,\nT127 -> T169,\nT128 -> T170,\nX155 -> .(T166, .(T167, .(T168, .(T169, .(T170, []))))),\nX156 -> .(T170, .(T169, .(T168, .(T167, .(T166, .(T164, T165))))))", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 277 [arrowhead = none ];
277 -> 117;

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

279 [label="EVAL with clause\nreverse3([], X248, X248).\nand substitutionT124 -> [],\nT123 -> T387,\nT125 -> T386,\nT126 -> T385,\nT127 -> T386,\nT128 -> T387,\nX248 -> .(T387, .(T386, .(T385, .(T386, .(T387, []))))),\nT383 -> T387,\nT384 -> T386", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 279 [arrowhead = none ];
279 -> 196;

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

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

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

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

284 [label="EVAL with clause\nreverse3(.(X177, X178), X179, X180) :- reverse3(X178, .(X177, X179), X180).\nand substitutionX177 -> T211,\nX178 -> T212,\nT165 -> .(T211, T212),\nT164 -> T213,\nT166 -> T214,\nT167 -> T215,\nT168 -> T216,\nT169 -> T217,\nT170 -> T218,\nX179 -> .(T213, .(T214, .(T215, .(T216, .(T217, .(T218, [])))))),\nX180 -> .(T218, .(T217, .(T216, .(T215, .(T214, .(T213, .(T211, T212)))))))", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 284 [arrowhead = none ];
284 -> 126;

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

286 [label="EVAL with clause\nreverse3([], X245, X245).\nand substitutionT165 -> [],\nT164 -> T372,\nT166 -> T371,\nT167 -> T370,\nT168 -> T370,\nT169 -> T371,\nT170 -> T372,\nX245 -> .(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))),\nT367 -> T372,\nT368 -> T371,\nT369 -> T370", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 286 [arrowhead = none ];
286 -> 190;

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

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

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

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

291 [label="EVAL with clause\nreverse3(.(X201, X202), X203, X204) :- reverse3(X202, .(X201, X203), X204).\nand substitutionX201 -> T264,\nX202 -> T265,\nT212 -> .(T264, T265),\nT211 -> T266,\nT213 -> T267,\nT214 -> T268,\nT215 -> T269,\nT216 -> T270,\nT217 -> T271,\nT218 -> T272,\nX203 -> .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))),\nX204 -> .(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 291 [arrowhead = none ];
291 -> 143;

292 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 292 [arrowhead = none ];
292 -> 144;

293 [label="EVAL with clause\nreverse3([], X242, X242).\nand substitutionT212 -> [],\nT211 -> T354,\nT213 -> T353,\nT214 -> T352,\nT215 -> T351,\nT216 -> T352,\nT217 -> T353,\nT218 -> T354,\nX242 -> .(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))),\nT348 -> T354,\nT349 -> T353,\nT350 -> T352", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 293 [arrowhead = none ];
293 -> 182;

294 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 294 [arrowhead = none ];
294 -> 183;

295 [label="GENERALIZATION\nT283 <-- .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, [])))))))\nT284 <-- .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))\n\nNew Knowledge:\nT283 is ground\nT284 is ground", fontsize=14, style = filled, fillcolor = violet];
143 -> 295 [arrowhead = none ];
295 -> 148;

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

297 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
153 -> 297 [arrowhead = none ];
297 -> 158;

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

299 [label="EVAL with clause\nreverse3(.(X229, X230), X231, X232) :- reverse3(X230, .(X229, X231), X232).\nand substitutionX229 -> T315,\nX230 -> T316,\nT265 -> .(T315, T316),\nT264 -> T317,\nT283 -> T318,\nX231 -> .(T317, T318),\nT272 -> T319,\nT284 -> T320,\nX232 -> .(T319, T320)", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 299 [arrowhead = none ];
299 -> 163;

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

301 [label="EVAL with clause\nreverse3([], X239, X239).\nand substitutionT265 -> [],\nT264 -> T332,\nT283 -> T333,\nX239 -> .(T332, T333),\nT272 -> T332,\nT284 -> T333", fontsize=14, style = filled, fillcolor = lightblue];
159 -> 301 [arrowhead = none ];
301 -> 177;

302 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
159 -> 302 [arrowhead = none ];
302 -> 178;

303 [label="INSTANCE with matching:\nT265 -> T316\nT264 -> T315\nT283 -> .(T317, T318)\nT272 -> T319\nT284 -> T320", fontsize=14, style = filled, fillcolor = lightgrey];
163 -> 303 [arrowhead = none , style=dashed];
303 -> 148[style=dashed];

304 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 304 [arrowhead = none ];
304 -> 179;

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

306 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
190 -> 306 [arrowhead = none ];
306 -> 192;

307 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 307 [arrowhead = none ];
307 -> 198;

308 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
202 -> 308 [arrowhead = none ];
308 -> 204;

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

310 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
226 -> 310 [arrowhead = none ];
310 -> 228;

311 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
229 -> 311 [arrowhead = none ];
311 -> 231;

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

}

(2) Obligation:

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

palindromeA_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U1_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3B_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U2_ggggg(T315, T316, T317, T318, T319, T320, reverse3B_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3B_in_ggggg([], T332, T333, T332, T333) → reverse3B_out_ggggg([], T332, T333, T332, T333)
U2_ggggg(T315, T316, T317, T318, T319, T320, reverse3B_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3B_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U1_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeA_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeA_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeA_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeA_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeA_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeA_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeA_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeA_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeA_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeA_in_g(.(T408, .(T407, .(T408, [])))) → palindromeA_out_g(.(T408, .(T407, .(T408, []))))
palindromeA_in_g(.(T414, .(T414, []))) → palindromeA_out_g(.(T414, .(T414, [])))
palindromeA_in_g(.(T417, [])) → palindromeA_out_g(.(T417, []))
palindromeA_in_g([]) → palindromeA_out_g([])

Pi is empty.

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

PALINDROMEA_IN_G(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U1_G(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
PALINDROMEA_IN_G(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → REVERSE3B_IN_GGGGG(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))
REVERSE3B_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → U2_GGGGG(T315, T316, T317, T318, T319, T320, reverse3B_in_ggggg(T316, T315, .(T317, T318), T319, T320))
REVERSE3B_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3B_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)

The TRS R consists of the following rules:

palindromeA_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U1_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3B_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U2_ggggg(T315, T316, T317, T318, T319, T320, reverse3B_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3B_in_ggggg([], T332, T333, T332, T333) → reverse3B_out_ggggg([], T332, T333, T332, T333)
U2_ggggg(T315, T316, T317, T318, T319, T320, reverse3B_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3B_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U1_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeA_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeA_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeA_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeA_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeA_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeA_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeA_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeA_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeA_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeA_in_g(.(T408, .(T407, .(T408, [])))) → palindromeA_out_g(.(T408, .(T407, .(T408, []))))
palindromeA_in_g(.(T414, .(T414, []))) → palindromeA_out_g(.(T414, .(T414, [])))
palindromeA_in_g(.(T417, [])) → palindromeA_out_g(.(T417, []))
palindromeA_in_g([]) → palindromeA_out_g([])

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

(4) Obligation:

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

PALINDROMEA_IN_G(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U1_G(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
PALINDROMEA_IN_G(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → REVERSE3B_IN_GGGGG(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))
REVERSE3B_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → U2_GGGGG(T315, T316, T317, T318, T319, T320, reverse3B_in_ggggg(T316, T315, .(T317, T318), T319, T320))
REVERSE3B_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3B_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)

The TRS R consists of the following rules:

palindromeA_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U1_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3B_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U2_ggggg(T315, T316, T317, T318, T319, T320, reverse3B_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3B_in_ggggg([], T332, T333, T332, T333) → reverse3B_out_ggggg([], T332, T333, T332, T333)
U2_ggggg(T315, T316, T317, T318, T319, T320, reverse3B_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3B_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U1_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeA_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeA_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeA_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeA_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeA_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeA_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeA_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeA_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeA_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeA_in_g(.(T408, .(T407, .(T408, [])))) → palindromeA_out_g(.(T408, .(T407, .(T408, []))))
palindromeA_in_g(.(T414, .(T414, []))) → palindromeA_out_g(.(T414, .(T414, [])))
palindromeA_in_g(.(T417, [])) → palindromeA_out_g(.(T417, []))
palindromeA_in_g([]) → palindromeA_out_g([])

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(6) Obligation:

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

REVERSE3B_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3B_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)

The TRS R consists of the following rules:

palindromeA_in_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → U1_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_in_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
reverse3B_in_ggggg(.(T315, T316), T317, T318, T319, T320) → U2_ggggg(T315, T316, T317, T318, T319, T320, reverse3B_in_ggggg(T316, T315, .(T317, T318), T319, T320))
reverse3B_in_ggggg([], T332, T333, T332, T333) → reverse3B_out_ggggg([], T332, T333, T332, T333)
U2_ggggg(T315, T316, T317, T318, T319, T320, reverse3B_out_ggggg(T316, T315, .(T317, T318), T319, T320)) → reverse3B_out_ggggg(.(T315, T316), T317, T318, T319, T320)
U1_g(T272, T271, T270, T269, T268, T267, T266, T264, T265, reverse3B_out_ggggg(T265, T264, .(T266, .(T267, .(T268, .(T269, .(T270, .(T271, .(T272, []))))))), T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265))))))))) → palindromeA_out_g(.(T272, .(T271, .(T270, .(T269, .(T268, .(T267, .(T266, .(T264, T265)))))))))
palindromeA_in_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, [])))))))) → palindromeA_out_g(.(T354, .(T353, .(T352, .(T351, .(T352, .(T353, .(T354, []))))))))
palindromeA_in_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, []))))))) → palindromeA_out_g(.(T372, .(T371, .(T370, .(T370, .(T371, .(T372, [])))))))
palindromeA_in_g(.(T387, .(T386, .(T385, .(T386, .(T387, [])))))) → palindromeA_out_g(.(T387, .(T386, .(T385, .(T386, .(T387, []))))))
palindromeA_in_g(.(T399, .(T398, .(T398, .(T399, []))))) → palindromeA_out_g(.(T399, .(T398, .(T398, .(T399, [])))))
palindromeA_in_g(.(T408, .(T407, .(T408, [])))) → palindromeA_out_g(.(T408, .(T407, .(T408, []))))
palindromeA_in_g(.(T414, .(T414, []))) → palindromeA_out_g(.(T414, .(T414, [])))
palindromeA_in_g(.(T417, [])) → palindromeA_out_g(.(T417, []))
palindromeA_in_g([]) → palindromeA_out_g([])

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

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

REVERSE3B_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3B_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)

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

(9) PiDPToQDPProof (EQUIVALENT transformation)

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

(10) Obligation:

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

REVERSE3B_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3B_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)

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

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

• REVERSE3B_IN_GGGGG(.(T315, T316), T317, T318, T319, T320) → REVERSE3B_IN_GGGGG(T316, T315, .(T317, T318), T319, T320)
  The graph contains the following edges 1 > 1, 1 > 2, 4 >= 4, 5 >= 5

(12) YES