YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    O: Unit
    ack: (Unit, Unit) -> Unit
    s: Unit -> Unit
  Rules
    ack(O, ?8) -> s(?8)
    ack(s(?9), O) -> ack(?9, s(O))
    ack(s(?10), s(?11)) -> ack(?10, ack(s(?10), ?11))
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  37.61 ms