0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔)
↳11 PiDP
↳12 PiDPToQDPProof (⇐)
↳13 QDP
↳14 QDPOrderProof (⇔)
↳15 QDP
↳16 DependencyGraphProof (⇔)
↳17 QDP
↳18 UsableRulesProof (⇔)
↳19 QDP
↳20 QReductionProof (⇔)
↳21 QDP
↳22 NonTerminationProof (⇔)
↳23 NO
↳24 PiDP
↳25 UsableRulesProof (⇔)
↳26 PiDP
↳27 PiDPToQDPProof (⇐)
↳28 QDP
↳29 QDPSizeChangeProof (⇔)
↳30 YES
↳31 PiDP
↳32 UsableRulesProof (⇔)
↳33 PiDP
↳34 PiDPToQDPProof (⇐)
↳35 QDP
↳36 QDPSizeChangeProof (⇔)
↳37 YES
↳38 PrologToPiTRSProof (⇐)
↳39 PiTRS
↳40 DependencyPairsProof (⇔)
↳41 PiDP
↳42 DependencyGraphProof (⇔)
↳43 AND
↳44 PiDP
↳45 UsableRulesProof (⇔)
↳46 PiDP
↳47 PiDPToQDPProof (⇐)
↳48 QDP
↳49 QDPOrderProof (⇔)
↳50 QDP
↳51 DependencyGraphProof (⇔)
↳52 QDP
↳53 UsableRulesProof (⇔)
↳54 QDP
↳55 QReductionProof (⇔)
↳56 QDP
↳57 NonTerminationProof (⇔)
↳58 NO
↳59 PiDP
↳60 UsableRulesProof (⇔)
↳61 PiDP
↳62 PiDPToQDPProof (⇐)
↳63 QDP
↳64 QDPSizeChangeProof (⇔)
↳65 YES
↳66 PiDP
↳67 UsableRulesProof (⇔)
↳68 PiDP
↳69 PiDPToQDPProof (⇐)
↳70 QDP
↳71 QDPSizeChangeProof (⇔)
↳72 YES
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → U9_GGA(T20, T22, ackermann21_in_ga(T20, X40))
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → ACKERMANN21_IN_GA(T20, X40)
ACKERMANN21_IN_GA(T30, X73) → U1_GA(T30, X73, ackermann27_in_ga(T30, X73))
ACKERMANN21_IN_GA(T30, X73) → ACKERMANN27_IN_GA(T30, X73)
ACKERMANN27_IN_GA(s(T34), X97) → U2_GA(T34, X97, ackermann21_in_ga(T34, X96))
ACKERMANN27_IN_GA(s(T34), X97) → ACKERMANN21_IN_GA(T34, X96)
ACKERMANN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackermann21_in_ga(T34, T36))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → U4_GA(T34, X97, ackermann38_in_gaa(T34, T36, X97))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → ACKERMANN38_IN_GAA(T34, T36, X97)
ACKERMANN38_IN_GAA(s(T49), 0, X133) → U5_GAA(T49, X133, ackermann27_in_ga(T49, X133))
ACKERMANN38_IN_GAA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U6_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → ACKERMANN38_IN_GAA(s(T54), T55, X150)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_GAA(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → U10_GGA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GGA(T20, T22, ackermann21_out_ga(T20, T24)) → U11_GGA(T20, T22, ackermann1_in_gaa(T20, T24, T22))
U10_GGA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U9_GAA(T20, T22, ackermann21_in_ga(T20, X40))
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → ACKERMANN21_IN_GA(T20, X40)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → U11_GAA(T20, T22, ackermann1_in_gaa(T20, T24, T22))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U12_GAA(T76, T71, ackermann27_in_ga(T76, X200))
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → ACKERMANN27_IN_GA(T76, X200)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → U14_GAA(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U15_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → ACKERMANN38_IN_GAA(s(T84), T85, X221)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → ACKERMANN38_IN_GAA(T84, T87, X222)
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_GAA(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → U12_GGA(T76, T71, ackermann27_in_ga(T76, X200))
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → ACKERMANN27_IN_GA(T76, X200)
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → U13_GGA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GGA(T76, T71, ackermann27_out_ga(T76, T77)) → U14_GGA(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U13_GGA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → U15_GGA(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → ACKERMANN38_IN_GGA(s(T84), T85, X221)
ACKERMANN38_IN_GGA(s(T49), 0, X133) → U5_GGA(T49, X133, ackermann27_in_ga(T49, X133))
ACKERMANN38_IN_GGA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → U6_GGA(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → ACKERMANN38_IN_GGA(s(T54), T55, X150)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → U7_GGA(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_GGA(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_GGA(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U7_GGA(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → U16_GGA(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_GGA(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → ACKERMANN38_IN_GAA(T84, T87, X222)
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_GGA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GGA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_GGA(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U18_GGA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → U9_GGA(T20, T22, ackermann21_in_ga(T20, X40))
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → ACKERMANN21_IN_GA(T20, X40)
ACKERMANN21_IN_GA(T30, X73) → U1_GA(T30, X73, ackermann27_in_ga(T30, X73))
ACKERMANN21_IN_GA(T30, X73) → ACKERMANN27_IN_GA(T30, X73)
ACKERMANN27_IN_GA(s(T34), X97) → U2_GA(T34, X97, ackermann21_in_ga(T34, X96))
ACKERMANN27_IN_GA(s(T34), X97) → ACKERMANN21_IN_GA(T34, X96)
ACKERMANN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackermann21_in_ga(T34, T36))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → U4_GA(T34, X97, ackermann38_in_gaa(T34, T36, X97))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → ACKERMANN38_IN_GAA(T34, T36, X97)
ACKERMANN38_IN_GAA(s(T49), 0, X133) → U5_GAA(T49, X133, ackermann27_in_ga(T49, X133))
ACKERMANN38_IN_GAA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U6_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → ACKERMANN38_IN_GAA(s(T54), T55, X150)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_GAA(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → U10_GGA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GGA(T20, T22, ackermann21_out_ga(T20, T24)) → U11_GGA(T20, T22, ackermann1_in_gaa(T20, T24, T22))
U10_GGA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U9_GAA(T20, T22, ackermann21_in_ga(T20, X40))
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → ACKERMANN21_IN_GA(T20, X40)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → U11_GAA(T20, T22, ackermann1_in_gaa(T20, T24, T22))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U12_GAA(T76, T71, ackermann27_in_ga(T76, X200))
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → ACKERMANN27_IN_GA(T76, X200)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → U14_GAA(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U15_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → ACKERMANN38_IN_GAA(s(T84), T85, X221)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → ACKERMANN38_IN_GAA(T84, T87, X222)
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_GAA(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → U12_GGA(T76, T71, ackermann27_in_ga(T76, X200))
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → ACKERMANN27_IN_GA(T76, X200)
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → U13_GGA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GGA(T76, T71, ackermann27_out_ga(T76, T77)) → U14_GGA(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U13_GGA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → U15_GGA(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → ACKERMANN38_IN_GGA(s(T84), T85, X221)
ACKERMANN38_IN_GGA(s(T49), 0, X133) → U5_GGA(T49, X133, ackermann27_in_ga(T49, X133))
ACKERMANN38_IN_GGA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → U6_GGA(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → ACKERMANN38_IN_GGA(s(T54), T55, X150)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → U7_GGA(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_GGA(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_GGA(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U7_GGA(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → U16_GGA(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_GGA(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → ACKERMANN38_IN_GAA(T84, T87, X222)
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_GGA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GGA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_GGA(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U18_GGA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN21_IN_GA(T30, X73) → ACKERMANN27_IN_GA(T30, X73)
ACKERMANN27_IN_GA(s(T34), X97) → ACKERMANN21_IN_GA(T34, X96)
ACKERMANN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackermann21_in_ga(T34, T36))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → ACKERMANN38_IN_GAA(T34, T36, X97)
ACKERMANN38_IN_GAA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → ACKERMANN38_IN_GAA(s(T54), T55, X150)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN21_IN_GA(T30, X73) → ACKERMANN27_IN_GA(T30, X73)
ACKERMANN27_IN_GA(s(T34), X97) → ACKERMANN21_IN_GA(T34, X96)
ACKERMANN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackermann21_in_ga(T34, T36))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → ACKERMANN38_IN_GAA(T34, T36, X97)
ACKERMANN38_IN_GAA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → ACKERMANN38_IN_GAA(s(T54), T55, X150)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
ACKERMANN21_IN_GA(T30) → ACKERMANN27_IN_GA(T30)
ACKERMANN27_IN_GA(s(T34)) → ACKERMANN21_IN_GA(T34)
ACKERMANN27_IN_GA(s(T34)) → U3_GA(T34, ackermann21_in_ga(T34))
U3_GA(T34, ackermann21_out_ga) → ACKERMANN38_IN_GAA(T34)
ACKERMANN38_IN_GAA(s(T49)) → ACKERMANN27_IN_GA(T49)
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ACKERMANN38_IN_GAA(s(T54)) → U7_GAA(T54, ackermann38_in_gaa(s(T54)))
U7_GAA(T54, ackermann38_out_gaa) → ACKERMANN38_IN_GAA(T54)
ackermann21_in_ga(T30) → U1_ga(ackermann27_in_ga(T30))
ackermann38_in_gaa(s(T49)) → U5_gaa(ackermann27_in_ga(T49))
ackermann38_in_gaa(s(T54)) → U6_gaa(ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(s(T54)) → U7_gaa(T54, ackermann38_in_gaa(s(T54)))
U1_ga(ackermann27_out_ga) → ackermann21_out_ga
U5_gaa(ackermann27_out_ga) → ackermann38_out_gaa
U6_gaa(ackermann38_out_gaa) → ackermann38_out_gaa
U7_gaa(T54, ackermann38_out_gaa) → U8_gaa(ackermann38_in_gaa(T54))
ackermann27_in_ga(0) → ackermann27_out_ga
ackermann27_in_ga(s(T34)) → U2_ga(ackermann21_in_ga(T34))
ackermann27_in_ga(s(T34)) → U3_ga(T34, ackermann21_in_ga(T34))
U8_gaa(ackermann38_out_gaa) → ackermann38_out_gaa
U2_ga(ackermann21_out_ga) → ackermann27_out_ga
U3_ga(T34, ackermann21_out_ga) → U4_ga(ackermann38_in_gaa(T34))
ackermann38_in_gaa(0) → ackermann38_out_gaa
U4_ga(ackermann38_out_gaa) → ackermann27_out_ga
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACKERMANN27_IN_GA(s(T34)) → ACKERMANN21_IN_GA(T34)
U3_GA(T34, ackermann21_out_ga) → ACKERMANN38_IN_GAA(T34)
ACKERMANN38_IN_GAA(s(T49)) → ACKERMANN27_IN_GA(T49)
U7_GAA(T54, ackermann38_out_gaa) → ACKERMANN38_IN_GAA(T54)
POL( U3_GA(x1, x2) ) = 2x1 + 2
POL( U7_GAA(x1, x2) ) = x1 + 1
POL( ackermann21_in_ga(x1) ) = max{0, -2}
POL( U1_ga(x1) ) = max{0, -1}
POL( ackermann27_in_ga(x1) ) = 0
POL( ackermann38_in_gaa(x1) ) = 2
POL( s(x1) ) = 2x1 + 2
POL( U5_gaa(x1) ) = max{0, -2}
POL( U6_gaa(x1) ) = 1
POL( U7_gaa(x1, x2) ) = max{0, 2x1 - 2}
POL( U2_ga(x1) ) = 2
POL( ackermann21_out_ga ) = 2
POL( ackermann27_out_ga ) = 2
POL( 0 ) = 0
POL( U3_ga(x1, x2) ) = x1 + x2 + 1
POL( U4_ga(x1) ) = max{0, -2}
POL( U8_gaa(x1) ) = 2x1 + 2
POL( ackermann38_out_gaa ) = 2
POL( ACKERMANN21_IN_GA(x1) ) = x1
POL( ACKERMANN27_IN_GA(x1) ) = x1
POL( ACKERMANN38_IN_GAA(x1) ) = max{0, x1 - 1}
ACKERMANN21_IN_GA(T30) → ACKERMANN27_IN_GA(T30)
ACKERMANN27_IN_GA(s(T34)) → U3_GA(T34, ackermann21_in_ga(T34))
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ACKERMANN38_IN_GAA(s(T54)) → U7_GAA(T54, ackermann38_in_gaa(s(T54)))
ackermann21_in_ga(T30) → U1_ga(ackermann27_in_ga(T30))
ackermann38_in_gaa(s(T49)) → U5_gaa(ackermann27_in_ga(T49))
ackermann38_in_gaa(s(T54)) → U6_gaa(ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(s(T54)) → U7_gaa(T54, ackermann38_in_gaa(s(T54)))
U1_ga(ackermann27_out_ga) → ackermann21_out_ga
U5_gaa(ackermann27_out_ga) → ackermann38_out_gaa
U6_gaa(ackermann38_out_gaa) → ackermann38_out_gaa
U7_gaa(T54, ackermann38_out_gaa) → U8_gaa(ackermann38_in_gaa(T54))
ackermann27_in_ga(0) → ackermann27_out_ga
ackermann27_in_ga(s(T34)) → U2_ga(ackermann21_in_ga(T34))
ackermann27_in_ga(s(T34)) → U3_ga(T34, ackermann21_in_ga(T34))
U8_gaa(ackermann38_out_gaa) → ackermann38_out_gaa
U2_ga(ackermann21_out_ga) → ackermann27_out_ga
U3_ga(T34, ackermann21_out_ga) → U4_ga(ackermann38_in_gaa(T34))
ackermann38_in_gaa(0) → ackermann38_out_gaa
U4_ga(ackermann38_out_gaa) → ackermann27_out_ga
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ackermann21_in_ga(T30) → U1_ga(ackermann27_in_ga(T30))
ackermann38_in_gaa(s(T49)) → U5_gaa(ackermann27_in_ga(T49))
ackermann38_in_gaa(s(T54)) → U6_gaa(ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(s(T54)) → U7_gaa(T54, ackermann38_in_gaa(s(T54)))
U1_ga(ackermann27_out_ga) → ackermann21_out_ga
U5_gaa(ackermann27_out_ga) → ackermann38_out_gaa
U6_gaa(ackermann38_out_gaa) → ackermann38_out_gaa
U7_gaa(T54, ackermann38_out_gaa) → U8_gaa(ackermann38_in_gaa(T54))
ackermann27_in_ga(0) → ackermann27_out_ga
ackermann27_in_ga(s(T34)) → U2_ga(ackermann21_in_ga(T34))
ackermann27_in_ga(s(T34)) → U3_ga(T34, ackermann21_in_ga(T34))
U8_gaa(ackermann38_out_gaa) → ackermann38_out_gaa
U2_ga(ackermann21_out_ga) → ackermann27_out_ga
U3_ga(T34, ackermann21_out_ga) → U4_ga(ackermann38_in_gaa(T34))
ackermann38_in_gaa(0) → ackermann38_out_gaa
U4_ga(ackermann38_out_gaa) → ackermann27_out_ga
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → ACKERMANN38_IN_GGA(s(T54), T55, X150)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → ACKERMANN38_IN_GGA(s(T54), T55, X150)
ACKERMANN38_IN_GGA(s(T54), s(T55)) → ACKERMANN38_IN_GGA(s(T54), T55)
From the DPs we obtained the following set of size-change graphs:
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
ACKERMANN1_IN_GAA(s(s(T20))) → U10_GAA(T20, ackermann21_in_ga(T20))
U10_GAA(T20, ackermann21_out_ga) → ACKERMANN1_IN_GAA(T20)
ACKERMANN1_IN_GAA(s(T76)) → U13_GAA(T76, ackermann27_in_ga(T76))
U13_GAA(T76, ackermann27_out_ga) → ACKERMANN1_IN_GAA(T76)
ACKERMANN1_IN_GAA(s(T84)) → U16_GAA(T84, ackermann38_in_gaa(s(T84)))
U16_GAA(T84, ackermann38_out_gaa) → U18_GAA(T84, ackermann38_in_gaa(T84))
U18_GAA(T84, ackermann38_out_gaa) → ACKERMANN1_IN_GAA(T84)
ackermann21_in_ga(T30) → U1_ga(ackermann27_in_ga(T30))
ackermann27_in_ga(0) → ackermann27_out_ga
ackermann27_in_ga(s(T34)) → U2_ga(ackermann21_in_ga(T34))
ackermann27_in_ga(s(T34)) → U3_ga(T34, ackermann21_in_ga(T34))
ackermann38_in_gaa(s(T49)) → U5_gaa(ackermann27_in_ga(T49))
ackermann38_in_gaa(s(T54)) → U6_gaa(ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(s(T54)) → U7_gaa(T54, ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(0) → ackermann38_out_gaa
U1_ga(ackermann27_out_ga) → ackermann21_out_ga
U2_ga(ackermann21_out_ga) → ackermann27_out_ga
U3_ga(T34, ackermann21_out_ga) → U4_ga(ackermann38_in_gaa(T34))
U5_gaa(ackermann27_out_ga) → ackermann38_out_gaa
U6_gaa(ackermann38_out_gaa) → ackermann38_out_gaa
U7_gaa(T54, ackermann38_out_gaa) → U8_gaa(ackermann38_in_gaa(T54))
U4_ga(ackermann38_out_gaa) → ackermann27_out_ga
U8_gaa(ackermann38_out_gaa) → ackermann38_out_gaa
ackermann21_in_ga(x0)
ackermann27_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
U4_ga(x0)
U8_gaa(x0)
From the DPs we obtained the following set of size-change graphs:
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → U9_GGA(T20, T22, ackermann21_in_ga(T20, X40))
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → ACKERMANN21_IN_GA(T20, X40)
ACKERMANN21_IN_GA(T30, X73) → U1_GA(T30, X73, ackermann27_in_ga(T30, X73))
ACKERMANN21_IN_GA(T30, X73) → ACKERMANN27_IN_GA(T30, X73)
ACKERMANN27_IN_GA(s(T34), X97) → U2_GA(T34, X97, ackermann21_in_ga(T34, X96))
ACKERMANN27_IN_GA(s(T34), X97) → ACKERMANN21_IN_GA(T34, X96)
ACKERMANN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackermann21_in_ga(T34, T36))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → U4_GA(T34, X97, ackermann38_in_gaa(T34, T36, X97))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → ACKERMANN38_IN_GAA(T34, T36, X97)
ACKERMANN38_IN_GAA(s(T49), 0, X133) → U5_GAA(T49, X133, ackermann27_in_ga(T49, X133))
ACKERMANN38_IN_GAA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U6_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → ACKERMANN38_IN_GAA(s(T54), T55, X150)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_GAA(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → U10_GGA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GGA(T20, T22, ackermann21_out_ga(T20, T24)) → U11_GGA(T20, T22, ackermann1_in_gaa(T20, T24, T22))
U10_GGA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U9_GAA(T20, T22, ackermann21_in_ga(T20, X40))
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → ACKERMANN21_IN_GA(T20, X40)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → U11_GAA(T20, T22, ackermann1_in_gaa(T20, T24, T22))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U12_GAA(T76, T71, ackermann27_in_ga(T76, X200))
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → ACKERMANN27_IN_GA(T76, X200)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → U14_GAA(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U15_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → ACKERMANN38_IN_GAA(s(T84), T85, X221)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → ACKERMANN38_IN_GAA(T84, T87, X222)
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_GAA(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → U12_GGA(T76, T71, ackermann27_in_ga(T76, X200))
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → ACKERMANN27_IN_GA(T76, X200)
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → U13_GGA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GGA(T76, T71, ackermann27_out_ga(T76, T77)) → U14_GGA(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U13_GGA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → U15_GGA(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → ACKERMANN38_IN_GGA(s(T84), T85, X221)
ACKERMANN38_IN_GGA(s(T49), 0, X133) → U5_GGA(T49, X133, ackermann27_in_ga(T49, X133))
ACKERMANN38_IN_GGA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → U6_GGA(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → ACKERMANN38_IN_GGA(s(T54), T55, X150)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → U7_GGA(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_GGA(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_GGA(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U7_GGA(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → U16_GGA(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_GGA(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → ACKERMANN38_IN_GAA(T84, T87, X222)
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_GGA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GGA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_GGA(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U18_GGA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → U9_GGA(T20, T22, ackermann21_in_ga(T20, X40))
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → ACKERMANN21_IN_GA(T20, X40)
ACKERMANN21_IN_GA(T30, X73) → U1_GA(T30, X73, ackermann27_in_ga(T30, X73))
ACKERMANN21_IN_GA(T30, X73) → ACKERMANN27_IN_GA(T30, X73)
ACKERMANN27_IN_GA(s(T34), X97) → U2_GA(T34, X97, ackermann21_in_ga(T34, X96))
ACKERMANN27_IN_GA(s(T34), X97) → ACKERMANN21_IN_GA(T34, X96)
ACKERMANN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackermann21_in_ga(T34, T36))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → U4_GA(T34, X97, ackermann38_in_gaa(T34, T36, X97))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → ACKERMANN38_IN_GAA(T34, T36, X97)
ACKERMANN38_IN_GAA(s(T49), 0, X133) → U5_GAA(T49, X133, ackermann27_in_ga(T49, X133))
ACKERMANN38_IN_GAA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U6_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → ACKERMANN38_IN_GAA(s(T54), T55, X150)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_GAA(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ACKERMANN1_IN_GGA(s(s(T20)), 0, T22) → U10_GGA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GGA(T20, T22, ackermann21_out_ga(T20, T24)) → U11_GGA(T20, T22, ackermann1_in_gaa(T20, T24, T22))
U10_GGA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U9_GAA(T20, T22, ackermann21_in_ga(T20, X40))
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → ACKERMANN21_IN_GA(T20, X40)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → U11_GAA(T20, T22, ackermann1_in_gaa(T20, T24, T22))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U12_GAA(T76, T71, ackermann27_in_ga(T76, X200))
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → ACKERMANN27_IN_GA(T76, X200)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → U14_GAA(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U15_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → ACKERMANN38_IN_GAA(s(T84), T85, X221)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → ACKERMANN38_IN_GAA(T84, T87, X222)
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_GAA(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → U12_GGA(T76, T71, ackermann27_in_ga(T76, X200))
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → ACKERMANN27_IN_GA(T76, X200)
ACKERMANN1_IN_GGA(s(T76), s(0), T71) → U13_GGA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GGA(T76, T71, ackermann27_out_ga(T76, T77)) → U14_GGA(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U13_GGA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → U15_GGA(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → ACKERMANN38_IN_GGA(s(T84), T85, X221)
ACKERMANN38_IN_GGA(s(T49), 0, X133) → U5_GGA(T49, X133, ackermann27_in_ga(T49, X133))
ACKERMANN38_IN_GGA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → U6_GGA(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → ACKERMANN38_IN_GGA(s(T54), T55, X150)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → U7_GGA(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_GGA(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_GGA(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U7_GGA(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ACKERMANN1_IN_GGA(s(T84), s(s(T85)), T71) → U16_GGA(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_GGA(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → ACKERMANN38_IN_GAA(T84, T87, X222)
U16_GGA(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_GGA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GGA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_GGA(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U18_GGA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN21_IN_GA(T30, X73) → ACKERMANN27_IN_GA(T30, X73)
ACKERMANN27_IN_GA(s(T34), X97) → ACKERMANN21_IN_GA(T34, X96)
ACKERMANN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackermann21_in_ga(T34, T36))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → ACKERMANN38_IN_GAA(T34, T36, X97)
ACKERMANN38_IN_GAA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → ACKERMANN38_IN_GAA(s(T54), T55, X150)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN21_IN_GA(T30, X73) → ACKERMANN27_IN_GA(T30, X73)
ACKERMANN27_IN_GA(s(T34), X97) → ACKERMANN21_IN_GA(T34, X96)
ACKERMANN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackermann21_in_ga(T34, T36))
U3_GA(T34, X97, ackermann21_out_ga(T34, T36)) → ACKERMANN38_IN_GAA(T34, T36, X97)
ACKERMANN38_IN_GAA(s(T49), 0, X133) → ACKERMANN27_IN_GA(T49, X133)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → ACKERMANN38_IN_GAA(s(T54), T55, X150)
ACKERMANN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → ACKERMANN38_IN_GAA(T54, T57, X151)
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
ACKERMANN21_IN_GA(T30) → ACKERMANN27_IN_GA(T30)
ACKERMANN27_IN_GA(s(T34)) → ACKERMANN21_IN_GA(T34)
ACKERMANN27_IN_GA(s(T34)) → U3_GA(T34, ackermann21_in_ga(T34))
U3_GA(T34, ackermann21_out_ga(T34)) → ACKERMANN38_IN_GAA(T34)
ACKERMANN38_IN_GAA(s(T49)) → ACKERMANN27_IN_GA(T49)
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ACKERMANN38_IN_GAA(s(T54)) → U7_GAA(T54, ackermann38_in_gaa(s(T54)))
U7_GAA(T54, ackermann38_out_gaa(s(T54))) → ACKERMANN38_IN_GAA(T54)
ackermann21_in_ga(T30) → U1_ga(T30, ackermann27_in_ga(T30))
ackermann38_in_gaa(s(T49)) → U5_gaa(T49, ackermann27_in_ga(T49))
ackermann38_in_gaa(s(T54)) → U6_gaa(T54, ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(s(T54)) → U7_gaa(T54, ackermann38_in_gaa(s(T54)))
U1_ga(T30, ackermann27_out_ga(T30)) → ackermann21_out_ga(T30)
U5_gaa(T49, ackermann27_out_ga(T49)) → ackermann38_out_gaa(s(T49))
U6_gaa(T54, ackermann38_out_gaa(s(T54))) → ackermann38_out_gaa(s(T54))
U7_gaa(T54, ackermann38_out_gaa(s(T54))) → U8_gaa(T54, ackermann38_in_gaa(T54))
ackermann27_in_ga(0) → ackermann27_out_ga(0)
ackermann27_in_ga(s(T34)) → U2_ga(T34, ackermann21_in_ga(T34))
ackermann27_in_ga(s(T34)) → U3_ga(T34, ackermann21_in_ga(T34))
U8_gaa(T54, ackermann38_out_gaa(T54)) → ackermann38_out_gaa(s(T54))
U2_ga(T34, ackermann21_out_ga(T34)) → ackermann27_out_ga(s(T34))
U3_ga(T34, ackermann21_out_ga(T34)) → U4_ga(T34, ackermann38_in_gaa(T34))
ackermann38_in_gaa(0) → ackermann38_out_gaa(0)
U4_ga(T34, ackermann38_out_gaa(T34)) → ackermann27_out_ga(s(T34))
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
ACKERMANN27_IN_GA(s(T34)) → ACKERMANN21_IN_GA(T34)
U3_GA(T34, ackermann21_out_ga(T34)) → ACKERMANN38_IN_GAA(T34)
ACKERMANN38_IN_GAA(s(T49)) → ACKERMANN27_IN_GA(T49)
U7_GAA(T54, ackermann38_out_gaa(s(T54))) → ACKERMANN38_IN_GAA(T54)
POL(0) = 1
POL(ACKERMANN21_IN_GA(x1)) = x1
POL(ACKERMANN27_IN_GA(x1)) = x1
POL(ACKERMANN38_IN_GAA(x1)) = x1
POL(U1_ga(x1, x2)) = 0
POL(U2_ga(x1, x2)) = 0
POL(U3_GA(x1, x2)) = 1 + x1
POL(U3_ga(x1, x2)) = 0
POL(U4_ga(x1, x2)) = 0
POL(U5_gaa(x1, x2)) = 0
POL(U6_gaa(x1, x2)) = 0
POL(U7_GAA(x1, x2)) = 1 + x1
POL(U7_gaa(x1, x2)) = 0
POL(U8_gaa(x1, x2)) = 0
POL(ackermann21_in_ga(x1)) = 0
POL(ackermann21_out_ga(x1)) = 0
POL(ackermann27_in_ga(x1)) = 1 + x1
POL(ackermann27_out_ga(x1)) = 1
POL(ackermann38_in_gaa(x1)) = 1 + x1
POL(ackermann38_out_gaa(x1)) = 1
POL(s(x1)) = 1 + x1
ACKERMANN21_IN_GA(T30) → ACKERMANN27_IN_GA(T30)
ACKERMANN27_IN_GA(s(T34)) → U3_GA(T34, ackermann21_in_ga(T34))
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ACKERMANN38_IN_GAA(s(T54)) → U7_GAA(T54, ackermann38_in_gaa(s(T54)))
ackermann21_in_ga(T30) → U1_ga(T30, ackermann27_in_ga(T30))
ackermann38_in_gaa(s(T49)) → U5_gaa(T49, ackermann27_in_ga(T49))
ackermann38_in_gaa(s(T54)) → U6_gaa(T54, ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(s(T54)) → U7_gaa(T54, ackermann38_in_gaa(s(T54)))
U1_ga(T30, ackermann27_out_ga(T30)) → ackermann21_out_ga(T30)
U5_gaa(T49, ackermann27_out_ga(T49)) → ackermann38_out_gaa(s(T49))
U6_gaa(T54, ackermann38_out_gaa(s(T54))) → ackermann38_out_gaa(s(T54))
U7_gaa(T54, ackermann38_out_gaa(s(T54))) → U8_gaa(T54, ackermann38_in_gaa(T54))
ackermann27_in_ga(0) → ackermann27_out_ga(0)
ackermann27_in_ga(s(T34)) → U2_ga(T34, ackermann21_in_ga(T34))
ackermann27_in_ga(s(T34)) → U3_ga(T34, ackermann21_in_ga(T34))
U8_gaa(T54, ackermann38_out_gaa(T54)) → ackermann38_out_gaa(s(T54))
U2_ga(T34, ackermann21_out_ga(T34)) → ackermann27_out_ga(s(T34))
U3_ga(T34, ackermann21_out_ga(T34)) → U4_ga(T34, ackermann38_in_gaa(T34))
ackermann38_in_gaa(0) → ackermann38_out_gaa(0)
U4_ga(T34, ackermann38_out_gaa(T34)) → ackermann27_out_ga(s(T34))
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ackermann21_in_ga(T30) → U1_ga(T30, ackermann27_in_ga(T30))
ackermann38_in_gaa(s(T49)) → U5_gaa(T49, ackermann27_in_ga(T49))
ackermann38_in_gaa(s(T54)) → U6_gaa(T54, ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(s(T54)) → U7_gaa(T54, ackermann38_in_gaa(s(T54)))
U1_ga(T30, ackermann27_out_ga(T30)) → ackermann21_out_ga(T30)
U5_gaa(T49, ackermann27_out_ga(T49)) → ackermann38_out_gaa(s(T49))
U6_gaa(T54, ackermann38_out_gaa(s(T54))) → ackermann38_out_gaa(s(T54))
U7_gaa(T54, ackermann38_out_gaa(s(T54))) → U8_gaa(T54, ackermann38_in_gaa(T54))
ackermann27_in_ga(0) → ackermann27_out_ga(0)
ackermann27_in_ga(s(T34)) → U2_ga(T34, ackermann21_in_ga(T34))
ackermann27_in_ga(s(T34)) → U3_ga(T34, ackermann21_in_ga(T34))
U8_gaa(T54, ackermann38_out_gaa(T54)) → ackermann38_out_gaa(s(T54))
U2_ga(T34, ackermann21_out_ga(T34)) → ackermann27_out_ga(s(T34))
U3_ga(T34, ackermann21_out_ga(T34)) → U4_ga(T34, ackermann38_in_gaa(T34))
ackermann38_in_gaa(0) → ackermann38_out_gaa(0)
U4_ga(T34, ackermann38_out_gaa(T34)) → ackermann27_out_ga(s(T34))
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
ackermann21_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackermann27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
ACKERMANN38_IN_GAA(s(T54)) → ACKERMANN38_IN_GAA(s(T54))
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → ACKERMANN38_IN_GGA(s(T54), T55, X150)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN38_IN_GGA(s(T54), s(T55), X151) → ACKERMANN38_IN_GGA(s(T54), T55, X150)
ACKERMANN38_IN_GGA(s(T54), s(T55)) → ACKERMANN38_IN_GGA(s(T54), T55)
From the DPs we obtained the following set of size-change graphs:
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ackermann1_in_gga(0, T5, s(T5)) → ackermann1_out_gga(0, T5, s(T5))
ackermann1_in_gga(s(0), 0, s(s(0))) → ackermann1_out_gga(s(0), 0, s(s(0)))
ackermann1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackermann21_in_ga(T20, X40))
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U9_gga(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackermann21_in_ga(T20, T24))
U10_gga(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gga(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(0, T5, s(T5)) → ackermann1_out_gaa(0, T5, s(T5))
ackermann1_in_gaa(s(0), 0, s(s(0))) → ackermann1_out_gaa(s(0), 0, s(s(0)))
ackermann1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackermann21_in_ga(T20, X40))
U9_gaa(T20, T22, ackermann21_out_ga(T20, X40)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
ackermann1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackermann21_in_ga(T20, T24))
U10_gaa(T20, T22, ackermann21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackermann1_in_gaa(T20, T24, T22))
ackermann1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackermann27_in_ga(T76, X200))
U12_gaa(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gaa(s(T76), s(0), T71)
ackermann1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackermann27_in_ga(T76, T77))
U13_gaa(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackermann1_in_gaa(T76, T77, T71))
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, X221)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
ackermann1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackermann1_out_gaa(T20, T24, T22)) → ackermann1_out_gga(s(s(T20)), 0, T22)
ackermann1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackermann27_in_ga(T76, X200))
U12_gga(T76, T71, ackermann27_out_ga(T76, X200)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackermann27_in_ga(T76, T77))
U13_gga(T76, T71, ackermann27_out_ga(T76, T77)) → U14_gga(T76, T71, ackermann1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackermann1_out_gaa(T76, T77, T71)) → ackermann1_out_gga(s(T76), s(0), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, X221))
ackermann38_in_gga(0, T44, s(T44)) → ackermann38_out_gga(0, T44, s(T44))
ackermann38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackermann27_in_ga(T49, X133))
U5_gga(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gga(s(T49), 0, X133)
ackermann38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, X150))
ackermann38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackermann38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackermann38_out_gga(s(T54), T55, X150)) → ackermann38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, X221)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ackermann1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackermann38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, X222)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackermann38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackermann1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackermann1_out_gaa(T84, T91, T71)) → ackermann1_out_gga(s(T84), s(s(T85)), T71)
ACKERMANN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackermann21_in_ga(T20, T24))
U10_GAA(T20, T22, ackermann21_out_ga(T20, T24)) → ACKERMANN1_IN_GAA(T20, T24, T22)
ACKERMANN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackermann27_in_ga(T76, T77))
U13_GAA(T76, T71, ackermann27_out_ga(T76, T77)) → ACKERMANN1_IN_GAA(T76, T77, T71)
ACKERMANN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackermann38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackermann38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackermann38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackermann38_out_gaa(T84, T87, T91)) → ACKERMANN1_IN_GAA(T84, T91, T71)
ackermann21_in_ga(T30, X73) → U1_ga(T30, X73, ackermann27_in_ga(T30, X73))
ackermann27_in_ga(0, s(s(0))) → ackermann27_out_ga(0, s(s(0)))
ackermann27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackermann21_in_ga(T34, X96))
ackermann27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackermann21_in_ga(T34, T36))
ackermann38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackermann27_in_ga(T49, X133))
ackermann38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, X150))
ackermann38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackermann38_in_gaa(s(T54), T55, T57))
ackermann38_in_gaa(0, T44, s(T44)) → ackermann38_out_gaa(0, T44, s(T44))
U1_ga(T30, X73, ackermann27_out_ga(T30, X73)) → ackermann21_out_ga(T30, X73)
U2_ga(T34, X97, ackermann21_out_ga(T34, X96)) → ackermann27_out_ga(s(T34), X97)
U3_ga(T34, X97, ackermann21_out_ga(T34, T36)) → U4_ga(T34, X97, ackermann38_in_gaa(T34, T36, X97))
U5_gaa(T49, X133, ackermann27_out_ga(T49, X133)) → ackermann38_out_gaa(s(T49), 0, X133)
U6_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, X150)) → ackermann38_out_gaa(s(T54), s(T55), X151)
U7_gaa(T54, T55, X151, ackermann38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackermann38_in_gaa(T54, T57, X151))
U4_ga(T34, X97, ackermann38_out_gaa(T34, T36, X97)) → ackermann27_out_ga(s(T34), X97)
U8_gaa(T54, T55, X151, ackermann38_out_gaa(T54, T57, X151)) → ackermann38_out_gaa(s(T54), s(T55), X151)
ACKERMANN1_IN_GAA(s(s(T20))) → U10_GAA(T20, ackermann21_in_ga(T20))
U10_GAA(T20, ackermann21_out_ga(T20)) → ACKERMANN1_IN_GAA(T20)
ACKERMANN1_IN_GAA(s(T76)) → U13_GAA(T76, ackermann27_in_ga(T76))
U13_GAA(T76, ackermann27_out_ga(T76)) → ACKERMANN1_IN_GAA(T76)
ACKERMANN1_IN_GAA(s(T84)) → U16_GAA(T84, ackermann38_in_gaa(s(T84)))
U16_GAA(T84, ackermann38_out_gaa(s(T84))) → U18_GAA(T84, ackermann38_in_gaa(T84))
U18_GAA(T84, ackermann38_out_gaa(T84)) → ACKERMANN1_IN_GAA(T84)
ackermann21_in_ga(T30) → U1_ga(T30, ackermann27_in_ga(T30))
ackermann27_in_ga(0) → ackermann27_out_ga(0)
ackermann27_in_ga(s(T34)) → U2_ga(T34, ackermann21_in_ga(T34))
ackermann27_in_ga(s(T34)) → U3_ga(T34, ackermann21_in_ga(T34))
ackermann38_in_gaa(s(T49)) → U5_gaa(T49, ackermann27_in_ga(T49))
ackermann38_in_gaa(s(T54)) → U6_gaa(T54, ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(s(T54)) → U7_gaa(T54, ackermann38_in_gaa(s(T54)))
ackermann38_in_gaa(0) → ackermann38_out_gaa(0)
U1_ga(T30, ackermann27_out_ga(T30)) → ackermann21_out_ga(T30)
U2_ga(T34, ackermann21_out_ga(T34)) → ackermann27_out_ga(s(T34))
U3_ga(T34, ackermann21_out_ga(T34)) → U4_ga(T34, ackermann38_in_gaa(T34))
U5_gaa(T49, ackermann27_out_ga(T49)) → ackermann38_out_gaa(s(T49))
U6_gaa(T54, ackermann38_out_gaa(s(T54))) → ackermann38_out_gaa(s(T54))
U7_gaa(T54, ackermann38_out_gaa(s(T54))) → U8_gaa(T54, ackermann38_in_gaa(T54))
U4_ga(T34, ackermann38_out_gaa(T34)) → ackermann27_out_ga(s(T34))
U8_gaa(T54, ackermann38_out_gaa(T54)) → ackermann38_out_gaa(s(T54))
ackermann21_in_ga(x0)
ackermann27_in_ga(x0)
ackermann38_in_gaa(x0)
U1_ga(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
U4_ga(x0, x1)
U8_gaa(x0, x1)
From the DPs we obtained the following set of size-change graphs: