Theorem DUAL-BA-6. Independence of a majority 2-basis for BA. The following set is not a basis for Boolean algebra.

\{ \begin{matrix}y + (x · (y · z)) = y & (L1) \\ ((x · y) + (y · z)) + y = y & (L3) \\ (x + y) · (x + y′) = x & (B1) \\ ((x · z) + x) · (x + z) = x \\ ((x · x) + y) · (x + x) = x \\ ((y · x) + x) · (y + x) = x \end{matrix} \} .

The clauses

y + (x · (y · z)) = y ((x · y) + (y · z)) + y = y (x + y) · (x + y′) = x ((x · z) + x) · (x + z) = x ((x · x) + y) · (x + x) = x ((y · x) + x) · (y + x) = x A′′ ≠ A

have the following model (found by MACE 1.2.0 on gyro at 0.03 seconds).

+ | 0 1        . | 0 1        '   0 1        A: 0
--+----        --+----        -------
0 | 0 0        0 | 0 1            1 1
1 | 0 1        1 | 1 1