YES
Time: 0.039703
TRS:
 {  a c d x -> c x,
  u b d d x -> b x,
      v c x -> b x,
    v a c x -> u b d x,
    v a a x -> u v x,
      w c x -> b x,
    w a c x -> u b d x,
    w a a x -> u w x}
 DP:
  DP:
   {v# a c x -> u# b d x,
    v# a a x -> u# v x,
    v# a a x -> v# x,
    w# a c x -> u# b d x,
    w# a a x -> u# w x,
    w# a a x -> w# x}
  TRS:
  {  a c d x -> c x,
   u b d d x -> b x,
       v c x -> b x,
     v a c x -> u b d x,
     v a a x -> u v x,
       w c x -> b x,
     w a c x -> u b d x,
     w a a x -> u w x}
  UR:
   {u b d d x -> b x,
        v c x -> b x,
      v a c x -> u b d x,
      v a a x -> u v x,
        w c x -> b x,
      w a c x -> u b d x,
      w a a x -> u w x}
   EDG:
    {(w# a a x -> w# x, w# a a x -> w# x)
     (w# a a x -> w# x, w# a a x -> u# w x)
     (w# a a x -> w# x, w# a c x -> u# b d x)
     (v# a a x -> v# x, v# a c x -> u# b d x)
     (v# a a x -> v# x, v# a a x -> u# v x)
     (v# a a x -> v# x, v# a a x -> v# x)}
    STATUS:
     arrows: 0.833333
     SCCS (2):
      Scc:
       {w# a a x -> w# x}
      Scc:
       {v# a a x -> v# x}
      
      SCC (1):
       Strict:
        {w# a a x -> w# x}
       Weak:
       {  a c d x -> c x,
        u b d d x -> b x,
            v c x -> b x,
          v a c x -> u b d x,
          v a a x -> u v x,
            w c x -> b x,
          w a c x -> u b d x,
          w a a x -> u w x}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [c](x0) = 1,
         
         [a](x0) = x0 + 1,
         
         [d](x0) = x0 + 1,
         
         [b](x0) = 0,
         
         [u](x0) = 0,
         
         [v](x0) = x0 + 1,
         
         [w](x0) = x0 + 1,
         
         [w#](x0) = x0
        Strict:
         w# a a x -> w# x
         2 + 1x >= 0 + 1x
        Weak:
         w a a x -> u w x
         3 + 1x >= 0 + 0x
         w a c x -> u b d x
         3 + 0x >= 0 + 0x
         w c x -> b x
         2 + 0x >= 0 + 0x
         v a a x -> u v x
         3 + 1x >= 0 + 0x
         v a c x -> u b d x
         3 + 0x >= 0 + 0x
         v c x -> b x
         2 + 0x >= 0 + 0x
         u b d d x -> b x
         0 + 0x >= 0 + 0x
         a c d x -> c x
         2 + 0x >= 1 + 0x
       Qed
     
     SCC (1):
      Strict:
       {v# a a x -> v# x}
      Weak:
      {  a c d x -> c x,
       u b d d x -> b x,
           v c x -> b x,
         v a c x -> u b d x,
         v a a x -> u v x,
           w c x -> b x,
         w a c x -> u b d x,
         w a a x -> u w x}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [c](x0) = 1,
        
        [a](x0) = x0 + 1,
        
        [d](x0) = x0 + 1,
        
        [b](x0) = 0,
        
        [u](x0) = 0,
        
        [v](x0) = x0 + 1,
        
        [w](x0) = x0 + 1,
        
        [v#](x0) = x0
       Strict:
        v# a a x -> v# x
        2 + 1x >= 0 + 1x
       Weak:
        w a a x -> u w x
        3 + 1x >= 0 + 0x
        w a c x -> u b d x
        3 + 0x >= 0 + 0x
        w c x -> b x
        2 + 0x >= 0 + 0x
        v a a x -> u v x
        3 + 1x >= 0 + 0x
        v a c x -> u b d x
        3 + 0x >= 0 + 0x
        v c x -> b x
        2 + 0x >= 0 + 0x
        u b d d x -> b x
        0 + 0x >= 0 + 0x
        a c d x -> c x
        2 + 0x >= 1 + 0x
      Qed