TRS:
 {    ack_in(0(), n) -> ack_out(s(n)),
   ack_in(s(m), 0()) -> u11(ack_in(m, s(0()))),
     u11(ack_out(n)) -> ack_out(n),
  ack_in(s(m), s(n)) -> u21(ack_in(s(m), n), m),
  u21(ack_out(n), m) -> u22(ack_in(m, n)),
     u22(ack_out(n)) -> ack_out(n)}
 Fail