(VAR x y)
(THEORY (AC p))
(RULES
f(p(x,y)) -> p(f(x),f(y))
f(zero) -> zero
p(x,zero) -> x
)