YES
Time: 0.008840
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:
  DP:
   {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:
   {(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 (1):
    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 (4):
     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:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [f](x0, x1) = x0 + x1,
       
       [s](x0) = x0,
       
       [a] = 0,
       
       [b] = 0,
       
       [c] = 1,
       
       [f#](x0, x1) = x0
      Strict:
       f#(c(), c()) -> f#(a(), a())
       1 >= 0
       f#(s X, c()) -> f#(X, c())
       0 + 1X >= 0 + 1X
       f#(a(), b()) -> f#(s a(), c())
       0 >= 0
       f#(a(), a()) -> f#(a(), b())
       0 >= 0
      Weak:
       
     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 (1):
       Scc:
        {f#(s X, c()) -> f#(X, c())}
       SCC (1):
        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