YES

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

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