MAYBE

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

Proof:
 Complexity Transformation Processor:
  strict:
   b(a(b(x1))) -> b(a(a(a(b(x1)))))
   b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
   b(a(a(a(b(a(a(a(b(x1))))))))) -> b(x1)
   b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
   b(a(a(b(b(x1))))) -> b(x1)
   b(b(a(a(b(x1))))) -> b(x1)
   b(a(a(a(b(a(b(x1))))))) -> b(x1)
   b(a(b(a(a(a(b(x1))))))) -> b(x1)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 3
   max_matrix:
    [1 1 0]
    [0 0 1]
    [0 0 0]
    interpretation:
               [1 0 0]  
     [a](x0) = [0 0 1]x0
               [0 0 0]  ,
     
               [1 1 0]     [0]
     [b](x0) = [0 0 0]x0 + [0]
               [0 0 0]     [1]
    orientation:
                   [1 1 0]     [1]    [1 1 0]     [0]                    
     b(a(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(a(a(a(b(x1)))))
                   [0 0 0]     [1]    [0 0 0]     [1]                    
     
                                  [1 1 0]     [0]    [1 1 0]     [0]                                         
     b(a(a(a(b(a(a(b(x1)))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
                                  [0 0 0]     [1]    [0 0 0]     [1]                                         
     
                                     [1 1 0]     [0]    [1 1 0]     [0]        
     b(a(a(a(b(a(a(a(b(x1))))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
                                     [0 0 0]     [1]    [0 0 0]     [1]        
     
                               [1 1 0]     [0]    [1 1 0]     [0]                          
     b(a(a(a(b(b(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(b(b(a(a(a(b(x1)))))))
                               [0 0 0]     [1]    [0 0 0]     [1]                          
     
                         [1 1 0]     [0]    [1 1 0]     [0]        
     b(a(a(b(b(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
                         [0 0 0]     [1]    [0 0 0]     [1]        
     
                         [1 1 0]     [0]    [1 1 0]     [0]        
     b(b(a(a(b(x1))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
                         [0 0 0]     [1]    [0 0 0]     [1]        
     
                               [1 1 0]     [1]    [1 1 0]     [0]        
     b(a(a(a(b(a(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
                               [0 0 0]     [1]    [0 0 0]     [1]        
     
                               [1 1 0]     [1]    [1 1 0]     [0]        
     b(a(b(a(a(a(b(x1))))))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(x1)
                               [0 0 0]     [1]    [0 0 0]     [1]        
    problem:
     strict:
      b(a(a(a(b(a(a(b(x1)))))))) -> b(a(a(b(a(a(b(a(a(a(b(b(x1))))))))))))
      b(a(a(a(b(a(a(a(b(x1))))))))) -> b(x1)
      b(a(a(a(b(b(b(x1))))))) -> b(b(b(a(a(a(b(x1)))))))
      b(a(a(b(b(x1))))) -> b(x1)
      b(b(a(a(b(x1))))) -> b(x1)
     weak:
      b(a(b(x1))) -> b(a(a(a(b(x1)))))
      b(a(a(a(b(a(b(x1))))))) -> b(x1)
      b(a(b(a(a(a(b(x1))))))) -> b(x1)
    Open