YES(?,O(n^1))

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

Proof:
 RT Transformation Processor:
  strict:
   a(a(x1)) -> a(b(a(x1)))
   b(a(b(x1))) -> a(c(a(x1)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [c](x0) = x0 + 6,
    
    [b](x0) = x0 + 9,
    
    [a](x0) = x0 + 9
   orientation:
    a(a(x1)) = x1 + 18 >= x1 + 27 = a(b(a(x1)))
    
    b(a(b(x1))) = x1 + 27 >= x1 + 24 = a(c(a(x1)))
   problem:
    strict:
     a(a(x1)) -> a(b(a(x1)))
    weak:
     b(a(b(x1))) -> a(c(a(x1)))
   Arctic Interpretation Processor:
    dimension: 3
    interpretation:
               [0  0  -&]  
     [c](x0) = [-& -& -&]x0
               [-& -& -&]  ,
     
               [0  -& 0 ]  
     [b](x0) = [0  1  0 ]x0
               [-& 1  -&]  ,
     
               [0  -& 1 ]  
     [a](x0) = [-& 0  1 ]x0
               [0  2  3 ]  
    orientation:
                [1 3 4]      [0 2 3]                
     a(a(x1)) = [1 3 4]x1 >= [0 2 3]x1 = a(b(a(x1)))
                [3 5 6]      [2 4 5]                
     
                   [2 4 2]      [0  0  1 ]                
     b(a(b(x1))) = [2 4 2]x1 >= [-& -& -&]x1 = a(c(a(x1)))
                   [1 3 1]      [0  0  1 ]                
    problem:
     strict:
      
     weak:
      a(a(x1)) -> a(b(a(x1)))
      b(a(b(x1))) -> a(c(a(x1)))
    Qed