Theorem QLT-1. A new form of distributivity for QLT.

\{ \begin{matrix}QLT \\ x ∧ (y ∨ (x ∧ z)) = x ∧ (y ∨ z) \end{matrix} \} ⇒ \{x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)\}.

Proof (found by Otter 3.0.4 on gyro at 4.96 seconds).

2 x ∧ x = x 4 x ∧ y = y ∧ x 6,5 (x ∧ y) ∧ z = x ∧ (y ∧ z) 7 x ∨ x = x 9 x ∨ y = y ∨ x 11,10 (x ∨ y) ∨ z = x ∨ (y ∨ z) 12 (x ∧ (y ∨ z)) ∨ (x ∧ y) = x ∧ (y ∨ z) 15,14 (x ∨ (y ∧ z)) ∧ (x ∨ y) = x ∨ (y ∧ z) 17,16 x ∧ (y ∨ (x ∧ z)) = x ∧ (y ∨ z) 18 A ∧ (B ∨ C) ≠ (A ∧ B) ∨ (A ∧ C)

19  (A ∧ B) ∨ (A ∧ C) ≠ A ∧ (B ∨ C)  [flip 18]
20  x ∧ (y ∧ z) = y ∧ (x ∧ z)  [4 → 5 :6]
22,21  x ∧ (x ∧ y) = x ∧ y  [2 → 5, flip]
29,28  x ∨ (x ∨ y) = x ∨ y  [7 → 10, flip]
30  x ∨ (y ∨ z) = y ∨ (z ∨ x)  [9 → 10]
37,36  x ∧ (y ∧ x) = x ∧ y  [4 → 21]
41,40  x ∨ (y ∨ x) = x ∨ y  [9 → 28]
44  x ∧ (y ∧ (x ∧ z)) = x ∧ (y ∧ z)  [36 → 5 :6,6, flip]
49,48  x ∨ (y ∨ (x ∨ z)) = x ∨ (y ∨ z)  [40 → 10 :11,11, flip]
51,50  (x ∧ (y ∨ z)) ∨ (x ∧ z) = x ∧ (z ∨ y)  [9 → 12]
52  ((x ∨ y) ∧ z) ∨ (z ∧ x) = z ∧ (x ∨ y)  [4 → 12]
70  x ∧ (y ∧ z) = x ∧ (z ∧ y)  [4 → 20 :6]
100  (x ∨ ((x ∨ y) ∧ z)) ∧ (x ∨ y) = x ∨ ((x ∨ y) ∧ z)  [28 → 14]
104  (x ∨ (x ∧ y)) ∧ x = x ∨ (x ∧ y)  [7 → 14]
123  x ∨ (y ∨ z) = z ∨ (y ∨ x)  [9 → 30]
154,153 x ∧ (y ∨ (z ∧ x)) = x ∧ (y ∨ z)  [36 → 16 :17, flip]
159,158 x ∧ (y ∨ (z ∧ (x ∧ u))) = x ∧ (y ∨ (z ∧ u))  [20 → 16]
161,160 x ∧ (y ∨ (z ∨ (x ∧ u))) = x ∧ (y ∨ (z ∨ u))  [16 → 16 :17, flip]
167 x ∧ ((x ∧ y) ∨ y) = x ∧ y [7 → 16 :22, flip]
170,169 (x ∨ (y ∧ z)) ∧ y = y ∧ (x ∨ z)  [4 → 16]
172 x ∨ (x ∧ y) = x ∧ (x ∨ y) [104 :170, flip]
175,174 x ∨ ((x ∨ y) ∧ z) = (x ∨ y) ∧ (x ∨ z)  [100 :170, flip]

207 (x ∨ (y ∧ z)) ∧ (x ∨ ((y ∧ z) ∨ y)) = x ∨ (y ∧ z)

[14 → 167 :11,49,15]
213 x ∧ (y ∨ z) = x ∧ (z ∨ y) [123 → 167 :161,29,41]
230,229 x ∧ (y ∧ ((x ∧ z) ∨ z)) = y ∧ (x ∧ z)  [167 → 20, flip]
245 x ∨ (y ∧ x) = x ∧ (x ∨ y) [4 → 172]
250,249 (x ∧ y) ∨ x = x ∧ (x ∨ y)  [9 → 172]
254,253 (x ∨ (y ∧ z)) ∧ (x ∨ (y ∧ (y ∨ z))) = x ∨ (y ∧ z)  [207 :250]

269  (B ∧ A) ∨ (A ∧ C) ≠ A ∧ (B ∨ C)  [4 → 19]
276  (x ∨ y) ∧ z = z ∧ (y ∨ x)  [4 → 213]
280  x ∧ (y ∨ z) = (z ∨ y) ∧ x  [flip 276]
350  (x ∧ y) ∨ (y ∧ x) = y ∧ x  [36 → 245 :6,230,37]

356 x ∨ ((y ∧ z) ∨ (y ∧ (x ∨ z))) = x ∨ (y ∧ z)

[16 → 245 :11,11,250,254]
361,360 (x ∧ y) ∨ y = y ∧ (y ∨ x)  [9 → 245]
615 x ∨ (y ∧ z) = (y ∧ z) ∨ ((z ∧ y) ∨ x) [350 → 123]
621,620 (x ∧ y) ∨ ((y ∧ x) ∨ z) = (y ∧ x) ∨ z  [350 → 10, flip]
623 x ∨ (y ∧ z) = (z ∧ y) ∨ x [615 :621]
866,865 x ∧ ((y ∧ (x ∧ z)) ∨ u) = x ∧ ((y ∧ z) ∨ u)  [44 → 50 :159,51, flip]
869 x ∧ ((y ∧ x) ∨ z) = x ∧ (y ∨ z) [36 → 50 :154,51, flip]
880,879 (x ∧ y) ∨ (x ∧ (z ∨ y)) = x ∧ (y ∨ z)  [9 → 50]
884  x ∨ (y ∧ (z ∨ x)) = x ∨ (y ∧ z)  [356 :880]
957  (C ∧ A) ∨ (B ∧ A) ≠ A ∧ (B ∨ C)  [623 → 269]
977  (x ∧ y) ∨ ((x ∨ z) ∧ y) = y ∧ (x ∨ z)  [623 → 52]
1053,1052 x ∧ (y ∧ ((z ∧ x) ∨ u)) = x ∧ (y ∧ (z ∨ u))  [70 → 869 :6,866,6]
1114,1113 x ∨ (y ∧ z) = (x ∨ z) ∧ (x ∨ y)  [280 → 884 :175, flip]
1133,1132 x ∧ ((x ∨ y) ∧ (y ∨ z)) = x ∧ (y ∨ z)  [977 :1114,361,6,1053,29]
1134  A ∧ (C ∨ B) ≠ A ∧ (B ∨ C)  [957 :1114,361,6,1053,1133]
1135  □  [1134,213]