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:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 11
   a() <-0|[]- b() -1|[]-> c()
   c() <-1|[]- b() -0|[]-> a()
   f(c(),x) <-2|0[]- f(c(),x) -8|[]-> A()
   c() <-3|[]- d() -4|[]-> e()
   e() <-4|[]- d() -3|[]-> c()
   A() <-5|[]- f(c(),a()) -8|[]-> A()
   A() <-6|[]- f(c(),e()) -8|[]-> A()
   A() <-7|[]- f(c(),A()) -8|[]-> A()
   A() <-8|[]- f(c(),a()) -5|[]-> A()
   A() <-8|[]- f(c(),e()) -6|[]-> A()
   A() <-8|[]- f(c(),A()) -7|[]-> A()
  Redundant Rules Transformation:
   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()
   f(b(),a()) -> A()
   f(x59,b()) -> A()
   f(c(),a()) -> A()
   f(d(),a()) -> A()
   f(f(x,a()),a()) -> A()
   f(f(x,e()),a()) -> A()
   f(f(x,A()),a()) -> A()
   f(f(c(),x),a()) -> A()
   f(b(),e()) -> A()
   f(c(),e()) -> A()
   f(d(),e()) -> A()
   f(x60,d()) -> A()
   f(f(x,a()),e()) -> A()
   f(f(x,e()),e()) -> A()
   f(f(x,A()),e()) -> A()
   f(f(c(),x),e()) -> A()
   f(b(),A()) -> A()
   f(c(),A()) -> A()
   f(d(),A()) -> A()
   f(f(x,a()),A()) -> A()
   f(x61,f(x,a())) -> A()
   f(f(x,e()),A()) -> A()
   f(x61,f(x,e())) -> A()
   f(f(x,A()),A()) -> A()
   f(x61,f(x,A())) -> A()
   f(f(c(),x),A()) -> A()
   f(x61,f(c(),x)) -> A()
   f(c(),b()) -> A()
   f(b(),x62) -> A()
   f(c(),x62) -> A()
   f(c(),c()) -> A()
   f(d(),x62) -> A()
   f(c(),d()) -> A()
   f(c(),f(x,a())) -> A()
   f(c(),f(x,e())) -> A()
   f(c(),f(x,A())) -> A()
   f(c(),f(c(),x)) -> A()
   Nonconfluence Processor:
    terms: f(a(),x62) *<- f(b(),x62) ->* A()
    Qed