Theorem QLT-6. Another modularity axiom for quasilattices.

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

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

2 x ∧ x = x 4 x ∧ y = y ∧ x 6,5 (x ∧ y) ∧ z = x ∧ (y ∧ z) 8,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) 14 (x ∨ (y ∧ z)) ∧ (x ∨ y) = x ∨ (y ∧ z) 16 ((x ∨ y) ∧ z) ∨ y = ((z ∨ y) ∧ x) ∨ y 17 A ∧ (B ∨ (A ∧ C)) ≠ (A ∧ B) ∨ (A ∧ C)

18  (A ∧ B) ∨ (A ∧ C) ≠ A ∧ (B ∨ (A ∧ C))  [flip 17]
19  x ∧ (y ∧ z) = y ∧ (x ∧ z)  [4 → 5 :6]
21,20  x ∧ (x ∧ y) = x ∧ y  [2 → 5, flip]
22  x ∧ (y ∧ z) = y ∧ (z ∧ x)  [4 → 5]
26  x ∨ (y ∨ z) = y ∨ (x ∨ z)  [9 → 10 :11]
28,27  x ∨ (x ∨ y) = x ∨ y  [7 → 10, flip]
29  x ∨ (y ∨ z) = y ∨ (z ∨ x)  [9 → 10]
32  x ∨ (y ∨ z) = z ∨ (x ∨ y)  [flip 29]
35  x ∧ (y ∧ x) = x ∧ y  [4 → 20]
40,39  x ∨ (y ∨ x) = x ∨ y  [9 → 27]
44,43  x ∧ (y ∧ (x ∧ z)) = x ∧ (y ∧ z)  [35 → 5 :6,6, flip]
47  x ∨ (y ∨ (x ∨ z)) = x ∨ (y ∨ z)  [39 → 10 :11,11, flip]
52,51  (x ∧ (y ∨ z)) ∨ (x ∧ z) = x ∧ (z ∨ y)  [9 → 12]
59  (x ∧ ((y ∧ x) ∨ z)) ∨ (x ∧ y) = x ∧ ((y ∧ x) ∨ z)  [35 → 12]
65  (x ∧ (x ∨ y)) ∨ x = x ∧ (x ∨ y)  [2 → 12]
73  x ∧ (y ∧ z) = x ∧ (z ∧ y)  [4 → 19 :6]
79  x ∧ (y ∧ z) = z ∧ (y ∧ x)  [4 → 22]
94  x ∨ (y ∨ z) = x ∨ (z ∨ y)  [9 → 26 :11]
99  (x ∨ (y ∧ (z ∧ u))) ∧ (x ∨ u) = x ∨ (u ∧ (y ∧ z))  [22 → 14]
101  (x ∨ (y ∧ (z ∧ u))) ∧ (x ∨ (y ∧ z)) = x ∨ (y ∧ (z ∧ u))  [5 → 14 :6]
108  ((x ∧ y) ∨ z) ∧ (z ∨ x) = z ∨ (x ∧ y)  [9 → 14]
109  x ∧ (y ∧ ((x ∧ y) ∨ x)) = x ∧ y  [7 → 14 :6,8]
121  (x ∨ y) ∧ (x ∨ (y ∧ z)) = x ∨ (y ∧ z)  [4 → 14]
186  ((x ∨ y) ∧ (z ∧ u)) ∨ y = (((u ∧ z) ∨ y) ∧ x) ∨ y  [73 → 16]
197  ((x ∨ y) ∧ x) ∨ y = x ∨ y  [2 → 16 :11,8,11,8, flip]
203,202 ((x ∨ y) ∧ z) ∨ y = y ∨ ((z ∨ y) ∧ x)  [9 → 16, flip]
222,221 x ∨ ((y ∨ x) ∧ y) = y ∨ x  [197 :203]
226  x ∨ (((y ∧ z) ∨ x) ∧ u) = x ∨ ((u ∨ x) ∧ (z ∧ y))  [186 :203,203]
258  x ∨ ((x ∨ y) ∧ y) = y ∨ x  [9 → 221]

