YES
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())}
 DP:
  Strict:
   { 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())}
  Weak:
  { 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:
   {(f#(a(), b()) -> f#(s(a()), c()), f#(s(X), c()) -> f#(X, c()))
    (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(), a()) -> f#(a(), b()), f#(a(), b()) -> f#(s(a()), c()))}
   SCCS:
    Scc:
     { 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:
     Strict:
      { 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())}
     Weak:
     { 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())}
     POLY:
      Argument Filtering:
       pi(c) = [], pi(s) = 0, pi(b) = [], pi(a) = [], pi(f#) = 0, pi(f) = []
      Usable Rules:
       {}
      Interpretation:
       [c] = 1,
       [a] = 0
      Strict:
       { f#(a(), a()) -> f#(a(), b()),
         f#(a(), b()) -> f#(s(a()), c()),
        f#(s(X), c()) -> f#(X, c())}
      Weak:
       { 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:
       {(f#(a(), b()) -> f#(s(a()), c()), f#(s(X), c()) -> f#(X, c()))
        (f#(s(X), c()) -> f#(X, c()), f#(s(X), c()) -> f#(X, c()))
        (f#(a(), a()) -> f#(a(), b()), f#(a(), b()) -> f#(s(a()), c()))}
       SCCS:
        Scc:
         {f#(s(X), c()) -> f#(X, c())}
        SCC:
         Strict:
          {f#(s(X), c()) -> f#(X, c())}
         Weak:
         { 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())}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed