(VAR x y z)
(THEORY (AC +) (AC *))
(RULES
s(p(x)) -> x
p(s(x)) -> x
-(x,zero) -> x
-(x,s(y)) -> p(-(x,y))
-(x,p(y)) -> s(-(x,y))
+(x,zero) -> x
+(x,s(y)) -> s(+(x,y))
+(x,p(y)) -> p(+(x,y))
-(-(x,y),z) -> -(x,+(y,z))
+(-(x,y),z) -> -(+(x,z),y)
*(x,zero) -> zero
*(x,s(y)) -> +(*(x,y),x)
*(x,p(y)) -> -(*(x,y),x)
*(+(x,y),z) -> +(*(x,z),*(y,z))
*(-(x,y),z) -> -(*(x,z),*(y,z))
)