Problem QLT-5. Self-dual modularity axiom for quasilattices.

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

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

(Otter’s original proof, which was found with the standard strategy with max_weight=23 and the flag control_memory, is 125 steps and was found in 914 seconds. Larry Wos, starting with that proof, found the following 30-step proof by using the resonance strategy [?]).

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

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

20  (A ∧ B) ∨ (A ∧ C) ≠ A ∧ (B ∨ (A ∧ C))  [flip 19]
22  x ∨ (y ∨ ((x ∨ y) ∧ x)) = x ∨ y  [4 → 14 :13,5]
31,30  x ∨ (((y ∨ x) ∧ y) ∨ y) = y ∨ x  [2 → 22 :13]
38  (x ∧ y) ∨ (x ∧ (y ∨ z)) = x ∧ (y ∨ z)  [14 → 30 :5,10,15]
46  (x ∧ (y ∨ z)) ∨ (x ∧ z) = x ∧ (y ∨ z)  [30 → 14 :31]
50  (x ∨ y) ∧ (x ∨ (y ∧ z)) = x ∨ (y ∧ z)  [16 → 6, flip]
53,52  (x ∨ y) ∧ (y ∨ (x ∧ z)) = y ∨ (x ∧ z)  [2 → 50]
78  (x ∨ (y ∧ z)) ∧ (x ∨ z) = x ∨ (z ∧ y)  [6 → 16]
79  (x ∧ y) ∨ (y ∧ (x ∨ z)) = y ∧ (x ∨ z)  [6 → 38]
100  x ∨ (y ∧ z) = (x ∨ (z ∧ y)) ∧ (x ∨ y)  [flip 78]
219  x ∧ (x ∧ y) = x ∧ y  [4 → 7, flip]
231  (x ∨ (y ∧ z)) ∧ (x ∨ z) = x ∨ (y ∧ z)  [6 → 100, flip]
238,237 (x ∨ (y ∧ z)) ∧ (z ∨ x) = x ∨ (y ∧ z)  [2 → 231]
283,282 x ∧ (y ∧ x) = x ∧ y  [6 → 219]
284  (x ∧ (y ∨ (x ∧ z))) ∨ (x ∧ z) = x ∧ (y ∨ (x ∧ z))  [219 → 46]
292  (x ∨ (y ∧ z)) ∧ ((x ∨ z) ∧ u) = (x ∨ (y ∧ z)) ∧ u  [231 → 7, flip]
300  (x ∨ (y ∧ z)) ∧ ((z ∨ x) ∧ u) = (x ∨ (y ∧ z)) ∧ u  [2 → 292]

382 ((x ∧ y) ∨ (z ∧ u)) ∧ (y ∨ u) = (x ∧ y) ∨ (z ∧ u)

[237 → 300 :238, flip]

438 (x ∨ y) ∧ ((z ∧ x) ∨ (u ∧ y)) = (z ∧ x) ∨ (u ∧ y) [6 → 382]
441,440 (x ∨ y) ∧ ((z ∧ y) ∨ (u ∧ x)) = (z ∧ y) ∨ (u ∧ x)  [2 → 438]

447 (x ∧ y) ∨ (z ∧ (u ∧ (x ∨ y))) = (x ∨ y) ∧ ((z ∧ u) ∨ (x ∧ y))

[7 → 18]

448 x ∧ (y ∨ x) = x ∨ (y ∧ x) [79 → 18 :53]

452 (x ∨ y) ∧ ((z ∧ u) ∨ (x ∧ y)) = (x ∧ y) ∨ (z ∧ (u ∧ (x ∨ y)))

[flip 447]

456,455 x ∨ (y ∧ x) = x ∧ (x ∨ y)  [2 → 448, flip]

463,462 (x ∧ y) ∨ (z ∧ (u ∧ (x ∨ y))) = (x ∨ y) ∧ ((x ∧ y) ∨ (z ∧ u))

[2 → 452, flip]

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

[455 → 18 :283,463,441,456,283,8]

520 (x ∧ y) ∨ (x ∧ z) = x ∧ ((x ∨ y) ∧ (z ∨ (x ∧ y))) [6 → 474]
524,523 (x ∧ y) ∨ (x ∧ z) = x ∧ ((x ∨ z) ∧ (y ∨ (x ∧ z)))  [2 → 520]
527,526 x ∧ ((x ∨ y) ∧ (z ∨ (x ∧ y))) = x ∧ (z ∨ (x ∧ y))  [284 :524,13,10]
532  A ∧ (B ∨ (A ∧ C)) ≠ A ∧ (B ∨ (A ∧ C))  [20 :524,527]
533  □  [532,3]