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