Example TNL-2. Uniqueness of the meet operation in TNL. Let ⟨S; ∨, ∧⟩ and ⟨S; ∨, ·⟩ be two transitive near lattices. Are the two meet operations necessarily the same?

Counterexample. The clauses

x ∧ x = x x ∧ y = y ∧ x x ∧ (x ∨ y) = x x ∧ (y ∨ (x ∨ z)) = x x ∨ x = x x ∨ y = y ∨ x x ∨ (x ∧ y) = x x ∨ (y ∧ (x ∧ z)) = x x · x = x x · y = y · x x · (x ∨ y) = x x · (y ∨ (x ∨ z)) = x x ∨ x = x x ∨ y = y ∨ x x ∨ (x · y) = x x ∨ (y · (x · z)) = x 0 ∧ 1 ≠ 0 · 1

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

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

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