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