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