Left Termination proof of /tmp/tmpf_VF

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 189 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 344 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 18 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 51 ms)

        ↳11 QDP

        ↳12 Rewriting (⇔, 17 ms)

        ↳13 QDP

        ↳14 QDPOrderProof (⇔, 182 ms)

        ↳15 QDP

        ↳16 DependencyGraphProof (⇔, 0 ms)

        ↳17 QDP

        ↳18 UsableRulesProof (⇔, 0 ms)

        ↳19 QDP

        ↳20 QReductionProof (⇔, 0 ms)

        ↳21 QDP

        ↳22 QDPSizeChangeProof (⇔, 0 ms)

        ↳23 YES

    ↳24 PiDP

        ↳25 UsableRulesProof (⇔, 11 ms)

        ↳26 PiDP

        ↳27 PiDPToQDPProof (⇒, 0 ms)

        ↳28 QDP

        ↳29 QDPSizeChangeProof (⇔, 0 ms)

        ↳30 YES

(0) Obligation:

Clauses:

ackermann(0, N, s(N)).
ackermann(s(M), 0, Res) :- ackermann(M, s(0), Res).
ackermann(s(M), s(N), Res) :- ','(ackermann(s(M), N, Res1), ackermann(M, Res1, Res)).

Query: ackermann(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: ackermann(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: ackermann(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | ackermann(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ackermann(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | ackermann(0, T5, T3), SCOPE: 1, CLAUSE: 1 | ackermann(0, T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ackermann(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ackermann(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX2 is free\nackermann(T1, T2, T3) !=? ackermann(0, X2, s(X2))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ackermann(0, T5, T3), SCOPE: 1, CLAUSE: 1 | ackermann(0, T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ackermann(0, T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ackermann(T8, s(0), T10) | ackermann(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ackermann(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX2 is free\nX10 is free\nX11 is free\nackermann(T1, T2, T3) !=? ackermann(0, X2, s(X2))\nackermann(T1, T2, T3) !=? ackermann(s(X10), 0, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ackermann(T8, s(0), T10), SCOPE: 2, CLAUSE: 0 | ackermann(T8, s(0), T10), SCOPE: 2, CLAUSE: 1 | ackermann(T8, s(0), T10), SCOPE: 2, CLAUSE: 2 | ?_2 | ackermann(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ackermann(T8, s(0), T10), SCOPE: 2, CLAUSE: 0\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ackermann(T8, s(0), T10), SCOPE: 2, CLAUSE: 1 | ackermann(T8, s(0), T10), SCOPE: 2, CLAUSE: 2 | ?_2 | ackermann(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ackermann(T8, s(0), T10), SCOPE: 2, CLAUSE: 2 | ?_2 | ackermann(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ackermann(T8, s(0), T10), SCOPE: 2, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ?_2 | ackermann(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="B: ','(ackermann(s(T20), 0, X36), ackermann(T20, X36, T22))\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="E: ackermann(s(T20), 0, X36)\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ackermann(T20, T23, T22)\n\nT20 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ackermann(s(T20), 0, X36), SCOPE: 3, CLAUSE: 0 | ackermann(s(T20), 0, X36), SCOPE: 3, CLAUSE: 1 | ackermann(s(T20), 0, X36), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ackermann(s(T20), 0, X36), SCOPE: 3, CLAUSE: 1 | ackermann(s(T20), 0, X36), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ackermann(s(T20), 0, X36), SCOPE: 3, CLAUSE: 1\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ackermann(s(T20), 0, X36), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="F: ackermann(T28, s(0), X60)\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ackermann(T28, s(0), X60), SCOPE: 4, CLAUSE: 0 | ackermann(T28, s(0), X60), SCOPE: 4, CLAUSE: 1 | ackermann(T28, s(0), X60), SCOPE: 4, CLAUSE: 2\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ackermann(T28, s(0), X60), SCOPE: 4, CLAUSE: 0\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ackermann(T28, s(0), X60), SCOPE: 4, CLAUSE: 1 | ackermann(T28, s(0), X60), SCOPE: 4, CLAUSE: 2\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: ackermann(T28, s(0), X60), SCOPE: 4, CLAUSE: 2\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="G: ','(ackermann(s(T32), 0, X82), ackermann(T32, X82, X83))\n\nT32 is ground\nX83 is free\nX82 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: ackermann(s(T32), 0, X82)\n\nT32 is ground\nX82 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="H: ackermann(T32, T33, X83)\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ackermann(T32, T33, X83), SCOPE: 5, CLAUSE: 0 | ackermann(T32, T33, X83), SCOPE: 5, CLAUSE: 1 | ackermann(T32, T33, X83), SCOPE: 5, CLAUSE: 2\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ackermann(T32, T33, X83), SCOPE: 5, CLAUSE: 0\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: ackermann(T32, T33, X83), SCOPE: 5, CLAUSE: 1 | ackermann(T32, T33, X83), SCOPE: 5, CLAUSE: 2\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ackermann(T32, T33, X83), SCOPE: 5, CLAUSE: 1\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ackermann(T32, T33, X83), SCOPE: 5, CLAUSE: 2\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ackermann(T45, s(0), X109)\n\nT45 is ground\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="I: ','(ackermann(s(T50), T51, X124), ackermann(T50, X124, X125))\n\nT50 is ground\nT51 is ground\nX125 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ackermann(s(T50), T51, X124)\n\nT50 is ground\nT51 is ground\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ackermann(T50, T52, X125)\n\nT50 is ground\nT52 is ground\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ackermann(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ','(ackermann(s(T62), T63, X146), ackermann(T62, X146, T65))\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ','(ackermann(s(T62), T63, X146), ackermann(T62, X146, T65)), SCOPE: 6, CLAUSE: 0 | ','(ackermann(s(T62), T63, X146), ackermann(T62, X146, T65)), SCOPE: 6, CLAUSE: 1 | ','(ackermann(s(T62), T63, X146), ackermann(T62, X146, T65)), SCOPE: 6, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ','(ackermann(s(T62), T63, X146), ackermann(T62, X146, T65)), SCOPE: 6, CLAUSE: 1 | ','(ackermann(s(T62), T63, X146), ackermann(T62, X146, T65)), SCOPE: 6, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ','(ackermann(s(T62), T63, X146), ackermann(T62, X146, T65)), SCOPE: 6, CLAUSE: 1\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(ackermann(s(T62), T63, X146), ackermann(T62, X146, T65)), SCOPE: 6, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="C: ','(ackermann(T70, s(0), X162), ackermann(T70, X162, T65))\n\nT70 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ackermann(T70, s(0), X162)\n\nT70 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ackermann(T70, T71, T65)\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="D: ','(','(ackermann(s(T78), T79, X181), ackermann(T78, X181, X182)), ackermann(T78, X182, T65))\n\nT78 is ground\nT79 is ground\nX182 is free\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ackermann(s(T78), T79, X181)\n\nT78 is ground\nT79 is ground\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="J: ','(ackermann(T78, T80, X182), ackermann(T78, X182, T65))\n\nT78 is ground\nT80 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: ackermann(T78, T80, X182)\n\nT78 is ground\nT80 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ackermann(T78, T83, T65)\n\nT78 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 200 [arrowhead = none ];
200 -> 5;

201 [label="EVAL with clause\nackermann(0, X2, s(X2)).\nand substitutionT1 -> 0,\nT2 -> T5,\nX2 -> T5,\nT3 -> s(T5)", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 201 [arrowhead = none ];
201 -> 10;

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

203 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 203 [arrowhead = none ];
203 -> 17;

204 [label="EVAL with clause\nackermann(s(X10), 0, X11) :- ackermann(X10, s(0), X11).\nand substitutionX10 -> T8,\nT1 -> s(T8),\nT2 -> 0,\nT3 -> T10,\nX11 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 204 [arrowhead = none ];
204 -> 25;

205 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 205 [arrowhead = none ];
205 -> 29;

206 [label="BACKTRACK\nfor clause: ackermann(s(M), 0, Res) :- ackermann(M, s(0), Res)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 206 [arrowhead = none ];
206 -> 19;

207 [label="BACKTRACK\nfor clause: ackermann(s(M), s(N), Res) :- ','(ackermann(s(M), N, Res1), ackermann(M, Res1, Res))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 207 [arrowhead = none ];
207 -> 23;

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

209 [label="EVAL with clause\nackermann(s(X143), s(X144), X145) :- ','(ackermann(s(X143), X144, X146), ackermann(X143, X146, X145)).\nand substitutionX143 -> T62,\nT1 -> s(T62),\nX144 -> T63,\nT2 -> s(T63),\nT3 -> T65,\nX145 -> T65,\nT64 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 209 [arrowhead = none ];
209 -> 178;

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

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

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

213 [label="EVAL with clause\nackermann(0, X16, s(X16)).\nand substitutionT8 -> 0,\nX16 -> s(0),\nT10 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 213 [arrowhead = none ];
213 -> 39;

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

215 [label="BACKTRACK\nfor clause: ackermann(s(M), 0, Res) :- ackermann(M, s(0), Res)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 215 [arrowhead = none ];
215 -> 43;

216 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 216 [arrowhead = none ];
216 -> 42;

217 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
43 -> 217 [arrowhead = none ];
217 -> 49;

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

219 [label="EVAL with clause\nackermann(s(X33), s(X34), X35) :- ','(ackermann(s(X33), X34, X36), ackermann(X33, X36, X35)).\nand substitutionX33 -> T20,\nT8 -> s(T20),\nX34 -> 0,\nT10 -> T22,\nX35 -> T22,\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 219 [arrowhead = none ];
219 -> 57;

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

221 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 221 [arrowhead = none ];
221 -> 176;

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

223 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nT23 is ground\nreplacements:X36 -> T23", fontsize=14, style = filled, fillcolor = violet];
57 -> 223 [arrowhead = none ];
223 -> 68;

224 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
63 -> 224 [arrowhead = none ];
224 -> 70;

225 [label="INSTANCE with matching:\nT1 -> T20\nT2 -> T23\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
68 -> 225 [arrowhead = none , style=dashed];
225 -> 1[style=dashed];

226 [label="BACKTRACK\nfor clause: ackermann(0, N, s(N))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 226 [arrowhead = none ];
226 -> 74;

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

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

229 [label="ONLY EVAL with clause\nackermann(s(X58), 0, X59) :- ackermann(X58, s(0), X59).\nand substitutionT20 -> T28,\nX58 -> T28,\nX36 -> X60,\nX59 -> X60", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 229 [arrowhead = none ];
229 -> 84;

230 [label="BACKTRACK\nfor clause: ackermann(s(M), s(N), Res) :- ','(ackermann(s(M), N, Res1), ackermann(M, Res1, Res))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 230 [arrowhead = none ];
230 -> 175;

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

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

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

234 [label="EVAL with clause\nackermann(0, X67, s(X67)).\nand substitutionT28 -> 0,\nX67 -> s(0),\nX60 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 234 [arrowhead = none ];
234 -> 107;

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

236 [label="BACKTRACK\nfor clause: ackermann(s(M), 0, Res) :- ackermann(M, s(0), Res)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 236 [arrowhead = none ];
236 -> 110;

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

238 [label="EVAL with clause\nackermann(s(X79), s(X80), X81) :- ','(ackermann(s(X79), X80, X82), ackermann(X79, X82, X81)).\nand substitutionX79 -> T32,\nT28 -> s(T32),\nX80 -> 0,\nX60 -> X83,\nX81 -> X83", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 238 [arrowhead = none ];
238 -> 114;

239 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 239 [arrowhead = none ];
239 -> 116;

240 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
114 -> 240 [arrowhead = none ];
240 -> 121;

241 [label="SPLIT 2\nnew knowledge:\nT32 is ground\nT33 is ground\nreplacements:X82 -> T33", fontsize=14, style = filled, fillcolor = violet];
114 -> 241 [arrowhead = none ];
241 -> 122;

242 [label="INSTANCE with matching:\nT20 -> T32\nX36 -> X82", fontsize=14, style = filled, fillcolor = lightgrey];
121 -> 242 [arrowhead = none , style=dashed];
242 -> 63[style=dashed];

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

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

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

246 [label="EVAL with clause\nackermann(0, X94, s(X94)).\nand substitutionT32 -> 0,\nT33 -> T40,\nX94 -> T40,\nX83 -> s(T40)", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 246 [arrowhead = none ];
246 -> 136;

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

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

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

250 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 250 [arrowhead = none ];
250 -> 138;

251 [label="EVAL with clause\nackermann(s(X107), 0, X108) :- ackermann(X107, s(0), X108).\nand substitutionX107 -> T45,\nT32 -> s(T45),\nT33 -> 0,\nX83 -> X109,\nX108 -> X109", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 251 [arrowhead = none ];
251 -> 147;

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

253 [label="EVAL with clause\nackermann(s(X121), s(X122), X123) :- ','(ackermann(s(X121), X122, X124), ackermann(X121, X124, X123)).\nand substitutionX121 -> T50,\nT32 -> s(T50),\nX122 -> T51,\nT33 -> s(T51),\nX83 -> X125,\nX123 -> X125", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 253 [arrowhead = none ];
253 -> 152;

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

255 [label="INSTANCE with matching:\nT28 -> T45\nX60 -> X109", fontsize=14, style = filled, fillcolor = lightgrey];
147 -> 255 [arrowhead = none , style=dashed];
255 -> 84[style=dashed];

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

257 [label="SPLIT 2\nnew knowledge:\nT50 is ground\nT51 is ground\nT52 is ground\nreplacements:X124 -> T52", fontsize=14, style = filled, fillcolor = violet];
152 -> 257 [arrowhead = none ];
257 -> 165;

258 [label="INSTANCE with matching:\nT32 -> s(T50)\nT33 -> T51\nX83 -> X124", fontsize=14, style = filled, fillcolor = lightgrey];
164 -> 258 [arrowhead = none , style=dashed];
258 -> 122[style=dashed];

259 [label="INSTANCE with matching:\nT32 -> T50\nT33 -> T52\nX83 -> X125", fontsize=14, style = filled, fillcolor = lightgrey];
165 -> 259 [arrowhead = none , style=dashed];
259 -> 122[style=dashed];

260 [label="BACKTRACK\nfor clause: ackermann(s(M), s(N), Res) :- ','(ackermann(s(M), N, Res1), ackermann(M, Res1, Res))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 260 [arrowhead = none ];
260 -> 177;

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

262 [label="BACKTRACK\nfor clause: ackermann(0, N, s(N))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 262 [arrowhead = none ];
262 -> 183;

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

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

265 [label="EVAL with clause\nackermann(s(X160), 0, X161) :- ackermann(X160, s(0), X161).\nand substitutionT62 -> T70,\nX160 -> T70,\nT63 -> 0,\nX146 -> X162,\nX161 -> X162", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 265 [arrowhead = none ];
265 -> 186;

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

267 [label="EVAL with clause\nackermann(s(X178), s(X179), X180) :- ','(ackermann(s(X178), X179, X181), ackermann(X178, X181, X180)).\nand substitutionT62 -> T78,\nX178 -> T78,\nX179 -> T79,\nT63 -> s(T79),\nX146 -> X182,\nX180 -> X182", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 267 [arrowhead = none ];
267 -> 194;

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

269 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
186 -> 269 [arrowhead = none ];
269 -> 190;

270 [label="SPLIT 2\nnew knowledge:\nT70 is ground\nT71 is ground\nreplacements:X162 -> T71", fontsize=14, style = filled, fillcolor = violet];
186 -> 270 [arrowhead = none ];
270 -> 191;

271 [label="INSTANCE with matching:\nT28 -> T70\nX60 -> X162", fontsize=14, style = filled, fillcolor = lightgrey];
190 -> 271 [arrowhead = none , style=dashed];
271 -> 84[style=dashed];

272 [label="INSTANCE with matching:\nT1 -> T70\nT2 -> T71\nT3 -> T65", fontsize=14, style = filled, fillcolor = lightgrey];
191 -> 272 [arrowhead = none , style=dashed];
272 -> 1[style=dashed];

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

274 [label="SPLIT 2\nnew knowledge:\nT78 is ground\nT79 is ground\nT80 is ground\nreplacements:X181 -> T80", fontsize=14, style = filled, fillcolor = violet];
194 -> 274 [arrowhead = none ];
274 -> 197;

275 [label="INSTANCE with matching:\nT32 -> s(T78)\nT33 -> T79\nX83 -> X181", fontsize=14, style = filled, fillcolor = lightgrey];
196 -> 275 [arrowhead = none , style=dashed];
275 -> 122[style=dashed];

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

277 [label="SPLIT 2\nnew knowledge:\nT78 is ground\nT80 is ground\nT83 is ground\nreplacements:X182 -> T83", fontsize=14, style = filled, fillcolor = violet];
197 -> 277 [arrowhead = none ];
277 -> 199;

278 [label="INSTANCE with matching:\nT32 -> T78\nT33 -> T80\nX83 -> X182", fontsize=14, style = filled, fillcolor = lightgrey];
198 -> 278 [arrowhead = none , style=dashed];
278 -> 122[style=dashed];

279 [label="INSTANCE with matching:\nT1 -> T78\nT2 -> T83\nT3 -> T65", fontsize=14, style = filled, fillcolor = lightgrey];
199 -> 279 [arrowhead = none , style=dashed];
279 -> 1[style=dashed];

}

(2) Obligation:

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

ackermannA_in_gga(0, T5, s(T5)) → ackermannA_out_gga(0, T5, s(T5))
ackermannA_in_gga(s(0), 0, s(s(0))) → ackermannA_out_gga(s(0), 0, s(s(0)))
ackermannA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackermannE_in_ga(T20, T23))
ackermannE_in_ga(T28, X60) → U4_ga(T28, X60, ackermannF_in_ga(T28, X60))
ackermannF_in_ga(0, s(s(0))) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermannE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
ackermannH_in_gga(0, T40, s(T40)) → ackermannH_out_gga(0, T40, s(T40))
ackermannH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermannF_in_ga(T45, X109))
U6_gga(T45, X109, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
ackermannH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermannE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermannA_in_gga(T20, T23, T22))
ackermannA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackermannF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermannF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermannA_in_gga(T70, T71, T65))
ackermannA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermannA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermannA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackermannA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermannA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermannA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermannA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermannA_out_gga(s(s(T20)), 0, T22)

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

ACKERMANNA_IN_GGA(s(s(T20)), 0, T22) → U1_GGA(T20, T22, pB_in_gaa(T20, X36, T22))
ACKERMANNA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackermannE_in_ga(T20, T23))
PB_IN_GAA(T20, T23, T22) → ACKERMANNE_IN_GA(T20, T23)
ACKERMANNE_IN_GA(T28, X60) → U4_GA(T28, X60, ackermannF_in_ga(T28, X60))
ACKERMANNE_IN_GA(T28, X60) → ACKERMANNF_IN_GA(T28, X60)
ACKERMANNF_IN_GA(s(T32), X83) → U5_GA(T32, X83, pG_in_gaa(T32, X82, X83))
ACKERMANNF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackermannE_in_ga(T32, T33))
PG_IN_GAA(T32, T33, X83) → ACKERMANNE_IN_GA(T32, T33)
U10_GAA(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_GAA(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
U10_GAA(T32, T33, X83, ackermannE_out_ga(T32, T33)) → ACKERMANNH_IN_GGA(T32, T33, X83)
ACKERMANNH_IN_GGA(s(T45), 0, X109) → U6_GGA(T45, X109, ackermannF_in_ga(T45, X109))
ACKERMANNH_IN_GGA(s(T45), 0, X109) → ACKERMANNF_IN_GA(T45, X109)
ACKERMANNH_IN_GGA(s(T50), s(T51), X125) → U7_GGA(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ACKERMANNH_IN_GGA(s(T50), s(T51), X125) → PI_IN_GGAA(T50, T51, X124, X125)
PI_IN_GGAA(T50, T51, T52, X125) → U12_GGAA(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
PI_IN_GGAA(T50, T51, T52, X125) → ACKERMANNH_IN_GGA(s(T50), T51, T52)
U12_GGAA(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_GGAA(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
U12_GGAA(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → ACKERMANNH_IN_GGA(T50, T52, X125)
U8_GAA(T20, T23, T22, ackermannE_out_ga(T20, T23)) → U9_GAA(T20, T23, T22, ackermannA_in_gga(T20, T23, T22))
U8_GAA(T20, T23, T22, ackermannE_out_ga(T20, T23)) → ACKERMANNA_IN_GGA(T20, T23, T22)
ACKERMANNA_IN_GGA(s(T70), s(0), T65) → U2_GGA(T70, T65, pC_in_gaa(T70, X162, T65))
ACKERMANNA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackermannF_in_ga(T70, T71))
PC_IN_GAA(T70, T71, T65) → ACKERMANNF_IN_GA(T70, T71)
U14_GAA(T70, T71, T65, ackermannF_out_ga(T70, T71)) → U15_GAA(T70, T71, T65, ackermannA_in_gga(T70, T71, T65))
U14_GAA(T70, T71, T65, ackermannF_out_ga(T70, T71)) → ACKERMANNA_IN_GGA(T70, T71, T65)
ACKERMANNA_IN_GGA(s(T78), s(s(T79)), T65) → U3_GGA(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
ACKERMANNA_IN_GGA(s(T78), s(s(T79)), T65) → PD_IN_GGAAA(T78, T79, X181, X182, T65)
PD_IN_GGAAA(T78, T79, T80, X182, T65) → U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
PD_IN_GGAAA(T78, T79, T80, X182, T65) → ACKERMANNH_IN_GGA(s(T78), T79, T80)
U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → U17_GGAAA(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80, X182, T65)
PJ_IN_GGAA(T78, T80, T83, T65) → U18_GGAA(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
PJ_IN_GGAA(T78, T80, T83, T65) → ACKERMANNH_IN_GGA(T78, T80, T83)
U18_GGAA(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → U19_GGAA(T78, T80, T83, T65, ackermannA_in_gga(T78, T83, T65))
U18_GGAA(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → ACKERMANNA_IN_GGA(T78, T83, T65)

The TRS R consists of the following rules:

ackermannA_in_gga(0, T5, s(T5)) → ackermannA_out_gga(0, T5, s(T5))
ackermannA_in_gga(s(0), 0, s(s(0))) → ackermannA_out_gga(s(0), 0, s(s(0)))
ackermannA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackermannE_in_ga(T20, T23))
ackermannE_in_ga(T28, X60) → U4_ga(T28, X60, ackermannF_in_ga(T28, X60))
ackermannF_in_ga(0, s(s(0))) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermannE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
ackermannH_in_gga(0, T40, s(T40)) → ackermannH_out_gga(0, T40, s(T40))
ackermannH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermannF_in_ga(T45, X109))
U6_gga(T45, X109, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
ackermannH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermannE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermannA_in_gga(T20, T23, T22))
ackermannA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackermannF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermannF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermannA_in_gga(T70, T71, T65))
ackermannA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermannA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermannA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackermannA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermannA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermannA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermannA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermannA_out_gga(s(s(T20)), 0, T22)

The argument filtering Pi contains the following mapping:
ackermannA_in_gga(x1, x2, x3) = ackermannA_in_gga(x1, x2)
0 = 0
ackermannA_out_gga(x1, x2, x3) = ackermannA_out_gga(x1, x2, x3)
s(x1) = s(x1)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4) = U8_gaa(x1, x4)
ackermannE_in_ga(x1, x2) = ackermannE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackermannF_in_ga(x1, x2) = ackermannF_in_ga(x1)
ackermannF_out_ga(x1, x2) = ackermannF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackermannE_out_ga(x1, x2) = ackermannE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackermannH_in_gga(x1, x2, x3) = ackermannH_in_gga(x1, x2)
ackermannH_out_gga(x1, x2, x3) = ackermannH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4) = U9_gaa(x1, x2, x4)
U2_gga(x1, x2, x3) = U2_gga(x1, x3)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
U14_gaa(x1, x2, x3, x4) = U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4) = U15_gaa(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
pD_in_ggaaa(x1, x2, x3, x4, x5) = pD_in_ggaaa(x1, x2)
U16_ggaaa(x1, x2, x3, x4, x5, x6) = U16_ggaaa(x1, x2, x6)
U17_ggaaa(x1, x2, x3, x4, x5, x6) = U17_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4) = pJ_in_ggaa(x1, x2)
U18_ggaa(x1, x2, x3, x4, x5) = U18_ggaa(x1, x2, x5)
U19_ggaa(x1, x2, x3, x4, x5) = U19_ggaa(x1, x2, x3, x5)
pJ_out_ggaa(x1, x2, x3, x4) = pJ_out_ggaa(x1, x2, x3, x4)
pD_out_ggaaa(x1, x2, x3, x4, x5) = pD_out_ggaaa(x1, x2, x3, x4, x5)
pC_out_gaa(x1, x2, x3) = pC_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
ACKERMANNA_IN_GGA(x1, x2, x3) = ACKERMANNA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3) = U1_GGA(x1, x3)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4) = U8_GAA(x1, x4)
ACKERMANNE_IN_GA(x1, x2) = ACKERMANNE_IN_GA(x1)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
ACKERMANNF_IN_GA(x1, x2) = ACKERMANNF_IN_GA(x1)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
PG_IN_GAA(x1, x2, x3) = PG_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x1, x4)
U11_GAA(x1, x2, x3, x4) = U11_GAA(x1, x2, x4)
ACKERMANNH_IN_GGA(x1, x2, x3) = ACKERMANNH_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3) = U6_GGA(x1, x3)
U7_GGA(x1, x2, x3, x4) = U7_GGA(x1, x2, x4)
PI_IN_GGAA(x1, x2, x3, x4) = PI_IN_GGAA(x1, x2)
U12_GGAA(x1, x2, x3, x4, x5) = U12_GGAA(x1, x2, x5)
U13_GGAA(x1, x2, x3, x4, x5) = U13_GGAA(x1, x2, x3, x5)
U9_GAA(x1, x2, x3, x4) = U9_GAA(x1, x2, x4)
U2_GGA(x1, x2, x3) = U2_GGA(x1, x3)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x1, x4)
U15_GAA(x1, x2, x3, x4) = U15_GAA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
PD_IN_GGAAA(x1, x2, x3, x4, x5) = PD_IN_GGAAA(x1, x2)
U16_GGAAA(x1, x2, x3, x4, x5, x6) = U16_GGAAA(x1, x2, x6)
U17_GGAAA(x1, x2, x3, x4, x5, x6) = U17_GGAAA(x1, x2, x3, x6)
PJ_IN_GGAA(x1, x2, x3, x4) = PJ_IN_GGAA(x1, x2)
U18_GGAA(x1, x2, x3, x4, x5) = U18_GGAA(x1, x2, x5)
U19_GGAA(x1, x2, x3, x4, x5) = U19_GGAA(x1, x2, x3, x5)

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

(4) Obligation:

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

ACKERMANNA_IN_GGA(s(s(T20)), 0, T22) → U1_GGA(T20, T22, pB_in_gaa(T20, X36, T22))
ACKERMANNA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackermannE_in_ga(T20, T23))
PB_IN_GAA(T20, T23, T22) → ACKERMANNE_IN_GA(T20, T23)
ACKERMANNE_IN_GA(T28, X60) → U4_GA(T28, X60, ackermannF_in_ga(T28, X60))
ACKERMANNE_IN_GA(T28, X60) → ACKERMANNF_IN_GA(T28, X60)
ACKERMANNF_IN_GA(s(T32), X83) → U5_GA(T32, X83, pG_in_gaa(T32, X82, X83))
ACKERMANNF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackermannE_in_ga(T32, T33))
PG_IN_GAA(T32, T33, X83) → ACKERMANNE_IN_GA(T32, T33)
U10_GAA(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_GAA(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
U10_GAA(T32, T33, X83, ackermannE_out_ga(T32, T33)) → ACKERMANNH_IN_GGA(T32, T33, X83)
ACKERMANNH_IN_GGA(s(T45), 0, X109) → U6_GGA(T45, X109, ackermannF_in_ga(T45, X109))
ACKERMANNH_IN_GGA(s(T45), 0, X109) → ACKERMANNF_IN_GA(T45, X109)
ACKERMANNH_IN_GGA(s(T50), s(T51), X125) → U7_GGA(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ACKERMANNH_IN_GGA(s(T50), s(T51), X125) → PI_IN_GGAA(T50, T51, X124, X125)
PI_IN_GGAA(T50, T51, T52, X125) → U12_GGAA(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
PI_IN_GGAA(T50, T51, T52, X125) → ACKERMANNH_IN_GGA(s(T50), T51, T52)
U12_GGAA(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_GGAA(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
U12_GGAA(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → ACKERMANNH_IN_GGA(T50, T52, X125)
U8_GAA(T20, T23, T22, ackermannE_out_ga(T20, T23)) → U9_GAA(T20, T23, T22, ackermannA_in_gga(T20, T23, T22))
U8_GAA(T20, T23, T22, ackermannE_out_ga(T20, T23)) → ACKERMANNA_IN_GGA(T20, T23, T22)
ACKERMANNA_IN_GGA(s(T70), s(0), T65) → U2_GGA(T70, T65, pC_in_gaa(T70, X162, T65))
ACKERMANNA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackermannF_in_ga(T70, T71))
PC_IN_GAA(T70, T71, T65) → ACKERMANNF_IN_GA(T70, T71)
U14_GAA(T70, T71, T65, ackermannF_out_ga(T70, T71)) → U15_GAA(T70, T71, T65, ackermannA_in_gga(T70, T71, T65))
U14_GAA(T70, T71, T65, ackermannF_out_ga(T70, T71)) → ACKERMANNA_IN_GGA(T70, T71, T65)
ACKERMANNA_IN_GGA(s(T78), s(s(T79)), T65) → U3_GGA(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
ACKERMANNA_IN_GGA(s(T78), s(s(T79)), T65) → PD_IN_GGAAA(T78, T79, X181, X182, T65)
PD_IN_GGAAA(T78, T79, T80, X182, T65) → U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
PD_IN_GGAAA(T78, T79, T80, X182, T65) → ACKERMANNH_IN_GGA(s(T78), T79, T80)
U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → U17_GGAAA(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80, X182, T65)
PJ_IN_GGAA(T78, T80, T83, T65) → U18_GGAA(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
PJ_IN_GGAA(T78, T80, T83, T65) → ACKERMANNH_IN_GGA(T78, T80, T83)
U18_GGAA(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → U19_GGAA(T78, T80, T83, T65, ackermannA_in_gga(T78, T83, T65))
U18_GGAA(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → ACKERMANNA_IN_GGA(T78, T83, T65)

The TRS R consists of the following rules:

ackermannA_in_gga(0, T5, s(T5)) → ackermannA_out_gga(0, T5, s(T5))
ackermannA_in_gga(s(0), 0, s(s(0))) → ackermannA_out_gga(s(0), 0, s(s(0)))
ackermannA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackermannE_in_ga(T20, T23))
ackermannE_in_ga(T28, X60) → U4_ga(T28, X60, ackermannF_in_ga(T28, X60))
ackermannF_in_ga(0, s(s(0))) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermannE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
ackermannH_in_gga(0, T40, s(T40)) → ackermannH_out_gga(0, T40, s(T40))
ackermannH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermannF_in_ga(T45, X109))
U6_gga(T45, X109, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
ackermannH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermannE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermannA_in_gga(T20, T23, T22))
ackermannA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackermannF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermannF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermannA_in_gga(T70, T71, T65))
ackermannA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermannA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermannA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackermannA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermannA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermannA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermannA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermannA_out_gga(s(s(T20)), 0, T22)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

ACKERMANNE_IN_GA(T28, X60) → ACKERMANNF_IN_GA(T28, X60)
ACKERMANNF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackermannE_in_ga(T32, T33))
U10_GAA(T32, T33, X83, ackermannE_out_ga(T32, T33)) → ACKERMANNH_IN_GGA(T32, T33, X83)
ACKERMANNH_IN_GGA(s(T45), 0, X109) → ACKERMANNF_IN_GA(T45, X109)
ACKERMANNH_IN_GGA(s(T50), s(T51), X125) → PI_IN_GGAA(T50, T51, X124, X125)
PI_IN_GGAA(T50, T51, T52, X125) → U12_GGAA(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U12_GGAA(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → ACKERMANNH_IN_GGA(T50, T52, X125)
PI_IN_GGAA(T50, T51, T52, X125) → ACKERMANNH_IN_GGA(s(T50), T51, T52)
PG_IN_GAA(T32, T33, X83) → ACKERMANNE_IN_GA(T32, T33)

The TRS R consists of the following rules:

ackermannA_in_gga(0, T5, s(T5)) → ackermannA_out_gga(0, T5, s(T5))
ackermannA_in_gga(s(0), 0, s(s(0))) → ackermannA_out_gga(s(0), 0, s(s(0)))
ackermannA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackermannE_in_ga(T20, T23))
ackermannE_in_ga(T28, X60) → U4_ga(T28, X60, ackermannF_in_ga(T28, X60))
ackermannF_in_ga(0, s(s(0))) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermannE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
ackermannH_in_gga(0, T40, s(T40)) → ackermannH_out_gga(0, T40, s(T40))
ackermannH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermannF_in_ga(T45, X109))
U6_gga(T45, X109, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
ackermannH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermannE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermannA_in_gga(T20, T23, T22))
ackermannA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackermannF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermannF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermannA_in_gga(T70, T71, T65))
ackermannA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermannA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermannA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackermannA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermannA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermannA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermannA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermannA_out_gga(s(s(T20)), 0, T22)

The argument filtering Pi contains the following mapping:
ackermannA_in_gga(x1, x2, x3) = ackermannA_in_gga(x1, x2)
0 = 0
ackermannA_out_gga(x1, x2, x3) = ackermannA_out_gga(x1, x2, x3)
s(x1) = s(x1)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4) = U8_gaa(x1, x4)
ackermannE_in_ga(x1, x2) = ackermannE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackermannF_in_ga(x1, x2) = ackermannF_in_ga(x1)
ackermannF_out_ga(x1, x2) = ackermannF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackermannE_out_ga(x1, x2) = ackermannE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackermannH_in_gga(x1, x2, x3) = ackermannH_in_gga(x1, x2)
ackermannH_out_gga(x1, x2, x3) = ackermannH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4) = U9_gaa(x1, x2, x4)
U2_gga(x1, x2, x3) = U2_gga(x1, x3)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
U14_gaa(x1, x2, x3, x4) = U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4) = U15_gaa(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
pD_in_ggaaa(x1, x2, x3, x4, x5) = pD_in_ggaaa(x1, x2)
U16_ggaaa(x1, x2, x3, x4, x5, x6) = U16_ggaaa(x1, x2, x6)
U17_ggaaa(x1, x2, x3, x4, x5, x6) = U17_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4) = pJ_in_ggaa(x1, x2)
U18_ggaa(x1, x2, x3, x4, x5) = U18_ggaa(x1, x2, x5)
U19_ggaa(x1, x2, x3, x4, x5) = U19_ggaa(x1, x2, x3, x5)
pJ_out_ggaa(x1, x2, x3, x4) = pJ_out_ggaa(x1, x2, x3, x4)
pD_out_ggaaa(x1, x2, x3, x4, x5) = pD_out_ggaaa(x1, x2, x3, x4, x5)
pC_out_gaa(x1, x2, x3) = pC_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
ACKERMANNE_IN_GA(x1, x2) = ACKERMANNE_IN_GA(x1)
ACKERMANNF_IN_GA(x1, x2) = ACKERMANNF_IN_GA(x1)
PG_IN_GAA(x1, x2, x3) = PG_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x1, x4)
ACKERMANNH_IN_GGA(x1, x2, x3) = ACKERMANNH_IN_GGA(x1, x2)
PI_IN_GGAA(x1, x2, x3, x4) = PI_IN_GGAA(x1, x2)
U12_GGAA(x1, x2, x3, x4, x5) = U12_GGAA(x1, x2, x5)

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:

ACKERMANNE_IN_GA(T28, X60) → ACKERMANNF_IN_GA(T28, X60)
ACKERMANNF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackermannE_in_ga(T32, T33))
U10_GAA(T32, T33, X83, ackermannE_out_ga(T32, T33)) → ACKERMANNH_IN_GGA(T32, T33, X83)
ACKERMANNH_IN_GGA(s(T45), 0, X109) → ACKERMANNF_IN_GA(T45, X109)
ACKERMANNH_IN_GGA(s(T50), s(T51), X125) → PI_IN_GGAA(T50, T51, X124, X125)
PI_IN_GGAA(T50, T51, T52, X125) → U12_GGAA(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U12_GGAA(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → ACKERMANNH_IN_GGA(T50, T52, X125)
PI_IN_GGAA(T50, T51, T52, X125) → ACKERMANNH_IN_GGA(s(T50), T51, T52)
PG_IN_GAA(T32, T33, X83) → ACKERMANNE_IN_GA(T32, T33)

The TRS R consists of the following rules:

ackermannE_in_ga(T28, X60) → U4_ga(T28, X60, ackermannF_in_ga(T28, X60))
ackermannH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermannF_in_ga(T45, X109))
ackermannH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
U4_ga(T28, X60, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U6_gga(T45, X109, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
ackermannF_in_ga(0, s(s(0))) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermannE_in_ga(T32, T33))
U13_ggaa(T50, T51, T52, X125, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
ackermannH_in_gga(0, T40, s(T40)) → ackermannH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, X83, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermannE_in_ga(x1, x2) = ackermannE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackermannF_in_ga(x1, x2) = ackermannF_in_ga(x1)
ackermannF_out_ga(x1, x2) = ackermannF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackermannE_out_ga(x1, x2) = ackermannE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackermannH_in_gga(x1, x2, x3) = ackermannH_in_gga(x1, x2)
ackermannH_out_gga(x1, x2, x3) = ackermannH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
ACKERMANNE_IN_GA(x1, x2) = ACKERMANNE_IN_GA(x1)
ACKERMANNF_IN_GA(x1, x2) = ACKERMANNF_IN_GA(x1)
PG_IN_GAA(x1, x2, x3) = PG_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x1, x4)
ACKERMANNH_IN_GGA(x1, x2, x3) = ACKERMANNH_IN_GGA(x1, x2)
PI_IN_GGAA(x1, x2, x3, x4) = PI_IN_GGAA(x1, x2)
U12_GGAA(x1, x2, x3, x4, x5) = U12_GGAA(x1, x2, x5)

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:

ACKERMANNE_IN_GA(T28) → ACKERMANNF_IN_GA(T28)
ACKERMANNF_IN_GA(s(T32)) → PG_IN_GAA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, ackermannE_in_ga(T32))
U10_GAA(T32, ackermannE_out_ga(T32, T33)) → ACKERMANNH_IN_GGA(T32, T33)
ACKERMANNH_IN_GGA(s(T45), 0) → ACKERMANNF_IN_GA(T45)
ACKERMANNH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackermannH_in_gga(s(T50), T51))
U12_GGAA(T50, T51, ackermannH_out_gga(s(T50), T51, T52)) → ACKERMANNH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKERMANNH_IN_GGA(s(T50), T51)
PG_IN_GAA(T32) → ACKERMANNE_IN_GA(T32)

The TRS R consists of the following rules:

ackermannE_in_ga(T28) → U4_ga(T28, ackermannF_in_ga(T28))
ackermannH_in_gga(s(T45), 0) → U6_gga(T45, ackermannF_in_ga(T45))
ackermannH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U6_gga(T45, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
ackermannF_in_ga(0) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermannH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermannH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackermannE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermannH_in_gga(T32, T33))
ackermannH_in_gga(0, T40) → ackermannH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The set Q consists of the following terms:

ackermannE_in_ga(x0)
ackermannH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermannF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(12) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PG_IN_GAA(T32) → U10_GAA(T32, ackermannE_in_ga(T32)) at position [1] we obtained the following new rules [LPAR04]:

PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackermannF_in_ga(T32)))

(13) Obligation:

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

ACKERMANNE_IN_GA(T28) → ACKERMANNF_IN_GA(T28)
ACKERMANNF_IN_GA(s(T32)) → PG_IN_GAA(T32)
U10_GAA(T32, ackermannE_out_ga(T32, T33)) → ACKERMANNH_IN_GGA(T32, T33)
ACKERMANNH_IN_GGA(s(T45), 0) → ACKERMANNF_IN_GA(T45)
ACKERMANNH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackermannH_in_gga(s(T50), T51))
U12_GGAA(T50, T51, ackermannH_out_gga(s(T50), T51, T52)) → ACKERMANNH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKERMANNH_IN_GGA(s(T50), T51)
PG_IN_GAA(T32) → ACKERMANNE_IN_GA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackermannF_in_ga(T32)))

The TRS R consists of the following rules:

ackermannE_in_ga(T28) → U4_ga(T28, ackermannF_in_ga(T28))
ackermannH_in_gga(s(T45), 0) → U6_gga(T45, ackermannF_in_ga(T45))
ackermannH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U6_gga(T45, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
ackermannF_in_ga(0) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermannH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermannH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackermannE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermannH_in_gga(T32, T33))
ackermannH_in_gga(0, T40) → ackermannH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The set Q consists of the following terms:

ackermannE_in_ga(x0)
ackermannH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermannF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(14) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

ACKERMANNH_IN_GGA(s(T45), 0) → ACKERMANNF_IN_GA(T45)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackermannH_in_gga(s(T50), T51))
PG_IN_GAA(T32) → ACKERMANNE_IN_GA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackermannF_in_ga(T32)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 1
POL(ACKERMANNE_IN_GA(x₁)) = x₁
POL(ACKERMANNF_IN_GA(x₁)) = x₁
POL(ACKERMANNH_IN_GGA(x₁, x₂)) = x₁
POL(PG_IN_GAA(x₁)) = 1 + x₁
POL(PI_IN_GGAA(x₁, x₂)) = 1 + x₁
POL(U10_GAA(x₁, x₂)) = x₁
POL(U10_gaa(x₁, x₂)) = 0
POL(U11_gaa(x₁, x₂, x₃)) = 0
POL(U12_GGAA(x₁, x₂, x₃)) = x₁
POL(U12_ggaa(x₁, x₂, x₃)) = 0
POL(U13_ggaa(x₁, x₂, x₃, x₄)) = 0
POL(U4_ga(x₁, x₂)) = 0
POL(U5_ga(x₁, x₂)) = 0
POL(U6_gga(x₁, x₂)) = 0
POL(U7_gga(x₁, x₂, x₃)) = 0
POL(ackermannE_in_ga(x₁)) = 0
POL(ackermannE_out_ga(x₁, x₂)) = 0
POL(ackermannF_in_ga(x₁)) = x₁
POL(ackermannF_out_ga(x₁, x₂)) = 0
POL(ackermannH_in_gga(x₁, x₂)) = 1 + x₁ + x₂
POL(ackermannH_out_gga(x₁, x₂, x₃)) = x₁
POL(pG_in_gaa(x₁)) = 0
POL(pG_out_gaa(x₁, x₂, x₃)) = 0
POL(pI_in_ggaa(x₁, x₂)) = 0
POL(pI_out_ggaa(x₁, x₂, x₃, x₄)) = 0
POL(s(x₁)) = 1 + x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(15) Obligation:

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

ACKERMANNE_IN_GA(T28) → ACKERMANNF_IN_GA(T28)
ACKERMANNF_IN_GA(s(T32)) → PG_IN_GAA(T32)
U10_GAA(T32, ackermannE_out_ga(T32, T33)) → ACKERMANNH_IN_GGA(T32, T33)
ACKERMANNH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
U12_GGAA(T50, T51, ackermannH_out_gga(s(T50), T51, T52)) → ACKERMANNH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKERMANNH_IN_GGA(s(T50), T51)

The TRS R consists of the following rules:

ackermannE_in_ga(T28) → U4_ga(T28, ackermannF_in_ga(T28))
ackermannH_in_gga(s(T45), 0) → U6_gga(T45, ackermannF_in_ga(T45))
ackermannH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U6_gga(T45, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
ackermannF_in_ga(0) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermannH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermannH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackermannE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermannH_in_gga(T32, T33))
ackermannH_in_gga(0, T40) → ackermannH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The set Q consists of the following terms:

ackermannE_in_ga(x0)
ackermannH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermannF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(16) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 4 less nodes.

(17) Obligation:

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

PI_IN_GGAA(T50, T51) → ACKERMANNH_IN_GGA(s(T50), T51)
ACKERMANNH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)

The TRS R consists of the following rules:

ackermannE_in_ga(T28) → U4_ga(T28, ackermannF_in_ga(T28))
ackermannH_in_gga(s(T45), 0) → U6_gga(T45, ackermannF_in_ga(T45))
ackermannH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U6_gga(T45, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
ackermannF_in_ga(0) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermannH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermannH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackermannE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermannH_in_gga(T32, T33))
ackermannH_in_gga(0, T40) → ackermannH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The set Q consists of the following terms:

ackermannE_in_ga(x0)
ackermannH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermannF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(18) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(19) Obligation:

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

PI_IN_GGAA(T50, T51) → ACKERMANNH_IN_GGA(s(T50), T51)
ACKERMANNH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)

R is empty.
The set Q consists of the following terms:

ackermannE_in_ga(x0)
ackermannH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermannF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(20) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

ackermannE_in_ga(x0)
ackermannH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermannF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

(21) Obligation:

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

PI_IN_GGAA(T50, T51) → ACKERMANNH_IN_GGA(s(T50), T51)
ACKERMANNH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)

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

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

ACKERMANNH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
The graph contains the following edges 1 > 1, 2 > 2
PI_IN_GGAA(T50, T51) → ACKERMANNH_IN_GGA(s(T50), T51)
The graph contains the following edges 2 >= 2

(23) YES

(24) Obligation:

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

ACKERMANNA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackermannE_in_ga(T20, T23))
U8_GAA(T20, T23, T22, ackermannE_out_ga(T20, T23)) → ACKERMANNA_IN_GGA(T20, T23, T22)
ACKERMANNA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackermannF_in_ga(T70, T71))
U14_GAA(T70, T71, T65, ackermannF_out_ga(T70, T71)) → ACKERMANNA_IN_GGA(T70, T71, T65)
ACKERMANNA_IN_GGA(s(T78), s(s(T79)), T65) → PD_IN_GGAAA(T78, T79, X181, X182, T65)
PD_IN_GGAAA(T78, T79, T80, X182, T65) → U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80, X182, T65)
PJ_IN_GGAA(T78, T80, T83, T65) → U18_GGAA(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
U18_GGAA(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → ACKERMANNA_IN_GGA(T78, T83, T65)

The TRS R consists of the following rules:

ackermannA_in_gga(0, T5, s(T5)) → ackermannA_out_gga(0, T5, s(T5))
ackermannA_in_gga(s(0), 0, s(s(0))) → ackermannA_out_gga(s(0), 0, s(s(0)))
ackermannA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackermannE_in_ga(T20, T23))
ackermannE_in_ga(T28, X60) → U4_ga(T28, X60, ackermannF_in_ga(T28, X60))
ackermannF_in_ga(0, s(s(0))) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermannE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
ackermannH_in_gga(0, T40, s(T40)) → ackermannH_out_gga(0, T40, s(T40))
ackermannH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermannF_in_ga(T45, X109))
U6_gga(T45, X109, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
ackermannH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermannE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermannA_in_gga(T20, T23, T22))
ackermannA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackermannF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermannF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermannA_in_gga(T70, T71, T65))
ackermannA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermannA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermannA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackermannA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermannA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermannA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermannA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermannA_out_gga(s(s(T20)), 0, T22)

The argument filtering Pi contains the following mapping:
ackermannA_in_gga(x1, x2, x3) = ackermannA_in_gga(x1, x2)
0 = 0
ackermannA_out_gga(x1, x2, x3) = ackermannA_out_gga(x1, x2, x3)
s(x1) = s(x1)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4) = U8_gaa(x1, x4)
ackermannE_in_ga(x1, x2) = ackermannE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackermannF_in_ga(x1, x2) = ackermannF_in_ga(x1)
ackermannF_out_ga(x1, x2) = ackermannF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackermannE_out_ga(x1, x2) = ackermannE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackermannH_in_gga(x1, x2, x3) = ackermannH_in_gga(x1, x2)
ackermannH_out_gga(x1, x2, x3) = ackermannH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4) = U9_gaa(x1, x2, x4)
U2_gga(x1, x2, x3) = U2_gga(x1, x3)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
U14_gaa(x1, x2, x3, x4) = U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4) = U15_gaa(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
pD_in_ggaaa(x1, x2, x3, x4, x5) = pD_in_ggaaa(x1, x2)
U16_ggaaa(x1, x2, x3, x4, x5, x6) = U16_ggaaa(x1, x2, x6)
U17_ggaaa(x1, x2, x3, x4, x5, x6) = U17_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4) = pJ_in_ggaa(x1, x2)
U18_ggaa(x1, x2, x3, x4, x5) = U18_ggaa(x1, x2, x5)
U19_ggaa(x1, x2, x3, x4, x5) = U19_ggaa(x1, x2, x3, x5)
pJ_out_ggaa(x1, x2, x3, x4) = pJ_out_ggaa(x1, x2, x3, x4)
pD_out_ggaaa(x1, x2, x3, x4, x5) = pD_out_ggaaa(x1, x2, x3, x4, x5)
pC_out_gaa(x1, x2, x3) = pC_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
ACKERMANNA_IN_GGA(x1, x2, x3) = ACKERMANNA_IN_GGA(x1, x2)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4) = U8_GAA(x1, x4)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x1, x4)
PD_IN_GGAAA(x1, x2, x3, x4, x5) = PD_IN_GGAAA(x1, x2)
U16_GGAAA(x1, x2, x3, x4, x5, x6) = U16_GGAAA(x1, x2, x6)
PJ_IN_GGAA(x1, x2, x3, x4) = PJ_IN_GGAA(x1, x2)
U18_GGAA(x1, x2, x3, x4, x5) = U18_GGAA(x1, x2, x5)

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

(25) UsableRulesProof (EQUIVALENT transformation)

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

(26) Obligation:

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

ACKERMANNA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackermannE_in_ga(T20, T23))
U8_GAA(T20, T23, T22, ackermannE_out_ga(T20, T23)) → ACKERMANNA_IN_GGA(T20, T23, T22)
ACKERMANNA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackermannF_in_ga(T70, T71))
U14_GAA(T70, T71, T65, ackermannF_out_ga(T70, T71)) → ACKERMANNA_IN_GGA(T70, T71, T65)
ACKERMANNA_IN_GGA(s(T78), s(s(T79)), T65) → PD_IN_GGAAA(T78, T79, X181, X182, T65)
PD_IN_GGAAA(T78, T79, T80, X182, T65) → U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_in_gga(s(T78), T79, T80))
U16_GGAAA(T78, T79, T80, X182, T65, ackermannH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80, X182, T65)
PJ_IN_GGAA(T78, T80, T83, T65) → U18_GGAA(T78, T80, T83, T65, ackermannH_in_gga(T78, T80, T83))
U18_GGAA(T78, T80, T83, T65, ackermannH_out_gga(T78, T80, T83)) → ACKERMANNA_IN_GGA(T78, T83, T65)

The TRS R consists of the following rules:

ackermannE_in_ga(T28, X60) → U4_ga(T28, X60, ackermannF_in_ga(T28, X60))
ackermannF_in_ga(0, s(s(0))) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
ackermannH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermannF_in_ga(T45, X109))
ackermannH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ackermannH_in_gga(0, T40, s(T40)) → ackermannH_out_gga(0, T40, s(T40))
U4_ga(T28, X60, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U6_gga(T45, X109, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermannE_in_ga(T32, T33))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackermannH_in_gga(s(T50), T51, T52))
U10_gaa(T32, T33, X83, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermannH_in_gga(T32, T33, X83))
U12_ggaa(T50, T51, T52, X125, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermannH_in_gga(T50, T52, X125))
U11_gaa(T32, T33, X83, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U13_ggaa(T50, T51, T52, X125, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackermannE_in_ga(x1, x2) = ackermannE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackermannF_in_ga(x1, x2) = ackermannF_in_ga(x1)
ackermannF_out_ga(x1, x2) = ackermannF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackermannE_out_ga(x1, x2) = ackermannE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackermannH_in_gga(x1, x2, x3) = ackermannH_in_gga(x1, x2)
ackermannH_out_gga(x1, x2, x3) = ackermannH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
ACKERMANNA_IN_GGA(x1, x2, x3) = ACKERMANNA_IN_GGA(x1, x2)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4) = U8_GAA(x1, x4)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x1, x4)
PD_IN_GGAAA(x1, x2, x3, x4, x5) = PD_IN_GGAAA(x1, x2)
U16_GGAAA(x1, x2, x3, x4, x5, x6) = U16_GGAAA(x1, x2, x6)
PJ_IN_GGAA(x1, x2, x3, x4) = PJ_IN_GGAA(x1, x2)
U18_GGAA(x1, x2, x3, x4, x5) = U18_GGAA(x1, x2, x5)

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

(27) PiDPToQDPProof (SOUND transformation)

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

(28) Obligation:

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

ACKERMANNA_IN_GGA(s(s(T20)), 0) → PB_IN_GAA(T20)
PB_IN_GAA(T20) → U8_GAA(T20, ackermannE_in_ga(T20))
U8_GAA(T20, ackermannE_out_ga(T20, T23)) → ACKERMANNA_IN_GGA(T20, T23)
ACKERMANNA_IN_GGA(s(T70), s(0)) → PC_IN_GAA(T70)
PC_IN_GAA(T70) → U14_GAA(T70, ackermannF_in_ga(T70))
U14_GAA(T70, ackermannF_out_ga(T70, T71)) → ACKERMANNA_IN_GGA(T70, T71)
ACKERMANNA_IN_GGA(s(T78), s(s(T79))) → PD_IN_GGAAA(T78, T79)
PD_IN_GGAAA(T78, T79) → U16_GGAAA(T78, T79, ackermannH_in_gga(s(T78), T79))
U16_GGAAA(T78, T79, ackermannH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80)
PJ_IN_GGAA(T78, T80) → U18_GGAA(T78, T80, ackermannH_in_gga(T78, T80))
U18_GGAA(T78, T80, ackermannH_out_gga(T78, T80, T83)) → ACKERMANNA_IN_GGA(T78, T83)

The TRS R consists of the following rules:

ackermannE_in_ga(T28) → U4_ga(T28, ackermannF_in_ga(T28))
ackermannF_in_ga(0) → ackermannF_out_ga(0, s(s(0)))
ackermannF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
ackermannH_in_gga(s(T45), 0) → U6_gga(T45, ackermannF_in_ga(T45))
ackermannH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
ackermannH_in_gga(0, T40) → ackermannH_out_gga(0, T40, s(T40))
U4_ga(T28, ackermannF_out_ga(T28, X60)) → ackermannE_out_ga(T28, X60)
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermannF_out_ga(s(T32), X83)
U6_gga(T45, ackermannF_out_ga(T45, X109)) → ackermannH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermannH_out_gga(s(T50), s(T51), X125)
pG_in_gaa(T32) → U10_gaa(T32, ackermannE_in_ga(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermannH_in_gga(s(T50), T51))
U10_gaa(T32, ackermannE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermannH_in_gga(T32, T33))
U12_ggaa(T50, T51, ackermannH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermannH_in_gga(T50, T52))
U11_gaa(T32, T33, ackermannH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U13_ggaa(T50, T51, T52, ackermannH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)

The set Q consists of the following terms:

ackermannE_in_ga(x0)
ackermannF_in_ga(x0)
ackermannH_in_gga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
pG_in_gaa(x0)
pI_in_ggaa(x0, x1)
U10_gaa(x0, x1)
U12_ggaa(x0, x1, x2)
U11_gaa(x0, x1, x2)
U13_ggaa(x0, x1, x2, x3)

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

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

PB_IN_GAA(T20) → U8_GAA(T20, ackermannE_in_ga(T20))
The graph contains the following edges 1 >= 1
U8_GAA(T20, ackermannE_out_ga(T20, T23)) → ACKERMANNA_IN_GGA(T20, T23)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2
ACKERMANNA_IN_GGA(s(s(T20)), 0) → PB_IN_GAA(T20)
The graph contains the following edges 1 > 1
PC_IN_GAA(T70) → U14_GAA(T70, ackermannF_in_ga(T70))
The graph contains the following edges 1 >= 1
U14_GAA(T70, ackermannF_out_ga(T70, T71)) → ACKERMANNA_IN_GGA(T70, T71)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2
U18_GGAA(T78, T80, ackermannH_out_gga(T78, T80, T83)) → ACKERMANNA_IN_GGA(T78, T83)
The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2
ACKERMANNA_IN_GGA(s(T70), s(0)) → PC_IN_GAA(T70)
The graph contains the following edges 1 > 1
ACKERMANNA_IN_GGA(s(T78), s(s(T79))) → PD_IN_GGAAA(T78, T79)
The graph contains the following edges 1 > 1, 2 > 2
PD_IN_GGAAA(T78, T79) → U16_GGAAA(T78, T79, ackermannH_in_gga(s(T78), T79))
The graph contains the following edges 1 >= 1, 2 >= 2
U16_GGAAA(T78, T79, ackermannH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80)
The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2
PJ_IN_GGAA(T78, T80) → U18_GGAA(T78, T80, ackermannH_in_gga(T78, T80))
The graph contains the following edges 1 >= 1, 2 >= 2

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) Rewriting (EQUIVALENT transformation)

(13) Obligation:

(14) QDPOrderProof (EQUIVALENT transformation)

(15) Obligation:

(16) DependencyGraphProof (EQUIVALENT transformation)

(17) Obligation:

(18) UsableRulesProof (EQUIVALENT transformation)

(19) Obligation:

(20) QReductionProof (EQUIVALENT transformation)

(21) Obligation:

(22) QDPSizeChangeProof (EQUIVALENT transformation)

(23) YES

(24) Obligation:

(25) UsableRulesProof (EQUIVALENT transformation)

(26) Obligation:

(27) PiDPToQDPProof (SOUND transformation)

(28) Obligation:

(29) QDPSizeChangeProof (EQUIVALENT transformation)

(30) YES