YES

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

Proof:
 DP Processor:
  DPs:
   a#(b(x1)) -> d#(x1)
   b#(a(x1)) -> b#(x1)
   b#(a(x1)) -> a#(b(x1))
   d#(c(x1)) -> b#(c(x1))
   d#(c(x1)) -> b#(b(c(x1)))
   d#(c(x1)) -> a#(b(b(c(x1))))
   d#(f(x1)) -> b#(x1)
   d#(f(x1)) -> a#(b(x1))
   a#(f(x1)) -> a#(x1)
  TRS:
   a(b(x1)) -> d(x1)
   b(a(x1)) -> a(b(x1))
   d(c(x1)) -> f(a(b(b(c(x1)))))
   d(f(x1)) -> f(a(b(x1)))
   a(f(x1)) -> a(x1)
  Matrix Interpretation Processor: dim=5
   
   interpretation:
    [b#](x0) = [1 0 1 1 0]x0,
    
    [d#](x0) = [1 1 0 1 0]x0,
    
    [a#](x0) = [1 0 1 0 1]x0 + [1],
    
              [1 0 0 0 0]     [1]
              [0 0 1 0 0]     [0]
    [f](x0) = [0 1 1 0 0]x0 + [0]
              [0 1 0 1 0]     [1]
              [0 1 0 0 1]     [0],
    
              [0 0 1 0 1]     [1]
              [0 0 1 0 0]     [1]
    [c](x0) = [0 0 0 0 0]x0 + [0]
              [0 0 1 0 1]     [1]
              [0 0 0 0 1]     [0],
    
              [1 0 0 1 0]     [1]
              [0 0 0 0 0]     [0]
    [d](x0) = [0 0 0 0 0]x0 + [0]
              [0 1 0 1 1]     [1]
              [1 1 0 0 1]     [1],
    
              [1 1 0 0 1]     [1]
              [0 0 0 0 0]     [0]
    [a](x0) = [0 0 0 0 0]x0 + [0]
              [1 0 1 1 0]     [1]
              [0 1 1 1 1]     [1],
    
              [0 0 0 1 0]  
              [0 0 0 0 0]  
    [b](x0) = [0 1 0 0 0]x0
              [0 0 0 0 1]  
              [1 0 0 0 0]  
   orientation:
    a#(b(x1)) = [1 1 0 1 0]x1 + [1] >= [1 1 0 1 0]x1 = d#(x1)
    
    b#(a(x1)) = [2 1 1 1 1]x1 + [2] >= [1 0 1 1 0]x1 = b#(x1)
    
    b#(a(x1)) = [2 1 1 1 1]x1 + [2] >= [1 1 0 1 0]x1 + [1] = a#(b(x1))
    
    d#(c(x1)) = [0 0 3 0 2]x1 + [3] >= [0 0 2 0 2]x1 + [2] = b#(c(x1))
    
    d#(c(x1)) = [0 0 3 0 2]x1 + [3] >= [0 0 2 0 2]x1 + [2] = b#(b(c(x1)))
    
    d#(c(x1)) = [0 0 3 0 2]x1 + [3] >= [0 0 1 0 2]x1 + [2] = a#(b(b(c(x1))))
    
    d#(f(x1)) = [1 1 1 1 0]x1 + [2] >= [1 0 1 1 0]x1 = b#(x1)
    
    d#(f(x1)) = [1 1 1 1 0]x1 + [2] >= [1 1 0 1 0]x1 + [1] = a#(b(x1))
    
    a#(f(x1)) = [1 2 1 0 1]x1 + [2] >= [1 0 1 0 1]x1 + [1] = a#(x1)
    
               [1 0 0 1 0]     [1]    [1 0 0 1 0]     [1]        
               [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]        
    a(b(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = d(x1)
               [0 1 0 1 1]     [1]    [0 1 0 1 1]     [1]        
               [1 1 0 0 1]     [1]    [1 1 0 0 1]     [1]        
    
               [1 0 1 1 0]     [1]    [1 0 0 1 0]     [1]           
               [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]           
    b(a(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = a(b(x1))
               [0 1 1 1 1]     [1]    [0 1 0 1 1]     [1]           
               [1 1 0 0 1]     [1]    [1 1 0 0 1]     [1]           
    
               [0 0 2 0 2]     [3]    [0 0 1 0 2]     [3]                    
               [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]                    
    d(c(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = f(a(b(b(c(x1)))))
               [0 0 2 0 2]     [3]    [0 0 1 0 2]     [3]                    
               [0 0 2 0 2]     [3]    [0 0 2 0 2]     [3]                    
    
               [1 1 0 1 0]     [3]    [1 0 0 1 0]     [2]              
               [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]              
    d(f(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = f(a(b(x1)))
               [0 2 1 1 1]     [2]    [0 1 0 1 1]     [2]              
               [1 1 1 0 1]     [2]    [1 1 0 0 1]     [1]              
    
               [1 1 1 0 1]     [2]    [1 1 0 0 1]     [1]        
               [0 0 0 0 0]     [0]    [0 0 0 0 0]     [0]        
    a(f(x1)) = [0 0 0 0 0]x1 + [0] >= [0 0 0 0 0]x1 + [0] = a(x1)
               [1 2 1 1 0]     [3]    [1 0 1 1 0]     [1]        
               [0 3 2 1 1]     [2]    [0 1 1 1 1]     [1]        
   problem:
    DPs:
     
    TRS:
     a(b(x1)) -> d(x1)
     b(a(x1)) -> a(b(x1))
     d(c(x1)) -> f(a(b(b(c(x1)))))
     d(f(x1)) -> f(a(b(x1)))
     a(f(x1)) -> a(x1)
   Qed