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

Proof:
 Nonconfluence Processor:
  terms: h(b(),f(h(a(),h(h(b(),a()),a())))) *<- h(b(),f(c())) ->* b()
  Qed
  
  first automaton:
   final states: {1}
   transitions:
    b() -> 10,4
    a() -> 7,3,2
    c() -> 2,7,3
    f(8) -> 9*
    h(2,6) -> 3,2,7
    h(7,6) -> 8*
    h(2,2) -> 2,7,3
    h(10,9) -> 1*
    h(5,2) -> 6*
    h(4,3) -> 5*
  
  second automaton:
   final states: {11}
   transitions:
    b() -> 11*