Theorem LT-12. A short single axiom for LT.

We use the majority polynomial p(x, y, z) = (x ∧ z) ∨ (y ∧ (x ∨ z)). With the axiom schema axiom of Thm. MAJ-3, we substitute the two additional equations from Lem. LT-11. (The three equations (B) need not be used in the construction, because they are already satisfied.) When the schema is expanded with the majority polynomial and written in terms of ∧ and ∨, it has length 79, with 7 variables:

(((x ∧ y) ∨ (y ∧ (x ∨ y))) ∧ z) ∨ (((x ∧ (((x_{1} ∧ y) ∨ (y ∧ x_{2}))∨
y)) ∨ (((y ∧ (((x_{1} ∨ (y ∨ x_{2})) ∧ (x_{3} ∨ y)) ∧ y)) ∨ (u ∧ (y∨
(((x_{1} ∨ (y ∨ x_{2})) ∧ (x_{3} ∨ y)) ∧ y)))) ∧ (x ∨ (((x_{1} ∧ y) ∨ (y∧
x_{2})) ∨ y)))) ∧ (((x ∧ y) ∨ (y ∧ (x ∨ y))) ∨ z)) = y.