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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 6
   f(c(),b()) <-0|0[]- f(a(),b()) -2|[]-> d()
   f(a(),c()) <-1|1[]- f(a(),b()) -2|[]-> d()
   f(c(),c()) <-3|[]- f(c(),c()) -4|[]-> f(c(),c())
   f(c(),c()) <-4|[]- f(c(),c()) -3|[]-> f(c(),c())
   f(a(),c()) <-5|[]- d() -6|[]-> f(c(),b())
   f(c(),b()) <-6|[]- d() -5|[]-> f(a(),c())
  Redundant Rules Transformation:
   a() -> c()
   b() -> c()
   f(x,c()) -> f(c(),c())
   f(c(),x) -> f(c(),c())
   d() -> f(c(),b())
   Church Rosser Transformation Processor (no redundant rules):
    strict:
     d() -> f(c(),b())
     f(c(),x) -> f(c(),c())
     f(x,c()) -> f(c(),c())
     b() -> c()
     a() -> c()
    weak:
     
    critical peaks: 2
     f(c(),c()) <-1|[]- f(c(),c()) -2|[]-> f(c(),c())
     f(c(),c()) <-2|[]- f(c(),c()) -1|[]-> f(c(),c())
    Closedness Processor (*feeble*):
     
     Qed