YES

Problem:
 or(true(),y) -> true()
 or(x,true()) -> true()
 or(false(),false()) -> false()
 mem(x,nil()) -> false()
 mem(x,set(y)) -> =(x,y)
 mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))

Proof:
 DP Processor:
  DPs:
   mem#(x,union(y,z)) -> mem#(x,z)
   mem#(x,union(y,z)) -> mem#(x,y)
   mem#(x,union(y,z)) -> or#(mem(x,y),mem(x,z))
  TRS:
   or(true(),y) -> true()
   or(x,true()) -> true()
   or(false(),false()) -> false()
   mem(x,nil()) -> false()
   mem(x,set(y)) -> =(x,y)
   mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
  TDG Processor:
   DPs:
    mem#(x,union(y,z)) -> mem#(x,z)
    mem#(x,union(y,z)) -> mem#(x,y)
    mem#(x,union(y,z)) -> or#(mem(x,y),mem(x,z))
   TRS:
    or(true(),y) -> true()
    or(x,true()) -> true()
    or(false(),false()) -> false()
    mem(x,nil()) -> false()
    mem(x,set(y)) -> =(x,y)
    mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
   graph:
    mem#(x,union(y,z)) -> mem#(x,z) ->
    mem#(x,union(y,z)) -> or#(mem(x,y),mem(x,z))
    mem#(x,union(y,z)) -> mem#(x,z) ->
    mem#(x,union(y,z)) -> mem#(x,y)
    mem#(x,union(y,z)) -> mem#(x,z) ->
    mem#(x,union(y,z)) -> mem#(x,z)
    mem#(x,union(y,z)) -> mem#(x,y) ->
    mem#(x,union(y,z)) -> or#(mem(x,y),mem(x,z))
    mem#(x,union(y,z)) -> mem#(x,y) ->
    mem#(x,union(y,z)) -> mem#(x,y)
    mem#(x,union(y,z)) -> mem#(x,y) -> mem#(x,union(y,z)) -> mem#(x,z)
   SCC Processor:
    #sccs: 1
    #rules: 2
    #arcs: 6/9
    DPs:
     mem#(x,union(y,z)) -> mem#(x,z)
     mem#(x,union(y,z)) -> mem#(x,y)
    TRS:
     or(true(),y) -> true()
     or(x,true()) -> true()
     or(false(),false()) -> false()
     mem(x,nil()) -> false()
     mem(x,set(y)) -> =(x,y)
     mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
    KBO Processor:
     argument filtering:
      pi(true) = []
      pi(or) = [0]
      pi(false) = []
      pi(nil) = []
      pi(mem) = 1
      pi(set) = 0
      pi(=) = 1
      pi(union) = [0,1]
      pi(mem#) = [0,1]
     weight function:
      w0 = 1
      w(mem#) = w(=) = w(set) = w(nil) = w(false) = w(or) = w(true) = 1
      w(union) = w(mem) = 0
     precedence:
      mem > mem# ~ union ~ nil ~ true > = ~ set ~ false ~ or
     problem:
      DPs:
       
      TRS:
       or(true(),y) -> true()
       or(x,true()) -> true()
       or(false(),false()) -> false()
       mem(x,nil()) -> false()
       mem(x,set(y)) -> =(x,y)
       mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
     Qed