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