YES(?,O(n^2))

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

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
             [1 1]     [1]
   [b](x0) = [0 1]x0 + [1],
   
             [1 2]     [0]
   [a](x0) = [0 1]x0 + [4]
  orientation:
              [1 3]     [5]    [1 3]     [3]           
   b(a(x1)) = [0 1]x1 + [5] >= [0 1]x1 + [5] = a(b(x1))
   
                 [1 6]     [24]    [1 6]     [23]                 
   a(a(a(x1))) = [0 1]x1 + [12] >= [0 1]x1 + [10] = b(a(a(b(x1))))
   
                    [1 4]     [10]    [1 2]     [0]        
   b(b(b(b(x1)))) = [0 1]x1 + [4 ] >= [0 1]x1 + [4] = a(x1)
  problem:
   
  Qed