YES(?,ELEMENTARY)

We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).

Strict 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)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,ELEMENTARY)

The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping

 safe(or) = {1, 2}, safe(true) = {}, safe(false) = {},
 safe(mem) = {1}, safe(nil) = {}, safe(set) = {1}, safe(=) = {1, 2},
 safe(union) = {1, 2}

and precedence

 mem > or .

Following symbols are considered recursive:

 {or, mem}

The recursion depth is 2.

For your convenience, here are the satisfied ordering constraints:

         or(; x,  true()) > true()                     
                                                       
         or(; true(),  y) > true()                     
                                                       
  or(; false(),  false()) > false()                    
                                                       
            mem(nil(); x) > false()                    
                                                       
         mem(set(; y); x) > =(; x,  y)                 
                                                       
   mem(union(; y,  z); x) > or(; mem(y; x),  mem(z; x))
                                                       

Hurray, we answered YES(?,ELEMENTARY)