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