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