(VAR x) (RULES a -> h(c) a -> f(c) f(x) -> h(g(x)) h(x) -> f(k(x)) ) (COMMENT from the collection of \cite{Aoto2013})