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