YES(?,O(n^1))

Problem:
 a(c(d(x))) -> c(x)
 u(b(d(d(x)))) -> b(x)
 v(a(a(x))) -> u(v(x))
 v(a(c(x))) -> u(b(d(x)))
 v(c(x)) -> b(x)
 w(a(a(x))) -> u(w(x))
 w(a(c(x))) -> u(b(d(x)))
 w(c(x)) -> b(x)

Proof:
 Complexity Transformation Processor:
  strict:
   a(c(d(x))) -> c(x)
   u(b(d(d(x)))) -> b(x)
   v(a(a(x))) -> u(v(x))
   v(a(c(x))) -> u(b(d(x)))
   v(c(x)) -> b(x)
   w(a(a(x))) -> u(w(x))
   w(a(c(x))) -> u(b(d(x)))
   w(c(x)) -> b(x)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [w](x0) = x0 + 1,
     
     [v](x0) = x0,
     
     [u](x0) = x0,
     
     [b](x0) = x0,
     
     [a](x0) = x0 + 1,
     
     [c](x0) = x0 + 1,
     
     [d](x0) = x0
    orientation:
     a(c(d(x))) = x + 2 >= x + 1 = c(x)
     
     u(b(d(d(x)))) = x >= x = b(x)
     
     v(a(a(x))) = x + 2 >= x = u(v(x))
     
     v(a(c(x))) = x + 2 >= x = u(b(d(x)))
     
     v(c(x)) = x + 1 >= x = b(x)
     
     w(a(a(x))) = x + 3 >= x + 1 = u(w(x))
     
     w(a(c(x))) = x + 3 >= x = u(b(d(x)))
     
     w(c(x)) = x + 2 >= x = b(x)
    problem:
     strict:
      u(b(d(d(x)))) -> b(x)
     weak:
      a(c(d(x))) -> c(x)
      v(a(a(x))) -> u(v(x))
      v(a(c(x))) -> u(b(d(x)))
      v(c(x)) -> b(x)
      w(a(a(x))) -> u(w(x))
      w(a(c(x))) -> u(b(d(x)))
      w(c(x)) -> b(x)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [w](x0) = x0 + 1,
       
       [v](x0) = x0 + 1,
       
       [u](x0) = x0,
       
       [b](x0) = x0,
       
       [a](x0) = x0,
       
       [c](x0) = x0,
       
       [d](x0) = x0 + 1
      orientation:
       u(b(d(d(x)))) = x + 2 >= x = b(x)
       
       a(c(d(x))) = x + 1 >= x = c(x)
       
       v(a(a(x))) = x + 1 >= x + 1 = u(v(x))
       
       v(a(c(x))) = x + 1 >= x + 1 = u(b(d(x)))
       
       v(c(x)) = x + 1 >= x = b(x)
       
       w(a(a(x))) = x + 1 >= x + 1 = u(w(x))
       
       w(a(c(x))) = x + 1 >= x + 1 = u(b(d(x)))
       
       w(c(x)) = x + 1 >= x = b(x)
      problem:
       strict:
        
       weak:
        u(b(d(d(x)))) -> b(x)
        a(c(d(x))) -> c(x)
        v(a(a(x))) -> u(v(x))
        v(a(c(x))) -> u(b(d(x)))
        v(c(x)) -> b(x)
        w(a(a(x))) -> u(w(x))
        w(a(c(x))) -> u(b(d(x)))
        w(c(x)) -> b(x)
      Qed