Problem:
 c() -> f(h(b(),b()))
 c() -> b()
 b() -> b()
 c() -> a()

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