On biconjunctive reduction classes

A predicate formula is biconjunctive if it is of the form
$$ P\biggl(\bigvee_{i=1}^l\&_{j=1}^{\delta_i}F_{ij}\biggr) $$
where $P$ is prefix, $\delta_i\leq2$ and $F_{ij}$ are atomic formulas possibly with negation. There are described 4 classes of biconjunctive formulas each having both undecidable problem of derivability in classical predicate calculus and undecidable problem of finite refutability.