(VAR x y z)
(RULES
  a -> b
  f(x, a) -> f(b, b)
  f(b, x) -> f(b, b)
  f(f(x, y), z) -> f(b, b)
)
(COMMENT Example 1 on p.28 of \cite{IWC16})