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

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