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))
   String Reversal Processor:
    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))
    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 1 0]x0 + [0]
                [1 0 1]     [1],
      
                [1 0 1]  
      [d](x0) = [0 1 0]x0
                [0 1 1]  ,
      
                [1 0 1]  
      [a](x0) = [0 1 0]x0
                [0 0 0]  ,
      
                [1 0 1]  
      [b](x0) = [0 0 0]x0
                [0 0 0]  
     orientation:
                    [1 0 1]      [1 0 1]             
      b(e(b(x1))) = [0 0 0]x1 >= [0 0 0]x1 = e(d(x1))
                    [0 0 0]      [0 0 0]             
      
                 [1 1 2]      [1 0 1]             
      b(d(x1)) = [0 0 0]x1 >= [0 0 0]x1 = e(b(x1))
                 [0 0 0]      [0 0 0]             
      
                    [1 0 1]      [1 0 0]             
      b(b(b(x1))) = [0 0 0]x1 >= [0 0 0]x1 = e(e(x1))
                    [0 0 0]      [0 0 0]             
      
                    [1 0 0]      [1 0 0]             
      e(e(e(x1))) = [0 0 0]x1 >= [0 0 0]x1 = d(e(x1))
                    [0 0 0]      [0 0 0]             
      
              [1 0 1]      [1 0 0]             
      d(x1) = [0 1 0]x1 >= [0 0 0]x1 = b(e(x1))
              [0 1 1]      [0 0 0]             
      
                    [1 0 1]     [0]    [1 0 0]     [0]        
      c(d(a(x1))) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = c(x1)
                    [1 1 1]     [1]    [1 0 1]     [1]        
      
                 [2 0 1]     [1]    [1 0 1]     [0]              
      d(c(x1)) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = c(d(a(x1)))
                 [1 1 1]     [1]    [1 1 1]     [1]              
      
              [1 0 1]      [1 0 1]             
      a(x1) = [0 1 0]x1 >= [0 0 0]x1 = e(b(x1))
              [0 0 0]      [0 0 0]             
     problem:
      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)
      a(x1) -> e(b(x1))
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [e](x0) = x0,
       
       [c](x0) = x0,
       
       [d](x0) = x0,
       
       [a](x0) = 5x0,
       
       [b](x0) = x0
      orientation:
       b(e(b(x1))) = x1 >= x1 = e(d(x1))
       
       b(d(x1)) = x1 >= x1 = e(b(x1))
       
       b(b(b(x1))) = x1 >= x1 = e(e(x1))
       
       e(e(e(x1))) = x1 >= x1 = d(e(x1))
       
       d(x1) = x1 >= x1 = b(e(x1))
       
       c(d(a(x1))) = 5x1 >= x1 = c(x1)
       
       a(x1) = 5x1 >= x1 = e(b(x1))
      problem:
       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))
      Arctic Interpretation Processor:
       dimension: 2
       interpretation:
                  [0 0]  
        [e](x0) = [1 1]x0,
        
                  [2 1]  
        [d](x0) = [2 2]x0,
        
                  [0 0]  
        [b](x0) = [1 1]x0
       orientation:
                      [2 2]      [2 2]             
        b(e(b(x1))) = [3 3]x1 >= [3 3]x1 = e(d(x1))
        
                   [2 2]      [1 1]             
        b(d(x1)) = [3 3]x1 >= [2 2]x1 = e(b(x1))
        
                      [2 2]      [1 1]             
        b(b(b(x1))) = [3 3]x1 >= [2 2]x1 = e(e(x1))
        
                      [2 2]      [2 2]             
        e(e(e(x1))) = [3 3]x1 >= [3 3]x1 = d(e(x1))
        
                [2 1]      [1 1]             
        d(x1) = [2 2]x1 >= [2 2]x1 = b(e(x1))
       problem:
        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
          usable rules:
           b(e(b(x1))) -> e(d(x1))
           e(e(e(x1))) -> d(e(x1))
           d(x1) -> b(e(x1))
          interpretation:
           [e#](x0) = x0,
           
           [d#](x0) = 1x0 + 1,
           
           [b#](x0) = x0 + 0,
           
           [e](x0) = 1x0 + 1,
           
           [d](x0) = 2x0 + 2,
           
           [b](x0) = 1x0 + 2
          orientation:
           b#(e(b(x1))) = 2x1 + 3 >= 1x1 + 1 = d#(x1)
           
           b#(e(b(x1))) = 2x1 + 3 >= 2x1 + 2 = e#(d(x1))
           
           e#(e(e(x1))) = 2x1 + 2 >= 2x1 + 2 = d#(e(x1))
           
           d#(x1) = 1x1 + 1 >= x1 = e#(x1)
           
           d#(x1) = 1x1 + 1 >= 1x1 + 1 = b#(e(x1))
           
           b(e(b(x1))) = 3x1 + 4 >= 3x1 + 3 = e(d(x1))
           
           e(e(e(x1))) = 3x1 + 3 >= 3x1 + 3 = d(e(x1))
           
           d(x1) = 2x1 + 2 >= 2x1 + 2 = 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))
          Restore Modifier:
           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
             usable rules:
              b(e(b(x1))) -> e(d(x1))
              e(e(e(x1))) -> d(e(x1))
              d(x1) -> b(e(x1))
             interpretation:
              [e#](x0) = [0 1 0]x0 + [0],
              
              [d#](x0) = [0 1 1]x0 + [1],
              
              [b#](x0) = [1 0 1]x0 + [0],
              
                        [-& -& 0 ]     [0]
              [e](x0) = [0  1  0 ]x0 + [1]
                        [-& 0  -&]     [0],
              
                        [0 0 1]     [1]
              [d](x0) = [0 0 1]x0 + [1]
                        [0 1 0]     [1],
              
                        [1  -& 0 ]     [0]
              [b](x0) = [1  -& -&]x0 + [0]
                        [0  0  1 ]     [1]
             orientation:
              b#(e(b(x1))) = [2 1 2]x1 + [2] >= [1 1 2]x1 + [2] = e#(d(x1))
              
              e#(e(e(x1))) = [2 3 2]x1 + [3] >= [1 2 1]x1 + [2] = d#(e(x1))
              
              d#(x1) = [0 1 1]x1 + [1] >= [0 1 1]x1 + [1] = b#(e(x1))
              
                            [1 1 2]     [2]    [0 1 0]     [1]           
              b(e(b(x1))) = [1 1 2]x1 + [2] >= [1 1 2]x1 + [2] = e(d(x1))
                            [2 0 1]     [1]    [0 0 1]     [1]           
              
                            [0 1 0]     [1]    [0 1 0]     [1]           
              e(e(e(x1))) = [2 3 2]x1 + [3] >= [0 1 0]x1 + [1] = d(e(x1))
                            [1 2 1]     [2]    [1 2 1]     [2]           
              
                      [0 0 1]     [1]    [-& 0  1 ]     [1]           
              d(x1) = [0 0 1]x1 + [1] >= [-& -& 1 ]x1 + [1] = b(e(x1))
                      [0 1 0]     [1]    [0  1  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))
             Restore Modifier:
              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