YES(?,O(n^1))

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

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