YES

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

Proof:
 DP Processor:
  DPs:
   a#(a(x1)) -> b#(x1)
   a#(a(x1)) -> b#(b(x1))
   a#(a(x1)) -> b#(b(b(x1)))
   a#(x1) -> c#(d(x1))
   b#(b(b(x1))) -> f#(x1)
   b#(b(b(x1))) -> a#(f(x1))
   b#(b(x1)) -> c#(x1)
   b#(b(x1)) -> c#(c(x1))
   b#(b(x1)) -> c#(c(c(x1)))
   c#(d(d(x1))) -> f#(x1)
   f#(f(x1)) -> a#(x1)
   f#(f(x1)) -> f#(a(x1))
  TRS:
   a(a(x1)) -> b(b(b(x1)))
   a(x1) -> d(c(d(x1)))
   b(b(b(x1))) -> a(f(x1))
   b(b(x1)) -> c(c(c(x1)))
   c(c(x1)) -> d(d(d(x1)))
   c(d(d(x1))) -> f(x1)
   f(f(x1)) -> f(a(x1))
  TDG Processor:
   DPs:
    a#(a(x1)) -> b#(x1)
    a#(a(x1)) -> b#(b(x1))
    a#(a(x1)) -> b#(b(b(x1)))
    a#(x1) -> c#(d(x1))
    b#(b(b(x1))) -> f#(x1)
    b#(b(b(x1))) -> a#(f(x1))
    b#(b(x1)) -> c#(x1)
    b#(b(x1)) -> c#(c(x1))
    b#(b(x1)) -> c#(c(c(x1)))
    c#(d(d(x1))) -> f#(x1)
    f#(f(x1)) -> a#(x1)
    f#(f(x1)) -> f#(a(x1))
   TRS:
    a(a(x1)) -> b(b(b(x1)))
    a(x1) -> d(c(d(x1)))
    b(b(b(x1))) -> a(f(x1))
    b(b(x1)) -> c(c(c(x1)))
    c(c(x1)) -> d(d(d(x1)))
    c(d(d(x1))) -> f(x1)
    f(f(x1)) -> f(a(x1))
   graph:
    f#(f(x1)) -> f#(a(x1)) -> f#(f(x1)) -> f#(a(x1))
    f#(f(x1)) -> f#(a(x1)) -> f#(f(x1)) -> a#(x1)
    f#(f(x1)) -> a#(x1) -> a#(x1) -> c#(d(x1))
    f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> b#(b(b(x1)))
    f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> b#(b(x1))
    f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> b#(x1)
    c#(d(d(x1))) -> f#(x1) -> f#(f(x1)) -> f#(a(x1))
    c#(d(d(x1))) -> f#(x1) -> f#(f(x1)) -> a#(x1)
    b#(b(b(x1))) -> f#(x1) -> f#(f(x1)) -> f#(a(x1))
    b#(b(b(x1))) -> f#(x1) -> f#(f(x1)) -> a#(x1)
    b#(b(b(x1))) -> a#(f(x1)) -> a#(x1) -> c#(d(x1))
    b#(b(b(x1))) -> a#(f(x1)) -> a#(a(x1)) -> b#(b(b(x1)))
    b#(b(b(x1))) -> a#(f(x1)) -> a#(a(x1)) -> b#(b(x1))
    b#(b(b(x1))) -> a#(f(x1)) -> a#(a(x1)) -> b#(x1)
    b#(b(x1)) -> c#(c(c(x1))) -> c#(d(d(x1))) -> f#(x1)
    b#(b(x1)) -> c#(c(x1)) -> c#(d(d(x1))) -> f#(x1)
    b#(b(x1)) -> c#(x1) -> c#(d(d(x1))) -> f#(x1)
    a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(c(c(x1)))
    a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(c(x1))
    a#(a(x1)) -> b#(b(b(x1))) -> b#(b(x1)) -> c#(x1)
    a#(a(x1)) -> b#(b(b(x1))) -> b#(b(b(x1))) -> a#(f(x1))
    a#(a(x1)) -> b#(b(b(x1))) -> b#(b(b(x1))) -> f#(x1)
    a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(c(c(x1)))
    a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(c(x1))
    a#(a(x1)) -> b#(b(x1)) -> b#(b(x1)) -> c#(x1)
    a#(a(x1)) -> b#(b(x1)) -> b#(b(b(x1))) -> a#(f(x1))
    a#(a(x1)) -> b#(b(x1)) -> b#(b(b(x1))) -> f#(x1)
    a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(c(c(x1)))
    a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(c(x1))
    a#(a(x1)) -> b#(x1) -> b#(b(x1)) -> c#(x1)
    a#(a(x1)) -> b#(x1) -> b#(b(b(x1))) -> a#(f(x1))
    a#(a(x1)) -> b#(x1) -> b#(b(b(x1))) -> f#(x1)
    a#(x1) -> c#(d(x1)) -> c#(d(d(x1))) -> f#(x1)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [f#](x0) = x0,
     
     [c#](x0) = x0,
     
     [b#](x0) = x0 + 6,
     
     [a#](x0) = x0 + 12,
     
     [f](x0) = x0 + 18,
     
     [c](x0) = x0 + 8,
     
     [d](x0) = x0 + 5,
     
     [b](x0) = x0 + 12,
     
     [a](x0) = x0 + 18
    orientation:
     a#(a(x1)) = x1 + 30 >= x1 + 6 = b#(x1)
     
     a#(a(x1)) = x1 + 30 >= x1 + 18 = b#(b(x1))
     
     a#(a(x1)) = x1 + 30 >= x1 + 30 = b#(b(b(x1)))
     
     a#(x1) = x1 + 12 >= x1 + 5 = c#(d(x1))
     
     b#(b(b(x1))) = x1 + 30 >= x1 = f#(x1)
     
     b#(b(b(x1))) = x1 + 30 >= x1 + 30 = a#(f(x1))
     
     b#(b(x1)) = x1 + 18 >= x1 = c#(x1)
     
     b#(b(x1)) = x1 + 18 >= x1 + 8 = c#(c(x1))
     
     b#(b(x1)) = x1 + 18 >= x1 + 16 = c#(c(c(x1)))
     
     c#(d(d(x1))) = x1 + 10 >= x1 = f#(x1)
     
     f#(f(x1)) = x1 + 18 >= x1 + 12 = a#(x1)
     
     f#(f(x1)) = x1 + 18 >= x1 + 18 = f#(a(x1))
     
     a(a(x1)) = x1 + 36 >= x1 + 36 = b(b(b(x1)))
     
     a(x1) = x1 + 18 >= x1 + 18 = d(c(d(x1)))
     
     b(b(b(x1))) = x1 + 36 >= x1 + 36 = a(f(x1))
     
     b(b(x1)) = x1 + 24 >= x1 + 24 = c(c(c(x1)))
     
     c(c(x1)) = x1 + 16 >= x1 + 15 = d(d(d(x1)))
     
     c(d(d(x1))) = x1 + 18 >= x1 + 18 = f(x1)
     
     f(f(x1)) = x1 + 36 >= x1 + 36 = f(a(x1))
    problem:
     DPs:
      a#(a(x1)) -> b#(b(b(x1)))
      b#(b(b(x1))) -> a#(f(x1))
      f#(f(x1)) -> f#(a(x1))
     TRS:
      a(a(x1)) -> b(b(b(x1)))
      a(x1) -> d(c(d(x1)))
      b(b(b(x1))) -> a(f(x1))
      b(b(x1)) -> c(c(c(x1)))
      c(c(x1)) -> d(d(d(x1)))
      c(d(d(x1))) -> f(x1)
      f(f(x1)) -> f(a(x1))
    EDG Processor:
     DPs:
      a#(a(x1)) -> b#(b(b(x1)))
      b#(b(b(x1))) -> a#(f(x1))
      f#(f(x1)) -> f#(a(x1))
     TRS:
      a(a(x1)) -> b(b(b(x1)))
      a(x1) -> d(c(d(x1)))
      b(b(b(x1))) -> a(f(x1))
      b(b(x1)) -> c(c(c(x1)))
      c(c(x1)) -> d(d(d(x1)))
      c(d(d(x1))) -> f(x1)
      f(f(x1)) -> f(a(x1))
     graph:
      f#(f(x1)) -> f#(a(x1)) -> f#(f(x1)) -> f#(a(x1))
      b#(b(b(x1))) -> a#(f(x1)) -> a#(a(x1)) -> b#(b(b(x1)))
      a#(a(x1)) -> b#(b(b(x1))) -> b#(b(b(x1))) -> a#(f(x1))
     SCC Processor:
      #sccs: 2
      #rules: 3
      #arcs: 3/9
      DPs:
       b#(b(b(x1))) -> a#(f(x1))
       a#(a(x1)) -> b#(b(b(x1)))
      TRS:
       a(a(x1)) -> b(b(b(x1)))
       a(x1) -> d(c(d(x1)))
       b(b(b(x1))) -> a(f(x1))
       b(b(x1)) -> c(c(c(x1)))
       c(c(x1)) -> d(d(d(x1)))
       c(d(d(x1))) -> f(x1)
       f(f(x1)) -> f(a(x1))
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [b#](x0) = 8,
        
        [a#](x0) = 1x0 + 8,
        
        [f](x0) = 3,
        
        [c](x0) = 4,
        
        [d](x0) = 4,
        
        [b](x0) = 8,
        
        [a](x0) = 8
       orientation:
        b#(b(b(x1))) = 8 >= 8 = a#(f(x1))
        
        a#(a(x1)) = 9 >= 8 = b#(b(b(x1)))
        
        a(a(x1)) = 8 >= 8 = b(b(b(x1)))
        
        a(x1) = 8 >= 4 = d(c(d(x1)))
        
        b(b(b(x1))) = 8 >= 8 = a(f(x1))
        
        b(b(x1)) = 8 >= 4 = c(c(c(x1)))
        
        c(c(x1)) = 4 >= 4 = d(d(d(x1)))
        
        c(d(d(x1))) = 4 >= 3 = f(x1)
        
        f(f(x1)) = 3 >= 3 = f(a(x1))
       problem:
        DPs:
         b#(b(b(x1))) -> a#(f(x1))
        TRS:
         a(a(x1)) -> b(b(b(x1)))
         a(x1) -> d(c(d(x1)))
         b(b(b(x1))) -> a(f(x1))
         b(b(x1)) -> c(c(c(x1)))
         c(c(x1)) -> d(d(d(x1)))
         c(d(d(x1))) -> f(x1)
         f(f(x1)) -> f(a(x1))
       EDG Processor:
        DPs:
         b#(b(b(x1))) -> a#(f(x1))
        TRS:
         a(a(x1)) -> b(b(b(x1)))
         a(x1) -> d(c(d(x1)))
         b(b(b(x1))) -> a(f(x1))
         b(b(x1)) -> c(c(c(x1)))
         c(c(x1)) -> d(d(d(x1)))
         c(d(d(x1))) -> f(x1)
         f(f(x1)) -> f(a(x1))
        graph:
         
        Qed
      
      DPs:
       f#(f(x1)) -> f#(a(x1))
      TRS:
       a(a(x1)) -> b(b(b(x1)))
       a(x1) -> d(c(d(x1)))
       b(b(b(x1))) -> a(f(x1))
       b(b(x1)) -> c(c(c(x1)))
       c(c(x1)) -> d(d(d(x1)))
       c(d(d(x1))) -> f(x1)
       f(f(x1)) -> f(a(x1))
      Matrix Interpretation Processor: dim=5
       
       interpretation:
        [f#](x0) = [0 0 1 0 0]x0 + [1],
        
                  [0 0 0 0 0]     [0]
                  [0 0 0 0 0]     [0]
        [f](x0) = [1 0 1 0 0]x0 + [1]
                  [0 0 0 0 0]     [0]
                  [0 0 0 0 0]     [0],
        
                  [0 0 0 0 0]     [0]
                  [0 0 0 0 0]     [0]
        [c](x0) = [0 0 0 1 0]x0 + [1]
                  [0 0 0 0 0]     [0]
                  [0 0 0 0 0]     [0],
        
                  [0 0 0 0 0]  
                  [0 0 0 0 0]  
        [d](x0) = [0 0 0 0 0]x0
                  [0 0 0 0 1]  
                  [1 0 1 0 0]  ,
        
                  [0 0 0 0 1]     [0]
                  [0 0 0 0 0]     [0]
        [b](x0) = [0 0 0 0 0]x0 + [1]
                  [0 0 0 0 0]     [0]
                  [0 0 1 0 0]     [0],
        
                  [0 0 0 0 0]     [1]
                  [0 0 0 0 0]     [0]
        [a](x0) = [1 0 0 0 0]x0 + [0]
                  [0 0 0 0 0]     [0]
                  [1 0 0 0 1]     [1]
       orientation:
        f#(f(x1)) = [1 0 1 0 0]x1 + [2] >= [1 0 0 0 0]x1 + [1] = f#(a(x1))
        
                   [0 0 0 0 0]     [1]    [1]              
                   [0 0 0 0 0]     [0]    [0]              
        a(a(x1)) = [0 0 0 0 0]x1 + [1] >= [1] = b(b(b(x1)))
                   [0 0 0 0 0]     [0]    [0]              
                   [1 0 0 0 1]     [3]    [1]              
        
                [0 0 0 0 0]     [1]    [0 0 0 0 0]     [0]              
                [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]              
        a(x1) = [1 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = d(c(d(x1)))
                [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]              
                [1 0 0 0 1]     [1]    [0 0 0 0 1]     [1]              
        
                      [1]    [1]           
                      [0]    [0]           
        b(b(b(x1))) = [1] >= [0] = a(f(x1))
                      [0]    [0]           
                      [1]    [1]           
        
                   [0 0 1 0 0]     [0]    [0]              
                   [0 0 0 0 0]     [0]    [0]              
        b(b(x1)) = [0 0 0 0 0]x1 + [1] >= [1] = c(c(c(x1)))
                   [0 0 0 0 0]     [0]    [0]              
                   [0 0 0 0 0]     [1]    [0]              
        
                   [0]    [0]              
                   [0]    [0]              
        c(c(x1)) = [1] >= [0] = d(d(d(x1)))
                   [0]    [0]              
                   [0]    [0]              
        
                      [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]        
                      [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]        
        c(d(d(x1))) = [1 0 1 0 0]x1 + [1] >= [1 0 1 0 0]x1 + [1] = f(x1)
                      [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]        
                      [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]        
        
                   [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]           
                   [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]           
        f(f(x1)) = [1 0 1 0 0]x1 + [2] >= [1 0 0 0 0]x1 + [2] = f(a(x1))
                   [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]           
                   [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]           
       problem:
        DPs:
         
        TRS:
         a(a(x1)) -> b(b(b(x1)))
         a(x1) -> d(c(d(x1)))
         b(b(b(x1))) -> a(f(x1))
         b(b(x1)) -> c(c(c(x1)))
         c(c(x1)) -> d(d(d(x1)))
         c(d(d(x1))) -> f(x1)
         f(f(x1)) -> f(a(x1))
       Qed