YES(?,O(n^1))

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

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