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