YES

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

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