Problem:
 c() -> f(c())
 c() -> h(c())
 f(x) -> f(g(x))
 h(x) -> h(g(x))
 g(x) -> g(f(h(x)))

Proof:
 Nonconfluence Processor:
  terms: f(c()) *<- c() ->* h(c())
  Qed