YES
Time: 0.001189
TRS:
 {       or(x, true()) -> true(),
         or(true(), y) -> 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))}
 DP:
  DP:
   {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)}
  TRS:
  {       or(x, true()) -> true(),
          or(true(), y) -> 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:
   {(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)) -> 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))}
   SCCS (1):
    Scc:
     {mem#(x, union(y, z)) -> mem#(x, y),
      mem#(x, union(y, z)) -> mem#(x, z)}
    SCC (2):
     Strict:
      {mem#(x, union(y, z)) -> mem#(x, y),
       mem#(x, union(y, z)) -> mem#(x, z)}
     Weak:
     {       or(x, true()) -> true(),
             or(true(), y) -> 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))}
     SPSC:
      Simple Projection:
       pi(mem#) = 1
      Strict:
       {mem#(x, union(y, z)) -> mem#(x, y)}
      EDG:
       {(mem#(x, union(y, z)) -> mem#(x, y), mem#(x, union(y, z)) -> mem#(x, y))}
       SCCS (1):
        Scc:
         {mem#(x, union(y, z)) -> mem#(x, y)}
        SCC (1):
         Strict:
          {mem#(x, union(y, z)) -> mem#(x, y)}
         Weak:
         {       or(x, true()) -> true(),
                 or(true(), y) -> 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))}
         SPSC:
          Simple Projection:
           pi(mem#) = 1
          Strict:
           {}
          Qed