YES
TRS:
 {b(c(x)) -> c(b(b(x))),
  b(v(x)) -> x,
  a(b(x)) -> b(a(a(x))),
  a(u(x)) -> x,
  c(a(x)) -> a(c(c(x))),
  c(w(x)) -> x,
  u(a(x)) -> x,
  v(b(x)) -> x,
  w(c(x)) -> x}
 RUF:
  Strict:
   {b(c(x)) -> c(b(b(x))),
    a(b(x)) -> b(a(a(x))),
    c(a(x)) -> a(c(c(x)))}
  Weak:
   {}
  DP:
   Strict:
    {b#(c(x)) -> b#(x),
     b#(c(x)) -> b#(b(x)),
     b#(c(x)) -> c#(b(b(x))),
     a#(b(x)) -> b#(a(a(x))),
     a#(b(x)) -> a#(x),
     a#(b(x)) -> a#(a(x)),
     c#(a(x)) -> a#(c(c(x))),
     c#(a(x)) -> c#(x),
     c#(a(x)) -> c#(c(x))}
   Weak:
   {b(c(x)) -> c(b(b(x))),
    a(b(x)) -> b(a(a(x))),
    c(a(x)) -> a(c(c(x)))}
   EDG:
    {(a#(b(x)) -> b#(a(a(x))), b#(c(x)) -> c#(b(b(x))))
     (a#(b(x)) -> b#(a(a(x))), b#(c(x)) -> b#(b(x)))
     (a#(b(x)) -> b#(a(a(x))), b#(c(x)) -> b#(x))
     (b#(c(x)) -> b#(x), b#(c(x)) -> c#(b(b(x))))
     (b#(c(x)) -> b#(x), b#(c(x)) -> b#(b(x)))
     (b#(c(x)) -> b#(x), b#(c(x)) -> b#(x))
     (c#(a(x)) -> c#(x), c#(a(x)) -> c#(c(x)))
     (c#(a(x)) -> c#(x), c#(a(x)) -> c#(x))
     (c#(a(x)) -> c#(x), c#(a(x)) -> a#(c(c(x))))
     (a#(b(x)) -> a#(a(x)), a#(b(x)) -> a#(a(x)))
     (a#(b(x)) -> a#(a(x)), a#(b(x)) -> a#(x))
     (a#(b(x)) -> a#(a(x)), a#(b(x)) -> b#(a(a(x))))
     (c#(a(x)) -> c#(c(x)), c#(a(x)) -> a#(c(c(x))))
     (c#(a(x)) -> c#(c(x)), c#(a(x)) -> c#(x))
     (c#(a(x)) -> c#(c(x)), c#(a(x)) -> c#(c(x)))
     (b#(c(x)) -> b#(b(x)), b#(c(x)) -> b#(x))
     (b#(c(x)) -> b#(b(x)), b#(c(x)) -> b#(b(x)))
     (b#(c(x)) -> b#(b(x)), b#(c(x)) -> c#(b(b(x))))
     (a#(b(x)) -> a#(x), a#(b(x)) -> b#(a(a(x))))
     (a#(b(x)) -> a#(x), a#(b(x)) -> a#(x))
     (a#(b(x)) -> a#(x), a#(b(x)) -> a#(a(x)))
     (c#(a(x)) -> a#(c(c(x))), a#(b(x)) -> b#(a(a(x))))
     (c#(a(x)) -> a#(c(c(x))), a#(b(x)) -> a#(x))
     (c#(a(x)) -> a#(c(c(x))), a#(b(x)) -> a#(a(x)))
     (b#(c(x)) -> c#(b(b(x))), c#(a(x)) -> a#(c(c(x))))
     (b#(c(x)) -> c#(b(b(x))), c#(a(x)) -> c#(x))
     (b#(c(x)) -> c#(b(b(x))), c#(a(x)) -> c#(c(x)))}
    SCCS:
     Scc:
      {b#(c(x)) -> b#(x),
       b#(c(x)) -> b#(b(x)),
       b#(c(x)) -> c#(b(b(x))),
       a#(b(x)) -> b#(a(a(x))),
       a#(b(x)) -> a#(x),
       a#(b(x)) -> a#(a(x)),
       c#(a(x)) -> a#(c(c(x))),
       c#(a(x)) -> c#(x),
       c#(a(x)) -> c#(c(x))}
     SCC:
      Strict:
       {b#(c(x)) -> b#(x),
        b#(c(x)) -> b#(b(x)),
        b#(c(x)) -> c#(b(b(x))),
        a#(b(x)) -> b#(a(a(x))),
        a#(b(x)) -> a#(x),
        a#(b(x)) -> a#(a(x)),
        c#(a(x)) -> a#(c(c(x))),
        c#(a(x)) -> c#(x),
        c#(a(x)) -> c#(c(x))}
      Weak:
      {b(c(x)) -> c(b(b(x))),
       a(b(x)) -> b(a(a(x))),
       c(a(x)) -> a(c(c(x)))}
      POLY:
       Argument Filtering:
        pi(c#) = [], pi(c) = [], pi(a#) = 0, pi(a) = 0, pi(b#) = [], pi(b) = [0]
       Usable Rules:
        {}
       Interpretation:
        [c#] = 0,
        [b#] = 0,
        [c] = 0,
        [b](x0) = x0 + 1
       Strict:
        {b#(c(x)) -> b#(x),
         b#(c(x)) -> b#(b(x)),
         b#(c(x)) -> c#(b(b(x))),
         c#(a(x)) -> a#(c(c(x))),
         c#(a(x)) -> c#(x),
         c#(a(x)) -> c#(c(x))}
       Weak:
        {b(c(x)) -> c(b(b(x))),
         a(b(x)) -> b(a(a(x))),
         c(a(x)) -> a(c(c(x)))}
       EDG:
        {(c#(a(x)) -> c#(x), c#(a(x)) -> c#(c(x)))
         (c#(a(x)) -> c#(x), c#(a(x)) -> c#(x))
         (c#(a(x)) -> c#(x), c#(a(x)) -> a#(c(c(x))))
         (c#(a(x)) -> c#(c(x)), c#(a(x)) -> c#(c(x)))
         (c#(a(x)) -> c#(c(x)), c#(a(x)) -> c#(x))
         (c#(a(x)) -> c#(c(x)), c#(a(x)) -> a#(c(c(x))))
         (b#(c(x)) -> b#(b(x)), b#(c(x)) -> b#(x))
         (b#(c(x)) -> b#(b(x)), b#(c(x)) -> b#(b(x)))
         (b#(c(x)) -> b#(b(x)), b#(c(x)) -> c#(b(b(x))))
         (b#(c(x)) -> b#(x), b#(c(x)) -> b#(x))
         (b#(c(x)) -> b#(x), b#(c(x)) -> b#(b(x)))
         (b#(c(x)) -> b#(x), b#(c(x)) -> c#(b(b(x))))
         (b#(c(x)) -> c#(b(b(x))), c#(a(x)) -> a#(c(c(x))))
         (b#(c(x)) -> c#(b(b(x))), c#(a(x)) -> c#(x))
         (b#(c(x)) -> c#(b(b(x))), c#(a(x)) -> c#(c(x)))}
        SCCS:
         Scc:
          {c#(a(x)) -> c#(x),
           c#(a(x)) -> c#(c(x))}
         Scc:
          {b#(c(x)) -> b#(x),
           b#(c(x)) -> b#(b(x))}
         SCC:
          Strict:
           {c#(a(x)) -> c#(x),
            c#(a(x)) -> c#(c(x))}
          Weak:
          {b(c(x)) -> c(b(b(x))),
           a(b(x)) -> b(a(a(x))),
           c(a(x)) -> a(c(c(x)))}
          POLY:
           Argument Filtering:
            pi(c#) = 0, pi(c) = 0, pi(a) = [0], pi(b) = []
           Usable Rules:
            {}
           Interpretation:
            [a](x0) = x0 + 1
           Strict:
            {}
           Weak:
            {b(c(x)) -> c(b(b(x))),
             a(b(x)) -> b(a(a(x))),
             c(a(x)) -> a(c(c(x)))}
           Qed
         SCC:
          Strict:
           {b#(c(x)) -> b#(x),
            b#(c(x)) -> b#(b(x))}
          Weak:
          {b(c(x)) -> c(b(b(x))),
           a(b(x)) -> b(a(a(x))),
           c(a(x)) -> a(c(c(x)))}
          POLY:
           Argument Filtering:
            pi(c) = [0], pi(a) = [], pi(b#) = 0, pi(b) = 0
           Usable Rules:
            {}
           Interpretation:
            [c](x0) = x0 + 1
           Strict:
            {}
           Weak:
            {b(c(x)) -> c(b(b(x))),
             a(b(x)) -> b(a(a(x))),
             c(a(x)) -> a(c(c(x)))}
           Qed