Example QLT-7. Uniqueness of the meet operation in QLT. Let ∧, ∨, and · be binary operations such that both ⟨QL; ∨, ∧⟩ and ⟨QL; ∨, ·⟩ are quasilattices. Are the two meet operations necessarily the same?

Counterexample. The clauses

x ∨ x = x x ∧ x = x x · x = x x ∨ y = y ∨ x x ∧ y = y ∧ x x · y = y · x (x ∨ y) ∨ z = x ∨ (y ∨ z) (x ∧ y) ∧ z = x ∧ (y ∧ z) (x · y) · z = x · (y · z) (x ∧ (y ∨ z)) ∨ (x ∧ y) = x ∧ (y ∨ z) (x ∨ (y ∧ z)) ∧ (x ∨ y) = x ∨ (y ∧ z) (x · (y ∨ z)) ∨ (x · y) = x · (y ∨ z) (x ∨ (y · z)) · (x ∨ y) = x ∨ (y · z) A · B ≠ A ∧ B

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

    ^| 0 1 2             v | 0 1 2
    --+------             --+------
    0 | 0 0 0             0 | 0 0 0
    1 | 0 1 0             1 | 0 1 0
    2 | 0 0 2             2 | 0 0 2

    . | 0 1 2
    --+------
    0 | 0 1 0
    1 | 1 1 1
    2 | 0 1 2           A: 0,  B: 1