(VAR x y z)
(THEORY (AC p) (AC g))
(RULES
p(x,zero) -> x
p(i(x),x) -> zero
m(one,x) -> x
m(x,one) -> x
m(x,m(y,z)) -> m(m(x,y),z)
m(z,p(x,y)) -> p(m(z,x),m(z,y))
m(p(x,y),z) -> p(m(x,z),m(y,z))
g(x,n) -> x
g(x,inv(x)) -> n
sm(x,sm(y,z)) -> sm(m(x,y),z)
sm(one,z) -> z
g(sm(x,z),sm(y,z)) -> sm(p(x,y),z)
sm(x,g(y,z)) -> g(sm(x,y),sm(x,z))
smm(x,smm(y,z)) -> smm(m(x,y),z)
smm(one,z) -> z
g(smm(x,z),smm(y,z)) -> smm(p(x,y),z)
smm(x,g(y,z)) -> g(smm(x,y),smm(x,z))
)