YES

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

Proof:
 DP Processor:
  DPs:
   a#(a(x1)) -> c#(x1)
   a#(a(x1)) -> b#(c(x1))
   b#(b(x1)) -> d#(x1)
   b#(b(x1)) -> c#(d(x1))
   c#(c(x1)) -> d#(x1)
   c#(c(x1)) -> d#(d(x1))
   c#(c(x1)) -> d#(d(d(x1)))
   d#(c(x1)) -> f#(x1)
   d#(c(x1)) -> b#(f(x1))
   d#(d(d(x1))) -> c#(x1)
   d#(d(d(x1))) -> a#(c(x1))
   f#(f(x1)) -> b#(x1)
   f#(f(x1)) -> f#(b(x1))
  TRS:
   a(a(x1)) -> b(c(x1))
   b(b(x1)) -> c(d(x1))
   c(c(x1)) -> d(d(d(x1)))
   d(c(x1)) -> b(f(x1))
   d(d(d(x1))) -> a(c(x1))
   f(f(x1)) -> f(b(x1))
  TDG Processor:
   DPs:
    a#(a(x1)) -> c#(x1)
    a#(a(x1)) -> b#(c(x1))
    b#(b(x1)) -> d#(x1)
    b#(b(x1)) -> c#(d(x1))
    c#(c(x1)) -> d#(x1)
    c#(c(x1)) -> d#(d(x1))
    c#(c(x1)) -> d#(d(d(x1)))
    d#(c(x1)) -> f#(x1)
    d#(c(x1)) -> b#(f(x1))
    d#(d(d(x1))) -> c#(x1)
    d#(d(d(x1))) -> a#(c(x1))
    f#(f(x1)) -> b#(x1)
    f#(f(x1)) -> f#(b(x1))
   TRS:
    a(a(x1)) -> b(c(x1))
    b(b(x1)) -> c(d(x1))
    c(c(x1)) -> d(d(d(x1)))
    d(c(x1)) -> b(f(x1))
    d(d(d(x1))) -> a(c(x1))
    f(f(x1)) -> f(b(x1))
   graph:
    f#(f(x1)) -> f#(b(x1)) -> f#(f(x1)) -> f#(b(x1))
    f#(f(x1)) -> f#(b(x1)) -> f#(f(x1)) -> b#(x1)
    f#(f(x1)) -> b#(x1) -> b#(b(x1)) -> c#(d(x1))
    f#(f(x1)) -> b#(x1) -> b#(b(x1)) -> d#(x1)
    d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
    d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
    d#(d(d(x1))) -> c#(x1) -> c#(c(x1)) -> d#(x1)
    d#(d(d(x1))) -> a#(c(x1)) -> a#(a(x1)) -> b#(c(x1))
    d#(d(d(x1))) -> a#(c(x1)) -> a#(a(x1)) -> c#(x1)
    d#(c(x1)) -> f#(x1) -> f#(f(x1)) -> f#(b(x1))
    d#(c(x1)) -> f#(x1) -> f#(f(x1)) -> b#(x1)
    d#(c(x1)) -> b#(f(x1)) -> b#(b(x1)) -> c#(d(x1))
    d#(c(x1)) -> b#(f(x1)) -> b#(b(x1)) -> d#(x1)
    b#(b(x1)) -> d#(x1) -> d#(d(d(x1))) -> a#(c(x1))
    b#(b(x1)) -> d#(x1) -> d#(d(d(x1))) -> c#(x1)
    b#(b(x1)) -> d#(x1) -> d#(c(x1)) -> b#(f(x1))
    b#(b(x1)) -> d#(x1) -> d#(c(x1)) -> f#(x1)
    b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(d(x1)))
    b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(x1))
    b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(x1)
    c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> a#(c(x1))
    c#(c(x1)) -> d#(d(d(x1))) -> d#(d(d(x1))) -> c#(x1)
    c#(c(x1)) -> d#(d(d(x1))) -> d#(c(x1)) -> b#(f(x1))
    c#(c(x1)) -> d#(d(d(x1))) -> d#(c(x1)) -> f#(x1)
    c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> a#(c(x1))
    c#(c(x1)) -> d#(d(x1)) -> d#(d(d(x1))) -> c#(x1)
    c#(c(x1)) -> d#(d(x1)) -> d#(c(x1)) -> b#(f(x1))
    c#(c(x1)) -> d#(d(x1)) -> d#(c(x1)) -> f#(x1)
    c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> a#(c(x1))
    c#(c(x1)) -> d#(x1) -> d#(d(d(x1))) -> c#(x1)
    c#(c(x1)) -> d#(x1) -> d#(c(x1)) -> b#(f(x1))
    c#(c(x1)) -> d#(x1) -> d#(c(x1)) -> f#(x1)
    a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1))
    a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1)
    a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(d(x1)))
    a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> d#(d(x1))
    a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> d#(x1)
   Arctic Interpretation Processor:
    dimension: 1
    interpretation:
     [f#](x0) = x0,
     
     [d#](x0) = 1x0,
     
     [b#](x0) = 2x0,
     
     [c#](x0) = 3x0,
     
     [a#](x0) = 2x0,
     
     [f](x0) = 5x0,
     
     [d](x0) = 4x0,
     
     [b](x0) = 5x0,
     
     [c](x0) = 6x0,
     
     [a](x0) = 6x0
    orientation:
     a#(a(x1)) = 8x1 >= 3x1 = c#(x1)
     
     a#(a(x1)) = 8x1 >= 8x1 = b#(c(x1))
     
     b#(b(x1)) = 7x1 >= 1x1 = d#(x1)
     
     b#(b(x1)) = 7x1 >= 7x1 = c#(d(x1))
     
     c#(c(x1)) = 9x1 >= 1x1 = d#(x1)
     
     c#(c(x1)) = 9x1 >= 5x1 = d#(d(x1))
     
     c#(c(x1)) = 9x1 >= 9x1 = d#(d(d(x1)))
     
     d#(c(x1)) = 7x1 >= x1 = f#(x1)
     
     d#(c(x1)) = 7x1 >= 7x1 = b#(f(x1))
     
     d#(d(d(x1))) = 9x1 >= 3x1 = c#(x1)
     
     d#(d(d(x1))) = 9x1 >= 8x1 = a#(c(x1))
     
     f#(f(x1)) = 5x1 >= 2x1 = b#(x1)
     
     f#(f(x1)) = 5x1 >= 5x1 = f#(b(x1))
     
     a(a(x1)) = 12x1 >= 11x1 = b(c(x1))
     
     b(b(x1)) = 10x1 >= 10x1 = c(d(x1))
     
     c(c(x1)) = 12x1 >= 12x1 = d(d(d(x1)))
     
     d(c(x1)) = 10x1 >= 10x1 = b(f(x1))
     
     d(d(d(x1))) = 12x1 >= 12x1 = a(c(x1))
     
     f(f(x1)) = 10x1 >= 10x1 = f(b(x1))
    problem:
     DPs:
      a#(a(x1)) -> b#(c(x1))
      b#(b(x1)) -> c#(d(x1))
      c#(c(x1)) -> d#(d(d(x1)))
      d#(c(x1)) -> b#(f(x1))
      f#(f(x1)) -> f#(b(x1))
     TRS:
      a(a(x1)) -> b(c(x1))
      b(b(x1)) -> c(d(x1))
      c(c(x1)) -> d(d(d(x1)))
      d(c(x1)) -> b(f(x1))
      d(d(d(x1))) -> a(c(x1))
      f(f(x1)) -> f(b(x1))
    EDG Processor:
     DPs:
      a#(a(x1)) -> b#(c(x1))
      b#(b(x1)) -> c#(d(x1))
      c#(c(x1)) -> d#(d(d(x1)))
      d#(c(x1)) -> b#(f(x1))
      f#(f(x1)) -> f#(b(x1))
     TRS:
      a(a(x1)) -> b(c(x1))
      b(b(x1)) -> c(d(x1))
      c(c(x1)) -> d(d(d(x1)))
      d(c(x1)) -> b(f(x1))
      d(d(d(x1))) -> a(c(x1))
      f(f(x1)) -> f(b(x1))
     graph:
      f#(f(x1)) -> f#(b(x1)) -> f#(f(x1)) -> f#(b(x1))
      d#(c(x1)) -> b#(f(x1)) -> b#(b(x1)) -> c#(d(x1))
      b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(d(d(x1)))
      c#(c(x1)) -> d#(d(d(x1))) -> d#(c(x1)) -> b#(f(x1))
      a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1))
     SCC Processor:
      #sccs: 2
      #rules: 4
      #arcs: 5/25
      DPs:
       d#(c(x1)) -> b#(f(x1))
       b#(b(x1)) -> c#(d(x1))
       c#(c(x1)) -> d#(d(d(x1)))
      TRS:
       a(a(x1)) -> b(c(x1))
       b(b(x1)) -> c(d(x1))
       c(c(x1)) -> d(d(d(x1)))
       d(c(x1)) -> b(f(x1))
       d(d(d(x1))) -> a(c(x1))
       f(f(x1)) -> f(b(x1))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [d#](x0) = 9x0 + 0,
        
        [b#](x0) = 13x0 + 0,
        
        [c#](x0) = 15x0 + 0,
        
        [f](x0) = 0,
        
        [d](x0) = 7x0 + 1,
        
        [b](x0) = 9x0 + 3,
        
        [c](x0) = 11x0 + 4,
        
        [a](x0) = 10x0 + 3
       orientation:
        d#(c(x1)) = 20x1 + 13 >= 13 = b#(f(x1))
        
        b#(b(x1)) = 22x1 + 16 >= 22x1 + 16 = c#(d(x1))
        
        c#(c(x1)) = 26x1 + 19 >= 23x1 + 17 = d#(d(d(x1)))
        
        a(a(x1)) = 20x1 + 13 >= 20x1 + 13 = b(c(x1))
        
        b(b(x1)) = 18x1 + 12 >= 18x1 + 12 = c(d(x1))
        
        c(c(x1)) = 22x1 + 15 >= 21x1 + 15 = d(d(d(x1)))
        
        d(c(x1)) = 18x1 + 11 >= 9 = b(f(x1))
        
        d(d(d(x1))) = 21x1 + 15 >= 21x1 + 14 = a(c(x1))
        
        f(f(x1)) = 0 >= 0 = f(b(x1))
       problem:
        DPs:
         d#(c(x1)) -> b#(f(x1))
         b#(b(x1)) -> c#(d(x1))
        TRS:
         a(a(x1)) -> b(c(x1))
         b(b(x1)) -> c(d(x1))
         c(c(x1)) -> d(d(d(x1)))
         d(c(x1)) -> b(f(x1))
         d(d(d(x1))) -> a(c(x1))
         f(f(x1)) -> f(b(x1))
       EDG Processor:
        DPs:
         d#(c(x1)) -> b#(f(x1))
         b#(b(x1)) -> c#(d(x1))
        TRS:
         a(a(x1)) -> b(c(x1))
         b(b(x1)) -> c(d(x1))
         c(c(x1)) -> d(d(d(x1)))
         d(c(x1)) -> b(f(x1))
         d(d(d(x1))) -> a(c(x1))
         f(f(x1)) -> f(b(x1))
        graph:
         d#(c(x1)) -> b#(f(x1)) -> b#(b(x1)) -> c#(d(x1))
        SCC Processor:
         #sccs: 0
         #rules: 0
         #arcs: 1/4
         
      
      DPs:
       f#(f(x1)) -> f#(b(x1))
      TRS:
       a(a(x1)) -> b(c(x1))
       b(b(x1)) -> c(d(x1))
       c(c(x1)) -> d(d(d(x1)))
       d(c(x1)) -> b(f(x1))
       d(d(d(x1))) -> a(c(x1))
       f(f(x1)) -> f(b(x1))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [f#](x0) = 8x0 + 0,
        
        [f](x0) = x0 + 8,
        
        [d](x0) = 0,
        
        [b](x0) = 0,
        
        [c](x0) = x0 + 0,
        
        [a](x0) = 0
       orientation:
        f#(f(x1)) = 8x1 + 16 >= 8 = f#(b(x1))
        
        a(a(x1)) = 0 >= 0 = b(c(x1))
        
        b(b(x1)) = 0 >= 0 = c(d(x1))
        
        c(c(x1)) = x1 + 0 >= 0 = d(d(d(x1)))
        
        d(c(x1)) = 0 >= 0 = b(f(x1))
        
        d(d(d(x1))) = 0 >= 0 = a(c(x1))
        
        f(f(x1)) = x1 + 8 >= 8 = f(b(x1))
       problem:
        DPs:
         
        TRS:
         a(a(x1)) -> b(c(x1))
         b(b(x1)) -> c(d(x1))
         c(c(x1)) -> d(d(d(x1)))
         d(c(x1)) -> b(f(x1))
         d(d(d(x1))) -> a(c(x1))
         f(f(x1)) -> f(b(x1))
       Qed