YES

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

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