(VAR x y z)
(SIG (f 2) (a 0) (b 0) (c 0))
(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} with additional c)