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
   [1>7, 1>9, 2>6, 2>9, 3>4, 3>8, 4>5, 4>6, 4>7, 8>9]
 sort attachment (non-strict)
   b : 1
   a : 7
   c : 9
   d : 2
   e : 6
   f : 8 x 4 -> 3
   A : 5
 -----
 0:b() -> a()
   b() -> c()
   c() -> c()
   Nonconfluence Processor:
    terms: c() *<- b() ->* a()
    Qed
 
 
 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