YES

Problem:
 a(a(x1)) -> d(c(x1))
 a(b(x1)) -> c(c(c(x1)))
 b(b(x1)) -> a(c(c(x1)))
 c(c(x1)) -> b(x1)
 c(d(x1)) -> a(a(x1))
 d(d(x1)) -> b(a(c(x1)))

Proof:
 Arctic Interpretation Processor:
  dimension: 1
  interpretation:
   [b](x0) = 4x0,
   
   [d](x0) = 6x0,
   
   [c](x0) = 2x0,
   
   [a](x0) = 4x0
  orientation:
   a(a(x1)) = 8x1 >= 8x1 = d(c(x1))
   
   a(b(x1)) = 8x1 >= 6x1 = c(c(c(x1)))
   
   b(b(x1)) = 8x1 >= 8x1 = a(c(c(x1)))
   
   c(c(x1)) = 4x1 >= 4x1 = b(x1)
   
   c(d(x1)) = 8x1 >= 8x1 = a(a(x1))
   
   d(d(x1)) = 12x1 >= 10x1 = b(a(c(x1)))
  problem:
   a(a(x1)) -> d(c(x1))
   b(b(x1)) -> a(c(c(x1)))
   c(c(x1)) -> b(x1)
   c(d(x1)) -> a(a(x1))
  Arctic Interpretation Processor:
   dimension: 2
   interpretation:
              [2  1 ]  
    [b](x0) = [-& 2 ]x0,
    
              [1  0 ]  
    [d](x0) = [-& 1 ]x0,
    
              [1  0 ]  
    [c](x0) = [-& 1 ]x0,
    
              [1  0 ]  
    [a](x0) = [-& 1 ]x0
   orientation:
               [2  1 ]      [2  1 ]             
    a(a(x1)) = [-& 2 ]x1 >= [-& 2 ]x1 = d(c(x1))
    
               [4  3 ]      [3  2 ]                
    b(b(x1)) = [-& 4 ]x1 >= [-& 3 ]x1 = a(c(c(x1)))
    
               [2  1 ]      [2  1 ]          
    c(c(x1)) = [-& 2 ]x1 >= [-& 2 ]x1 = b(x1)
    
               [2  1 ]      [2  1 ]             
    c(d(x1)) = [-& 2 ]x1 >= [-& 2 ]x1 = a(a(x1))
   problem:
    a(a(x1)) -> d(c(x1))
    c(c(x1)) -> b(x1)
    c(d(x1)) -> a(a(x1))
   Arctic Interpretation Processor:
    dimension: 2
    interpretation:
               [0  -&]  
     [b](x0) = [-& -&]x0,
     
               [0  -&]  
     [d](x0) = [3  0 ]x0,
     
               [0 0]  
     [c](x0) = [3 3]x0,
     
               [0 0]  
     [a](x0) = [3 0]x0
    orientation:
                [3 0]      [0 0]             
     a(a(x1)) = [3 3]x1 >= [3 3]x1 = d(c(x1))
     
                [3 3]      [0  -&]          
     c(c(x1)) = [6 6]x1 >= [-& -&]x1 = b(x1)
     
                [3 0]      [3 0]             
     c(d(x1)) = [6 3]x1 >= [3 3]x1 = a(a(x1))
    problem:
     a(a(x1)) -> d(c(x1))
     c(d(x1)) -> a(a(x1))
    KBO Processor:
     weight function:
      w0 = 1
      w(d) = w(c) = w(a) = 1
     precedence:
      c > a > d
     problem:
      
     Qed