(VAR x y z)
(RULES
  c0 -> c1
  f0(x, c0) -> f0(c1, c1)
  f0(c1, x) -> f0(c1, c1)
  f0(f0(x, y), z) -> f0(c1, c1)
)
(COMMENT Example 1 on p.28 of \cite{IWC16})