YES

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

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