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(·, ·)’.