0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 201 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 298 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 39 ms)
↳11 QDP
↳12 Rewriting (⇔, 0 ms)
↳13 QDP
↳14 QDPOrderProof (⇔, 160 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 (⇔, 2 ms)
↳26 PiDP
↳27 PiDPToQDPProof (⇒, 0 ms)
↳28 QDP
↳29 QDPSizeChangeProof (⇔, 0 ms)
↳30 YES
ackermanA_in_gga(0, T5, s(T5)) → ackermanA_out_gga(0, T5, s(T5))
ackermanA_in_gga(s(0), 0, s(s(0))) → ackermanA_out_gga(s(0), 0, s(s(0)))
ackermanA_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, ackermanE_in_ga(T20, T23))
ackermanE_in_ga(T28, X60) → U4_ga(T28, X60, ackermanF_in_ga(T28, X60))
ackermanF_in_ga(0, s(s(0))) → ackermanF_out_ga(0, s(s(0)))
ackermanF_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, ackermanE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
ackermanH_in_gga(0, T40, s(T40)) → ackermanH_out_gga(0, T40, s(T40))
ackermanH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermanF_in_ga(T45, X109))
U6_gga(T45, X109, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
ackermanH_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, ackermanH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermanE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermanA_in_gga(T20, T23, T22))
ackermanA_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, ackermanF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermanF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermanA_in_gga(T70, T71, T65))
ackermanA_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, ackermanH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermanA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermanA_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)) → ackermanA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermanA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermanA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermanA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermanA_out_gga(s(s(T20)), 0, T22)
ACKERMANA_IN_GGA(s(s(T20)), 0, T22) → U1_GGA(T20, T22, pB_in_gaa(T20, X36, T22))
ACKERMANA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackermanE_in_ga(T20, T23))
PB_IN_GAA(T20, T23, T22) → ACKERMANE_IN_GA(T20, T23)
ACKERMANE_IN_GA(T28, X60) → U4_GA(T28, X60, ackermanF_in_ga(T28, X60))
ACKERMANE_IN_GA(T28, X60) → ACKERMANF_IN_GA(T28, X60)
ACKERMANF_IN_GA(s(T32), X83) → U5_GA(T32, X83, pG_in_gaa(T32, X82, X83))
ACKERMANF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackermanE_in_ga(T32, T33))
PG_IN_GAA(T32, T33, X83) → ACKERMANE_IN_GA(T32, T33)
U10_GAA(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_GAA(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
U10_GAA(T32, T33, X83, ackermanE_out_ga(T32, T33)) → ACKERMANH_IN_GGA(T32, T33, X83)
ACKERMANH_IN_GGA(s(T45), 0, X109) → U6_GGA(T45, X109, ackermanF_in_ga(T45, X109))
ACKERMANH_IN_GGA(s(T45), 0, X109) → ACKERMANF_IN_GA(T45, X109)
ACKERMANH_IN_GGA(s(T50), s(T51), X125) → U7_GGA(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ACKERMANH_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, ackermanH_in_gga(s(T50), T51, T52))
PI_IN_GGAA(T50, T51, T52, X125) → ACKERMANH_IN_GGA(s(T50), T51, T52)
U12_GGAA(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_GGAA(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
U12_GGAA(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → ACKERMANH_IN_GGA(T50, T52, X125)
U8_GAA(T20, T23, T22, ackermanE_out_ga(T20, T23)) → U9_GAA(T20, T23, T22, ackermanA_in_gga(T20, T23, T22))
U8_GAA(T20, T23, T22, ackermanE_out_ga(T20, T23)) → ACKERMANA_IN_GGA(T20, T23, T22)
ACKERMANA_IN_GGA(s(T70), s(0), T65) → U2_GGA(T70, T65, pC_in_gaa(T70, X162, T65))
ACKERMANA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackermanF_in_ga(T70, T71))
PC_IN_GAA(T70, T71, T65) → ACKERMANF_IN_GA(T70, T71)
U14_GAA(T70, T71, T65, ackermanF_out_ga(T70, T71)) → U15_GAA(T70, T71, T65, ackermanA_in_gga(T70, T71, T65))
U14_GAA(T70, T71, T65, ackermanF_out_ga(T70, T71)) → ACKERMANA_IN_GGA(T70, T71, T65)
ACKERMANA_IN_GGA(s(T78), s(s(T79)), T65) → U3_GGA(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
ACKERMANA_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, ackermanH_in_gga(s(T78), T79, T80))
PD_IN_GGAAA(T78, T79, T80, X182, T65) → ACKERMANH_IN_GGA(s(T78), T79, T80)
U16_GGAAA(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
PJ_IN_GGAA(T78, T80, T83, T65) → ACKERMANH_IN_GGA(T78, T80, T83)
U18_GGAA(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → U19_GGAA(T78, T80, T83, T65, ackermanA_in_gga(T78, T83, T65))
U18_GGAA(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → ACKERMANA_IN_GGA(T78, T83, T65)
ackermanA_in_gga(0, T5, s(T5)) → ackermanA_out_gga(0, T5, s(T5))
ackermanA_in_gga(s(0), 0, s(s(0))) → ackermanA_out_gga(s(0), 0, s(s(0)))
ackermanA_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, ackermanE_in_ga(T20, T23))
ackermanE_in_ga(T28, X60) → U4_ga(T28, X60, ackermanF_in_ga(T28, X60))
ackermanF_in_ga(0, s(s(0))) → ackermanF_out_ga(0, s(s(0)))
ackermanF_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, ackermanE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
ackermanH_in_gga(0, T40, s(T40)) → ackermanH_out_gga(0, T40, s(T40))
ackermanH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermanF_in_ga(T45, X109))
U6_gga(T45, X109, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
ackermanH_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, ackermanH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermanE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermanA_in_gga(T20, T23, T22))
ackermanA_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, ackermanF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermanF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermanA_in_gga(T70, T71, T65))
ackermanA_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, ackermanH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermanA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermanA_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)) → ackermanA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermanA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermanA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermanA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermanA_out_gga(s(s(T20)), 0, T22)
ACKERMANA_IN_GGA(s(s(T20)), 0, T22) → U1_GGA(T20, T22, pB_in_gaa(T20, X36, T22))
ACKERMANA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackermanE_in_ga(T20, T23))
PB_IN_GAA(T20, T23, T22) → ACKERMANE_IN_GA(T20, T23)
ACKERMANE_IN_GA(T28, X60) → U4_GA(T28, X60, ackermanF_in_ga(T28, X60))
ACKERMANE_IN_GA(T28, X60) → ACKERMANF_IN_GA(T28, X60)
ACKERMANF_IN_GA(s(T32), X83) → U5_GA(T32, X83, pG_in_gaa(T32, X82, X83))
ACKERMANF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackermanE_in_ga(T32, T33))
PG_IN_GAA(T32, T33, X83) → ACKERMANE_IN_GA(T32, T33)
U10_GAA(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_GAA(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
U10_GAA(T32, T33, X83, ackermanE_out_ga(T32, T33)) → ACKERMANH_IN_GGA(T32, T33, X83)
ACKERMANH_IN_GGA(s(T45), 0, X109) → U6_GGA(T45, X109, ackermanF_in_ga(T45, X109))
ACKERMANH_IN_GGA(s(T45), 0, X109) → ACKERMANF_IN_GA(T45, X109)
ACKERMANH_IN_GGA(s(T50), s(T51), X125) → U7_GGA(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ACKERMANH_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, ackermanH_in_gga(s(T50), T51, T52))
PI_IN_GGAA(T50, T51, T52, X125) → ACKERMANH_IN_GGA(s(T50), T51, T52)
U12_GGAA(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_GGAA(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
U12_GGAA(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → ACKERMANH_IN_GGA(T50, T52, X125)
U8_GAA(T20, T23, T22, ackermanE_out_ga(T20, T23)) → U9_GAA(T20, T23, T22, ackermanA_in_gga(T20, T23, T22))
U8_GAA(T20, T23, T22, ackermanE_out_ga(T20, T23)) → ACKERMANA_IN_GGA(T20, T23, T22)
ACKERMANA_IN_GGA(s(T70), s(0), T65) → U2_GGA(T70, T65, pC_in_gaa(T70, X162, T65))
ACKERMANA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackermanF_in_ga(T70, T71))
PC_IN_GAA(T70, T71, T65) → ACKERMANF_IN_GA(T70, T71)
U14_GAA(T70, T71, T65, ackermanF_out_ga(T70, T71)) → U15_GAA(T70, T71, T65, ackermanA_in_gga(T70, T71, T65))
U14_GAA(T70, T71, T65, ackermanF_out_ga(T70, T71)) → ACKERMANA_IN_GGA(T70, T71, T65)
ACKERMANA_IN_GGA(s(T78), s(s(T79)), T65) → U3_GGA(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
ACKERMANA_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, ackermanH_in_gga(s(T78), T79, T80))
PD_IN_GGAAA(T78, T79, T80, X182, T65) → ACKERMANH_IN_GGA(s(T78), T79, T80)
U16_GGAAA(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
PJ_IN_GGAA(T78, T80, T83, T65) → ACKERMANH_IN_GGA(T78, T80, T83)
U18_GGAA(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → U19_GGAA(T78, T80, T83, T65, ackermanA_in_gga(T78, T83, T65))
U18_GGAA(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → ACKERMANA_IN_GGA(T78, T83, T65)
ackermanA_in_gga(0, T5, s(T5)) → ackermanA_out_gga(0, T5, s(T5))
ackermanA_in_gga(s(0), 0, s(s(0))) → ackermanA_out_gga(s(0), 0, s(s(0)))
ackermanA_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, ackermanE_in_ga(T20, T23))
ackermanE_in_ga(T28, X60) → U4_ga(T28, X60, ackermanF_in_ga(T28, X60))
ackermanF_in_ga(0, s(s(0))) → ackermanF_out_ga(0, s(s(0)))
ackermanF_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, ackermanE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
ackermanH_in_gga(0, T40, s(T40)) → ackermanH_out_gga(0, T40, s(T40))
ackermanH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermanF_in_ga(T45, X109))
U6_gga(T45, X109, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
ackermanH_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, ackermanH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermanE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermanA_in_gga(T20, T23, T22))
ackermanA_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, ackermanF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermanF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermanA_in_gga(T70, T71, T65))
ackermanA_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, ackermanH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermanA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermanA_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)) → ackermanA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermanA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermanA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermanA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermanA_out_gga(s(s(T20)), 0, T22)
ACKERMANE_IN_GA(T28, X60) → ACKERMANF_IN_GA(T28, X60)
ACKERMANF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackermanE_in_ga(T32, T33))
U10_GAA(T32, T33, X83, ackermanE_out_ga(T32, T33)) → ACKERMANH_IN_GGA(T32, T33, X83)
ACKERMANH_IN_GGA(s(T45), 0, X109) → ACKERMANF_IN_GA(T45, X109)
ACKERMANH_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, ackermanH_in_gga(s(T50), T51, T52))
U12_GGAA(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → ACKERMANH_IN_GGA(T50, T52, X125)
PI_IN_GGAA(T50, T51, T52, X125) → ACKERMANH_IN_GGA(s(T50), T51, T52)
PG_IN_GAA(T32, T33, X83) → ACKERMANE_IN_GA(T32, T33)
ackermanA_in_gga(0, T5, s(T5)) → ackermanA_out_gga(0, T5, s(T5))
ackermanA_in_gga(s(0), 0, s(s(0))) → ackermanA_out_gga(s(0), 0, s(s(0)))
ackermanA_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, ackermanE_in_ga(T20, T23))
ackermanE_in_ga(T28, X60) → U4_ga(T28, X60, ackermanF_in_ga(T28, X60))
ackermanF_in_ga(0, s(s(0))) → ackermanF_out_ga(0, s(s(0)))
ackermanF_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, ackermanE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
ackermanH_in_gga(0, T40, s(T40)) → ackermanH_out_gga(0, T40, s(T40))
ackermanH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermanF_in_ga(T45, X109))
U6_gga(T45, X109, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
ackermanH_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, ackermanH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermanE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermanA_in_gga(T20, T23, T22))
ackermanA_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, ackermanF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermanF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermanA_in_gga(T70, T71, T65))
ackermanA_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, ackermanH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermanA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermanA_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)) → ackermanA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermanA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermanA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermanA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermanA_out_gga(s(s(T20)), 0, T22)
ACKERMANE_IN_GA(T28, X60) → ACKERMANF_IN_GA(T28, X60)
ACKERMANF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackermanE_in_ga(T32, T33))
U10_GAA(T32, T33, X83, ackermanE_out_ga(T32, T33)) → ACKERMANH_IN_GGA(T32, T33, X83)
ACKERMANH_IN_GGA(s(T45), 0, X109) → ACKERMANF_IN_GA(T45, X109)
ACKERMANH_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, ackermanH_in_gga(s(T50), T51, T52))
U12_GGAA(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → ACKERMANH_IN_GGA(T50, T52, X125)
PI_IN_GGAA(T50, T51, T52, X125) → ACKERMANH_IN_GGA(s(T50), T51, T52)
PG_IN_GAA(T32, T33, X83) → ACKERMANE_IN_GA(T32, T33)
ackermanE_in_ga(T28, X60) → U4_ga(T28, X60, ackermanF_in_ga(T28, X60))
ackermanH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermanF_in_ga(T45, X109))
ackermanH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
U4_ga(T28, X60, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U6_gga(T45, X109, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
ackermanF_in_ga(0, s(s(0))) → ackermanF_out_ga(0, s(s(0)))
ackermanF_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, ackermanH_in_gga(s(T50), T51, T52))
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermanE_in_ga(T32, T33))
U13_ggaa(T50, T51, T52, X125, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
ackermanH_in_gga(0, T40, s(T40)) → ackermanH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, X83, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
ACKERMANE_IN_GA(T28) → ACKERMANF_IN_GA(T28)
ACKERMANF_IN_GA(s(T32)) → PG_IN_GAA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, ackermanE_in_ga(T32))
U10_GAA(T32, ackermanE_out_ga(T32, T33)) → ACKERMANH_IN_GGA(T32, T33)
ACKERMANH_IN_GGA(s(T45), 0) → ACKERMANF_IN_GA(T45)
ACKERMANH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackermanH_in_gga(s(T50), T51))
U12_GGAA(T50, T51, ackermanH_out_gga(s(T50), T51, T52)) → ACKERMANH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKERMANH_IN_GGA(s(T50), T51)
PG_IN_GAA(T32) → ACKERMANE_IN_GA(T32)
ackermanE_in_ga(T28) → U4_ga(T28, ackermanF_in_ga(T28))
ackermanH_in_gga(s(T45), 0) → U6_gga(T45, ackermanF_in_ga(T45))
ackermanH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U6_gga(T45, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
ackermanF_in_ga(0) → ackermanF_out_ga(0, s(s(0)))
ackermanF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermanH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermanH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackermanE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermanH_in_gga(T32, T33))
ackermanH_in_gga(0, T40) → ackermanH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
ackermanE_in_ga(x0)
ackermanH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermanF_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)
PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackermanF_in_ga(T32)))
ACKERMANE_IN_GA(T28) → ACKERMANF_IN_GA(T28)
ACKERMANF_IN_GA(s(T32)) → PG_IN_GAA(T32)
U10_GAA(T32, ackermanE_out_ga(T32, T33)) → ACKERMANH_IN_GGA(T32, T33)
ACKERMANH_IN_GGA(s(T45), 0) → ACKERMANF_IN_GA(T45)
ACKERMANH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackermanH_in_gga(s(T50), T51))
U12_GGAA(T50, T51, ackermanH_out_gga(s(T50), T51, T52)) → ACKERMANH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKERMANH_IN_GGA(s(T50), T51)
PG_IN_GAA(T32) → ACKERMANE_IN_GA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackermanF_in_ga(T32)))
ackermanE_in_ga(T28) → U4_ga(T28, ackermanF_in_ga(T28))
ackermanH_in_gga(s(T45), 0) → U6_gga(T45, ackermanF_in_ga(T45))
ackermanH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U6_gga(T45, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
ackermanF_in_ga(0) → ackermanF_out_ga(0, s(s(0)))
ackermanF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermanH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermanH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackermanE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermanH_in_gga(T32, T33))
ackermanH_in_gga(0, T40) → ackermanH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
ackermanE_in_ga(x0)
ackermanH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermanF_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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACKERMANH_IN_GGA(s(T45), 0) → ACKERMANF_IN_GA(T45)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackermanH_in_gga(s(T50), T51))
PG_IN_GAA(T32) → ACKERMANE_IN_GA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackermanF_in_ga(T32)))
POL(0) = 1
POL(ACKERMANE_IN_GA(x1)) = x1
POL(ACKERMANF_IN_GA(x1)) = x1
POL(ACKERMANH_IN_GGA(x1, x2)) = x1
POL(PG_IN_GAA(x1)) = 1 + x1
POL(PI_IN_GGAA(x1, x2)) = 1 + x1
POL(U10_GAA(x1, x2)) = x1
POL(U10_gaa(x1, x2)) = 0
POL(U11_gaa(x1, x2, x3)) = 0
POL(U12_GGAA(x1, x2, x3)) = x1
POL(U12_ggaa(x1, x2, x3)) = 0
POL(U13_ggaa(x1, x2, x3, x4)) = 0
POL(U4_ga(x1, x2)) = 0
POL(U5_ga(x1, x2)) = 0
POL(U6_gga(x1, x2)) = 0
POL(U7_gga(x1, x2, x3)) = 0
POL(ackermanE_in_ga(x1)) = 0
POL(ackermanE_out_ga(x1, x2)) = 0
POL(ackermanF_in_ga(x1)) = x1
POL(ackermanF_out_ga(x1, x2)) = 0
POL(ackermanH_in_gga(x1, x2)) = 1 + x1 + x2
POL(ackermanH_out_gga(x1, x2, x3)) = x1
POL(pG_in_gaa(x1)) = 0
POL(pG_out_gaa(x1, x2, x3)) = 0
POL(pI_in_ggaa(x1, x2)) = 0
POL(pI_out_ggaa(x1, x2, x3, x4)) = 0
POL(s(x1)) = 1 + x1
ACKERMANE_IN_GA(T28) → ACKERMANF_IN_GA(T28)
ACKERMANF_IN_GA(s(T32)) → PG_IN_GAA(T32)
U10_GAA(T32, ackermanE_out_ga(T32, T33)) → ACKERMANH_IN_GGA(T32, T33)
ACKERMANH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
U12_GGAA(T50, T51, ackermanH_out_gga(s(T50), T51, T52)) → ACKERMANH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKERMANH_IN_GGA(s(T50), T51)
ackermanE_in_ga(T28) → U4_ga(T28, ackermanF_in_ga(T28))
ackermanH_in_gga(s(T45), 0) → U6_gga(T45, ackermanF_in_ga(T45))
ackermanH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U6_gga(T45, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
ackermanF_in_ga(0) → ackermanF_out_ga(0, s(s(0)))
ackermanF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermanH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermanH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackermanE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermanH_in_gga(T32, T33))
ackermanH_in_gga(0, T40) → ackermanH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
ackermanE_in_ga(x0)
ackermanH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermanF_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)
PI_IN_GGAA(T50, T51) → ACKERMANH_IN_GGA(s(T50), T51)
ACKERMANH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
ackermanE_in_ga(T28) → U4_ga(T28, ackermanF_in_ga(T28))
ackermanH_in_gga(s(T45), 0) → U6_gga(T45, ackermanF_in_ga(T45))
ackermanH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U6_gga(T45, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
ackermanF_in_ga(0) → ackermanF_out_ga(0, s(s(0)))
ackermanF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermanH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermanH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackermanE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermanH_in_gga(T32, T33))
ackermanH_in_gga(0, T40) → ackermanH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
ackermanE_in_ga(x0)
ackermanH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermanF_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)
PI_IN_GGAA(T50, T51) → ACKERMANH_IN_GGA(s(T50), T51)
ACKERMANH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
ackermanE_in_ga(x0)
ackermanH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermanF_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)
ackermanE_in_ga(x0)
ackermanH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackermanF_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)
PI_IN_GGAA(T50, T51) → ACKERMANH_IN_GGA(s(T50), T51)
ACKERMANH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
From the DPs we obtained the following set of size-change graphs:
ACKERMANA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackermanE_in_ga(T20, T23))
U8_GAA(T20, T23, T22, ackermanE_out_ga(T20, T23)) → ACKERMANA_IN_GGA(T20, T23, T22)
ACKERMANA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackermanF_in_ga(T70, T71))
U14_GAA(T70, T71, T65, ackermanF_out_ga(T70, T71)) → ACKERMANA_IN_GGA(T70, T71, T65)
ACKERMANA_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, ackermanH_in_gga(s(T78), T79, T80))
U16_GGAAA(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
U18_GGAA(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → ACKERMANA_IN_GGA(T78, T83, T65)
ackermanA_in_gga(0, T5, s(T5)) → ackermanA_out_gga(0, T5, s(T5))
ackermanA_in_gga(s(0), 0, s(s(0))) → ackermanA_out_gga(s(0), 0, s(s(0)))
ackermanA_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, ackermanE_in_ga(T20, T23))
ackermanE_in_ga(T28, X60) → U4_ga(T28, X60, ackermanF_in_ga(T28, X60))
ackermanF_in_ga(0, s(s(0))) → ackermanF_out_ga(0, s(s(0)))
ackermanF_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, ackermanE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
ackermanH_in_gga(0, T40, s(T40)) → ackermanH_out_gga(0, T40, s(T40))
ackermanH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermanF_in_ga(T45, X109))
U6_gga(T45, X109, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
ackermanH_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, ackermanH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackermanE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackermanA_in_gga(T20, T23, T22))
ackermanA_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, ackermanF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackermanF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackermanA_in_gga(T70, T71, T65))
ackermanA_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, ackermanH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackermanA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackermanA_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)) → ackermanA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackermanA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackermanA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackermanA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackermanA_out_gga(s(s(T20)), 0, T22)
ACKERMANA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackermanE_in_ga(T20, T23))
U8_GAA(T20, T23, T22, ackermanE_out_ga(T20, T23)) → ACKERMANA_IN_GGA(T20, T23, T22)
ACKERMANA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackermanF_in_ga(T70, T71))
U14_GAA(T70, T71, T65, ackermanF_out_ga(T70, T71)) → ACKERMANA_IN_GGA(T70, T71, T65)
ACKERMANA_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, ackermanH_in_gga(s(T78), T79, T80))
U16_GGAAA(T78, T79, T80, X182, T65, ackermanH_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, ackermanH_in_gga(T78, T80, T83))
U18_GGAA(T78, T80, T83, T65, ackermanH_out_gga(T78, T80, T83)) → ACKERMANA_IN_GGA(T78, T83, T65)
ackermanE_in_ga(T28, X60) → U4_ga(T28, X60, ackermanF_in_ga(T28, X60))
ackermanF_in_ga(0, s(s(0))) → ackermanF_out_ga(0, s(s(0)))
ackermanF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
ackermanH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackermanF_in_ga(T45, X109))
ackermanH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ackermanH_in_gga(0, T40, s(T40)) → ackermanH_out_gga(0, T40, s(T40))
U4_ga(T28, X60, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U6_gga(T45, X109, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackermanE_in_ga(T32, T33))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackermanH_in_gga(s(T50), T51, T52))
U10_gaa(T32, T33, X83, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackermanH_in_gga(T32, T33, X83))
U12_ggaa(T50, T51, T52, X125, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackermanH_in_gga(T50, T52, X125))
U11_gaa(T32, T33, X83, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U13_ggaa(T50, T51, T52, X125, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
ACKERMANA_IN_GGA(s(s(T20)), 0) → PB_IN_GAA(T20)
PB_IN_GAA(T20) → U8_GAA(T20, ackermanE_in_ga(T20))
U8_GAA(T20, ackermanE_out_ga(T20, T23)) → ACKERMANA_IN_GGA(T20, T23)
ACKERMANA_IN_GGA(s(T70), s(0)) → PC_IN_GAA(T70)
PC_IN_GAA(T70) → U14_GAA(T70, ackermanF_in_ga(T70))
U14_GAA(T70, ackermanF_out_ga(T70, T71)) → ACKERMANA_IN_GGA(T70, T71)
ACKERMANA_IN_GGA(s(T78), s(s(T79))) → PD_IN_GGAAA(T78, T79)
PD_IN_GGAAA(T78, T79) → U16_GGAAA(T78, T79, ackermanH_in_gga(s(T78), T79))
U16_GGAAA(T78, T79, ackermanH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80)
PJ_IN_GGAA(T78, T80) → U18_GGAA(T78, T80, ackermanH_in_gga(T78, T80))
U18_GGAA(T78, T80, ackermanH_out_gga(T78, T80, T83)) → ACKERMANA_IN_GGA(T78, T83)
ackermanE_in_ga(T28) → U4_ga(T28, ackermanF_in_ga(T28))
ackermanF_in_ga(0) → ackermanF_out_ga(0, s(s(0)))
ackermanF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
ackermanH_in_gga(s(T45), 0) → U6_gga(T45, ackermanF_in_ga(T45))
ackermanH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
ackermanH_in_gga(0, T40) → ackermanH_out_gga(0, T40, s(T40))
U4_ga(T28, ackermanF_out_ga(T28, X60)) → ackermanE_out_ga(T28, X60)
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackermanF_out_ga(s(T32), X83)
U6_gga(T45, ackermanF_out_ga(T45, X109)) → ackermanH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackermanH_out_gga(s(T50), s(T51), X125)
pG_in_gaa(T32) → U10_gaa(T32, ackermanE_in_ga(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackermanH_in_gga(s(T50), T51))
U10_gaa(T32, ackermanE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackermanH_in_gga(T32, T33))
U12_ggaa(T50, T51, ackermanH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackermanH_in_gga(T50, T52))
U11_gaa(T32, T33, ackermanH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U13_ggaa(T50, T51, T52, ackermanH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
ackermanE_in_ga(x0)
ackermanF_in_ga(x0)
ackermanH_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)
From the DPs we obtained the following set of size-change graphs: