MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. 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: MAYBE The input cannot be shown compatible Arrrr..