(VAR X Y ) (STRATEGY INNERMOST) (RULES ackin(s(X),s(Y)) -> u21(ackin(s(X),Y),X) u21(ackout(X),Y) -> u22(ackin(Y,X)) )