YES

Problem:
 r1(a(x1)) -> a(a(a(r1(x1))))
 r2(a(x1)) -> a(a(a(r2(x1))))
 a(l1(x1)) -> l1(a(a(a(x1))))
 a(a(l2(x1))) -> l2(a(a(x1)))
 r1(b(x1)) -> l1(b(x1))
 r2(b(x1)) -> l2(a(b(x1)))
 b(l1(x1)) -> b(r2(x1))
 b(l2(x1)) -> b(r1(x1))
 a(a(x1)) -> x1

Proof:
 String Reversal Processor:
  a(r1(x1)) -> r1(a(a(a(x1))))
  a(r2(x1)) -> r2(a(a(a(x1))))
  l1(a(x1)) -> a(a(a(l1(x1))))
  l2(a(a(x1))) -> a(a(l2(x1)))
  b(r1(x1)) -> b(l1(x1))
  b(r2(x1)) -> b(a(l2(x1)))
  l1(b(x1)) -> r2(b(x1))
  l2(b(x1)) -> r1(b(x1))
  a(a(x1)) -> x1
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 1 0]     [0]
    [b](x0) = [0 0 0]x0 + [0]
              [0 0 0]     [1],
    
               [1 0 1]  
    [l2](x0) = [0 1 1]x0
               [0 0 0]  ,
    
               [1 0 0]  
    [l1](x0) = [0 0 1]x0
               [0 1 0]  ,
    
               [1 0 0]  
    [r2](x0) = [0 0 1]x0
               [0 1 0]  ,
    
               [1 0 0]     [1]
    [r1](x0) = [0 0 1]x0 + [0]
               [0 1 0]     [0],
    
              [1 0 0]  
    [a](x0) = [0 0 1]x0
              [0 1 0]  
   orientation:
                     [1]         [1]                  
    a(r1(x1)) = x1 + [0] >= x1 + [0] = r1(a(a(a(x1))))
                     [0]         [0]                  
    
                                          
    a(r2(x1)) = x1 >= x1 = r2(a(a(a(x1))))
                                          
    
                                          
    l1(a(x1)) = x1 >= x1 = a(a(a(l1(x1))))
                                          
    
                   [1 0 1]      [1 0 1]                 
    l2(a(a(x1))) = [0 1 1]x1 >= [0 1 1]x1 = a(a(l2(x1)))
                   [0 0 0]      [0 0 0]                 
    
                [1 0 1]     [1]    [1 0 1]     [0]            
    b(r1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(l1(x1))
                [0 0 0]     [1]    [0 0 0]     [1]            
    
                [1 0 1]     [0]    [1 0 1]     [0]               
    b(r2(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(a(l2(x1)))
                [0 0 0]     [1]    [0 0 0]     [1]               
    
                [1 1 0]     [0]    [1 1 0]     [0]            
    l1(b(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r2(b(x1))
                [0 0 0]     [0]    [0 0 0]     [0]            
    
                [1 1 0]     [1]    [1 1 0]     [1]            
    l2(b(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = r1(b(x1))
                [0 0 0]     [0]    [0 0 0]     [0]            
    
                            
    a(a(x1)) = x1 >= x1 = x1
                            
   problem:
    a(r1(x1)) -> r1(a(a(a(x1))))
    a(r2(x1)) -> r2(a(a(a(x1))))
    l1(a(x1)) -> a(a(a(l1(x1))))
    l2(a(a(x1))) -> a(a(l2(x1)))
    b(r2(x1)) -> b(a(l2(x1)))
    l1(b(x1)) -> r2(b(x1))
    l2(b(x1)) -> r1(b(x1))
    a(a(x1)) -> x1
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [b](x0) = x0,
     
     [l2](x0) = 2x0,
     
     [l1](x0) = 5x0,
     
     [r2](x0) = 2x0,
     
     [r1](x0) = x0,
     
     [a](x0) = x0
    orientation:
     a(r1(x1)) = x1 >= x1 = r1(a(a(a(x1))))
     
     a(r2(x1)) = 2x1 >= 2x1 = r2(a(a(a(x1))))
     
     l1(a(x1)) = 5x1 >= 5x1 = a(a(a(l1(x1))))
     
     l2(a(a(x1))) = 2x1 >= 2x1 = a(a(l2(x1)))
     
     b(r2(x1)) = 2x1 >= 2x1 = b(a(l2(x1)))
     
     l1(b(x1)) = 5x1 >= 2x1 = r2(b(x1))
     
     l2(b(x1)) = 2x1 >= x1 = r1(b(x1))
     
     a(a(x1)) = x1 >= x1 = x1
    problem:
     a(r1(x1)) -> r1(a(a(a(x1))))
     a(r2(x1)) -> r2(a(a(a(x1))))
     l1(a(x1)) -> a(a(a(l1(x1))))
     l2(a(a(x1))) -> a(a(l2(x1)))
     b(r2(x1)) -> b(a(l2(x1)))
     a(a(x1)) -> x1
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [b](x0) = x0,
      
      [l2](x0) = x0,
      
      [l1](x0) = 5x0,
      
      [r2](x0) = 8x0,
      
      [r1](x0) = 4x0,
      
      [a](x0) = x0
     orientation:
      a(r1(x1)) = 4x1 >= 4x1 = r1(a(a(a(x1))))
      
      a(r2(x1)) = 8x1 >= 8x1 = r2(a(a(a(x1))))
      
      l1(a(x1)) = 5x1 >= 5x1 = a(a(a(l1(x1))))
      
      l2(a(a(x1))) = x1 >= x1 = a(a(l2(x1)))
      
      b(r2(x1)) = 8x1 >= x1 = b(a(l2(x1)))
      
      a(a(x1)) = x1 >= x1 = x1
     problem:
      a(r1(x1)) -> r1(a(a(a(x1))))
      a(r2(x1)) -> r2(a(a(a(x1))))
      l1(a(x1)) -> a(a(a(l1(x1))))
      l2(a(a(x1))) -> a(a(l2(x1)))
      a(a(x1)) -> x1
     Matrix Interpretation Processor: dim=2
      
      interpretation:
                  [2 2]  
       [l2](x0) = [0 1]x0,
       
                  [1 1]     [0]
       [l1](x0) = [0 3]x0 + [3],
       
                  [1 0]  
       [r2](x0) = [0 0]x0,
       
                  [1 0]  
       [r1](x0) = [1 0]x0,
       
                      [0]
       [a](x0) = x0 + [1]
      orientation:
                   [1 0]     [0]    [1 0]                    
       a(r1(x1)) = [1 0]x1 + [1] >= [1 0]x1 = r1(a(a(a(x1))))
       
                   [1 0]     [0]    [1 0]                    
       a(r2(x1)) = [0 0]x1 + [1] >= [0 0]x1 = r2(a(a(a(x1))))
       
                   [1 1]     [1]    [1 1]     [0]                  
       l1(a(x1)) = [0 3]x1 + [6] >= [0 3]x1 + [6] = a(a(a(l1(x1))))
       
                      [2 2]     [4]    [2 2]     [0]               
       l2(a(a(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = a(a(l2(x1)))
       
                       [0]           
       a(a(x1)) = x1 + [2] >= x1 = x1
      problem:
       a(r1(x1)) -> r1(a(a(a(x1))))
       a(r2(x1)) -> r2(a(a(a(x1))))
       a(a(x1)) -> x1
      KBO Processor:
       weight function:
        w0 = 1
        w(r2) = w(r1) = 1
        w(a) = 0
       precedence:
        a > r2 ~ r1
       problem:
        
       Qed