YES

Problem:
 ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil()))

Proof:
 DP Processor:
  DPs:
   ap#(ap(ff(),x),x) -> ap#(cons(),x)
   ap#(ap(ff(),x),x) -> ap#(ap(cons(),x),nil())
   ap#(ap(ff(),x),x) -> ap#(x,ap(ff(),x))
   ap#(ap(ff(),x),x) -> ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil()))
  TRS:
   ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil()))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
    [ap#](x0, x1) = [1 1 0]x0 + [0 1 1]x1 + [1],
    
            [0]
    [nil] = [0]
            [0],
    
             [0]
    [cons] = [0]
             [0],
    
                   [0 0 1]     [1 0 0]  
    [ap](x0, x1) = [0 0 1]x0 + [0 0 1]x1
                   [0 0 0]     [0 0 0]  ,
    
           [0]
    [ff] = [0]
           [1]
   orientation:
    ap#(ap(ff(),x),x) = [1 1 2]x + [3] >= [0 1 1]x + [1] = ap#(cons(),x)
    
    ap#(ap(ff(),x),x) = [1 1 2]x + [3] >= [1 0 1]x + [1] = ap#(ap(cons(),x),nil())
    
    ap#(ap(ff(),x),x) = [1 1 2]x + [3] >= [1 1 1]x + [2] = ap#(x,ap(ff(),x))
    
    ap#(ap(ff(),x),x) = [1 1 2]x + [3] >= [1 0 2]x + [2] = ap#(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil()))
    
                       [1 0 0]     [0]                                              
    ap(ap(ff(),x),x) = [0 0 1]x >= [0] = ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil()))
                       [0 0 0]     [0]                                              
   problem:
    DPs:
     
    TRS:
     ap(ap(ff(),x),x) -> ap(ap(x,ap(ff(),x)),ap(ap(cons(),x),nil()))
   Qed