YES

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

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