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:
 DP Processor:
  DPs:
   c#(b(x1)) -> d#(x1)
   e#(b(x1)) -> c#(x1)
   e#(b(x1)) -> c#(c(x1))
   d#(b(x1)) -> f#(x1)
   f#(x1) -> e#(x1)
   f#(x1) -> a#(e(x1))
   a#(a(x1)) -> f#(x1)
  TRS:
   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)
  TDG Processor:
   DPs:
    c#(b(x1)) -> d#(x1)
    e#(b(x1)) -> c#(x1)
    e#(b(x1)) -> c#(c(x1))
    d#(b(x1)) -> f#(x1)
    f#(x1) -> e#(x1)
    f#(x1) -> a#(e(x1))
    a#(a(x1)) -> f#(x1)
   TRS:
    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)
   graph:
    f#(x1) -> e#(x1) -> e#(b(x1)) -> c#(c(x1))
    f#(x1) -> e#(x1) -> e#(b(x1)) -> c#(x1)
    f#(x1) -> a#(e(x1)) -> a#(a(x1)) -> f#(x1)
    e#(b(x1)) -> c#(c(x1)) -> c#(b(x1)) -> d#(x1)
    e#(b(x1)) -> c#(x1) -> c#(b(x1)) -> d#(x1)
    d#(b(x1)) -> f#(x1) -> f#(x1) -> a#(e(x1))
    d#(b(x1)) -> f#(x1) -> f#(x1) -> e#(x1)
    c#(b(x1)) -> d#(x1) -> d#(b(x1)) -> f#(x1)
    a#(a(x1)) -> f#(x1) -> f#(x1) -> a#(e(x1))
    a#(a(x1)) -> f#(x1) -> f#(x1) -> e#(x1)
   Arctic Interpretation Processor:
    dimension: 3
    interpretation:
     [f#](x0) = [0  -& 0 ]x0 + [0],
     
     [e#](x0) = [-2 -& 0 ]x0 + [0],
     
     [d#](x0) = [-& -2 0 ]x0 + [0],
     
     [c#](x0) = [-1 -2 0 ]x0 + [0],
     
     [a#](x0) = [-& -& 0 ]x0 + [0],
     
               [0  -& 0 ]     [0]
     [f](x0) = [1  -& 1 ]x0 + [1]
               [1  -& 1 ]     [1],
     
               [0  -& 0 ]     [-&]
     [e](x0) = [0  -& 0 ]x0 + [0 ]
               [0  -& 0 ]     [-1],
     
               [1  -1 -1]  
     [d](x0) = [1  -1 -&]x0
               [1  -2 -2]  ,
     
               [0 0 0]     [-2]
     [c](x0) = [0 0 0]x0 + [0 ]
               [0 0 0]     [-2],
     
               [0  -2 0 ]     [0 ]
     [b](x0) = [1  0  0 ]x0 + [-&]
               [0  0  0 ]     [-&],
     
               [0 0 0]     [0]
     [a](x0) = [1 0 1]x0 + [1]
               [1 0 1]     [1]
    orientation:
     c#(b(x1)) = [0 0 0]x1 + [0] >= [-& -2 0 ]x1 + [0] = d#(x1)
     
     e#(b(x1)) = [0 0 0]x1 + [0] >= [-1 -2 0 ]x1 + [0] = c#(x1)
     
     e#(b(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = c#(c(x1))
     
     d#(b(x1)) = [0 0 0]x1 + [0] >= [0  -& 0 ]x1 + [0] = f#(x1)
     
     f#(x1) = [0  -& 0 ]x1 + [0] >= [-2 -& 0 ]x1 + [0] = e#(x1)
     
     f#(x1) = [0  -& 0 ]x1 + [0] >= [0  -& 0 ]x1 + [0] = a#(e(x1))
     
     a#(a(x1)) = [1 0 1]x1 + [1] >= [0  -& 0 ]x1 + [0] = f#(x1)
     
             [0 0 0]     [0]    [0 0 0]     [0]           
     a(x1) = [1 0 1]x1 + [1] >= [1 0 1]x1 + [1] = b(b(x1))
             [1 0 1]     [1]    [1 0 0]     [0]           
     
                [1 0 0]     [0]    [1  -1 -1]          
     c(b(x1)) = [1 0 0]x1 + [0] >= [1  -1 -&]x1 = d(x1)
                [1 0 0]     [0]    [1  -2 -2]          
     
                [0 0 0]     [0]    [0 0 0]     [0]           
     e(b(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = c(c(x1))
                [0 0 0]     [0]    [0 0 0]     [0]           
     
                [1  -1 1 ]     [1]    [1  -& 1 ]     [1]           
     d(b(x1)) = [1  -1 1 ]x1 + [1] >= [1  -& 1 ]x1 + [1] = b(f(x1))
                [1  -1 1 ]     [1]    [1  -& 1 ]     [1]           
     
             [0  -& 0 ]     [0]    [0  -& 0 ]     [0]           
     f(x1) = [1  -& 1 ]x1 + [1] >= [1  -& 1 ]x1 + [1] = a(e(x1))
             [1  -& 1 ]     [1]    [1  -& 1 ]     [1]           
     
             [0 0 0]     [-2]           
     c(x1) = [0 0 0]x1 + [0 ] >= x1 = x1
             [0 0 0]     [-2]           
     
                [1 0 1]     [1]    [0  -& 0 ]     [0]        
     a(a(x1)) = [2 1 2]x1 + [2] >= [1  -& 1 ]x1 + [1] = f(x1)
                [2 1 2]     [2]    [1  -& 1 ]     [1]        
    problem:
     DPs:
      c#(b(x1)) -> d#(x1)
      e#(b(x1)) -> c#(x1)
      e#(b(x1)) -> c#(c(x1))
      d#(b(x1)) -> f#(x1)
      f#(x1) -> e#(x1)
      f#(x1) -> a#(e(x1))
     TRS:
      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)
    EDG Processor:
     DPs:
      c#(b(x1)) -> d#(x1)
      e#(b(x1)) -> c#(x1)
      e#(b(x1)) -> c#(c(x1))
      d#(b(x1)) -> f#(x1)
      f#(x1) -> e#(x1)
      f#(x1) -> a#(e(x1))
     TRS:
      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)
     graph:
      f#(x1) -> e#(x1) -> e#(b(x1)) -> c#(x1)
      f#(x1) -> e#(x1) -> e#(b(x1)) -> c#(c(x1))
      e#(b(x1)) -> c#(c(x1)) -> c#(b(x1)) -> d#(x1)
      e#(b(x1)) -> c#(x1) -> c#(b(x1)) -> d#(x1)
      d#(b(x1)) -> f#(x1) -> f#(x1) -> e#(x1)
      d#(b(x1)) -> f#(x1) -> f#(x1) -> a#(e(x1))
      c#(b(x1)) -> d#(x1) -> d#(b(x1)) -> f#(x1)
     SCC Processor:
      #sccs: 1
      #rules: 5
      #arcs: 7/36
      DPs:
       f#(x1) -> e#(x1)
       e#(b(x1)) -> c#(c(x1))
       c#(b(x1)) -> d#(x1)
       d#(b(x1)) -> f#(x1)
       e#(b(x1)) -> c#(x1)
      TRS:
       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)
      Arctic Interpretation Processor:
       dimension: 3
       interpretation:
        [f#](x0) = [0  -& -&]x0,
        
        [e#](x0) = [0  -& -&]x0,
        
        [d#](x0) = [0 0 0]x0 + [0],
        
        [c#](x0) = [0  0  -&]x0,
        
                  [1 0 0]     [0]
        [f](x0) = [1 0 0]x0 + [0]
                  [1 0 0]     [0],
        
                  [0  -& -&]     [-&]
        [e](x0) = [0  -& -&]x0 + [-&]
                  [1  0  0 ]     [0 ],
        
                  [0 0 0]     [-&]
        [d](x0) = [0 0 0]x0 + [0 ]
                  [0 0 1]     [-&],
        
                  [0  0  -&]     [-&]
        [c](x0) = [0  0  -&]x0 + [-&]
                  [0  1  0 ]     [0 ],
        
                  [0  0  -&]     [-&]
        [b](x0) = [0  0  0 ]x0 + [0 ]
                  [1  0  0 ]     [0 ],
        
                  [0 0 0]     [0]
        [a](x0) = [1 0 0]x0 + [0]
                  [1 1 0]     [0]
       orientation:
        f#(x1) = [0  -& -&]x1 >= [0  -& -&]x1 = e#(x1)
        
        e#(b(x1)) = [0  0  -&]x1 >= [0  0  -&]x1 = c#(c(x1))
        
        c#(b(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = d#(x1)
        
        d#(b(x1)) = [1 0 0]x1 + [0] >= [0  -& -&]x1 = f#(x1)
        
        e#(b(x1)) = [0  0  -&]x1 >= [0  0  -&]x1 = c#(x1)
        
                [0 0 0]     [0]    [0 0 0]     [0]           
        a(x1) = [1 0 0]x1 + [0] >= [1 0 0]x1 + [0] = b(b(x1))
                [1 1 0]     [0]    [1 1 0]     [0]           
        
                   [0 0 0]     [0]    [0 0 0]     [-&]        
        c(b(x1)) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0 ] = d(x1)
                   [1 1 1]     [1]    [0 0 1]     [-&]        
        
                   [0  0  -&]     [-&]    [0  0  -&]     [-&]           
        e(b(x1)) = [0  0  -&]x1 + [-&] >= [0  0  -&]x1 + [-&] = c(c(x1))
                   [1  1  0 ]     [0 ]    [1  1  0 ]     [0 ]           
        
                   [1 0 0]     [0]    [1 0 0]     [0]           
        d(b(x1)) = [1 0 0]x1 + [0] >= [1 0 0]x1 + [0] = b(f(x1))
                   [2 1 1]     [1]    [2 1 1]     [1]           
        
                [1 0 0]     [0]    [1 0 0]     [0]           
        f(x1) = [1 0 0]x1 + [0] >= [1 0 0]x1 + [0] = a(e(x1))
                [1 0 0]     [0]    [1 0 0]     [0]           
        
                [0  0  -&]     [-&]           
        c(x1) = [0  0  -&]x1 + [-&] >= x1 = x1
                [0  1  0 ]     [0 ]           
        
                   [1 1 0]     [0]    [1 0 0]     [0]        
        a(a(x1)) = [1 1 1]x1 + [1] >= [1 0 0]x1 + [0] = f(x1)
                   [2 1 1]     [1]    [1 0 0]     [0]        
       problem:
        DPs:
         f#(x1) -> e#(x1)
         e#(b(x1)) -> c#(c(x1))
         c#(b(x1)) -> d#(x1)
         e#(b(x1)) -> c#(x1)
        TRS:
         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)
       EDG Processor:
        DPs:
         f#(x1) -> e#(x1)
         e#(b(x1)) -> c#(c(x1))
         c#(b(x1)) -> d#(x1)
         e#(b(x1)) -> c#(x1)
        TRS:
         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)
        graph:
         f#(x1) -> e#(x1) -> e#(b(x1)) -> c#(c(x1))
         f#(x1) -> e#(x1) -> e#(b(x1)) -> c#(x1)
         e#(b(x1)) -> c#(c(x1)) -> c#(b(x1)) -> d#(x1)
         e#(b(x1)) -> c#(x1) -> c#(b(x1)) -> d#(x1)
        CDG Processor:
         DPs:
          f#(x1) -> e#(x1)
          e#(b(x1)) -> c#(c(x1))
          c#(b(x1)) -> d#(x1)
          e#(b(x1)) -> c#(x1)
         TRS:
          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)
         graph:
          f#(x1) -> e#(x1) -> e#(b(x1)) -> c#(x1)
          f#(x1) -> e#(x1) -> e#(b(x1)) -> c#(c(x1))
          e#(b(x1)) -> c#(c(x1)) -> c#(b(x1)) -> d#(x1)
         SCC Processor:
          #sccs: 0
          #rules: 0
          #arcs: 3/16