(VAR x y z)
(THEORY (AC p))
(RULES
p(x,zero) -> x
p(i(x),x) -> zero
m(z,p(x,y)) -> p(m(z,x),m(z,y))
m(p(x,y),z) -> p(m(x,z),m(y,z))
b(x,x) -> zero
p(b(b(x,y),z),p(b(b(y,z),x),b(b(z,x),y))) -> zero
b(p(x,y),z) -> p(b(x,z),b(y,z))
b(x,p(y,z)) -> p(b(x,y),b(x,z))
)