YES

Problem:
 f(a(),a()) -> f(a(),b())
 f(a(),b()) -> f(s(a()),c())
 f(s(X),c()) -> f(X,c())
 f(c(),c()) -> f(a(),a())

Proof:
 DP Processor:
  DPs:
   f#(a(),a()) -> f#(a(),b())
   f#(a(),b()) -> f#(s(a()),c())
   f#(s(X),c()) -> f#(X,c())
   f#(c(),c()) -> f#(a(),a())
  TRS:
   f(a(),a()) -> f(a(),b())
   f(a(),b()) -> f(s(a()),c())
   f(s(X),c()) -> f(X,c())
   f(c(),c()) -> f(a(),a())
  EDG Processor:
   DPs:
    f#(a(),a()) -> f#(a(),b())
    f#(a(),b()) -> f#(s(a()),c())
    f#(s(X),c()) -> f#(X,c())
    f#(c(),c()) -> f#(a(),a())
   TRS:
    f(a(),a()) -> f(a(),b())
    f(a(),b()) -> f(s(a()),c())
    f(s(X),c()) -> f(X,c())
    f(c(),c()) -> f(a(),a())
   graph:
    f#(c(),c()) -> f#(a(),a()) -> f#(a(),a()) -> f#(a(),b())
    f#(s(X),c()) -> f#(X,c()) -> f#(s(X),c()) -> f#(X,c())
    f#(s(X),c()) -> f#(X,c()) -> f#(c(),c()) -> f#(a(),a())
    f#(a(),b()) -> f#(s(a()),c()) -> f#(s(X),c()) -> f#(X,c())
    f#(a(),a()) -> f#(a(),b()) -> f#(a(),b()) -> f#(s(a()),c())
   KBO Processor:
    argument filtering:
     pi(a) = []
     pi(f) = []
     pi(b) = []
     pi(s) = 0
     pi(c) = []
     pi(f#) = [0]
    weight function:
     w0 = 1
     w(f#) = w(c) = w(s) = w(b) = w(f) = w(a) = 1
    precedence:
     f# ~ c ~ f > s ~ b ~ a
    problem:
     DPs:
      f#(a(),a()) -> f#(a(),b())
      f#(a(),b()) -> f#(s(a()),c())
      f#(s(X),c()) -> f#(X,c())
     TRS:
      f(a(),a()) -> f(a(),b())
      f(a(),b()) -> f(s(a()),c())
      f(s(X),c()) -> f(X,c())
      f(c(),c()) -> f(a(),a())
    SCC Processor:
     #sccs: 1
     #rules: 1
     #arcs: 5/9
     DPs:
      f#(s(X),c()) -> f#(X,c())
     TRS:
      f(a(),a()) -> f(a(),b())
      f(a(),b()) -> f(s(a()),c())
      f(s(X),c()) -> f(X,c())
      f(c(),c()) -> f(a(),a())
     Subterm Criterion Processor:
      simple projection:
       pi(f#) = 0
      problem:
       DPs:
        
       TRS:
        f(a(),a()) -> f(a(),b())
        f(a(),b()) -> f(s(a()),c())
        f(s(X),c()) -> f(X,c())
        f(c(),c()) -> f(a(),a())
      Qed