(VAR x y z)
(THEORY (AC plus))
(RULES
s(p(x)) -> x
p(s(x)) -> x
minus(x,0) -> x
minus(x,s(y)) -> p(minus(x,y))
minus(x,p(y)) -> s(minus(x,y))
plus(x,0) -> x
plus(x,s(y)) -> s(plus(x,y))
plus(x,p(y)) -> p(plus(x,y))
)