(VAR x)
(RULES
   g(x) -> h(k(x))
   g(x) -> x
h(k(x)) -> f(x)
   f(x) -> x
   k(c) -> c
   f(c) -> g(c)
)
(COMMENT Example 3 of Ishizuki/Oyamaguchi/Sakai, IWC 2016)