Problem:
 b() -> a()
 b() -> c()
 c() -> c()
 d() -> c()
 d() -> e()
 f(x,a()) -> A()
 f(x,e()) -> A()
 f(x,A()) -> A()
 f(c(),x) -> A()

Proof:
 sorted: (order)
 0:b() -> a()
   b() -> c()
   c() -> c()
 1:c() -> c()
   d() -> c()
   d() -> e()
 2:c() -> c()
   f(x,a()) -> A()
   f(x,e()) -> A()
   f(x,A()) -> A()
   f(c(),x) -> A()
 -----
 sorts
   [0>6, 0>8, 1>5, 1>8, 2>3, 2>7, 3>4, 3>5, 3>6, 7>8]
 sort attachment (non-strict)
   b : 0
   a : 6
   c : 8
   d : 1
   e : 5
   f : 7 x 3 -> 2
   A : 4
 -----
 0:b() -> a()
   b() -> c()
   c() -> c()
   Nonconfluence Processor:
    terms: c() *<- b() ->* a()
    Qed
    
    first automaton:
     final states: {1}
     transitions:
      c() -> 1*
    
    second automaton:
     final states: {2}
     transitions:
      a() -> 2*
 
 
 1:c() -> c()
   d() -> c()
   d() -> e()
   Open
 
 
 2:c() -> c()
   f(x,a()) -> A()
   f(x,e()) -> A()
   f(x,A()) -> A()
   f(c(),x) -> A()
   Open