YES

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

Proof:
 Uncurry Processor:
  ff2(x,x) -> ap(ap(x,ff1(x)),cons2(x,nil()))
  ap(ff1(x1),x2) -> ff2(x1,x2)
  ap(ff(),x2) -> ff1(x2)
  ap(cons1(x1),x2) -> cons2(x1,x2)
  ap(cons(),x2) -> cons1(x2)
  DP Processor:
   DPs:
    ff{2,#}(x,x) -> ap#(x,ff1(x))
    ff{2,#}(x,x) -> ap#(ap(x,ff1(x)),cons2(x,nil()))
    ap#(ff1(x1),x2) -> ff{2,#}(x1,x2)
   TRS:
    ff2(x,x) -> ap(ap(x,ff1(x)),cons2(x,nil()))
    ap(ff1(x1),x2) -> ff2(x1,x2)
    ap(ff(),x2) -> ff1(x2)
    ap(cons1(x1),x2) -> cons2(x1,x2)
    ap(cons(),x2) -> cons1(x2)
   TDG Processor:
    DPs:
     ff{2,#}(x,x) -> ap#(x,ff1(x))
     ff{2,#}(x,x) -> ap#(ap(x,ff1(x)),cons2(x,nil()))
     ap#(ff1(x1),x2) -> ff{2,#}(x1,x2)
    TRS:
     ff2(x,x) -> ap(ap(x,ff1(x)),cons2(x,nil()))
     ap(ff1(x1),x2) -> ff2(x1,x2)
     ap(ff(),x2) -> ff1(x2)
     ap(cons1(x1),x2) -> cons2(x1,x2)
     ap(cons(),x2) -> cons1(x2)
    graph:
     ap#(ff1(x1),x2) -> ff{2,#}(x1,x2) ->
     ff{2,#}(x,x) -> ap#(ap(x,ff1(x)),cons2(x,nil()))
     ap#(ff1(x1),x2) -> ff{2,#}(x1,x2) ->
     ff{2,#}(x,x) -> ap#(x,ff1(x))
     ff{2,#}(x,x) -> ap#(ap(x,ff1(x)),cons2(x,nil())) ->
     ap#(ff1(x1),x2) -> ff{2,#}(x1,x2)
     ff{2,#}(x,x) -> ap#(x,ff1(x)) -> ap#(ff1(x1),x2) -> ff{2,#}(x1,x2)
    Matrix Interpretation Processor: dim=2
     
     usable rules:
      ff2(x,x) -> ap(ap(x,ff1(x)),cons2(x,nil()))
      ap(ff1(x1),x2) -> ff2(x1,x2)
      ap(ff(),x2) -> ff1(x2)
      ap(cons1(x1),x2) -> cons2(x1,x2)
      ap(cons(),x2) -> cons1(x2)
     interpretation:
      [ap#](x0, x1) = [0 1]x0 + [2 1]x1,
      
      [ff{2,#}](x0, x1) = [2 0]x0 + [2 1]x1 + [2],
      
                        [0]
      [cons2](x0, x1) = [0],
      
                    [0]
      [cons1](x0) = [0],
      
                      [0 0]  
      [ff2](x0, x1) = [1 0]x1,
      
                  [1 0]     [0]
      [ff1](x0) = [2 0]x0 + [2],
      
              [0]
      [nil] = [0],
      
               [1]
      [cons] = [0],
      
                     [0 0]     [1 0]  
      [ap](x0, x1) = [1 0]x0 + [2 0]x1,
      
             [2]
      [ff] = [0]
     orientation:
      ff{2,#}(x,x) = [4 1]x + [2] >= [4 1]x + [2] = ap#(x,ff1(x))
      
      ff{2,#}(x,x) = [4 1]x + [2] >= [3 0]x = ap#(ap(x,ff1(x)),cons2(x,nil()))
      
      ap#(ff1(x1),x2) = [2 0]x1 + [2 1]x2 + [2] >= [2 0]x1 + [2 1]x2 + [2] = ff{2,#}(x1,x2)
      
                 [0 0]     [0 0]                                   
      ff2(x,x) = [1 0]x >= [1 0]x = ap(ap(x,ff1(x)),cons2(x,nil()))
      
                       [0 0]     [1 0]      [0 0]               
      ap(ff1(x1),x2) = [1 0]x1 + [2 0]x2 >= [1 0]x2 = ff2(x1,x2)
      
                    [1 0]     [0]    [1 0]     [0]          
      ap(ff(),x2) = [2 0]x2 + [2] >= [2 0]x2 + [2] = ff1(x2)
      
                         [1 0]      [0]               
      ap(cons1(x1),x2) = [2 0]x2 >= [0] = cons2(x1,x2)
      
                      [1 0]     [0]    [0]            
      ap(cons(),x2) = [2 0]x2 + [1] >= [0] = cons1(x2)
     problem:
      DPs:
       ff{2,#}(x,x) -> ap#(x,ff1(x))
       ap#(ff1(x1),x2) -> ff{2,#}(x1,x2)
      TRS:
       ff2(x,x) -> ap(ap(x,ff1(x)),cons2(x,nil()))
       ap(ff1(x1),x2) -> ff2(x1,x2)
       ap(ff(),x2) -> ff1(x2)
       ap(cons1(x1),x2) -> cons2(x1,x2)
       ap(cons(),x2) -> cons1(x2)
     Restore Modifier:
      DPs:
       ff{2,#}(x,x) -> ap#(x,ff1(x))
       ap#(ff1(x1),x2) -> ff{2,#}(x1,x2)
      TRS:
       ff2(x,x) -> ap(ap(x,ff1(x)),cons2(x,nil()))
       ap(ff1(x1),x2) -> ff2(x1,x2)
       ap(ff(),x2) -> ff1(x2)
       ap(cons1(x1),x2) -> cons2(x1,x2)
       ap(cons(),x2) -> cons1(x2)
      Subterm Criterion Processor:
       simple projection:
        pi(ff{2,#}) = 0
        pi(ap#) = 0
       problem:
        DPs:
         ff{2,#}(x,x) -> ap#(x,ff1(x))
        TRS:
         ff2(x,x) -> ap(ap(x,ff1(x)),cons2(x,nil()))
         ap(ff1(x1),x2) -> ff2(x1,x2)
         ap(ff(),x2) -> ff1(x2)
         ap(cons1(x1),x2) -> cons2(x1,x2)
         ap(cons(),x2) -> cons1(x2)
       SCC Processor:
        #sccs: 0
        #rules: 0
        #arcs: 4/1