Polynomial-time satisfiability tests for boolean fragments of set theory

We recently undertook an investigation aimed at identifying small fragments of set theory (which in most cases are sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this note we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪, ∩, , the Boolean relators ⊆, /⊆, =, /=, and the predicates ‘· = ∅’ and ‘Disj(·, ·)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘· /= ∅’ and ‘¬Disj(·, ·)’.