Problem:
 a(x) -> g(b(x))
 a(x) -> c(x)
 b(x) -> g(b(x))

Proof:
 Nonconfluence Processor:
  terms: g(b(f4())) *<- a(f4()) ->* c(f4())
  Qed
  
  first automaton:
   final states: {3}
   transitions:
    b(4) -> 5*
    f4() -> 4*
    g(5) -> 5,3
  
  second automaton:
   final states: {1}
   transitions:
    c(2) -> 1*
    f4() -> 2*