Theorem QLT-3. A self-dual form of distributivity for QLT.

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

{x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)}.

(Otter’s original proof, which was found with the standard strategy with

max_weight=24, change_limit_after=50, and new_max_weight=17, is 183

steps and was found in about 15 minutes. We asked Larry Wos to try some of his new methods for shortening proofs by using the resonance strategy [?], and he found the following 113-step proof.)

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

3,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) 15,14 (x ∨ (y ∧ z)) ∧ (x ∨ y) = x ∨ (y ∧ z) 16 (((x ∧ y) ∨ z) ∧ y) ∨ (z ∧ x) = (((x ∨ y) ∧ z) ∨ y) ∧ (z ∨ x) 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]
23  x ∧ (y ∧ z) = y ∧ (z ∧ x)  [4 → 5]
26  x ∧ (y ∧ z) = z ∧ (x ∧ y)  [flip 23]
30,29 x ∧ (y ∧ x) = y ∧ x  [2 → 20, flip]
33,32 x ∧ (y ∧ (x ∧ z)) = x ∧ (y ∧ z)  [20 → 21]
57 x ∨ (y ∨ z) = y ∨ (x ∨ z) [9 → 10 :11]
59,58 x ∨ (x ∨ y) = x ∨ y  [7 → 10, flip]
60  x ∨ (y ∨ z) = y ∨ (z ∨ x)  [9 → 10]
63  x ∨ (y ∨ z) = z ∨ (x ∨ y)  [flip 60]
67,66 x ∨ (y ∨ x) = y ∨ x  [7 → 57, flip]
70,69 x ∨ (y ∨ (x ∨ z)) = x ∨ (y ∨ z)  [57 → 58]
74  x ∨ (y ∨ z) = z ∨ (y ∨ x)  [9 → 60]
80  x ∨ (y ∨ (z ∨ u)) = y ∨ (u ∨ (x ∨ z))  [57 → 63 :11]
81  x ∨ (y ∨ (z ∨ u)) = z ∨ (x ∨ (u ∨ y))  [flip 80]
94  (x ∧ (y ∨ (z ∨ u))) ∨ (x ∧ u) = x ∧ (u ∨ (y ∨ z))  [60 → 12]
99  (x ∧ (y ∧ (z ∨ u))) ∨ (x ∧ (y ∧ z)) = x ∧ (y ∧ (z ∨ u))  [5 → 12 :6,6]
101  ((x ∨ y) ∧ z) ∨ (z ∧ x) = z ∧ (x ∨ y)  [4 → 12]
103  x ∨ (y ∨ ((x ∨ y) ∧ x)) = x ∨ y  [2 → 12 :11,3]
105  (x ∧ ((y ∧ x) ∨ z)) ∨ (y ∧ x) = x ∧ ((y ∧ x) ∨ z)  [29 → 12]
110,109 (x ∧ (y ∨ z)) ∨ (y ∧ x) = x ∧ (y ∨ z)  [4 → 12]

