(VAR x)
(RULES
  a -> b
  f(b, b) -> f(a, a)
  f(x, a) -> f(a, a)
)
(COMMENT p.29 of \cite{IWC16}
  GNFP & ~NFP & ~GCR
)