YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 1
  interpretation:
   [d](x0) = 4x0,
   
   [c](x0) = 6x0,
   
   [b](x0) = 9x0,
   
   [a](x0) = 14x0
  orientation:
   a(a(x1)) = 28x1 >= 27x1 = b(b(b(x1)))
   
   b(b(x1)) = 18x1 >= 18x1 = c(c(c(x1)))
   
   c(c(x1)) = 12x1 >= 12x1 = d(d(d(x1)))
   
   b(x1) = 9x1 >= 8x1 = d(d(x1))
   
   c(d(d(x1))) = 14x1 >= 14x1 = a(x1)
  problem:
   b(b(x1)) -> c(c(c(x1)))
   c(c(x1)) -> d(d(d(x1)))
   c(d(d(x1))) -> a(x1)
  Arctic Interpretation Processor:
   dimension: 2
   interpretation:
              [0 0]  
    [d](x0) = [1 0]x0,
    
              [2 0]  
    [c](x0) = [2 2]x0,
    
              [0 3]  
    [b](x0) = [3 3]x0,
    
              [0  -&]  
    [a](x0) = [0  0 ]x0
   orientation:
               [6 6]      [6 4]                
    b(b(x1)) = [6 6]x1 >= [6 6]x1 = c(c(c(x1)))
    
               [4 2]      [1 1]                
    c(c(x1)) = [4 4]x1 >= [2 1]x1 = d(d(d(x1)))
    
                  [3 2]      [0  -&]          
    c(d(d(x1))) = [3 3]x1 >= [0  0 ]x1 = a(x1)
   problem:
    b(b(x1)) -> c(c(c(x1)))
   Arctic Interpretation Processor:
    dimension: 3
    interpretation:
               [0  -& 0 ]  
     [c](x0) = [-& -& 0 ]x0
               [0  0  0 ]  ,
     
               [0  1  0 ]  
     [b](x0) = [1  0  1 ]x0
               [1  1  -&]  
    orientation:
                [2 1 2]      [0 0 0]                
     b(b(x1)) = [2 2 1]x1 >= [0 0 0]x1 = c(c(c(x1)))
                [2 2 2]      [0 0 0]                
    problem:
     
    Qed