Two crucial cubic-time components of polynomial-maximal decidable Boolean languages

We continue our investigation aimed at spotting small fragments of Set Theory (in this paper, sublanguages of Boolean Set Theory) that might be of use in automated proof-checkers based on the set-theoretic formalism. Here we propose a method that leads to a cubic-time satisfiability decision test for the language involving, besides variables intended to range over the von Neumann set-universe, the Boolean operator $cup$ and the logical relators $=$ and $eq$. It can be seen that the dual language involving the Boolean operator $cap$ and, again, the relators $=$ and $eq$, also admits a decidable cubic-time satisfiability test; noticeably, the same algorithm can be used for both languages. Suitable pre-processing can reduce richer Boolean languages to the said two fragments, so that the same cubic satisfiability test can be used to treat the relators $subseteq,subseteq$ and the predicates `$sqdot= arnothing$' and `$Disj{sqdot}{sqdot}$', meaning `the argument is empty' and `the arguments are disjoint sets', along with their opposites `$sqdot eq arnothing$' and `$egDisj{sqdot}{sqdot}$'. Those richer languages are `polynomial maximal', in the sense that all languages strictly containing them have an NP-hard satisfiability problem.