YES

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:
 String Reversal Processor:
  a(x1) -> b(x1)
  a(a(x1)) -> a(b(a(x1)))
  b(a(x1)) -> b(b(b(x1)))
  a(a(a(x1))) -> a(a(b(a(a(x1)))))
  b(a(a(x1))) -> b(a(b(b(a(x1)))))
  a(b(a(x1))) -> a(b(b(a(b(x1)))))
  b(b(a(x1))) -> b(b(b(b(b(x1)))))
  a(b(x1)) -> b(b(b(x1)))
  a(b(a(x1))) -> b(a(b(b(a(x1)))))
  a(a(b(x1))) -> a(b(b(a(b(x1)))))
  a(b(b(x1))) -> b(b(b(b(b(x1)))))
  Matrix Interpretation Processor: dim=2
   
   interpretation:
              [1 0]  
    [b](x0) = [0 0]x0,
    
              [1 1]     [0]
    [a](x0) = [0 0]x0 + [2]
   orientation:
            [1 1]     [0]    [1 0]          
    a(x1) = [0 0]x1 + [2] >= [0 0]x1 = b(x1)
    
               [1 1]     [2]    [1 1]     [0]              
    a(a(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = a(b(a(x1)))
    
               [1 1]      [1 0]                
    b(a(x1)) = [0 0]x1 >= [0 0]x1 = b(b(b(x1)))
    
                  [1 1]     [4]    [1 1]     [4]                    
    a(a(a(x1))) = [0 0]x1 + [2] >= [0 0]x1 + [2] = a(a(b(a(a(x1)))))
    
                  [1 1]     [2]    [1 1]                      
    b(a(a(x1))) = [0 0]x1 + [0] >= [0 0]x1 = b(a(b(b(a(x1)))))
    
                  [1 1]     [0]    [1 0]     [0]                    
    a(b(a(x1))) = [0 0]x1 + [2] >= [0 0]x1 + [2] = a(b(b(a(b(x1)))))
    
                  [1 1]      [1 0]                      
    b(b(a(x1))) = [0 0]x1 >= [0 0]x1 = b(b(b(b(b(x1)))))
    
               [1 0]     [0]    [1 0]                
    a(b(x1)) = [0 0]x1 + [2] >= [0 0]x1 = b(b(b(x1)))
    
                  [1 1]     [0]    [1 1]                      
    a(b(a(x1))) = [0 0]x1 + [2] >= [0 0]x1 = b(a(b(b(a(x1)))))
    
                  [1 0]     [2]    [1 0]     [0]                    
    a(a(b(x1))) = [0 0]x1 + [2] >= [0 0]x1 + [2] = a(b(b(a(b(x1)))))
    
                  [1 0]     [0]    [1 0]                      
    a(b(b(x1))) = [0 0]x1 + [2] >= [0 0]x1 = b(b(b(b(b(x1)))))
   problem:
    a(x1) -> b(x1)
    b(a(x1)) -> b(b(b(x1)))
    a(a(a(x1))) -> a(a(b(a(a(x1)))))
    a(b(a(x1))) -> a(b(b(a(b(x1)))))
    b(b(a(x1))) -> b(b(b(b(b(x1)))))
    a(b(x1)) -> b(b(b(x1)))
    a(b(a(x1))) -> b(a(b(b(a(x1)))))
    a(b(b(x1))) -> b(b(b(b(b(x1)))))
   String Reversal Processor:
    a(x1) -> b(x1)
    a(b(x1)) -> b(b(b(x1)))
    a(a(a(x1))) -> a(a(b(a(a(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(b(a(x1))) -> b(b(b(b(b(x1)))))
    Matrix Interpretation Processor: dim=2
     
     interpretation:
                [1 0]  
      [b](x0) = [0 0]x0,
      
                [1 2]     [0]
      [a](x0) = [0 1]x0 + [1]
     orientation:
              [1 2]     [0]    [1 0]          
      a(x1) = [0 1]x1 + [1] >= [0 0]x1 = b(x1)
      
                 [1 0]     [0]    [1 0]                
      a(b(x1)) = [0 0]x1 + [1] >= [0 0]x1 = b(b(b(x1)))
      
                    [1 6]     [6]    [1 4]     [4]                    
      a(a(a(x1))) = [0 1]x1 + [3] >= [0 0]x1 + [2] = a(a(b(a(a(x1)))))
      
                    [1 2]     [0]    [1 2]                      
      a(b(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 = b(a(b(b(a(x1)))))
      
                    [1 0]     [0]    [1 0]                      
      a(b(b(x1))) = [0 0]x1 + [1] >= [0 0]x1 = b(b(b(b(b(x1)))))
      
                 [1 2]      [1 0]                
      b(a(x1)) = [0 0]x1 >= [0 0]x1 = b(b(b(x1)))
      
                    [1 2]     [0]    [1 0]     [0]                    
      a(b(a(x1))) = [0 0]x1 + [1] >= [0 0]x1 + [1] = a(b(b(a(b(x1)))))
      
                    [1 2]      [1 0]                      
      b(b(a(x1))) = [0 0]x1 >= [0 0]x1 = b(b(b(b(b(x1)))))
     problem:
      a(x1) -> b(x1)
      a(b(x1)) -> b(b(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(b(a(x1))) -> b(b(b(b(b(x1)))))
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [b](x0) = x0,
       
       [a](x0) = 6x0
      orientation:
       a(x1) = 6x1 >= x1 = b(x1)
       
       a(b(x1)) = 6x1 >= x1 = b(b(b(x1)))
       
       a(b(a(x1))) = 12x1 >= 12x1 = b(a(b(b(a(x1)))))
       
       a(b(b(x1))) = 6x1 >= x1 = b(b(b(b(b(x1)))))
       
       b(a(x1)) = 6x1 >= x1 = b(b(b(x1)))
       
       a(b(a(x1))) = 12x1 >= 12x1 = a(b(b(a(b(x1)))))
       
       b(b(a(x1))) = 6x1 >= x1 = b(b(b(b(b(x1)))))
      problem:
       a(b(a(x1))) -> b(a(b(b(a(x1)))))
       a(b(a(x1))) -> a(b(b(a(b(x1)))))
      String Reversal Processor:
       a(b(a(x1))) -> a(b(b(a(b(x1)))))
       a(b(a(x1))) -> b(a(b(b(a(x1)))))
       Bounds Processor:
        bound: 2
        enrichment: match
        automaton:
         final states: {2,1}
         transitions:
          b1(25) -> 26*
          b1(22) -> 23*
          b1(7) -> 8*
          b1(4) -> 5*
          b1(46) -> 47*
          b1(26) -> 27*
          b1(6) -> 7*
          b1(88) -> 89*
          b1(28) -> 29*
          a1(5) -> 6*
          a1(27) -> 28*
          a1(24) -> 25*
          a1(36) -> 37*
          a1(8) -> 9*
          b2(50) -> 51*
          b2(40) -> 41*
          b2(92) -> 93*
          b2(62) -> 63*
          b2(104) -> 105*
          b2(94) -> 95*
          b2(74) -> 75*
          b2(64) -> 65*
          b2(86) -> 87*
          b2(76) -> 77*
          b2(61) -> 62*
          b2(51) -> 52*
          b2(41) -> 42*
          b2(78) -> 79*
          b2(73) -> 74*
          b2(48) -> 49*
          b2(38) -> 39*
          a0(2) -> 1*
          a0(1) -> 1*
          a2(75) -> 76*
          a2(60) -> 61*
          a2(72) -> 73*
          a2(52) -> 53*
          a2(42) -> 43*
          a2(49) -> 50*
          a2(39) -> 40*
          a2(63) -> 64*
          a2(100) -> 101*
          b0(2) -> 2*
          b0(1) -> 2*
          1 -> 36,22
          2 -> 24,4
          5 -> 100,86
          7 -> 1*
          8 -> 72,48,46
          9 -> 6,25,1
          23 -> 5*
          27 -> 60,38
          29 -> 101,61,6,25,1
          37 -> 25*
          42 -> 92,88
          43 -> 104,1,37
          47 -> 5*
          52 -> 78*
          53 -> 101,61,94,37,6
          65 -> 37*
          77 -> 101,61,37,6
          79 -> 39*
          87 -> 39*
          89 -> 5*
          93 -> 49*
          95 -> 62*
          101 -> 61*
          105 -> 74*
        problem:
         
        Qed