YES(?,O(n^3))

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

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