YES

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

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