(VAR x y z)
(THEORY (AC p))
(RULES
p(x,zero) -> x
p(f(x),f(y)) -> f(p(x,y))
f(zero) -> zero
p(g(x),g(y)) -> g(p(x,y))
g(zero) -> zero
m(one,x) -> x
m(x,one) -> x
f(one) -> one
g(one) -> one
m(z,p(x,y)) -> p(m(z,x),m(z,y))
m(p(x,y),z) -> p(m(x,z),m(y,z))
m(f(x),f(y)) -> f(m(x,y))
m(g(x),g(y)) -> g(m(x,y))
)