(VAR x y z)
(THEORY (AC f))
(RULES
g(f(x,y)) -> f(g(x),g(y))
f(g(a),g(a)) -> f(a,g(g(a)))
)