YES(?,O(n^1))

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

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