(VAR x y)
(RULES
  f(g(x),g(y)) -> f(g(x),h(y))
  f(h(x),g(y)) -> f(g(x),g(y))
  f(g(x),h(y)) -> f(x,y)
  f(h(x),h(y)) -> f(y,x)
  f(x,y) -> f(y,x)
  g(x) -> h(x)
  h(x) -> g(x)
)
(COMMENT R8 of \cite{AT2012})