MAYBE
Time: 0.001361
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))}
   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))}
    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))}
     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))}
      STATUS:
       arrows: 0.333333
       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))}
         Open