(VAR x)
(RULES
   f(g(f(x))) -> g(f(g(x)))
   f(c) -> c
   g(c) -> c
)
(COMMENT Exmple 2.2 of Kapur/Narendran/Otto, IC 1990)