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

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