Problem:
 a() -> a()
 a() -> b()
 a() -> f(a(),a())
 f(b(),b()) -> f(a(),b())
 f(x0,a()) -> f(b(),b())

Proof:
 Nonconfluence Processor:
  terms: f(f3(),b()) *<- f(f3(),a()) ->* f(b(),b())
  Qed
  
  first automaton:
   final states: {14}
   transitions:
    f3() -> 16*
    b() -> 15*
    f(16,15) -> 14*
  
  second automaton:
   final states: {6}
   transitions:
    a() -> 8*
    b() -> 8,7
    f(8,7) -> 6*
    f(8,8) -> 8*