YES(?,O(n^1))

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

Proof:
 Arctic Interpretation Processor:
  dimension: 2
  interpretation:
             [0 3]  
   [a](x0) = [2 5]x0,
   
             [4  1 ]  
   [b](x0) = [1  -&]x0
  orientation:
                 [12 9 ]      [0 3]          
   b(b(b(x1))) = [9  6 ]x1 >= [2 5]x1 = a(x1)
   
              [5  8 ]      [4 7]                
   a(a(x1)) = [7  10]x1 >= [6 9]x1 = a(b(a(x1)))
   
                 [10 13]      [9  12]                
   a(a(a(x1))) = [12 15]x1 >= [6  9 ]x1 = b(a(a(x1)))
  problem:
   
  Qed