114,113 (x ∧ y) ∨ (x ∧ (y ∨ z)) = x ∧ (y ∨ z)  [9 → 12]
122 ((x ∧ y) ∨ z) ∧ (z ∨ x) = z ∨ (x ∧ y) [9 → 14]
126,125 (x ∨ (y ∧ z)) ∧ (y ∨ x) = x ∨ (y ∧ z)  [9 → 14]
127 (x ∨ (x ∧ y)) ∧ x = x ∨ (x ∧ y) [7 → 14]
130,129 (x ∨ y) ∧ (x ∨ (y ∧ z)) = x ∨ (y ∧ z)  [4 → 14]
134 ((x ∨ y) ∧ x) ∨ (y ∧ x) = ((x ∧ y) ∨ x) ∧ (y ∨ x) [2 → 16 :8]
136  (x ∧ ((y ∧ x) ∨ z)) ∨ (z ∧ y) = (((y ∨ x) ∧ z) ∨ x) ∧ (z ∨ y) [4 → 16]
147  (x ∧ (y ∧ (z ∨ u))) ∨ (x ∧ (y ∧ u)) = x ∧ (y ∧ (z ∨ u))  [66 → 99 :67]
150  (x ∧ (y ∨ z)) ∨ (x ∧ ((y ∨ z) ∧ y)) = x ∧ (y ∨ z)  [2 → 99 :3]
163,162 ((x ∨ y) ∧ z) ∨ (z ∧ y) = z ∧ (x ∨ y)  [66 → 101 :67]
165,164 (x ∧ y) ∨ (y ∧ x) = y ∧ x  [7 → 101 :8]
166  (((x ∧ y) ∨ z) ∧ y) ∨ (x ∧ y) = y ∧ ((x ∧ y) ∨ z)  [29 → 101]
170  ((x ∨ y) ∧ z) ∨ (x ∧ z) = z ∧ (x ∨ y)  [4 → 101]
173,172 ((x ∨ y) ∧ x) ∨ x = x ∧ (x ∨ y)  [2 → 101]
175,174 (x ∨ y) ∧ (y ∨ x) = x ∨ y  [94 → 101 :67,59,67,67,3]
176 (x ∧ y) ∨ ((y ∨ z) ∧ x) = x ∧ (y ∨ z) [9 → 101]
179,178 x ∨ (y ∨ ((y ∨ x) ∧ x)) = y ∨ x  [66 → 103 :11,70,67]
187,186 ((x ∨ y) ∧ x) ∨ (x ∨ y) = x ∨ y  [63 → 103]
193,192 x ∨ (y ∨ (z ∧ (z ∨ x))) = y ∨ (z ∨ x)  [103 → 81 :173, flip]
196 (x ∧ ((y ∧ x) ∨ z)) ∨ (x ∧ y) = x ∧ ((y ∧ x) ∨ z) [4 → 105]
199,198 (x ∧ y) ∨ (y ∧ ((x ∧ y) ∨ z)) = y ∧ ((x ∧ y) ∨ z)  [9 → 105]
205,204 (x ∧ y) ∨ (y ∧ (x ∨ z)) = y ∧ (x ∨ z)  [4 → 113]
208  (x ∧ y) ∨ (x ∧ (z ∨ y)) = x ∧ (z ∨ y)  [66 → 113 :67]
212  (x ∧ y) ∨ ((x ∧ (y ∨ z)) ∨ u) = (x ∧ (y ∨ z)) ∨ u  [113 → 10, flip]
214  ((x ∧ y) ∨ z) ∧ (z ∨ y) = z ∨ (x ∧ y)  [29 → 122 :30]
216  ((x ∧ y) ∨ z) ∧ (x ∨ z) = z ∨ (x ∧ y)  [9 → 122]
217  ((x ∧ y) ∨ x) ∧ x = x ∨ (x ∧ y)  [7 → 122]
224  x ∨ (y ∧ (x ∨ y)) = x ∨ y  [122 → 16 :11,110,67,187,3]
227,226 ((x ∧ y) ∨ z) ∧ (z ∨ x) = (x ∧ y) ∨ z  [122 → 12 :11,179, flip]
232  (x ∨ y) ∧ (y ∨ (x ∧ z)) = y ∨ (x ∧ z)  [9 → 129]
234  (x ∨ y) ∧ (x ∨ (z ∧ y)) = x ∨ (z ∧ y)  [29 → 129 :30]
236  ((x ∧ y) ∨ x) ∧ (x ∧ (y ∨ z)) = x ∧ (y ∨ z)  [113 → 129 :114]
243,242 (x ∧ y) ∨ x = x ∨ (y ∧ x)  [127 → 134 :6,30,11,165,22,3, flip]
247,246 x ∨ (y ∧ x) = x ∧ (x ∨ y)  [4 → 134 :163,243,126, flip]
254 x ∧ ((x ∨ y) ∧ (y ∨ z)) = x ∧ (y ∨ z) [236 :243,247,6,33]
257,256 x ∨ (x ∧ y) = (x ∨ y) ∧ x  [217 :243,247,6,30, flip]
265,264 (x ∧ y) ∨ x = x ∧ (x ∨ y)  [242 :247]

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

