(VAR x y z)
(THEORY (AC p) (AC m))
(RULES
p(x,zero) -> x
m(x,zero) -> zero
p(s(x),y) -> s(p(x,y))
m(s(x),y) -> p(m(x,y),y)
m(x,p(y,z)) -> p(m(x,y),m(x,z))
exp(x,zero) -> s(zero)
exp(s(zero),x) -> s(zero)
exp(x,s(y)) -> m(x,exp(x,y))
m(exp(x,y),exp(z,y)) -> exp(m(x,z),y)
exp(x,p(y,z)) -> m(exp(x,y),exp(x,z))
)