Polynomial-time satisfiability tests for ’small’ membership theories

We continue here our investigation aimed at the identification of ‘small’ fragments of set theory that are potentially useful in automated verification with proof-checkers based on the set-theoretic formalism, such as ÆtnaNova. More specifically, we provide a complete taxonomy of the polynomial and the NP-complete fragments comprising all conjunctions that may involve, besides variables intended to range over the von Neumann set-universe, the Boolean set operators ∪, ∩, and the membership relators ∈ and ∈/. This is in preparation of combining the aforementioned taxonomy with one recently developed for similar frag- ments, but involving, in place of the membership relators ∈ and ∈/, the Boolean relators ⊆,̸⊆,=,̸=, and the predicates ‘· = ∅’ and ‘Disj(·,·)’ (respectively meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’), along with their opposites ‘· ̸= ∅’ and ‘¬Disj(·, ·)’.