[4 → 136]
275  (x ∧ (y ∧ (z ∨ u))) ∨ (y ∧ (x ∧ u)) = y ∧ (x ∧ (z ∨ u))  [20 → 147]
287  (x ∧ (y ∨ z)) ∨ (x ∧ ((z ∨ y) ∧ y)) = x ∧ (y ∨ z)  [9 → 150]
291  ((x ∨ y) ∧ z) ∨ (y ∧ z) = z ∧ (x ∨ y)  [4 → 162]
294,293 ((x ∨ y) ∧ y) ∨ y = y ∧ (x ∨ y)  [2 → 162]
296,295 (x ∧ y) ∨ ((z ∨ y) ∧ x) = x ∧ (z ∨ y)  [9 → 162]
304  x ∨ (y ∧ z) = (y ∧ z) ∨ ((z ∧ y) ∨ x)  [164 → 74]

307,306 (x ∧ y) ∨ (z ∨ (y ∧ x)) = z ∨ (y ∧ x)  [164 → 57, flip]
309,308 (x ∧ y) ∨ ((y ∧ x) ∨ z) = (y ∧ x) ∨ z  [164 → 10, flip]
311  x ∨ (y ∧ z) = (z ∧ y) ∨ x  [304 :309]
314  (((x ∧ y) ∨ z) ∧ y) ∨ (y ∧ x) = y ∧ ((x ∧ y) ∨ z)  [4 → 166]
316  (x ∧ y) ∨ ((x ∨ z) ∧ y) = y ∧ (x ∨ z)  [9 → 170]
322  (x ∨ y) ∧ (z ∧ (y ∨ x)) = z ∧ (y ∨ x)  [174 → 26, flip]
330,329 ((x ∨ y) ∧ y) ∨ (y ∨ x) = x ∨ y  [174 → 176 :175]
333 x ∨ (y ∨ (z ∧ (x ∨ z))) = y ∨ (x ∨ z) [178 → 81 :294, flip]
359,358 x ∧ ((y ∧ x) ∨ x) = x ∧ (y ∨ x)  [136 → 196 :294,6,175, flip]
368  ((x ∧ y) ∨ y) ∧ (y ∧ (x ∨ z)) = y ∧ (x ∨ z)  [204 → 129 :205]
370  x ∧ ((y ∨ z) ∧ ((y ∧ x) ∨ x)) = x ∧ (y ∨ z)  [204 → 14 :6,205]
391,390 ((x ∧ y) ∨ z) ∧ (z ∨ y) = (x ∧ y) ∨ z  [214 → 113 :330, flip]
393  x ∧ ((y ∨ z) ∧ (y ∨ (x ∧ (y ∨ z)))) = x ∧ (y ∨ z)  [204 → 216 :6,110]
397  x ∧ (y ∨ (z ∧ (z ∨ x))) = x ∧ (y ∨ z)  [162 → 216 :11,247,6,130,296]
402  ((x ∧ y) ∨ z) ∧ (x ∨ z) = (x ∧ y) ∨ z  [216 → 208 :330, flip]
407,406 (x ∧ y) ∨ y = y ∧ (x ∨ y)  [198 → 224 :359, flip]
411,410 x ∧ ((y ∨ z) ∧ (y ∨ x)) = x ∧ (y ∨ z)  [370 :407,33]
413,412 x ∧ ((y ∨ x) ∧ (y ∨ z)) = x ∧ (y ∨ z)  [368 :407,6,33]

440,439 x ∧ ((x ∨ y) ∧ ((y ∧ x) ∨ z)) = x ∧ ((y ∧ x) ∨ z)

[198 → 232 :247,6,33,199]

