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

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