(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
doi:10.2168/LMCS-8(1:31)2012
[35] Example 3.37 (R_8)
)