MAYBE

Problem:
 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)

Proof:
 Open