(VAR x)
(RULES
  c0 -> c1
  f0(x, c0) -> c1
  f0(c1, c1) -> c1
)
(COMMENT from p.27 of \cite{IWC16})