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