(VAR x y) (RULES ack(0,y) -> s(y) ack(s(x),0) -> ack(x,s(0)) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) f(s(x),y) -> f(x,s(x)) f(x,s(y)) -> f(y,x) f(x,y) -> ack(x,y) ack(s(x),y) -> f(x,x) )