YES
Time: 0.017660
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:
   DP:
    {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}
   TRS:
   {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 -> a# x, a# b x -> a# a x)
     (a# b x -> a# x, a# b x -> a# x)
     (a# b x -> a# x, a# b x -> b# a a x)
     (b# c x -> c# b b x, c# a x -> 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 -> a# c c x)
     (c# a x -> a# c c x, a# b x -> 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 -> b# a a 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 -> b# a a x, b# c x -> 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 -> c# b b x)
     (c# a x -> c# x, c# a x -> a# c c x)
     (c# a x -> c# x, c# a x -> c# x)
     (c# a x -> c# x, c# a x -> c# c 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)}
    SCCS (1):
     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 (9):
      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:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [b](x0) = 0,
        
        [a](x0) = x0 + 1,
        
        [c](x0) = x0,
        
        [b#](x0) = 0,
        
        [a#](x0) = 0,
        
        [c#](x0) = x0
       Strict:
        c# a x -> c# c x
        1 + 1x >= 0 + 1x
        c# a x -> c# x
        1 + 1x >= 0 + 1x
        c# a x -> a# c c x
        1 + 1x >= 0 + 0x
        a# b x -> a# a x
        0 + 0x >= 0 + 0x
        a# b x -> a# x
        0 + 0x >= 0 + 0x
        a# b x -> b# a a x
        0 + 0x >= 0 + 0x
        b# c x -> c# b b x
        0 + 0x >= 0 + 0x
        b# c x -> b# b x
        0 + 0x >= 0 + 0x
        b# c x -> b# x
        0 + 0x >= 0 + 0x
       Weak:
        
      EDG:
       {(a# b x -> a# x, a# b x -> a# a x)
        (a# b x -> a# x, a# b x -> a# x)
        (a# b x -> a# x, a# b x -> b# a a x)
        (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)
        (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)
        (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)}
       SCCS (2):
        Scc:
         {a# b x -> a# x,
          a# b x -> a# a x}
        Scc:
         {b# c x -> b# x,
          b# c x -> b# b x}
        SCC (2):
         Strict:
          {a# b x -> a# x,
           a# b x -> a# a x}
         Weak:
         {b c x -> c b b x,
          a b x -> b a a x,
          c a x -> a c c x}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [b](x0) = x0 + 1,
           
           [a](x0) = x0,
           
           [c](x0) = 0,
           
           [a#](x0) = x0
          Strict:
           a# b x -> a# a x
           1 + 1x >= 0 + 1x
           a# b x -> a# x
           1 + 1x >= 0 + 1x
          Weak:
           
         Qed
       SCC (2):
        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:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [b](x0) = x0,
          
          [a](x0) = 0,
          
          [c](x0) = x0 + 1,
          
          [b#](x0) = x0 + 1
         Strict:
          b# c x -> b# b x
          2 + 1x >= 1 + 1x
          b# c x -> b# x
          2 + 1x >= 1 + 1x
         Weak:
          
        Qed