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:
 RT 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
   interpretation:
    [w](x0) = x0 + 1,
    
    [v](x0) = x0 + 1,
    
    [u](x0) = x0 + 7,
    
    [b](x0) = x0 + 2,
    
    [a](x0) = x0 + 2,
    
    [c](x0) = x0 + 2,
    
    [d](x0) = x0 + 17
   orientation:
    a(c(d(x))) = x + 21 >= x + 2 = c(x)
    
    u(b(d(d(x)))) = x + 43 >= x + 2 = b(x)
    
    v(a(a(x))) = x + 5 >= x + 8 = u(v(x))
    
    v(a(c(x))) = x + 5 >= x + 26 = u(b(d(x)))
    
    v(c(x)) = x + 3 >= x + 2 = b(x)
    
    w(a(a(x))) = x + 5 >= x + 8 = u(w(x))
    
    w(a(c(x))) = x + 5 >= x + 26 = u(b(d(x)))
    
    w(c(x)) = x + 3 >= x + 2 = b(x)
   problem:
    strict:
     v(a(a(x))) -> u(v(x))
     v(a(c(x))) -> u(b(d(x)))
     w(a(a(x))) -> u(w(x))
     w(a(c(x))) -> u(b(d(x)))
    weak:
     a(c(d(x))) -> c(x)
     u(b(d(d(x)))) -> b(x)
     v(c(x)) -> b(x)
     w(c(x)) -> b(x)
   Bounds Processor:
    bound: 1
    enrichment: match-rt
    automaton:
     final states: {8}
     transitions:
      u1(21) -> 22*
      b1(20) -> 21*
      b1(43) -> 44*
      d1(19) -> 20*
      v0(8) -> 8*
      a0(8) -> 8*
      u0(8) -> 8*
      c0(8) -> 8*
      b0(8) -> 8*
      d0(8) -> 8*
      w0(8) -> 8*
      8 -> 43,19
      22 -> 8*
      44 -> 22,8
    problem:
     strict:
      v(a(a(x))) -> u(v(x))
      w(a(a(x))) -> u(w(x))
      w(a(c(x))) -> u(b(d(x)))
     weak:
      v(a(c(x))) -> u(b(d(x)))
      a(c(d(x))) -> c(x)
      u(b(d(d(x)))) -> b(x)
      v(c(x)) -> b(x)
      w(c(x)) -> b(x)
    Bounds Processor:
     bound: 1
     enrichment: match-rt
     automaton:
      final states: {8}
      transitions:
       u1(27) -> 28*
       b1(29) -> 30*
       b1(26) -> 27*
       d1(25) -> 26*
       v0(8) -> 8*
       a0(8) -> 8*
       u0(8) -> 8*
       c0(8) -> 8*
       b0(8) -> 8*
       d0(8) -> 8*
       w0(8) -> 8*
       8 -> 29,25
       28 -> 8*
       30 -> 28,8
     problem:
      strict:
       v(a(a(x))) -> u(v(x))
       w(a(a(x))) -> u(w(x))
      weak:
       w(a(c(x))) -> u(b(d(x)))
       v(a(c(x))) -> u(b(d(x)))
       a(c(d(x))) -> c(x)
       u(b(d(d(x)))) -> b(x)
       v(c(x)) -> b(x)
       w(c(x)) -> b(x)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [w](x0) = x0 + 8,
       
       [v](x0) = x0 + 8,
       
       [u](x0) = x0,
       
       [b](x0) = x0 + 13,
       
       [a](x0) = x0 + 2,
       
       [c](x0) = x0 + 5,
       
       [d](x0) = x0
      orientation:
       v(a(a(x))) = x + 12 >= x + 8 = u(v(x))
       
       w(a(a(x))) = x + 12 >= x + 8 = u(w(x))
       
       w(a(c(x))) = x + 15 >= x + 13 = u(b(d(x)))
       
       v(a(c(x))) = x + 15 >= x + 13 = u(b(d(x)))
       
       a(c(d(x))) = x + 7 >= x + 5 = c(x)
       
       u(b(d(d(x)))) = x + 13 >= x + 13 = b(x)
       
       v(c(x)) = x + 13 >= x + 13 = b(x)
       
       w(c(x)) = x + 13 >= x + 13 = b(x)
      problem:
       strict:
        
       weak:
        v(a(a(x))) -> u(v(x))
        w(a(a(x))) -> u(w(x))
        w(a(c(x))) -> u(b(d(x)))
        v(a(c(x))) -> u(b(d(x)))
        a(c(d(x))) -> c(x)
        u(b(d(d(x)))) -> b(x)
        v(c(x)) -> b(x)
        w(c(x)) -> b(x)
      Qed