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
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → U9_GGA(T20, T22, ackerman21_in_ga(T20, X40))
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → ACKERMAN21_IN_GA(T20, X40)
ACKERMAN21_IN_GA(T30, X73) → U1_GA(T30, X73, ackerman27_in_ga(T30, X73))
ACKERMAN21_IN_GA(T30, X73) → ACKERMAN27_IN_GA(T30, X73)
ACKERMAN27_IN_GA(s(T34), X97) → U2_GA(T34, X97, ackerman21_in_ga(T34, X96))
ACKERMAN27_IN_GA(s(T34), X97) → ACKERMAN21_IN_GA(T34, X96)
ACKERMAN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackerman21_in_ga(T34, T36))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → U4_GA(T34, X97, ackerman38_in_gaa(T34, T36, X97))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → ACKERMAN38_IN_GAA(T34, T36, X97)
ACKERMAN38_IN_GAA(s(T49), 0, X133) → U5_GAA(T49, X133, ackerman27_in_ga(T49, X133))
ACKERMAN38_IN_GAA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U6_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → ACKERMAN38_IN_GAA(s(T54), T55, X150)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_GAA(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → U10_GGA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GGA(T20, T22, ackerman21_out_ga(T20, T24)) → U11_GGA(T20, T22, ackerman1_in_gaa(T20, T24, T22))
U10_GGA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U9_GAA(T20, T22, ackerman21_in_ga(T20, X40))
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → ACKERMAN21_IN_GA(T20, X40)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → U11_GAA(T20, T22, ackerman1_in_gaa(T20, T24, T22))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U12_GAA(T76, T71, ackerman27_in_ga(T76, X200))
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → ACKERMAN27_IN_GA(T76, X200)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → U14_GAA(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U15_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → ACKERMAN38_IN_GAA(s(T84), T85, X221)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → ACKERMAN38_IN_GAA(T84, T87, X222)
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_GAA(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → U12_GGA(T76, T71, ackerman27_in_ga(T76, X200))
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → ACKERMAN27_IN_GA(T76, X200)
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → U13_GGA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GGA(T76, T71, ackerman27_out_ga(T76, T77)) → U14_GGA(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U13_GGA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → U15_GGA(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → ACKERMAN38_IN_GGA(s(T84), T85, X221)
ACKERMAN38_IN_GGA(s(T49), 0, X133) → U5_GGA(T49, X133, ackerman27_in_ga(T49, X133))
ACKERMAN38_IN_GGA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → U6_GGA(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → ACKERMAN38_IN_GGA(s(T54), T55, X150)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → U7_GGA(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_GGA(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_GGA(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U7_GGA(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → U16_GGA(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_GGA(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → ACKERMAN38_IN_GAA(T84, T87, X222)
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_GGA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GGA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_GGA(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U18_GGA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → U9_GGA(T20, T22, ackerman21_in_ga(T20, X40))
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → ACKERMAN21_IN_GA(T20, X40)
ACKERMAN21_IN_GA(T30, X73) → U1_GA(T30, X73, ackerman27_in_ga(T30, X73))
ACKERMAN21_IN_GA(T30, X73) → ACKERMAN27_IN_GA(T30, X73)
ACKERMAN27_IN_GA(s(T34), X97) → U2_GA(T34, X97, ackerman21_in_ga(T34, X96))
ACKERMAN27_IN_GA(s(T34), X97) → ACKERMAN21_IN_GA(T34, X96)
ACKERMAN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackerman21_in_ga(T34, T36))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → U4_GA(T34, X97, ackerman38_in_gaa(T34, T36, X97))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → ACKERMAN38_IN_GAA(T34, T36, X97)
ACKERMAN38_IN_GAA(s(T49), 0, X133) → U5_GAA(T49, X133, ackerman27_in_ga(T49, X133))
ACKERMAN38_IN_GAA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U6_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → ACKERMAN38_IN_GAA(s(T54), T55, X150)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_GAA(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → U10_GGA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GGA(T20, T22, ackerman21_out_ga(T20, T24)) → U11_GGA(T20, T22, ackerman1_in_gaa(T20, T24, T22))
U10_GGA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U9_GAA(T20, T22, ackerman21_in_ga(T20, X40))
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → ACKERMAN21_IN_GA(T20, X40)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → U11_GAA(T20, T22, ackerman1_in_gaa(T20, T24, T22))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U12_GAA(T76, T71, ackerman27_in_ga(T76, X200))
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → ACKERMAN27_IN_GA(T76, X200)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → U14_GAA(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U15_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → ACKERMAN38_IN_GAA(s(T84), T85, X221)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → ACKERMAN38_IN_GAA(T84, T87, X222)
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_GAA(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → U12_GGA(T76, T71, ackerman27_in_ga(T76, X200))
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → ACKERMAN27_IN_GA(T76, X200)
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → U13_GGA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GGA(T76, T71, ackerman27_out_ga(T76, T77)) → U14_GGA(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U13_GGA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → U15_GGA(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → ACKERMAN38_IN_GGA(s(T84), T85, X221)
ACKERMAN38_IN_GGA(s(T49), 0, X133) → U5_GGA(T49, X133, ackerman27_in_ga(T49, X133))
ACKERMAN38_IN_GGA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → U6_GGA(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → ACKERMAN38_IN_GGA(s(T54), T55, X150)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → U7_GGA(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_GGA(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_GGA(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U7_GGA(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → U16_GGA(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_GGA(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → ACKERMAN38_IN_GAA(T84, T87, X222)
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_GGA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GGA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_GGA(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U18_GGA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN21_IN_GA(T30, X73) → ACKERMAN27_IN_GA(T30, X73)
ACKERMAN27_IN_GA(s(T34), X97) → ACKERMAN21_IN_GA(T34, X96)
ACKERMAN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackerman21_in_ga(T34, T36))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → ACKERMAN38_IN_GAA(T34, T36, X97)
ACKERMAN38_IN_GAA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → ACKERMAN38_IN_GAA(s(T54), T55, X150)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN21_IN_GA(T30, X73) → ACKERMAN27_IN_GA(T30, X73)
ACKERMAN27_IN_GA(s(T34), X97) → ACKERMAN21_IN_GA(T34, X96)
ACKERMAN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackerman21_in_ga(T34, T36))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → ACKERMAN38_IN_GAA(T34, T36, X97)
ACKERMAN38_IN_GAA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → ACKERMAN38_IN_GAA(s(T54), T55, X150)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
ACKERMAN21_IN_GA(T30) → ACKERMAN27_IN_GA(T30)
ACKERMAN27_IN_GA(s(T34)) → ACKERMAN21_IN_GA(T34)
ACKERMAN27_IN_GA(s(T34)) → U3_GA(T34, ackerman21_in_ga(T34))
U3_GA(T34, ackerman21_out_ga(T34)) → ACKERMAN38_IN_GAA(T34)
ACKERMAN38_IN_GAA(s(T49)) → ACKERMAN27_IN_GA(T49)
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ACKERMAN38_IN_GAA(s(T54)) → U7_GAA(T54, ackerman38_in_gaa(s(T54)))
U7_GAA(T54, ackerman38_out_gaa(s(T54))) → ACKERMAN38_IN_GAA(T54)
ackerman21_in_ga(T30) → U1_ga(T30, ackerman27_in_ga(T30))
ackerman38_in_gaa(s(T49)) → U5_gaa(T49, ackerman27_in_ga(T49))
ackerman38_in_gaa(s(T54)) → U6_gaa(T54, ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(s(T54)) → U7_gaa(T54, ackerman38_in_gaa(s(T54)))
U1_ga(T30, ackerman27_out_ga(T30)) → ackerman21_out_ga(T30)
U5_gaa(T49, ackerman27_out_ga(T49)) → ackerman38_out_gaa(s(T49))
U6_gaa(T54, ackerman38_out_gaa(s(T54))) → ackerman38_out_gaa(s(T54))
U7_gaa(T54, ackerman38_out_gaa(s(T54))) → U8_gaa(T54, ackerman38_in_gaa(T54))
ackerman27_in_ga(0) → ackerman27_out_ga(0)
ackerman27_in_ga(s(T34)) → U2_ga(T34, ackerman21_in_ga(T34))
ackerman27_in_ga(s(T34)) → U3_ga(T34, ackerman21_in_ga(T34))
U8_gaa(T54, ackerman38_out_gaa(T54)) → ackerman38_out_gaa(s(T54))
U2_ga(T34, ackerman21_out_ga(T34)) → ackerman27_out_ga(s(T34))
U3_ga(T34, ackerman21_out_ga(T34)) → U4_ga(T34, ackerman38_in_gaa(T34))
ackerman38_in_gaa(0) → ackerman38_out_gaa(0)
U4_ga(T34, ackerman38_out_gaa(T34)) → ackerman27_out_ga(s(T34))
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackerman27_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.
ACKERMAN27_IN_GA(s(T34)) → ACKERMAN21_IN_GA(T34)
U3_GA(T34, ackerman21_out_ga(T34)) → ACKERMAN38_IN_GAA(T34)
ACKERMAN38_IN_GAA(s(T49)) → ACKERMAN27_IN_GA(T49)
U7_GAA(T54, ackerman38_out_gaa(s(T54))) → ACKERMAN38_IN_GAA(T54)
POL(0) = 1
POL(ACKERMAN21_IN_GA(x1)) = x1
POL(ACKERMAN27_IN_GA(x1)) = x1
POL(ACKERMAN38_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(ackerman21_in_ga(x1)) = 0
POL(ackerman21_out_ga(x1)) = 0
POL(ackerman27_in_ga(x1)) = 1 + x1
POL(ackerman27_out_ga(x1)) = 1
POL(ackerman38_in_gaa(x1)) = 1 + x1
POL(ackerman38_out_gaa(x1)) = 1
POL(s(x1)) = 1 + x1
ACKERMAN21_IN_GA(T30) → ACKERMAN27_IN_GA(T30)
ACKERMAN27_IN_GA(s(T34)) → U3_GA(T34, ackerman21_in_ga(T34))
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ACKERMAN38_IN_GAA(s(T54)) → U7_GAA(T54, ackerman38_in_gaa(s(T54)))
ackerman21_in_ga(T30) → U1_ga(T30, ackerman27_in_ga(T30))
ackerman38_in_gaa(s(T49)) → U5_gaa(T49, ackerman27_in_ga(T49))
ackerman38_in_gaa(s(T54)) → U6_gaa(T54, ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(s(T54)) → U7_gaa(T54, ackerman38_in_gaa(s(T54)))
U1_ga(T30, ackerman27_out_ga(T30)) → ackerman21_out_ga(T30)
U5_gaa(T49, ackerman27_out_ga(T49)) → ackerman38_out_gaa(s(T49))
U6_gaa(T54, ackerman38_out_gaa(s(T54))) → ackerman38_out_gaa(s(T54))
U7_gaa(T54, ackerman38_out_gaa(s(T54))) → U8_gaa(T54, ackerman38_in_gaa(T54))
ackerman27_in_ga(0) → ackerman27_out_ga(0)
ackerman27_in_ga(s(T34)) → U2_ga(T34, ackerman21_in_ga(T34))
ackerman27_in_ga(s(T34)) → U3_ga(T34, ackerman21_in_ga(T34))
U8_gaa(T54, ackerman38_out_gaa(T54)) → ackerman38_out_gaa(s(T54))
U2_ga(T34, ackerman21_out_ga(T34)) → ackerman27_out_ga(s(T34))
U3_ga(T34, ackerman21_out_ga(T34)) → U4_ga(T34, ackerman38_in_gaa(T34))
ackerman38_in_gaa(0) → ackerman38_out_gaa(0)
U4_ga(T34, ackerman38_out_gaa(T34)) → ackerman27_out_ga(s(T34))
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackerman27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ackerman21_in_ga(T30) → U1_ga(T30, ackerman27_in_ga(T30))
ackerman38_in_gaa(s(T49)) → U5_gaa(T49, ackerman27_in_ga(T49))
ackerman38_in_gaa(s(T54)) → U6_gaa(T54, ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(s(T54)) → U7_gaa(T54, ackerman38_in_gaa(s(T54)))
U1_ga(T30, ackerman27_out_ga(T30)) → ackerman21_out_ga(T30)
U5_gaa(T49, ackerman27_out_ga(T49)) → ackerman38_out_gaa(s(T49))
U6_gaa(T54, ackerman38_out_gaa(s(T54))) → ackerman38_out_gaa(s(T54))
U7_gaa(T54, ackerman38_out_gaa(s(T54))) → U8_gaa(T54, ackerman38_in_gaa(T54))
ackerman27_in_ga(0) → ackerman27_out_ga(0)
ackerman27_in_ga(s(T34)) → U2_ga(T34, ackerman21_in_ga(T34))
ackerman27_in_ga(s(T34)) → U3_ga(T34, ackerman21_in_ga(T34))
U8_gaa(T54, ackerman38_out_gaa(T54)) → ackerman38_out_gaa(s(T54))
U2_ga(T34, ackerman21_out_ga(T34)) → ackerman27_out_ga(s(T34))
U3_ga(T34, ackerman21_out_ga(T34)) → U4_ga(T34, ackerman38_in_gaa(T34))
ackerman38_in_gaa(0) → ackerman38_out_gaa(0)
U4_ga(T34, ackerman38_out_gaa(T34)) → ackerman27_out_ga(s(T34))
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackerman27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackerman27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0, x1)
U5_gaa(x0, x1)
U6_gaa(x0, x1)
U7_gaa(x0, x1)
ackerman27_in_ga(x0)
U8_gaa(x0, x1)
U2_ga(x0, x1)
U3_ga(x0, x1)
U4_ga(x0, x1)
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → ACKERMAN38_IN_GGA(s(T54), T55, X150)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → ACKERMAN38_IN_GGA(s(T54), T55, X150)
ACKERMAN38_IN_GGA(s(T54), s(T55)) → ACKERMAN38_IN_GGA(s(T54), T55)
From the DPs we obtained the following set of size-change graphs:
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
ACKERMAN1_IN_GAA(s(s(T20))) → U10_GAA(T20, ackerman21_in_ga(T20))
U10_GAA(T20, ackerman21_out_ga(T20)) → ACKERMAN1_IN_GAA(T20)
ACKERMAN1_IN_GAA(s(T76)) → U13_GAA(T76, ackerman27_in_ga(T76))
U13_GAA(T76, ackerman27_out_ga(T76)) → ACKERMAN1_IN_GAA(T76)
ACKERMAN1_IN_GAA(s(T84)) → U16_GAA(T84, ackerman38_in_gaa(s(T84)))
U16_GAA(T84, ackerman38_out_gaa(s(T84))) → U18_GAA(T84, ackerman38_in_gaa(T84))
U18_GAA(T84, ackerman38_out_gaa(T84)) → ACKERMAN1_IN_GAA(T84)
ackerman21_in_ga(T30) → U1_ga(T30, ackerman27_in_ga(T30))
ackerman27_in_ga(0) → ackerman27_out_ga(0)
ackerman27_in_ga(s(T34)) → U2_ga(T34, ackerman21_in_ga(T34))
ackerman27_in_ga(s(T34)) → U3_ga(T34, ackerman21_in_ga(T34))
ackerman38_in_gaa(s(T49)) → U5_gaa(T49, ackerman27_in_ga(T49))
ackerman38_in_gaa(s(T54)) → U6_gaa(T54, ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(s(T54)) → U7_gaa(T54, ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(0) → ackerman38_out_gaa(0)
U1_ga(T30, ackerman27_out_ga(T30)) → ackerman21_out_ga(T30)
U2_ga(T34, ackerman21_out_ga(T34)) → ackerman27_out_ga(s(T34))
U3_ga(T34, ackerman21_out_ga(T34)) → U4_ga(T34, ackerman38_in_gaa(T34))
U5_gaa(T49, ackerman27_out_ga(T49)) → ackerman38_out_gaa(s(T49))
U6_gaa(T54, ackerman38_out_gaa(s(T54))) → ackerman38_out_gaa(s(T54))
U7_gaa(T54, ackerman38_out_gaa(s(T54))) → U8_gaa(T54, ackerman38_in_gaa(T54))
U4_ga(T34, ackerman38_out_gaa(T34)) → ackerman27_out_ga(s(T34))
U8_gaa(T54, ackerman38_out_gaa(T54)) → ackerman38_out_gaa(s(T54))
ackerman21_in_ga(x0)
ackerman27_in_ga(x0)
ackerman38_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:
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → U9_GGA(T20, T22, ackerman21_in_ga(T20, X40))
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → ACKERMAN21_IN_GA(T20, X40)
ACKERMAN21_IN_GA(T30, X73) → U1_GA(T30, X73, ackerman27_in_ga(T30, X73))
ACKERMAN21_IN_GA(T30, X73) → ACKERMAN27_IN_GA(T30, X73)
ACKERMAN27_IN_GA(s(T34), X97) → U2_GA(T34, X97, ackerman21_in_ga(T34, X96))
ACKERMAN27_IN_GA(s(T34), X97) → ACKERMAN21_IN_GA(T34, X96)
ACKERMAN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackerman21_in_ga(T34, T36))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → U4_GA(T34, X97, ackerman38_in_gaa(T34, T36, X97))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → ACKERMAN38_IN_GAA(T34, T36, X97)
ACKERMAN38_IN_GAA(s(T49), 0, X133) → U5_GAA(T49, X133, ackerman27_in_ga(T49, X133))
ACKERMAN38_IN_GAA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U6_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → ACKERMAN38_IN_GAA(s(T54), T55, X150)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_GAA(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → U10_GGA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GGA(T20, T22, ackerman21_out_ga(T20, T24)) → U11_GGA(T20, T22, ackerman1_in_gaa(T20, T24, T22))
U10_GGA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U9_GAA(T20, T22, ackerman21_in_ga(T20, X40))
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → ACKERMAN21_IN_GA(T20, X40)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → U11_GAA(T20, T22, ackerman1_in_gaa(T20, T24, T22))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U12_GAA(T76, T71, ackerman27_in_ga(T76, X200))
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → ACKERMAN27_IN_GA(T76, X200)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → U14_GAA(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U15_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → ACKERMAN38_IN_GAA(s(T84), T85, X221)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → ACKERMAN38_IN_GAA(T84, T87, X222)
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_GAA(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → U12_GGA(T76, T71, ackerman27_in_ga(T76, X200))
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → ACKERMAN27_IN_GA(T76, X200)
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → U13_GGA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GGA(T76, T71, ackerman27_out_ga(T76, T77)) → U14_GGA(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U13_GGA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → U15_GGA(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → ACKERMAN38_IN_GGA(s(T84), T85, X221)
ACKERMAN38_IN_GGA(s(T49), 0, X133) → U5_GGA(T49, X133, ackerman27_in_ga(T49, X133))
ACKERMAN38_IN_GGA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → U6_GGA(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → ACKERMAN38_IN_GGA(s(T54), T55, X150)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → U7_GGA(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_GGA(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_GGA(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U7_GGA(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → U16_GGA(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_GGA(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → ACKERMAN38_IN_GAA(T84, T87, X222)
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_GGA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GGA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_GGA(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U18_GGA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → U9_GGA(T20, T22, ackerman21_in_ga(T20, X40))
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → ACKERMAN21_IN_GA(T20, X40)
ACKERMAN21_IN_GA(T30, X73) → U1_GA(T30, X73, ackerman27_in_ga(T30, X73))
ACKERMAN21_IN_GA(T30, X73) → ACKERMAN27_IN_GA(T30, X73)
ACKERMAN27_IN_GA(s(T34), X97) → U2_GA(T34, X97, ackerman21_in_ga(T34, X96))
ACKERMAN27_IN_GA(s(T34), X97) → ACKERMAN21_IN_GA(T34, X96)
ACKERMAN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackerman21_in_ga(T34, T36))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → U4_GA(T34, X97, ackerman38_in_gaa(T34, T36, X97))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → ACKERMAN38_IN_GAA(T34, T36, X97)
ACKERMAN38_IN_GAA(s(T49), 0, X133) → U5_GAA(T49, X133, ackerman27_in_ga(T49, X133))
ACKERMAN38_IN_GAA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U6_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → ACKERMAN38_IN_GAA(s(T54), T55, X150)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_GAA(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ACKERMAN1_IN_GGA(s(s(T20)), 0, T22) → U10_GGA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GGA(T20, T22, ackerman21_out_ga(T20, T24)) → U11_GGA(T20, T22, ackerman1_in_gaa(T20, T24, T22))
U10_GGA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U9_GAA(T20, T22, ackerman21_in_ga(T20, X40))
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → ACKERMAN21_IN_GA(T20, X40)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → U11_GAA(T20, T22, ackerman1_in_gaa(T20, T24, T22))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U12_GAA(T76, T71, ackerman27_in_ga(T76, X200))
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → ACKERMAN27_IN_GA(T76, X200)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → U14_GAA(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U15_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → ACKERMAN38_IN_GAA(s(T84), T85, X221)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → ACKERMAN38_IN_GAA(T84, T87, X222)
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_GAA(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → U12_GGA(T76, T71, ackerman27_in_ga(T76, X200))
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → ACKERMAN27_IN_GA(T76, X200)
ACKERMAN1_IN_GGA(s(T76), s(0), T71) → U13_GGA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GGA(T76, T71, ackerman27_out_ga(T76, T77)) → U14_GGA(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U13_GGA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → U15_GGA(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → ACKERMAN38_IN_GGA(s(T84), T85, X221)
ACKERMAN38_IN_GGA(s(T49), 0, X133) → U5_GGA(T49, X133, ackerman27_in_ga(T49, X133))
ACKERMAN38_IN_GGA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → U6_GGA(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → ACKERMAN38_IN_GGA(s(T54), T55, X150)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → U7_GGA(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_GGA(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_GGA(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U7_GGA(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ACKERMAN1_IN_GGA(s(T84), s(s(T85)), T71) → U16_GGA(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_GGA(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → ACKERMAN38_IN_GAA(T84, T87, X222)
U16_GGA(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_GGA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GGA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_GGA(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U18_GGA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN21_IN_GA(T30, X73) → ACKERMAN27_IN_GA(T30, X73)
ACKERMAN27_IN_GA(s(T34), X97) → ACKERMAN21_IN_GA(T34, X96)
ACKERMAN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackerman21_in_ga(T34, T36))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → ACKERMAN38_IN_GAA(T34, T36, X97)
ACKERMAN38_IN_GAA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → ACKERMAN38_IN_GAA(s(T54), T55, X150)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN21_IN_GA(T30, X73) → ACKERMAN27_IN_GA(T30, X73)
ACKERMAN27_IN_GA(s(T34), X97) → ACKERMAN21_IN_GA(T34, X96)
ACKERMAN27_IN_GA(s(T34), X97) → U3_GA(T34, X97, ackerman21_in_ga(T34, T36))
U3_GA(T34, X97, ackerman21_out_ga(T34, T36)) → ACKERMAN38_IN_GAA(T34, T36, X97)
ACKERMAN38_IN_GAA(s(T49), 0, X133) → ACKERMAN27_IN_GA(T49, X133)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → ACKERMAN38_IN_GAA(s(T54), T55, X150)
ACKERMAN38_IN_GAA(s(T54), s(T55), X151) → U7_GAA(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_GAA(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → ACKERMAN38_IN_GAA(T54, T57, X151)
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
ACKERMAN21_IN_GA(T30) → ACKERMAN27_IN_GA(T30)
ACKERMAN27_IN_GA(s(T34)) → ACKERMAN21_IN_GA(T34)
ACKERMAN27_IN_GA(s(T34)) → U3_GA(T34, ackerman21_in_ga(T34))
U3_GA(T34, ackerman21_out_ga) → ACKERMAN38_IN_GAA(T34)
ACKERMAN38_IN_GAA(s(T49)) → ACKERMAN27_IN_GA(T49)
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ACKERMAN38_IN_GAA(s(T54)) → U7_GAA(T54, ackerman38_in_gaa(s(T54)))
U7_GAA(T54, ackerman38_out_gaa) → ACKERMAN38_IN_GAA(T54)
ackerman21_in_ga(T30) → U1_ga(ackerman27_in_ga(T30))
ackerman38_in_gaa(s(T49)) → U5_gaa(ackerman27_in_ga(T49))
ackerman38_in_gaa(s(T54)) → U6_gaa(ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(s(T54)) → U7_gaa(T54, ackerman38_in_gaa(s(T54)))
U1_ga(ackerman27_out_ga) → ackerman21_out_ga
U5_gaa(ackerman27_out_ga) → ackerman38_out_gaa
U6_gaa(ackerman38_out_gaa) → ackerman38_out_gaa
U7_gaa(T54, ackerman38_out_gaa) → U8_gaa(ackerman38_in_gaa(T54))
ackerman27_in_ga(0) → ackerman27_out_ga
ackerman27_in_ga(s(T34)) → U2_ga(ackerman21_in_ga(T34))
ackerman27_in_ga(s(T34)) → U3_ga(T34, ackerman21_in_ga(T34))
U8_gaa(ackerman38_out_gaa) → ackerman38_out_gaa
U2_ga(ackerman21_out_ga) → ackerman27_out_ga
U3_ga(T34, ackerman21_out_ga) → U4_ga(ackerman38_in_gaa(T34))
ackerman38_in_gaa(0) → ackerman38_out_gaa
U4_ga(ackerman38_out_gaa) → ackerman27_out_ga
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackerman27_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.
ACKERMAN27_IN_GA(s(T34)) → ACKERMAN21_IN_GA(T34)
U3_GA(T34, ackerman21_out_ga) → ACKERMAN38_IN_GAA(T34)
ACKERMAN38_IN_GAA(s(T49)) → ACKERMAN27_IN_GA(T49)
U7_GAA(T54, ackerman38_out_gaa) → ACKERMAN38_IN_GAA(T54)
POL(0) = 1
POL(ACKERMAN21_IN_GA(x1)) = x1
POL(ACKERMAN27_IN_GA(x1)) = x1
POL(ACKERMAN38_IN_GAA(x1)) = x1
POL(U1_ga(x1)) = 0
POL(U2_ga(x1)) = 0
POL(U3_GA(x1, x2)) = 1 + x1
POL(U3_ga(x1, x2)) = 0
POL(U4_ga(x1)) = 0
POL(U5_gaa(x1)) = 0
POL(U6_gaa(x1)) = 0
POL(U7_GAA(x1, x2)) = 1 + x1
POL(U7_gaa(x1, x2)) = 0
POL(U8_gaa(x1)) = 0
POL(ackerman21_in_ga(x1)) = 0
POL(ackerman21_out_ga) = 0
POL(ackerman27_in_ga(x1)) = 1 + x1
POL(ackerman27_out_ga) = 1
POL(ackerman38_in_gaa(x1)) = 1 + x1
POL(ackerman38_out_gaa) = 1
POL(s(x1)) = 1 + x1
ACKERMAN21_IN_GA(T30) → ACKERMAN27_IN_GA(T30)
ACKERMAN27_IN_GA(s(T34)) → U3_GA(T34, ackerman21_in_ga(T34))
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ACKERMAN38_IN_GAA(s(T54)) → U7_GAA(T54, ackerman38_in_gaa(s(T54)))
ackerman21_in_ga(T30) → U1_ga(ackerman27_in_ga(T30))
ackerman38_in_gaa(s(T49)) → U5_gaa(ackerman27_in_ga(T49))
ackerman38_in_gaa(s(T54)) → U6_gaa(ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(s(T54)) → U7_gaa(T54, ackerman38_in_gaa(s(T54)))
U1_ga(ackerman27_out_ga) → ackerman21_out_ga
U5_gaa(ackerman27_out_ga) → ackerman38_out_gaa
U6_gaa(ackerman38_out_gaa) → ackerman38_out_gaa
U7_gaa(T54, ackerman38_out_gaa) → U8_gaa(ackerman38_in_gaa(T54))
ackerman27_in_ga(0) → ackerman27_out_ga
ackerman27_in_ga(s(T34)) → U2_ga(ackerman21_in_ga(T34))
ackerman27_in_ga(s(T34)) → U3_ga(T34, ackerman21_in_ga(T34))
U8_gaa(ackerman38_out_gaa) → ackerman38_out_gaa
U2_ga(ackerman21_out_ga) → ackerman27_out_ga
U3_ga(T34, ackerman21_out_ga) → U4_ga(ackerman38_in_gaa(T34))
ackerman38_in_gaa(0) → ackerman38_out_gaa
U4_ga(ackerman38_out_gaa) → ackerman27_out_ga
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackerman27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ackerman21_in_ga(T30) → U1_ga(ackerman27_in_ga(T30))
ackerman38_in_gaa(s(T49)) → U5_gaa(ackerman27_in_ga(T49))
ackerman38_in_gaa(s(T54)) → U6_gaa(ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(s(T54)) → U7_gaa(T54, ackerman38_in_gaa(s(T54)))
U1_ga(ackerman27_out_ga) → ackerman21_out_ga
U5_gaa(ackerman27_out_ga) → ackerman38_out_gaa
U6_gaa(ackerman38_out_gaa) → ackerman38_out_gaa
U7_gaa(T54, ackerman38_out_gaa) → U8_gaa(ackerman38_in_gaa(T54))
ackerman27_in_ga(0) → ackerman27_out_ga
ackerman27_in_ga(s(T34)) → U2_ga(ackerman21_in_ga(T34))
ackerman27_in_ga(s(T34)) → U3_ga(T34, ackerman21_in_ga(T34))
U8_gaa(ackerman38_out_gaa) → ackerman38_out_gaa
U2_ga(ackerman21_out_ga) → ackerman27_out_ga
U3_ga(T34, ackerman21_out_ga) → U4_ga(ackerman38_in_gaa(T34))
ackerman38_in_gaa(0) → ackerman38_out_gaa
U4_ga(ackerman38_out_gaa) → ackerman27_out_ga
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackerman27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackerman27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
ackerman21_in_ga(x0)
ackerman38_in_gaa(x0)
U1_ga(x0)
U5_gaa(x0)
U6_gaa(x0)
U7_gaa(x0, x1)
ackerman27_in_ga(x0)
U8_gaa(x0)
U2_ga(x0)
U3_ga(x0, x1)
U4_ga(x0)
ACKERMAN38_IN_GAA(s(T54)) → ACKERMAN38_IN_GAA(s(T54))
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → ACKERMAN38_IN_GGA(s(T54), T55, X150)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN38_IN_GGA(s(T54), s(T55), X151) → ACKERMAN38_IN_GGA(s(T54), T55, X150)
ACKERMAN38_IN_GGA(s(T54), s(T55)) → ACKERMAN38_IN_GGA(s(T54), T55)
From the DPs we obtained the following set of size-change graphs:
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ackerman1_in_gga(0, T5, s(T5)) → ackerman1_out_gga(0, T5, s(T5))
ackerman1_in_gga(s(0), 0, s(s(0))) → ackerman1_out_gga(s(0), 0, s(s(0)))
ackerman1_in_gga(s(s(T20)), 0, T22) → U9_gga(T20, T22, ackerman21_in_ga(T20, X40))
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U9_gga(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(s(T20)), 0, T22) → U10_gga(T20, T22, ackerman21_in_ga(T20, T24))
U10_gga(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gga(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(0, T5, s(T5)) → ackerman1_out_gaa(0, T5, s(T5))
ackerman1_in_gaa(s(0), 0, s(s(0))) → ackerman1_out_gaa(s(0), 0, s(s(0)))
ackerman1_in_gaa(s(s(T20)), 0, T22) → U9_gaa(T20, T22, ackerman21_in_ga(T20, X40))
U9_gaa(T20, T22, ackerman21_out_ga(T20, X40)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
ackerman1_in_gaa(s(s(T20)), 0, T22) → U10_gaa(T20, T22, ackerman21_in_ga(T20, T24))
U10_gaa(T20, T22, ackerman21_out_ga(T20, T24)) → U11_gaa(T20, T22, ackerman1_in_gaa(T20, T24, T22))
ackerman1_in_gaa(s(T76), s(0), T71) → U12_gaa(T76, T71, ackerman27_in_ga(T76, X200))
U12_gaa(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gaa(s(T76), s(0), T71)
ackerman1_in_gaa(s(T76), s(0), T71) → U13_gaa(T76, T71, ackerman27_in_ga(T76, T77))
U13_gaa(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gaa(T76, T71, ackerman1_in_gaa(T76, T77, T71))
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U15_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, X221))
U15_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, X221)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
ackerman1_in_gaa(s(T84), s(s(T85)), T71) → U16_gaa(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U17_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U16_gaa(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_gaa(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gaa(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gaa(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gaa(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gaa(s(T84), s(s(T85)), T71)
U14_gaa(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gaa(s(T76), s(0), T71)
U11_gaa(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gaa(s(s(T20)), 0, T22)
U11_gga(T20, T22, ackerman1_out_gaa(T20, T24, T22)) → ackerman1_out_gga(s(s(T20)), 0, T22)
ackerman1_in_gga(s(T76), s(0), T71) → U12_gga(T76, T71, ackerman27_in_ga(T76, X200))
U12_gga(T76, T71, ackerman27_out_ga(T76, X200)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T76), s(0), T71) → U13_gga(T76, T71, ackerman27_in_ga(T76, T77))
U13_gga(T76, T71, ackerman27_out_ga(T76, T77)) → U14_gga(T76, T71, ackerman1_in_gaa(T76, T77, T71))
U14_gga(T76, T71, ackerman1_out_gaa(T76, T77, T71)) → ackerman1_out_gga(s(T76), s(0), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U15_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, X221))
ackerman38_in_gga(0, T44, s(T44)) → ackerman38_out_gga(0, T44, s(T44))
ackerman38_in_gga(s(T49), 0, X133) → U5_gga(T49, X133, ackerman27_in_ga(T49, X133))
U5_gga(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gga(s(T49), 0, X133)
ackerman38_in_gga(s(T54), s(T55), X151) → U6_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, X150))
ackerman38_in_gga(s(T54), s(T55), X151) → U7_gga(T54, T55, X151, ackerman38_in_gga(s(T54), T55, T57))
U7_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, T57)) → U8_gga(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U8_gga(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gga(s(T54), s(T55), X151)
U6_gga(T54, T55, X151, ackerman38_out_gga(s(T54), T55, X150)) → ackerman38_out_gga(s(T54), s(T55), X151)
U15_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, X221)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ackerman1_in_gga(s(T84), s(s(T85)), T71) → U16_gga(T84, T85, T71, ackerman38_in_gga(s(T84), T85, T87))
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U17_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, X222))
U17_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, X222)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
U16_gga(T84, T85, T71, ackerman38_out_gga(s(T84), T85, T87)) → U18_gga(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_gga(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → U19_gga(T84, T85, T71, ackerman1_in_gaa(T84, T91, T71))
U19_gga(T84, T85, T71, ackerman1_out_gaa(T84, T91, T71)) → ackerman1_out_gga(s(T84), s(s(T85)), T71)
ACKERMAN1_IN_GAA(s(s(T20)), 0, T22) → U10_GAA(T20, T22, ackerman21_in_ga(T20, T24))
U10_GAA(T20, T22, ackerman21_out_ga(T20, T24)) → ACKERMAN1_IN_GAA(T20, T24, T22)
ACKERMAN1_IN_GAA(s(T76), s(0), T71) → U13_GAA(T76, T71, ackerman27_in_ga(T76, T77))
U13_GAA(T76, T71, ackerman27_out_ga(T76, T77)) → ACKERMAN1_IN_GAA(T76, T77, T71)
ACKERMAN1_IN_GAA(s(T84), s(s(T85)), T71) → U16_GAA(T84, T85, T71, ackerman38_in_gaa(s(T84), T85, T87))
U16_GAA(T84, T85, T71, ackerman38_out_gaa(s(T84), T85, T87)) → U18_GAA(T84, T85, T71, ackerman38_in_gaa(T84, T87, T91))
U18_GAA(T84, T85, T71, ackerman38_out_gaa(T84, T87, T91)) → ACKERMAN1_IN_GAA(T84, T91, T71)
ackerman21_in_ga(T30, X73) → U1_ga(T30, X73, ackerman27_in_ga(T30, X73))
ackerman27_in_ga(0, s(s(0))) → ackerman27_out_ga(0, s(s(0)))
ackerman27_in_ga(s(T34), X97) → U2_ga(T34, X97, ackerman21_in_ga(T34, X96))
ackerman27_in_ga(s(T34), X97) → U3_ga(T34, X97, ackerman21_in_ga(T34, T36))
ackerman38_in_gaa(s(T49), 0, X133) → U5_gaa(T49, X133, ackerman27_in_ga(T49, X133))
ackerman38_in_gaa(s(T54), s(T55), X151) → U6_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, X150))
ackerman38_in_gaa(s(T54), s(T55), X151) → U7_gaa(T54, T55, X151, ackerman38_in_gaa(s(T54), T55, T57))
ackerman38_in_gaa(0, T44, s(T44)) → ackerman38_out_gaa(0, T44, s(T44))
U1_ga(T30, X73, ackerman27_out_ga(T30, X73)) → ackerman21_out_ga(T30, X73)
U2_ga(T34, X97, ackerman21_out_ga(T34, X96)) → ackerman27_out_ga(s(T34), X97)
U3_ga(T34, X97, ackerman21_out_ga(T34, T36)) → U4_ga(T34, X97, ackerman38_in_gaa(T34, T36, X97))
U5_gaa(T49, X133, ackerman27_out_ga(T49, X133)) → ackerman38_out_gaa(s(T49), 0, X133)
U6_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, X150)) → ackerman38_out_gaa(s(T54), s(T55), X151)
U7_gaa(T54, T55, X151, ackerman38_out_gaa(s(T54), T55, T57)) → U8_gaa(T54, T55, X151, ackerman38_in_gaa(T54, T57, X151))
U4_ga(T34, X97, ackerman38_out_gaa(T34, T36, X97)) → ackerman27_out_ga(s(T34), X97)
U8_gaa(T54, T55, X151, ackerman38_out_gaa(T54, T57, X151)) → ackerman38_out_gaa(s(T54), s(T55), X151)
ACKERMAN1_IN_GAA(s(s(T20))) → U10_GAA(T20, ackerman21_in_ga(T20))
U10_GAA(T20, ackerman21_out_ga) → ACKERMAN1_IN_GAA(T20)
ACKERMAN1_IN_GAA(s(T76)) → U13_GAA(T76, ackerman27_in_ga(T76))
U13_GAA(T76, ackerman27_out_ga) → ACKERMAN1_IN_GAA(T76)
ACKERMAN1_IN_GAA(s(T84)) → U16_GAA(T84, ackerman38_in_gaa(s(T84)))
U16_GAA(T84, ackerman38_out_gaa) → U18_GAA(T84, ackerman38_in_gaa(T84))
U18_GAA(T84, ackerman38_out_gaa) → ACKERMAN1_IN_GAA(T84)
ackerman21_in_ga(T30) → U1_ga(ackerman27_in_ga(T30))
ackerman27_in_ga(0) → ackerman27_out_ga
ackerman27_in_ga(s(T34)) → U2_ga(ackerman21_in_ga(T34))
ackerman27_in_ga(s(T34)) → U3_ga(T34, ackerman21_in_ga(T34))
ackerman38_in_gaa(s(T49)) → U5_gaa(ackerman27_in_ga(T49))
ackerman38_in_gaa(s(T54)) → U6_gaa(ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(s(T54)) → U7_gaa(T54, ackerman38_in_gaa(s(T54)))
ackerman38_in_gaa(0) → ackerman38_out_gaa
U1_ga(ackerman27_out_ga) → ackerman21_out_ga
U2_ga(ackerman21_out_ga) → ackerman27_out_ga
U3_ga(T34, ackerman21_out_ga) → U4_ga(ackerman38_in_gaa(T34))
U5_gaa(ackerman27_out_ga) → ackerman38_out_gaa
U6_gaa(ackerman38_out_gaa) → ackerman38_out_gaa
U7_gaa(T54, ackerman38_out_gaa) → U8_gaa(ackerman38_in_gaa(T54))
U4_ga(ackerman38_out_gaa) → ackerman27_out_ga
U8_gaa(ackerman38_out_gaa) → ackerman38_out_gaa
ackerman21_in_ga(x0)
ackerman27_in_ga(x0)
ackerman38_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: