YES
LCTRS
  Theories
    Core, Ints
  Signature
    ack: (Int, Int) -> Int
  Rules
    ack(?23, ?24) -> ack(-(?23, 1), ack(?23, -(?24, 1))) [and(>(?23, 0), >(?24, 0))]
    ack(?25, ?26) -> ack(-(?25, 1), 1) [?26 = 0, >(?25, 0)]
    ack(?27, ?28) -> +(?28, 1) [?27 = 0, >=(?28, 0)]
    ack(?29, ?30) -> 0 [or(<(?29, 0), <(?30, 0))]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  44.95 ms