YES

Problem:
 a(a(b(x1))) -> c(d(x1))
 b(e(b(x1))) -> e(d(x1))
 b(d(x1)) -> e(b(x1))
 b(b(b(x1))) -> e(e(x1))
 e(e(e(x1))) -> d(e(x1))
 d(x1) -> b(e(x1))
 c(d(a(x1))) -> c(x1)
 d(c(x1)) -> c(d(a(x1)))
 a(x1) -> e(b(x1))

Proof:
 String Reversal Processor:
  b(a(a(x1))) -> d(c(x1))
  b(e(b(x1))) -> d(e(x1))
  d(b(x1)) -> b(e(x1))
  b(b(b(x1))) -> e(e(x1))
  e(e(e(x1))) -> e(d(x1))
  d(x1) -> e(b(x1))
  a(d(c(x1))) -> c(x1)
  c(d(x1)) -> a(d(c(x1)))
  a(x1) -> b(e(x1))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
              [1 0 0]  
    [e](x0) = [0 0 0]x0
              [0 0 0]  ,
    
              [1 0 0]     [0]
    [c](x0) = [0 0 0]x0 + [1]
              [0 0 0]     [1],
    
              [1 0 0]     [0]
    [d](x0) = [0 0 0]x0 + [0]
              [0 0 0]     [1],
    
              [1 1 0]     [0]
    [a](x0) = [0 0 0]x0 + [1]
              [0 0 0]     [1],
    
              [1 0 0]     [0]
    [b](x0) = [0 0 1]x0 + [0]
              [0 1 0]     [1]
   orientation:
                  [1 1 0]     [1]    [1 0 0]     [0]           
    b(a(a(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = d(c(x1))
                  [0 0 0]     [2]    [0 0 0]     [1]           
    
                  [1 0 0]     [0]    [1 0 0]     [0]           
    b(e(b(x1))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = d(e(x1))
                  [0 0 0]     [1]    [0 0 0]     [1]           
    
               [1 0 0]     [0]    [1 0 0]     [0]           
    d(b(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = b(e(x1))
               [0 0 0]     [1]    [0 0 0]     [1]           
    
                  [1 0 0]     [0]    [1 0 0]             
    b(b(b(x1))) = [0 0 1]x1 + [1] >= [0 0 0]x1 = e(e(x1))
                  [0 1 0]     [2]    [0 0 0]             
    
                  [1 0 0]      [1 0 0]             
    e(e(e(x1))) = [0 0 0]x1 >= [0 0 0]x1 = e(d(x1))
                  [0 0 0]      [0 0 0]             
    
            [1 0 0]     [0]    [1 0 0]             
    d(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 = e(b(x1))
            [0 0 0]     [1]    [0 0 0]             
    
                  [1 0 0]     [0]    [1 0 0]     [0]        
    a(d(c(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = c(x1)
                  [0 0 0]     [1]    [0 0 0]     [1]        
    
               [1 0 0]     [0]    [1 0 0]     [0]              
    c(d(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = a(d(c(x1)))
               [0 0 0]     [1]    [0 0 0]     [1]              
    
            [1 1 0]     [0]    [1 0 0]     [0]           
    a(x1) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = b(e(x1))
            [0 0 0]     [1]    [0 0 0]     [1]           
   problem:
    b(e(b(x1))) -> d(e(x1))
    d(b(x1)) -> b(e(x1))
    b(b(b(x1))) -> e(e(x1))
    e(e(e(x1))) -> e(d(x1))
    d(x1) -> e(b(x1))
    a(d(c(x1))) -> c(x1)
    c(d(x1)) -> a(d(c(x1)))
    a(x1) -> b(e(x1))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [e](x0) = x0 + 2,
     
     [c](x0) = 4x0 + 4,
     
     [d](x0) = x0 + 4,
     
     [a](x0) = x0 + 4,
     
     [b](x0) = x0 + 2
    orientation:
     b(e(b(x1))) = x1 + 6 >= x1 + 6 = d(e(x1))
     
     d(b(x1)) = x1 + 6 >= x1 + 4 = b(e(x1))
     
     b(b(b(x1))) = x1 + 6 >= x1 + 4 = e(e(x1))
     
     e(e(e(x1))) = x1 + 6 >= x1 + 6 = e(d(x1))
     
     d(x1) = x1 + 4 >= x1 + 4 = e(b(x1))
     
     a(d(c(x1))) = 4x1 + 12 >= 4x1 + 4 = c(x1)
     
     c(d(x1)) = 4x1 + 20 >= 4x1 + 12 = a(d(c(x1)))
     
     a(x1) = x1 + 4 >= x1 + 4 = b(e(x1))
    problem:
     b(e(b(x1))) -> d(e(x1))
     e(e(e(x1))) -> e(d(x1))
     d(x1) -> e(b(x1))
     a(x1) -> b(e(x1))
    Arctic Interpretation Processor:
     dimension: 2
     interpretation:
                [0 0]  
      [e](x0) = [0 1]x0,
      
                [1 1]  
      [d](x0) = [1 2]x0,
      
                [2 2]  
      [a](x0) = [2 3]x0,
      
                [1 0]  
      [b](x0) = [0 1]x0
     orientation:
                    [2 2]      [1 2]             
      b(e(b(x1))) = [2 3]x1 >= [2 3]x1 = d(e(x1))
      
                    [1 2]      [1 2]             
      e(e(e(x1))) = [2 3]x1 >= [2 3]x1 = e(d(x1))
      
              [1 1]      [1 1]             
      d(x1) = [1 2]x1 >= [1 2]x1 = e(b(x1))
      
              [2 2]      [1 1]             
      a(x1) = [2 3]x1 >= [1 2]x1 = b(e(x1))
     problem:
      b(e(b(x1))) -> d(e(x1))
      e(e(e(x1))) -> e(d(x1))
      d(x1) -> e(b(x1))
     String Reversal Processor:
      b(e(b(x1))) -> e(d(x1))
      e(e(e(x1))) -> d(e(x1))
      d(x1) -> b(e(x1))
      DP Processor:
       DPs:
        b#(e(b(x1))) -> d#(x1)
        b#(e(b(x1))) -> e#(d(x1))
        e#(e(e(x1))) -> d#(e(x1))
        d#(x1) -> e#(x1)
        d#(x1) -> b#(e(x1))
       TRS:
        b(e(b(x1))) -> e(d(x1))
        e(e(e(x1))) -> d(e(x1))
        d(x1) -> b(e(x1))
       TDG Processor:
        DPs:
         b#(e(b(x1))) -> d#(x1)
         b#(e(b(x1))) -> e#(d(x1))
         e#(e(e(x1))) -> d#(e(x1))
         d#(x1) -> e#(x1)
         d#(x1) -> b#(e(x1))
        TRS:
         b(e(b(x1))) -> e(d(x1))
         e(e(e(x1))) -> d(e(x1))
         d(x1) -> b(e(x1))
        graph:
         e#(e(e(x1))) -> d#(e(x1)) -> d#(x1) -> b#(e(x1))
         e#(e(e(x1))) -> d#(e(x1)) -> d#(x1) -> e#(x1)
         d#(x1) -> e#(x1) -> e#(e(e(x1))) -> d#(e(x1))
         d#(x1) -> b#(e(x1)) -> b#(e(b(x1))) -> e#(d(x1))
         d#(x1) -> b#(e(x1)) -> b#(e(b(x1))) -> d#(x1)
         b#(e(b(x1))) -> e#(d(x1)) -> e#(e(e(x1))) -> d#(e(x1))
         b#(e(b(x1))) -> d#(x1) -> d#(x1) -> b#(e(x1))
         b#(e(b(x1))) -> d#(x1) -> d#(x1) -> e#(x1)
        Arctic Interpretation Processor:
         dimension: 1
         interpretation:
          [e#](x0) = -2x0 + 0,
          
          [d#](x0) = x0 + 1,
          
          [b#](x0) = -2x0 + 0,
          
          [e](x0) = 2x0 + 1,
          
          [d](x0) = 4x0 + 3,
          
          [b](x0) = 2x0 + 1
         orientation:
          b#(e(b(x1))) = 2x1 + 1 >= x1 + 1 = d#(x1)
          
          b#(e(b(x1))) = 2x1 + 1 >= 2x1 + 1 = e#(d(x1))
          
          e#(e(e(x1))) = 2x1 + 1 >= 2x1 + 1 = d#(e(x1))
          
          d#(x1) = x1 + 1 >= -2x1 + 0 = e#(x1)
          
          d#(x1) = x1 + 1 >= x1 + 0 = b#(e(x1))
          
          b(e(b(x1))) = 6x1 + 5 >= 6x1 + 5 = e(d(x1))
          
          e(e(e(x1))) = 6x1 + 5 >= 6x1 + 5 = d(e(x1))
          
          d(x1) = 4x1 + 3 >= 4x1 + 3 = b(e(x1))
         problem:
          DPs:
           b#(e(b(x1))) -> d#(x1)
           b#(e(b(x1))) -> e#(d(x1))
           e#(e(e(x1))) -> d#(e(x1))
           d#(x1) -> b#(e(x1))
          TRS:
           b(e(b(x1))) -> e(d(x1))
           e(e(e(x1))) -> d(e(x1))
           d(x1) -> b(e(x1))
         EDG Processor:
          DPs:
           b#(e(b(x1))) -> d#(x1)
           b#(e(b(x1))) -> e#(d(x1))
           e#(e(e(x1))) -> d#(e(x1))
           d#(x1) -> b#(e(x1))
          TRS:
           b(e(b(x1))) -> e(d(x1))
           e(e(e(x1))) -> d(e(x1))
           d(x1) -> b(e(x1))
          graph:
           e#(e(e(x1))) -> d#(e(x1)) -> d#(x1) -> b#(e(x1))
           d#(x1) -> b#(e(x1)) -> b#(e(b(x1))) -> d#(x1)
           d#(x1) -> b#(e(x1)) -> b#(e(b(x1))) -> e#(d(x1))
           b#(e(b(x1))) -> e#(d(x1)) -> e#(e(e(x1))) -> d#(e(x1))
           b#(e(b(x1))) -> d#(x1) -> d#(x1) -> b#(e(x1))
          Arctic Interpretation Processor:
           dimension: 1
           interpretation:
            [e#](x0) = x0,
            
            [d#](x0) = 2x0,
            
            [b#](x0) = x0,
            
            [e](x0) = 2x0,
            
            [d](x0) = 4x0,
            
            [b](x0) = 2x0
           orientation:
            b#(e(b(x1))) = 4x1 >= 2x1 = d#(x1)
            
            b#(e(b(x1))) = 4x1 >= 4x1 = e#(d(x1))
            
            e#(e(e(x1))) = 4x1 >= 4x1 = d#(e(x1))
            
            d#(x1) = 2x1 >= 2x1 = b#(e(x1))
            
            b(e(b(x1))) = 6x1 >= 6x1 = e(d(x1))
            
            e(e(e(x1))) = 6x1 >= 6x1 = d(e(x1))
            
            d(x1) = 4x1 >= 4x1 = b(e(x1))
           problem:
            DPs:
             b#(e(b(x1))) -> e#(d(x1))
             e#(e(e(x1))) -> d#(e(x1))
             d#(x1) -> b#(e(x1))
            TRS:
             b(e(b(x1))) -> e(d(x1))
             e(e(e(x1))) -> d(e(x1))
             d(x1) -> b(e(x1))
           EDG Processor:
            DPs:
             b#(e(b(x1))) -> e#(d(x1))
             e#(e(e(x1))) -> d#(e(x1))
             d#(x1) -> b#(e(x1))
            TRS:
             b(e(b(x1))) -> e(d(x1))
             e(e(e(x1))) -> d(e(x1))
             d(x1) -> b(e(x1))
            graph:
             e#(e(e(x1))) -> d#(e(x1)) -> d#(x1) -> b#(e(x1))
             d#(x1) -> b#(e(x1)) -> b#(e(b(x1))) -> e#(d(x1))
             b#(e(b(x1))) -> e#(d(x1)) -> e#(e(e(x1))) -> d#(e(x1))
            Arctic Interpretation Processor:
             dimension: 3
             interpretation:
              [e#](x0) = [1 1 0]x0 + [0],
              
              [d#](x0) = [1 1 1]x0 + [1],
              
              [b#](x0) = [0 1 1]x0 + [0],
              
                        [1  0  0 ]     [1 ]
              [e](x0) = [-& -& 0 ]x0 + [-&]
                        [0  -& -&]     [0 ],
              
                        [0 0 1]     [0]
              [d](x0) = [0 0 1]x0 + [0]
                        [1 0 0]     [1],
              
                        [-& 1  0 ]     [0]
              [b](x0) = [-& 1  0 ]x0 + [0]
                        [0  0  1 ]     [0]
             orientation:
              b#(e(b(x1))) = [1 2 2]x1 + [1] >= [1 1 2]x1 + [1] = e#(d(x1))
              
              e#(e(e(x1))) = [3 2 2]x1 + [3] >= [2 1 1]x1 + [2] = d#(e(x1))
              
              d#(x1) = [1 1 1]x1 + [1] >= [1 0 1]x1 + [1] = b#(e(x1))
              
                            [1 1 2]     [1]    [1 1 2]     [1]           
              b(e(b(x1))) = [1 1 2]x1 + [1] >= [1 0 0]x1 + [1] = e(d(x1))
                            [0 2 1]     [1]    [0 0 1]     [0]           
              
                            [3 2 2]     [3]    [1 0 0]     [1]           
              e(e(e(x1))) = [1 0 0]x1 + [1] >= [1 0 0]x1 + [1] = d(e(x1))
                            [2 1 1]     [2]    [2 1 1]     [2]           
              
                      [0 0 1]     [0]    [0  -& 1 ]     [0]           
              d(x1) = [0 0 1]x1 + [0] >= [0  -& 1 ]x1 + [0] = b(e(x1))
                      [1 0 0]     [1]    [1  0  0 ]     [1]           
             problem:
              DPs:
               b#(e(b(x1))) -> e#(d(x1))
               d#(x1) -> b#(e(x1))
              TRS:
               b(e(b(x1))) -> e(d(x1))
               e(e(e(x1))) -> d(e(x1))
               d(x1) -> b(e(x1))
             EDG Processor:
              DPs:
               b#(e(b(x1))) -> e#(d(x1))
               d#(x1) -> b#(e(x1))
              TRS:
               b(e(b(x1))) -> e(d(x1))
               e(e(e(x1))) -> d(e(x1))
               d(x1) -> b(e(x1))
              graph:
               d#(x1) -> b#(e(x1)) -> b#(e(b(x1))) -> e#(d(x1))
              SCC Processor:
               #sccs: 0
               #rules: 0
               #arcs: 1/4