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

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