(VAR x y z) (THEORY (AC p)) (RULES p(x,zero) -> x p(i(x),x) -> zero m(one,x) -> x m(x,one) -> x m(d(x),x) -> one 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)) )