(VAR x)
(RULES
  f0(c0, f0(c0, x)) -> c1
)
(COMMENT UNC & ~NFP)