282,281 (x ∨ y) ∧ (y ∨ x) = x ∨ y  [221 → 14 :40,222]
288 x ∧ (y ∨ z) = x ∧ (z ∨ y) [221 → 12 :52,222]
330,329 x ∨ ((x ∨ y) ∧ y) = x ∨ y  [258 → 27 :40, flip]
392 x ∧ (y ∨ z) = (z ∨ y) ∧ ((y ∨ z) ∧ x) [281 → 79]
399,398 (x ∨ y) ∧ ((y ∨ x) ∧ z) = (x ∨ y) ∧ z  [281 → 5, flip]
400  (x ∨ y) ∧ z = z ∧ (y ∨ x)  [flip 392 :399]
401  x ∧ (y ∨ z) = (z ∨ y) ∧ x  [392 :399]
641  x ∨ (x ∧ y) = x ∧ (x ∨ y)  [401 → 65 :203,8]
695,694 x ∨ (y ∧ x) = x ∧ (x ∨ y)  [4 → 641]
699,698 (x ∧ y) ∨ x = x ∧ (x ∨ y)  [9 → 641]
705  x ∧ (y ∧ (x ∨ y)) = x ∧ y  [109 :699,44]
735  (x ∧ y) ∨ (y ∧ x) = x ∧ (y ∧ ((x ∧ y) ∨ y))  [35 → 694 :6]
744,743 (x ∧ y) ∨ y = y ∧ (y ∨ x)  [9 → 694]
745 (x ∧ y) ∨ (y ∧ x) = x ∧ (y ∧ (y ∨ x)) [735 :744,21]
854,853 x ∧ (y ∧ (y ∨ x)) = x ∧ y  [9 → 705]
872,871 (x ∧ y) ∨ (y ∧ x) = x ∧ y  [745 :854]
1269,1268 (x ∧ y) ∨ (z ∨ (y ∧ x)) = (x ∧ y) ∨ z  [871 → 47 :40, flip]
1271  x ∨ (y ∧ z) = x ∨ (z ∧ y)  [871 → 94 :872]
1272  x ∨ (y ∧ z) = (z ∧ y) ∨ x  [871 → 32 :1269]
1341  x ∧ (y ∨ (z ∧ u)) = x ∧ ((u ∧ z) ∨ y)  [1271 → 288]
1358  x ∧ ((y ∧ z) ∨ u) = x ∧ (u ∨ (z ∧ y))  [flip 1341]
1408  (C ∧ A) ∨ (A ∧ B) ≠ A ∧ (B ∨ (A ∧ C))  [1272 → 18]
1431  (x ∧ ((y ∧ x) ∨ z)) ∨ (y ∧ x) = x ∧ ((y ∧ x) ∨ z)  [4 → 59]
3062  ((x ∧ y) ∨ z) ∧ (z ∨ x) = (x ∧ y) ∨ z  [108 → 20 :282, flip]
3234,3233 (x ∨ y) ∧ (x ∨ ((x ∨ y) ∧ z)) = x ∨ ((x ∨ y) ∧ z)  [27 → 121]
5031 x ∨ ((x ∨ (y ∧ z)) ∧ y) = x ∨ (y ∧ z) [329 → 101 :3234,330]
5341,5340 (x ∧ (y ∨ z)) ∨ y = y ∨ ((x ∨ y) ∧ z)  [400 → 202]
5400,5399 (x ∧ y) ∨ (y ∧ ((y ∨ x) ∧ z))=y ∧ ((x ∧ y) ∨ z)  [1431 :5341,695,6]
7284,7283 x ∨ ((x ∨ y) ∧ (z ∧ y)) = x ∨ (y ∧ z)  [3062 → 226 :40,11,40, flip]
7333 x ∨ (y ∧ ((x ∨ y) ∧ z)) = x ∨ (y ∧ z) [99 → 5031 :28,7284]
7550,7549 (x ∧ y) ∨ (y ∧ z) = y ∧ ((x ∧ y) ∨ z) [743 → 7333 :6,21,5400, flip]
7555  A ∧ ((C ∧ A) ∨ B) ≠ A ∧ (B ∨ (A ∧ C))  [1408 :7550]
7556  □  [7555,1358]