YES

Problem:
 app(app(lt(),app(s(),x)),app(s(),y)) -> app(app(lt(),x),y)
 app(app(lt(),0()),app(s(),y)) -> true()
 app(app(lt(),y),0()) -> false()
 app(app(eq(),x),x) -> true()
 app(app(eq(),app(s(),x)),0()) -> false()
 app(app(eq(),0()),app(s(),x)) -> false()
 app(app(member(),w),null()) -> false()
 app(app(member(),w),app(app(app(fork(),x),y),z)) ->
 app(app(app(if(),app(app(lt(),w),y)),app(app(member(),w),x)),app(app
                                                                  (app(if(),app(app(eq(),w),y)),
                                                                   true
                                                                   ()),
                                                                  app(app(member(),w),z)))

Proof:
 Uncurry Processor:
  lt2(s1(x),s1(y)) -> lt2(x,y)
  lt2(0(),s1(y)) -> true()
  lt2(y,0()) -> false()
  eq2(x,x) -> true()
  eq2(s1(x),0()) -> false()
  eq2(0(),s1(x)) -> false()
  member2(w,null()) -> false()
  member2(w,fork3(x,y,z)) -> if3(lt2(w,y),member2(w,x),if3(eq2(w,y),true(),member2(w,z)))
  app(lt1(x5),x6) -> lt2(x5,x6)
  app(lt(),x6) -> lt1(x6)
  app(s(),x6) -> s1(x6)
  app(eq1(x5),x6) -> eq2(x5,x6)
  app(eq(),x6) -> eq1(x6)
  app(member1(x5),x6) -> member2(x5,x6)
  app(member(),x6) -> member1(x6)
  app(fork2(x5,x4),x6) -> fork3(x5,x4,x6)
  app(fork1(x5),x6) -> fork2(x5,x6)
  app(fork(),x6) -> fork1(x6)
  app(if2(x5,x4),x6) -> if3(x5,x4,x6)
  app(if1(x5),x6) -> if2(x5,x6)
  app(if(),x6) -> if1(x6)
  DP Processor:
   DPs:
    lt{2,#}(s1(x),s1(y)) -> lt{2,#}(x,y)
    member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z)
    member{2,#}(w,fork3(x,y,z)) -> eq{2,#}(w,y)
    member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x)
    member{2,#}(w,fork3(x,y,z)) -> lt{2,#}(w,y)
    app#(lt1(x5),x6) -> lt{2,#}(x5,x6)
    app#(eq1(x5),x6) -> eq{2,#}(x5,x6)
    app#(member1(x5),x6) -> member{2,#}(x5,x6)
   TRS:
    lt2(s1(x),s1(y)) -> lt2(x,y)
    lt2(0(),s1(y)) -> true()
    lt2(y,0()) -> false()
    eq2(x,x) -> true()
    eq2(s1(x),0()) -> false()
    eq2(0(),s1(x)) -> false()
    member2(w,null()) -> false()
    member2(w,fork3(x,y,z)) -> if3(lt2(w,y),member2(w,x),if3(eq2(w,y),true(),member2(w,z)))
    app(lt1(x5),x6) -> lt2(x5,x6)
    app(lt(),x6) -> lt1(x6)
    app(s(),x6) -> s1(x6)
    app(eq1(x5),x6) -> eq2(x5,x6)
    app(eq(),x6) -> eq1(x6)
    app(member1(x5),x6) -> member2(x5,x6)
    app(member(),x6) -> member1(x6)
    app(fork2(x5,x4),x6) -> fork3(x5,x4,x6)
    app(fork1(x5),x6) -> fork2(x5,x6)
    app(fork(),x6) -> fork1(x6)
    app(if2(x5,x4),x6) -> if3(x5,x4,x6)
    app(if1(x5),x6) -> if2(x5,x6)
    app(if(),x6) -> if1(x6)
   TDG Processor:
    DPs:
     lt{2,#}(s1(x),s1(y)) -> lt{2,#}(x,y)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z)
     member{2,#}(w,fork3(x,y,z)) -> eq{2,#}(w,y)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x)
     member{2,#}(w,fork3(x,y,z)) -> lt{2,#}(w,y)
     app#(lt1(x5),x6) -> lt{2,#}(x5,x6)
     app#(eq1(x5),x6) -> eq{2,#}(x5,x6)
     app#(member1(x5),x6) -> member{2,#}(x5,x6)
    TRS:
     lt2(s1(x),s1(y)) -> lt2(x,y)
     lt2(0(),s1(y)) -> true()
     lt2(y,0()) -> false()
     eq2(x,x) -> true()
     eq2(s1(x),0()) -> false()
     eq2(0(),s1(x)) -> false()
     member2(w,null()) -> false()
     member2(w,fork3(x,y,z)) -> if3(lt2(w,y),member2(w,x),if3(eq2(w,y),true(),member2(w,z)))
     app(lt1(x5),x6) -> lt2(x5,x6)
     app(lt(),x6) -> lt1(x6)
     app(s(),x6) -> s1(x6)
     app(eq1(x5),x6) -> eq2(x5,x6)
     app(eq(),x6) -> eq1(x6)
     app(member1(x5),x6) -> member2(x5,x6)
     app(member(),x6) -> member1(x6)
     app(fork2(x5,x4),x6) -> fork3(x5,x4,x6)
     app(fork1(x5),x6) -> fork2(x5,x6)
     app(fork(),x6) -> fork1(x6)
     app(if2(x5,x4),x6) -> if3(x5,x4,x6)
     app(if1(x5),x6) -> if2(x5,x6)
     app(if(),x6) -> if1(x6)
    graph:
     app#(member1(x5),x6) -> member{2,#}(x5,x6) ->
     member{2,#}(w,fork3(x,y,z)) -> lt{2,#}(w,y)
     app#(member1(x5),x6) -> member{2,#}(x5,x6) ->
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x)
     app#(member1(x5),x6) -> member{2,#}(x5,x6) ->
     member{2,#}(w,fork3(x,y,z)) -> eq{2,#}(w,y)
     app#(member1(x5),x6) -> member{2,#}(x5,x6) ->
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z)
     app#(lt1(x5),x6) -> lt{2,#}(x5,x6) ->
     lt{2,#}(s1(x),s1(y)) -> lt{2,#}(x,y)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z) ->
     member{2,#}(w,fork3(x,y,z)) -> lt{2,#}(w,y)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z) ->
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z) ->
     member{2,#}(w,fork3(x,y,z)) -> eq{2,#}(w,y)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z) ->
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x) ->
     member{2,#}(w,fork3(x,y,z)) -> lt{2,#}(w,y)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x) ->
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x) ->
     member{2,#}(w,fork3(x,y,z)) -> eq{2,#}(w,y)
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x) ->
     member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z)
     member{2,#}(w,fork3(x,y,z)) -> lt{2,#}(w,y) ->
     lt{2,#}(s1(x),s1(y)) -> lt{2,#}(x,y)
     lt{2,#}(s1(x),s1(y)) -> lt{2,#}(x,y) -> lt{2,#}(s1(x),s1(y)) -> lt{2,#}(x,y)
    SCC Processor:
     #sccs: 2
     #rules: 3
     #arcs: 15/64
     DPs:
      member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,z)
      member{2,#}(w,fork3(x,y,z)) -> member{2,#}(w,x)
     TRS:
      lt2(s1(x),s1(y)) -> lt2(x,y)
      lt2(0(),s1(y)) -> true()
      lt2(y,0()) -> false()
      eq2(x,x) -> true()
      eq2(s1(x),0()) -> false()
      eq2(0(),s1(x)) -> false()
      member2(w,null()) -> false()
      member2(w,fork3(x,y,z)) -> if3(lt2(w,y),member2(w,x),if3(eq2(w,y),true(),member2(w,z)))
      app(lt1(x5),x6) -> lt2(x5,x6)
      app(lt(),x6) -> lt1(x6)
      app(s(),x6) -> s1(x6)
      app(eq1(x5),x6) -> eq2(x5,x6)
      app(eq(),x6) -> eq1(x6)
      app(member1(x5),x6) -> member2(x5,x6)
      app(member(),x6) -> member1(x6)
      app(fork2(x5,x4),x6) -> fork3(x5,x4,x6)
      app(fork1(x5),x6) -> fork2(x5,x6)
      app(fork(),x6) -> fork1(x6)
      app(if2(x5,x4),x6) -> if3(x5,x4,x6)
      app(if1(x5),x6) -> if2(x5,x6)
      app(if(),x6) -> if1(x6)
     Subterm Criterion Processor:
      simple projection:
       pi(member{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        lt2(s1(x),s1(y)) -> lt2(x,y)
        lt2(0(),s1(y)) -> true()
        lt2(y,0()) -> false()
        eq2(x,x) -> true()
        eq2(s1(x),0()) -> false()
        eq2(0(),s1(x)) -> false()
        member2(w,null()) -> false()
        member2(w,fork3(x,y,z)) -> if3(lt2(w,y),member2(w,x),if3(eq2(w,y),true(),member2(w,z)))
        app(lt1(x5),x6) -> lt2(x5,x6)
        app(lt(),x6) -> lt1(x6)
        app(s(),x6) -> s1(x6)
        app(eq1(x5),x6) -> eq2(x5,x6)
        app(eq(),x6) -> eq1(x6)
        app(member1(x5),x6) -> member2(x5,x6)
        app(member(),x6) -> member1(x6)
        app(fork2(x5,x4),x6) -> fork3(x5,x4,x6)
        app(fork1(x5),x6) -> fork2(x5,x6)
        app(fork(),x6) -> fork1(x6)
        app(if2(x5,x4),x6) -> if3(x5,x4,x6)
        app(if1(x5),x6) -> if2(x5,x6)
        app(if(),x6) -> if1(x6)
      Qed
     
     DPs:
      lt{2,#}(s1(x),s1(y)) -> lt{2,#}(x,y)
     TRS:
      lt2(s1(x),s1(y)) -> lt2(x,y)
      lt2(0(),s1(y)) -> true()
      lt2(y,0()) -> false()
      eq2(x,x) -> true()
      eq2(s1(x),0()) -> false()
      eq2(0(),s1(x)) -> false()
      member2(w,null()) -> false()
      member2(w,fork3(x,y,z)) -> if3(lt2(w,y),member2(w,x),if3(eq2(w,y),true(),member2(w,z)))
      app(lt1(x5),x6) -> lt2(x5,x6)
      app(lt(),x6) -> lt1(x6)
      app(s(),x6) -> s1(x6)
      app(eq1(x5),x6) -> eq2(x5,x6)
      app(eq(),x6) -> eq1(x6)
      app(member1(x5),x6) -> member2(x5,x6)
      app(member(),x6) -> member1(x6)
      app(fork2(x5,x4),x6) -> fork3(x5,x4,x6)
      app(fork1(x5),x6) -> fork2(x5,x6)
      app(fork(),x6) -> fork1(x6)
      app(if2(x5,x4),x6) -> if3(x5,x4,x6)
      app(if1(x5),x6) -> if2(x5,x6)
      app(if(),x6) -> if1(x6)
     Subterm Criterion Processor:
      simple projection:
       pi(lt{2,#}) = 1
      problem:
       DPs:
        
       TRS:
        lt2(s1(x),s1(y)) -> lt2(x,y)
        lt2(0(),s1(y)) -> true()
        lt2(y,0()) -> false()
        eq2(x,x) -> true()
        eq2(s1(x),0()) -> false()
        eq2(0(),s1(x)) -> false()
        member2(w,null()) -> false()
        member2(w,fork3(x,y,z)) -> if3(lt2(w,y),member2(w,x),if3(eq2(w,y),true(),member2(w,z)))
        app(lt1(x5),x6) -> lt2(x5,x6)
        app(lt(),x6) -> lt1(x6)
        app(s(),x6) -> s1(x6)
        app(eq1(x5),x6) -> eq2(x5,x6)
        app(eq(),x6) -> eq1(x6)
        app(member1(x5),x6) -> member2(x5,x6)
        app(member(),x6) -> member1(x6)
        app(fork2(x5,x4),x6) -> fork3(x5,x4,x6)
        app(fork1(x5),x6) -> fork2(x5,x6)
        app(fork(),x6) -> fork1(x6)
        app(if2(x5,x4),x6) -> if3(x5,x4,x6)
        app(if1(x5),x6) -> if2(x5,x6)
        app(if(),x6) -> if1(x6)
      Qed