YES

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

Proof:
 Arctic Interpretation Processor:
  dimension: 1
  interpretation:
   [d](x0) = 2x0,
   
   [b](x0) = 1x0,
   
   [c](x0) = 1x0,
   
   [a](x0) = x0
  orientation:
   b(c(a(x1))) = 2x1 >= 1x1 = a(b(x1))
   
   b(b(b(x1))) = 3x1 >= 2x1 = c(a(c(x1)))
   
   c(d(x1)) = 3x1 >= 3x1 = d(c(x1))
   
   c(d(b(x1))) = 4x1 >= 4x1 = d(c(c(x1)))
   
   d(c(x1)) = 3x1 >= 3x1 = b(b(b(x1)))
   
   c(b(x1)) = 2x1 >= 2x1 = d(a(x1))
   
   d(b(c(x1))) = 4x1 >= x1 = a(a(x1))
   
   d(a(x1)) = 2x1 >= 1x1 = b(x1)
  problem:
   c(d(x1)) -> d(c(x1))
   c(d(b(x1))) -> d(c(c(x1)))
   d(c(x1)) -> b(b(b(x1)))
   c(b(x1)) -> d(a(x1))
  String Reversal Processor:
   d(c(x1)) -> c(d(x1))
   b(d(c(x1))) -> c(c(d(x1)))
   c(d(x1)) -> b(b(b(x1)))
   b(c(x1)) -> a(d(x1))
   Matrix Interpretation Processor: dim=3
    
    interpretation:
               [1 1 1]  
     [d](x0) = [1 1 1]x0
               [1 0 1]  ,
     
               [1 0 1]  
     [b](x0) = [1 0 1]x0
               [0 1 0]  ,
     
               [1 0 1]     [0]
     [c](x0) = [1 0 1]x0 + [1]
               [0 1 0]     [0],
     
               [1 0 0]  
     [a](x0) = [0 0 0]x0
               [0 0 1]  
    orientation:
                [2 1 2]     [1]    [2 1 2]     [0]           
     d(c(x1)) = [2 1 2]x1 + [1] >= [2 1 2]x1 + [1] = c(d(x1))
                [1 1 1]     [0]    [1 1 1]     [0]           
     
                   [3 2 3]     [1]    [3 2 3]     [0]              
     b(d(c(x1))) = [3 2 3]x1 + [1] >= [3 2 3]x1 + [1] = c(c(d(x1)))
                   [2 1 2]     [1]    [2 1 2]     [1]              
     
                [2 1 2]     [0]    [2 1 2]                
     c(d(x1)) = [2 1 2]x1 + [1] >= [2 1 2]x1 = b(b(b(x1)))
                [1 1 1]     [0]    [1 1 1]                
     
                [1 1 1]     [0]    [1 1 1]             
     b(c(x1)) = [1 1 1]x1 + [0] >= [0 0 0]x1 = a(d(x1))
                [1 0 1]     [1]    [1 0 1]             
    problem:
     c(d(x1)) -> b(b(b(x1)))
     b(c(x1)) -> a(d(x1))
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
                [2 0]  
      [d](x0) = [1 3]x0,
      
                [0  -&]  
      [b](x0) = [0  2 ]x0,
      
                [3  1 ]  
      [c](x0) = [-& 3 ]x0,
      
                  
      [a](x0) = x0
     orientation:
                 [5 4]      [0  -&]                
      c(d(x1)) = [4 6]x1 >= [4  6 ]x1 = b(b(b(x1)))
      
                 [3 1]      [2 0]             
      b(c(x1)) = [3 5]x1 >= [1 3]x1 = a(d(x1))
     problem:
      c(d(x1)) -> b(b(b(x1)))
     Arctic Interpretation Processor:
      dimension: 2
      interpretation:
                 [0 2]  
       [d](x0) = [1 0]x0,
       
                 [0  -&]  
       [b](x0) = [1  0 ]x0,
       
                 [2 3]  
       [c](x0) = [1 2]x0
      orientation:
                  [4 4]      [0  -&]                
       c(d(x1)) = [3 3]x1 >= [1  0 ]x1 = b(b(b(x1)))
      problem:
       
      Qed