(COMMENT HOSC'08/Ex.5 from AAECC'01/p.46: R with U(R) non-terminating as TRS, terminating as CS-TRS) (VAR x) (RULES a -> b f(a) -> b g(x) -> g(a) | f(x) -> x )