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))
  EDG 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)) -> 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)) -> or#(mem(x,y),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,y) ->
    mem#(x,union(y,z)) -> mem#(x,y)
    mem#(x,union(y,z)) -> mem#(x,y) -> mem#(x,union(y,z)) -> or#(mem(x,y),mem(x,z))
   Restore Modifier:
    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))
    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))
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [mem#](x0, x1) = x1 + 1,
       
       [union](x0, x1) = x0 + x1 + 1,
       
       [=](x0, x1) = 0,
       
       [set](x0) = 0,
       
       [mem](x0, x1) = 0,
       
       [nil] = 0,
       
       [false] = 0,
       
       [or](x0, x1) = 0,
       
       [true] = 0
      orientation:
       mem#(x,union(y,z)) = y + z + 2 >= z + 1 = mem#(x,z)
       
       mem#(x,union(y,z)) = y + z + 2 >= y + 1 = mem#(x,y)
       
       or(true(),y) = 0 >= 0 = true()
       
       or(x,true()) = 0 >= 0 = true()
       
       or(false(),false()) = 0 >= 0 = false()
       
       mem(x,nil()) = 0 >= 0 = false()
       
       mem(x,set(y)) = 0 >= 0 = =(x,y)
       
       mem(x,union(y,z)) = 0 >= 0 = or(mem(x,y),mem(x,z))
      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