Problem:
 f(a()) -> b()
 a() -> a'()
 f(b()) -> c()

Proof:
 Nonconfluence Processor:
  terms: f(a'()) *<- f(a()) ->* b()
  Qed
  
  first automaton:
   final states: {1}
   transitions:
    a'() -> 2*
    f(2) -> 1*
  
  second automaton:
   final states: {3}
   transitions:
    b() -> 3*