446,445 (x ∨ y) ∧ (y ∨ (z ∧ (x ∨ y))) = y ∨ (z ∧ (x ∨ y))  [66 → 234]
448,447 (x ∨ y) ∧ (x ∨ (z ∧ (x ∨ y))) = x ∨ (z ∧ (x ∨ y))  [58 → 234]
449  x ∧ (y ∨ (x ∧ (y ∨ z))) = x ∧ (y ∨ z)  [393 :448]
457  x ∧ ((y ∧ x) ∨ (x ∧ z)) = (y ∧ x) ∨ (x ∧ z)  [246 → 232 :6,440]
480,479 x ∧ ((x ∨ y) ∧ (z ∨ (u ∨ y))) = x ∧ (z ∨ (u ∨ y))  [192 → 254 :193]

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

[9 → 268, flip]

539,538 (x ∧ y) ∨ (z ∧ (x ∨ z)) = (x ∧ y) ∨ z

[226 → 287 :257,11,247,67,15,227]

589  (C ∧ A) ∨ (A ∧ B) ≠ A ∧ (B ∨ C)  [311 → 19]
602  x ∧ (y ∨ (x ∧ (z ∨ y))) = x ∧ (z ∨ y)  [322 → 316 :407,6,446,6,175]
668,667 (x ∨ y) ∧ ((z ∧ y) ∨ x) = (z ∧ y) ∨ x  [4 → 390]
673,672 (x ∧ y) ∨ ((z ∨ y) ∧ z) = (x ∧ y) ∨ z  [390 → 291 :11,257,59,668]

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

[390 → 287 :257,11,247,67,15,391]

698,697 (x ∨ y) ∧ (z ∧ ((x ∧ u) ∨ y)) = z ∧ ((x ∧ u) ∨ y)  [402 → 26, flip]
704,703 (x ∧ y) ∨ (y ∨ z) = (y ∨ z) ∧ (x ∨ (y ∨ z))  [406 → 212 :539,407]
712,711 x ∧ (y ∧ (z ∨ (x ∧ y))) = x ∧ (y ∧ (z ∨ y))  [234 → 410 :6,6]
723 (x ∨ y) ∧ (z ∧ (x ∨ z)) = (x ∨ y) ∧ z [410 → 275 :3,165, flip]
765,764 x ∧ (y ∨ (x ∨ z)) = x ∧ ((x ∨ z) ∧ (y ∨ x))  [449 → 397 :6,712,480,6]

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

[9 → 532]
785 (x ∧ y) ∨ (z ∧ (u ∧ (x ∨ u))) = (x ∧ y) ∨ (z ∧ u) [5 → 538 :712]

796,795 x ∧ ((y ∨ x) ∧ ((y ∧ z) ∨ u)) = x ∧ ((y ∧ z) ∨ u)

[538 → 410 :6,698,411,6, flip]

807  x ∧ (((y ∨ z) ∧ x) ∨ z) = x ∧ (y ∨ z)  [311 → 602]
867,866 x ∨ ((y ∧ x) ∨ z) = (x ∨ z) ∧ (y ∨ (x ∨ z))  [676 → 333 :704]
928,927 (x ∧ y) ∨ (z ∧ (u ∧ (x ∨ z))) = (x ∧ y) ∨ (u ∧ z)  [20 → 785]

940,939 (x ∨ y) ∧ (((x ∨ z) ∧ y) ∨ z) = (x ∨ y) ∧ ((x ∧ y) ∨ z)

[779 → 807 :11,265,867,480,765,928,673, flip]

944,943 x ∧ ((y ∧ x) ∨ z) = x ∧ (y ∨ z)  [723 → 807 :6,940,796,6,413]
951,950 (x ∧ y) ∨ (y ∧ z) = y ∧ (x ∨ (y ∧ z))  [457 :944, flip]
952  x ∧ (y ∨ (x ∧ z)) = x ∧ (z ∨ y)  [314 :951,11,307,944]
957  A ∧ (C ∨ (A ∧ B)) ≠ A ∧ (B ∨ C)  [589 :951]
958  □  [957,952]