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:
 DP Processor:
  DPs:
   r1#(a(x1)) -> r1#(x1)
   r1#(a(x1)) -> a#(r1(x1))
   r1#(a(x1)) -> a#(a(r1(x1)))
   r1#(a(x1)) -> a#(a(a(r1(x1))))
   r2#(a(x1)) -> r2#(x1)
   r2#(a(x1)) -> a#(r2(x1))
   r2#(a(x1)) -> a#(a(r2(x1)))
   r2#(a(x1)) -> a#(a(a(r2(x1))))
   a#(l1(x1)) -> a#(x1)
   a#(l1(x1)) -> a#(a(x1))
   a#(l1(x1)) -> a#(a(a(x1)))
   a#(a(l2(x1))) -> a#(x1)
   a#(a(l2(x1))) -> a#(a(x1))
   r2#(b(x1)) -> a#(b(x1))
   b#(l1(x1)) -> r2#(x1)
   b#(l1(x1)) -> b#(r2(x1))
   b#(l2(x1)) -> r1#(x1)
   b#(l2(x1)) -> b#(r1(x1))
  TRS:
   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
  TDG Processor:
   DPs:
    r1#(a(x1)) -> r1#(x1)
    r1#(a(x1)) -> a#(r1(x1))
    r1#(a(x1)) -> a#(a(r1(x1)))
    r1#(a(x1)) -> a#(a(a(r1(x1))))
    r2#(a(x1)) -> r2#(x1)
    r2#(a(x1)) -> a#(r2(x1))
    r2#(a(x1)) -> a#(a(r2(x1)))
    r2#(a(x1)) -> a#(a(a(r2(x1))))
    a#(l1(x1)) -> a#(x1)
    a#(l1(x1)) -> a#(a(x1))
    a#(l1(x1)) -> a#(a(a(x1)))
    a#(a(l2(x1))) -> a#(x1)
    a#(a(l2(x1))) -> a#(a(x1))
    r2#(b(x1)) -> a#(b(x1))
    b#(l1(x1)) -> r2#(x1)
    b#(l1(x1)) -> b#(r2(x1))
    b#(l2(x1)) -> r1#(x1)
    b#(l2(x1)) -> b#(r1(x1))
   TRS:
    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
   graph:
    b#(l2(x1)) -> b#(r1(x1)) -> b#(l2(x1)) -> b#(r1(x1))
    b#(l2(x1)) -> b#(r1(x1)) -> b#(l2(x1)) -> r1#(x1)
    b#(l2(x1)) -> b#(r1(x1)) -> b#(l1(x1)) -> b#(r2(x1))
    b#(l2(x1)) -> b#(r1(x1)) -> b#(l1(x1)) -> r2#(x1)
    b#(l2(x1)) -> r1#(x1) -> r1#(a(x1)) -> a#(a(a(r1(x1))))
    b#(l2(x1)) -> r1#(x1) -> r1#(a(x1)) -> a#(a(r1(x1)))
    b#(l2(x1)) -> r1#(x1) -> r1#(a(x1)) -> a#(r1(x1))
    b#(l2(x1)) -> r1#(x1) -> r1#(a(x1)) -> r1#(x1)
    b#(l1(x1)) -> b#(r2(x1)) -> b#(l2(x1)) -> b#(r1(x1))
    b#(l1(x1)) -> b#(r2(x1)) -> b#(l2(x1)) -> r1#(x1)
    b#(l1(x1)) -> b#(r2(x1)) -> b#(l1(x1)) -> b#(r2(x1))
    b#(l1(x1)) -> b#(r2(x1)) -> b#(l1(x1)) -> r2#(x1)
    b#(l1(x1)) -> r2#(x1) -> r2#(b(x1)) -> a#(b(x1))
    b#(l1(x1)) -> r2#(x1) -> r2#(a(x1)) -> a#(a(a(r2(x1))))
    b#(l1(x1)) -> r2#(x1) -> r2#(a(x1)) -> a#(a(r2(x1)))
    b#(l1(x1)) -> r2#(x1) -> r2#(a(x1)) -> a#(r2(x1))
    b#(l1(x1)) -> r2#(x1) -> r2#(a(x1)) -> r2#(x1)
    r2#(b(x1)) -> a#(b(x1)) -> a#(a(l2(x1))) -> a#(a(x1))
    r2#(b(x1)) -> a#(b(x1)) -> a#(a(l2(x1))) -> a#(x1)
    r2#(b(x1)) -> a#(b(x1)) -> a#(l1(x1)) -> a#(a(a(x1)))
    r2#(b(x1)) -> a#(b(x1)) -> a#(l1(x1)) -> a#(a(x1))
    r2#(b(x1)) -> a#(b(x1)) -> a#(l1(x1)) -> a#(x1)
    r2#(a(x1)) -> r2#(x1) -> r2#(b(x1)) -> a#(b(x1))
    r2#(a(x1)) -> r2#(x1) -> r2#(a(x1)) -> a#(a(a(r2(x1))))
    r2#(a(x1)) -> r2#(x1) -> r2#(a(x1)) -> a#(a(r2(x1)))
    r2#(a(x1)) -> r2#(x1) -> r2#(a(x1)) -> a#(r2(x1))
    r2#(a(x1)) -> r2#(x1) -> r2#(a(x1)) -> r2#(x1)
    r2#(a(x1)) -> a#(r2(x1)) -> a#(a(l2(x1))) -> a#(a(x1))
    r2#(a(x1)) -> a#(r2(x1)) -> a#(a(l2(x1))) -> a#(x1)
    r2#(a(x1)) -> a#(r2(x1)) -> a#(l1(x1)) -> a#(a(a(x1)))
    r2#(a(x1)) -> a#(r2(x1)) -> a#(l1(x1)) -> a#(a(x1))
    r2#(a(x1)) -> a#(r2(x1)) -> a#(l1(x1)) -> a#(x1)
    r2#(a(x1)) -> a#(a(r2(x1))) -> a#(a(l2(x1))) -> a#(a(x1))
    r2#(a(x1)) -> a#(a(r2(x1))) -> a#(a(l2(x1))) -> a#(x1)
    r2#(a(x1)) -> a#(a(r2(x1))) -> a#(l1(x1)) -> a#(a(a(x1)))
    r2#(a(x1)) -> a#(a(r2(x1))) -> a#(l1(x1)) -> a#(a(x1))
    r2#(a(x1)) -> a#(a(r2(x1))) -> a#(l1(x1)) -> a#(x1)
    r2#(a(x1)) -> a#(a(a(r2(x1)))) -> a#(a(l2(x1))) -> a#(a(x1))
    r2#(a(x1)) -> a#(a(a(r2(x1)))) -> a#(a(l2(x1))) -> a#(x1)
    r2#(a(x1)) -> a#(a(a(r2(x1)))) -> a#(l1(x1)) -> a#(a(a(x1)))
    r2#(a(x1)) -> a#(a(a(r2(x1)))) -> a#(l1(x1)) -> a#(a(x1))
    r2#(a(x1)) -> a#(a(a(r2(x1)))) -> a#(l1(x1)) -> a#(x1)
    a#(l1(x1)) -> a#(a(a(x1))) -> a#(a(l2(x1))) -> a#(a(x1))
    a#(l1(x1)) -> a#(a(a(x1))) -> a#(a(l2(x1))) -> a#(x1)
    a#(l1(x1)) -> a#(a(a(x1))) -> a#(l1(x1)) -> a#(a(a(x1)))
    a#(l1(x1)) -> a#(a(a(x1))) -> a#(l1(x1)) -> a#(a(x1))
    a#(l1(x1)) -> a#(a(a(x1))) -> a#(l1(x1)) -> a#(x1)
    a#(l1(x1)) -> a#(a(x1)) -> a#(a(l2(x1))) -> a#(a(x1))
    a#(l1(x1)) -> a#(a(x1)) -> a#(a(l2(x1))) -> a#(x1)
    a#(l1(x1)) -> a#(a(x1)) -> a#(l1(x1)) -> a#(a(a(x1)))
    a#(l1(x1)) -> a#(a(x1)) -> a#(l1(x1)) -> a#(a(x1))
    a#(l1(x1)) -> a#(a(x1)) -> a#(l1(x1)) -> a#(x1)
    a#(l1(x1)) -> a#(x1) -> a#(a(l2(x1))) -> a#(a(x1))
    a#(l1(x1)) -> a#(x1) -> a#(a(l2(x1))) -> a#(x1)
    a#(l1(x1)) -> a#(x1) -> a#(l1(x1)) -> a#(a(a(x1)))
    a#(l1(x1)) -> a#(x1) -> a#(l1(x1)) -> a#(a(x1))
    a#(l1(x1)) -> a#(x1) -> a#(l1(x1)) -> a#(x1)
    a#(a(l2(x1))) -> a#(a(x1)) -> a#(a(l2(x1))) -> a#(a(x1))
    a#(a(l2(x1))) -> a#(a(x1)) -> a#(a(l2(x1))) -> a#(x1)
    a#(a(l2(x1))) -> a#(a(x1)) -> a#(l1(x1)) -> a#(a(a(x1)))
    a#(a(l2(x1))) -> a#(a(x1)) -> a#(l1(x1)) -> a#(a(x1))
    a#(a(l2(x1))) -> a#(a(x1)) -> a#(l1(x1)) -> a#(x1)
    a#(a(l2(x1))) -> a#(x1) -> a#(a(l2(x1))) -> a#(a(x1))
    a#(a(l2(x1))) -> a#(x1) -> a#(a(l2(x1))) -> a#(x1)
    a#(a(l2(x1))) -> a#(x1) -> a#(l1(x1)) -> a#(a(a(x1)))
    a#(a(l2(x1))) -> a#(x1) -> a#(l1(x1)) -> a#(a(x1))
    a#(a(l2(x1))) -> a#(x1) -> a#(l1(x1)) -> a#(x1)
    r1#(a(x1)) -> a#(r1(x1)) -> a#(a(l2(x1))) -> a#(a(x1))
    r1#(a(x1)) -> a#(r1(x1)) -> a#(a(l2(x1))) -> a#(x1)
    r1#(a(x1)) -> a#(r1(x1)) -> a#(l1(x1)) -> a#(a(a(x1)))
    r1#(a(x1)) -> a#(r1(x1)) -> a#(l1(x1)) -> a#(a(x1))
    r1#(a(x1)) -> a#(r1(x1)) -> a#(l1(x1)) -> a#(x1)
    r1#(a(x1)) -> a#(a(r1(x1))) -> a#(a(l2(x1))) -> a#(a(x1))
    r1#(a(x1)) -> a#(a(r1(x1))) -> a#(a(l2(x1))) -> a#(x1)
    r1#(a(x1)) -> a#(a(r1(x1))) -> a#(l1(x1)) -> a#(a(a(x1)))
    r1#(a(x1)) -> a#(a(r1(x1))) -> a#(l1(x1)) -> a#(a(x1))
    r1#(a(x1)) -> a#(a(r1(x1))) -> a#(l1(x1)) -> a#(x1)
    r1#(a(x1)) -> a#(a(a(r1(x1)))) -> a#(a(l2(x1))) -> a#(a(x1))
    r1#(a(x1)) -> a#(a(a(r1(x1)))) -> a#(a(l2(x1))) -> a#(x1)
    r1#(a(x1)) -> a#(a(a(r1(x1)))) -> a#(l1(x1)) -> a#(a(a(x1)))
    r1#(a(x1)) -> a#(a(a(r1(x1)))) -> a#(l1(x1)) -> a#(a(x1))
    r1#(a(x1)) -> a#(a(a(r1(x1)))) -> a#(l1(x1)) -> a#(x1)
    r1#(a(x1)) -> r1#(x1) -> r1#(a(x1)) -> a#(a(a(r1(x1))))
    r1#(a(x1)) -> r1#(x1) -> r1#(a(x1)) -> a#(a(r1(x1)))
    r1#(a(x1)) -> r1#(x1) -> r1#(a(x1)) -> a#(r1(x1))
    r1#(a(x1)) -> r1#(x1) -> r1#(a(x1)) -> r1#(x1)
   SCC Processor:
    #sccs: 4
    #rules: 9
    #arcs: 86/324
    DPs:
     b#(l2(x1)) -> b#(r1(x1))
     b#(l1(x1)) -> b#(r2(x1))
    TRS:
     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
    Matrix Interpretation Processor: dim=2
     
     interpretation:
      [b#](x0) = [2 0]x0,
      
                [4]
      [b](x0) = [0],
      
                 [1 0]     [3]
      [l2](x0) = [0 0]x0 + [0],
      
                      [1]
      [l1](x0) = x0 + [1],
      
                   
      [r2](x0) = x0,
      
                      [2]
      [r1](x0) = x0 + [2],
      
                [0 1]  
      [a](x0) = [1 0]x0
     orientation:
      b#(l2(x1)) = [2 0]x1 + [6] >= [2 0]x1 + [4] = b#(r1(x1))
      
      b#(l1(x1)) = [2 0]x1 + [2] >= [2 0]x1 = b#(r2(x1))
      
                  [0 1]     [2]    [0 1]     [2]                  
      r1(a(x1)) = [1 0]x1 + [2] >= [1 0]x1 + [2] = a(a(a(r1(x1))))
      
                  [0 1]      [0 1]                    
      r2(a(x1)) = [1 0]x1 >= [1 0]x1 = a(a(a(r2(x1))))
      
                  [0 1]     [1]    [0 1]     [1]                  
      a(l1(x1)) = [1 0]x1 + [1] >= [1 0]x1 + [1] = l1(a(a(a(x1))))
      
                     [1 0]     [3]    [1 0]     [3]               
      a(a(l2(x1))) = [0 0]x1 + [0] >= [0 0]x1 + [0] = l2(a(a(x1)))
      
                  [6]    [5]            
      r1(b(x1)) = [2] >= [1] = l1(b(x1))
      
                  [4]    [3]               
      r2(b(x1)) = [0] >= [0] = l2(a(b(x1)))
      
                  [4]    [4]            
      b(l1(x1)) = [0] >= [0] = b(r2(x1))
      
                  [4]    [4]            
      b(l2(x1)) = [0] >= [0] = b(r1(x1))
      
                              
      a(a(x1)) = x1 >= x1 = x1
     problem:
      DPs:
       
      TRS:
       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
     Qed
    
    DPs:
     r1#(a(x1)) -> r1#(x1)
    TRS:
     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
    LPO Processor:
     argument filtering:
      pi(a) = [0]
      pi(r1) = [0]
      pi(r2) = [0]
      pi(l1) = []
      pi(l2) = []
      pi(b) = []
      pi(r1#) = 0
     precedence:
      r1 > b > r2 > r1# ~ l2 ~ l1 ~ a
     problem:
      DPs:
       
      TRS:
       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
     Qed
    
    DPs:
     r2#(a(x1)) -> r2#(x1)
    TRS:
     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
    LPO Processor:
     argument filtering:
      pi(a) = [0]
      pi(r1) = [0]
      pi(r2) = [0]
      pi(l1) = []
      pi(l2) = []
      pi(b) = []
      pi(r2#) = 0
     precedence:
      r1 > b > r2 > r2# ~ l2 ~ l1 ~ a
     problem:
      DPs:
       
      TRS:
       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
     Qed
   
   DPs:
    a#(l1(x1)) -> a#(x1)
    a#(l1(x1)) -> a#(a(x1))
    a#(l1(x1)) -> a#(a(a(x1)))
    a#(a(l2(x1))) -> a#(x1)
    a#(a(l2(x1))) -> a#(a(x1))
   TRS:
    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
   Matrix Interpretation Processor: dim=3
    
    interpretation:
     [a#](x0) = [0 0 1]x0 + [1],
     
               [0]
     [b](x0) = [1]
               [1],
     
                [0 0 1]     [0]
     [l2](x0) = [0 0 1]x0 + [0]
                [0 0 1]     [1],
     
                [0 0 0]     [0]
     [l1](x0) = [0 0 0]x0 + [0]
                [0 0 1]     [1],
     
                [0 0 0]     [1]
     [r2](x0) = [0 1 1]x0 + [0]
                [0 1 1]     [0],
     
                [0 0 0]  
     [r1](x0) = [0 1 0]x0
                [0 1 1]  ,
     
                 
     [a](x0) = x0
                 
    orientation:
     a#(l1(x1)) = [0 0 1]x1 + [2] >= [0 0 1]x1 + [1] = a#(x1)
     
     a#(l1(x1)) = [0 0 1]x1 + [2] >= [0 0 1]x1 + [1] = a#(a(x1))
     
     a#(l1(x1)) = [0 0 1]x1 + [2] >= [0 0 1]x1 + [1] = a#(a(a(x1)))
     
     a#(a(l2(x1))) = [0 0 1]x1 + [2] >= [0 0 1]x1 + [1] = a#(x1)
     
     a#(a(l2(x1))) = [0 0 1]x1 + [2] >= [0 0 1]x1 + [1] = a#(a(x1))
     
                 [0 0 0]      [0 0 0]                    
     r1(a(x1)) = [0 1 0]x1 >= [0 1 0]x1 = a(a(a(r1(x1))))
                 [0 1 1]      [0 1 1]                    
     
                 [0 0 0]     [1]    [0 0 0]     [1]                  
     r2(a(x1)) = [0 1 1]x1 + [0] >= [0 1 1]x1 + [0] = a(a(a(r2(x1))))
                 [0 1 1]     [0]    [0 1 1]     [0]                  
     
                 [0 0 0]     [0]    [0 0 0]     [0]                  
     a(l1(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = l1(a(a(a(x1))))
                 [0 0 1]     [1]    [0 0 1]     [1]                  
     
                    [0 0 1]     [0]    [0 0 1]     [0]               
     a(a(l2(x1))) = [0 0 1]x1 + [0] >= [0 0 1]x1 + [0] = l2(a(a(x1)))
                    [0 0 1]     [1]    [0 0 1]     [1]               
     
                 [0]    [0]            
     r1(b(x1)) = [1] >= [0] = l1(b(x1))
                 [2]    [2]            
     
                 [1]    [1]               
     r2(b(x1)) = [2] >= [1] = l2(a(b(x1)))
                 [2]    [2]               
     
                 [0]    [0]            
     b(l1(x1)) = [1] >= [1] = b(r2(x1))
                 [1]    [1]            
     
                 [0]    [0]            
     b(l2(x1)) = [1] >= [1] = b(r1(x1))
                 [1]    [1]            
     
                             
     a(a(x1)) = x1 >= x1 = x1
                             
    problem:
     DPs:
      
     TRS:
      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
    Qed