(VAR x)
(RULES
  a -> b
  f(a, b) -> f(a, a)
  f(b, a) -> f(a, a)
  f(a, a) -> c
  g(x) -> f(x, x)
)
(COMMENT Example 5.11 from \cite{NFZ17})