YES(?,O(n^1))

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

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