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