Example DUAL-BA-9. Dual BA 3-basis, independence (1).

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

The clauses

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

    + | 0 1 2 3 4          . | 0 1 2 3 4
    --+----------         --+----------
    0 | 0 0 0 0 0          0 | 0 1 2 3 4
    1 | 0 1 2 3 4          1 | 1 1 1 1 1
    2 | 0 2 2 0 0          2 | 2 1 2 1 1
    3 | 0 3 0 3 0          3 | 3 1 1 3 1
    4 | 0 4 0 0 4          4 | 4 1 1 1 4

    '   0 1 2 3 4           A: 4
    -------------
        1 0 3 2 2