(VAR x y z)
(THEORY (AC a) (AC m))
(RULES
m(x,one) -> x
m(x,a(y,z)) -> a(m(x,y),m(x,z))
p(one,x) -> one
p(x,one) -> x
p(x,a(y,z)) -> m(p(x,y),p(x,z))
p(m(x,y),z) -> m(p(x,z),p(y,z))
p(p(x,y),z) -> p(x,m(y,z))
)