(VAR m n )
(STRATEGY INNERMOST)
(RULES 
        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)
        
)