Example DUAL-BA-10. Dual BA 3-basis, independence (2).

The set M̃ is independent of M ∪ {SD-dist}. We ask MACE to find a model of M ∪ {SD-dist} that is not a Boolean algebra.

The clauses

(x · y) + ((y · z) + (z · x)) = (x + y) · ((y + z) · (z + x)) y + (x · (y · z)) = y ((x · y) + (y · z)) + y = y (x + x′) · y = y ((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.63 seconds).

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