YES(?,O(n^1))
TRS:
 {
  u b d d x -> b x,
    a c d x -> c 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
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
    u b d d x -> b x,
      a c d x -> c 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
   }
  Natural interpretation:
   Strict:
    {
     u b d d x -> b x,
       a c d x -> c 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
    }
   Weak:
    {}
   Interpretation class: stronglylinear
   [w](X0) = + 1*X0 + 0
   [v](X0) = + 1*X0 + 5
   [b](X0) = + 1*X0 + 2
   [d](X0) = + 1*X0 + 5
   [a](X0) = + 1*X0 + 6
   [c](X0) = + 1*X0 + 3
   [u](X0) = + 1*X0 + 0
   
   Qed