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)
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [ap#](x0, x1) = x0 + x1 + 0,
      
      [ff{2,#}](x0, x1) = x1 + 1,
      
      [cons2](x0, x1) = -11x1 + 0,
      
      [cons1](x0) = 4,
      
      [ff2](x0, x1) = -6x0 + -2x1 + 0,
      
      [ff1](x0) = -2x0 + 1,
      
      [nil] = 11,
      
      [cons] = 8,
      
      [ap](x0, x1) = -4x0 + -2x1 + 0,
      
      [ff] = 6
     orientation:
      ff{2,#}(x,x) = x + 1 >= x + 1 = ap#(x,ff1(x))
      
      ff{2,#}(x,x) = x + 1 >= -4x + 0 = ap#(ap(x,ff1(x)),cons2(x,nil()))
      
      ap#(ff1(x1),x2) = -2x1 + x2 + 1 >= x2 + 1 = ff{2,#}(x1,x2)
      
      ff2(x,x) = -2x + 0 >= -8x + 0 = ap(ap(x,ff1(x)),cons2(x,nil()))
      
      ap(ff1(x1),x2) = -6x1 + -2x2 + 0 >= -6x1 + -2x2 + 0 = ff2(x1,x2)
      
      ap(ff(),x2) = -2x2 + 2 >= -2x2 + 1 = ff1(x2)
      
      ap(cons1(x1),x2) = -2x2 + 0 >= -11x2 + 0 = cons2(x1,x2)
      
      ap(cons(),x2) = -2x2 + 4 >= 4 = 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)
     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