(VAR x y z) (THEORY (AC p)) (RULES p(x,zero) -> x f(zero) -> zero p(f(x),f(y)) -> f(p(x,y)) g(zero) -> zero p(g(x),g(y)) -> g(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)) )