YES

Problem:
 app(app(and(),true()),true()) -> true()
 app(app(and(),true()),false()) -> false()
 app(app(and(),false()),true()) -> false()
 app(app(and(),false()),false()) -> false()
 app(app(or(),true()),true()) -> true()
 app(app(or(),true()),false()) -> true()
 app(app(or(),false()),true()) -> true()
 app(app(or(),false()),false()) -> false()
 app(app(forall(),p),nil()) -> true()
 app(app(forall(),p),app(app(cons(),x),xs)) -> app(app(and(),app(p,x)),app(app(forall(),p),xs))
 app(app(forsome(),p),nil()) -> false()
 app(app(forsome(),p),app(app(cons(),x),xs)) -> app(app(or(),app(p,x)),app(app(forsome(),p),xs))

Proof:
 Uncurry Processor:
  and2(true(),true()) -> true()
  and2(true(),false()) -> false()
  and2(false(),true()) -> false()
  and2(false(),false()) -> false()
  or2(true(),true()) -> true()
  or2(true(),false()) -> true()
  or2(false(),true()) -> true()
  or2(false(),false()) -> false()
  forall2(p,nil()) -> true()
  forall2(p,cons2(x,xs)) -> and2(app(p,x),forall2(p,xs))
  forsome2(p,nil()) -> false()
  forsome2(p,cons2(x,xs)) -> or2(app(p,x),forsome2(p,xs))
  app(and1(x3),x4) -> and2(x3,x4)
  app(and(),x4) -> and1(x4)
  app(or1(x3),x4) -> or2(x3,x4)
  app(or(),x4) -> or1(x4)
  app(forall1(x3),x4) -> forall2(x3,x4)
  app(forall(),x4) -> forall1(x4)
  app(cons1(x3),x4) -> cons2(x3,x4)
  app(cons(),x4) -> cons1(x4)
  app(forsome1(x3),x4) -> forsome2(x3,x4)
  app(forsome(),x4) -> forsome1(x4)
  DP Processor:
   DPs:
    forall{2,#}(p,cons2(x,xs)) -> forall{2,#}(p,xs)
    forall{2,#}(p,cons2(x,xs)) -> app#(p,x)
    forall{2,#}(p,cons2(x,xs)) -> and{2,#}(app(p,x),forall2(p,xs))
    forsome{2,#}(p,cons2(x,xs)) -> forsome{2,#}(p,xs)
    forsome{2,#}(p,cons2(x,xs)) -> app#(p,x)
    forsome{2,#}(p,cons2(x,xs)) -> or{2,#}(app(p,x),forsome2(p,xs))
    app#(and1(x3),x4) -> and{2,#}(x3,x4)
    app#(or1(x3),x4) -> or{2,#}(x3,x4)
    app#(forall1(x3),x4) -> forall{2,#}(x3,x4)
    app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4)
   TRS:
    and2(true(),true()) -> true()
    and2(true(),false()) -> false()
    and2(false(),true()) -> false()
    and2(false(),false()) -> false()
    or2(true(),true()) -> true()
    or2(true(),false()) -> true()
    or2(false(),true()) -> true()
    or2(false(),false()) -> false()
    forall2(p,nil()) -> true()
    forall2(p,cons2(x,xs)) -> and2(app(p,x),forall2(p,xs))
    forsome2(p,nil()) -> false()
    forsome2(p,cons2(x,xs)) -> or2(app(p,x),forsome2(p,xs))
    app(and1(x3),x4) -> and2(x3,x4)
    app(and(),x4) -> and1(x4)
    app(or1(x3),x4) -> or2(x3,x4)
    app(or(),x4) -> or1(x4)
    app(forall1(x3),x4) -> forall2(x3,x4)
    app(forall(),x4) -> forall1(x4)
    app(cons1(x3),x4) -> cons2(x3,x4)
    app(cons(),x4) -> cons1(x4)
    app(forsome1(x3),x4) -> forsome2(x3,x4)
    app(forsome(),x4) -> forsome1(x4)
   TDG Processor:
    DPs:
     forall{2,#}(p,cons2(x,xs)) -> forall{2,#}(p,xs)
     forall{2,#}(p,cons2(x,xs)) -> app#(p,x)
     forall{2,#}(p,cons2(x,xs)) -> and{2,#}(app(p,x),forall2(p,xs))
     forsome{2,#}(p,cons2(x,xs)) -> forsome{2,#}(p,xs)
     forsome{2,#}(p,cons2(x,xs)) -> app#(p,x)
     forsome{2,#}(p,cons2(x,xs)) -> or{2,#}(app(p,x),forsome2(p,xs))
     app#(and1(x3),x4) -> and{2,#}(x3,x4)
     app#(or1(x3),x4) -> or{2,#}(x3,x4)
     app#(forall1(x3),x4) -> forall{2,#}(x3,x4)
     app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4)
    TRS:
     and2(true(),true()) -> true()
     and2(true(),false()) -> false()
     and2(false(),true()) -> false()
     and2(false(),false()) -> false()
     or2(true(),true()) -> true()
     or2(true(),false()) -> true()
     or2(false(),true()) -> true()
     or2(false(),false()) -> false()
     forall2(p,nil()) -> true()
     forall2(p,cons2(x,xs)) -> and2(app(p,x),forall2(p,xs))
     forsome2(p,nil()) -> false()
     forsome2(p,cons2(x,xs)) -> or2(app(p,x),forsome2(p,xs))
     app(and1(x3),x4) -> and2(x3,x4)
     app(and(),x4) -> and1(x4)
     app(or1(x3),x4) -> or2(x3,x4)
     app(or(),x4) -> or1(x4)
     app(forall1(x3),x4) -> forall2(x3,x4)
     app(forall(),x4) -> forall1(x4)
     app(cons1(x3),x4) -> cons2(x3,x4)
     app(cons(),x4) -> cons1(x4)
     app(forsome1(x3),x4) -> forsome2(x3,x4)
     app(forsome(),x4) -> forsome1(x4)
    graph:
     forsome{2,#}(p,cons2(x,xs)) -> forsome{2,#}(p,xs) ->
     forsome{2,#}(p,cons2(x,xs)) -> or{2,#}(app(p,x),forsome2(p,xs))
     forsome{2,#}(p,cons2(x,xs)) -> forsome{2,#}(p,xs) ->
     forsome{2,#}(p,cons2(x,xs)) -> app#(p,x)
     forsome{2,#}(p,cons2(x,xs)) -> forsome{2,#}(p,xs) ->
     forsome{2,#}(p,cons2(x,xs)) -> forsome{2,#}(p,xs)
     forsome{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4)
     forsome{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(forall1(x3),x4) -> forall{2,#}(x3,x4)
     forsome{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(or1(x3),x4) -> or{2,#}(x3,x4)
     forsome{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(and1(x3),x4) -> and{2,#}(x3,x4)
     app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4) ->
     forsome{2,#}(p,cons2(x,xs)) -> or{2,#}(app(p,x),forsome2(p,xs))
     app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4) ->
     forsome{2,#}(p,cons2(x,xs)) -> app#(p,x)
     app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4) ->
     forsome{2,#}(p,cons2(x,xs)) -> forsome{2,#}(p,xs)
     app#(forall1(x3),x4) -> forall{2,#}(x3,x4) ->
     forall{2,#}(p,cons2(x,xs)) -> and{2,#}(app(p,x),forall2(p,xs))
     app#(forall1(x3),x4) -> forall{2,#}(x3,x4) ->
     forall{2,#}(p,cons2(x,xs)) -> app#(p,x)
     app#(forall1(x3),x4) -> forall{2,#}(x3,x4) ->
     forall{2,#}(p,cons2(x,xs)) -> forall{2,#}(p,xs)
     forall{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4)
     forall{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(forall1(x3),x4) -> forall{2,#}(x3,x4)
     forall{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(or1(x3),x4) -> or{2,#}(x3,x4)
     forall{2,#}(p,cons2(x,xs)) -> app#(p,x) ->
     app#(and1(x3),x4) -> and{2,#}(x3,x4)
     forall{2,#}(p,cons2(x,xs)) -> forall{2,#}(p,xs) ->
     forall{2,#}(p,cons2(x,xs)) -> and{2,#}(app(p,x),forall2(p,xs))
     forall{2,#}(p,cons2(x,xs)) -> forall{2,#}(p,xs) ->
     forall{2,#}(p,cons2(x,xs)) -> app#(p,x)
     forall{2,#}(p,cons2(x,xs)) -> forall{2,#}(p,xs) ->
     forall{2,#}(p,cons2(x,xs)) -> forall{2,#}(p,xs)
    SCC Processor:
     #sccs: 1
     #rules: 6
     #arcs: 20/100
     DPs:
      forsome{2,#}(p,cons2(x,xs)) -> forsome{2,#}(p,xs)
      forsome{2,#}(p,cons2(x,xs)) -> app#(p,x)
      app#(forall1(x3),x4) -> forall{2,#}(x3,x4)
      forall{2,#}(p,cons2(x,xs)) -> forall{2,#}(p,xs)
      forall{2,#}(p,cons2(x,xs)) -> app#(p,x)
      app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4)
     TRS:
      and2(true(),true()) -> true()
      and2(true(),false()) -> false()
      and2(false(),true()) -> false()
      and2(false(),false()) -> false()
      or2(true(),true()) -> true()
      or2(true(),false()) -> true()
      or2(false(),true()) -> true()
      or2(false(),false()) -> false()
      forall2(p,nil()) -> true()
      forall2(p,cons2(x,xs)) -> and2(app(p,x),forall2(p,xs))
      forsome2(p,nil()) -> false()
      forsome2(p,cons2(x,xs)) -> or2(app(p,x),forsome2(p,xs))
      app(and1(x3),x4) -> and2(x3,x4)
      app(and(),x4) -> and1(x4)
      app(or1(x3),x4) -> or2(x3,x4)
      app(or(),x4) -> or1(x4)
      app(forall1(x3),x4) -> forall2(x3,x4)
      app(forall(),x4) -> forall1(x4)
      app(cons1(x3),x4) -> cons2(x3,x4)
      app(cons(),x4) -> cons1(x4)
      app(forsome1(x3),x4) -> forsome2(x3,x4)
      app(forsome(),x4) -> forsome1(x4)
     Subterm Criterion Processor:
      simple projection:
       pi(forall{2,#}) = 1
       pi(app#) = 1
       pi(forsome{2,#}) = 1
      problem:
       DPs:
        app#(forall1(x3),x4) -> forall{2,#}(x3,x4)
        app#(forsome1(x3),x4) -> forsome{2,#}(x3,x4)
       TRS:
        and2(true(),true()) -> true()
        and2(true(),false()) -> false()
        and2(false(),true()) -> false()
        and2(false(),false()) -> false()
        or2(true(),true()) -> true()
        or2(true(),false()) -> true()
        or2(false(),true()) -> true()
        or2(false(),false()) -> false()
        forall2(p,nil()) -> true()
        forall2(p,cons2(x,xs)) -> and2(app(p,x),forall2(p,xs))
        forsome2(p,nil()) -> false()
        forsome2(p,cons2(x,xs)) -> or2(app(p,x),forsome2(p,xs))
        app(and1(x3),x4) -> and2(x3,x4)
        app(and(),x4) -> and1(x4)
        app(or1(x3),x4) -> or2(x3,x4)
        app(or(),x4) -> or1(x4)
        app(forall1(x3),x4) -> forall2(x3,x4)
        app(forall(),x4) -> forall1(x4)
        app(cons1(x3),x4) -> cons2(x3,x4)
        app(cons(),x4) -> cons1(x4)
        app(forsome1(x3),x4) -> forsome2(x3,x4)
        app(forsome(),x4) -> forsome1(x4)
      SCC Processor:
       #sccs: 0
       #rules: 0
       #arcs: 12/4