Theorem LT-6. McKenzie’s basis for the variety generated by N_{5}. (Suggested by David Kelly.)

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

1 x = x 2 x ∨ x = x 5,4 x ∧ x = x 6 x ∨ y = y ∨ x 7 x ∧ y = y ∧ x 9,8 (x ∨ y) ∨ z = x ∨ (y ∨ z) 11,10 (x ∧ y) ∧ z = x ∧ (y ∧ z) 13,12 x ∧ (x ∨ y) = x 15,14 x ∨ (x ∧ y) = x 16 x ∧ (y ∨ (z ∧ (x ∨ u))) =

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

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

x ∧ (y ∨ (z ∧ (x ∨ u)))  [flip 16]

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

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

20 (x ∨ (y ∧ z)) ∧ (z ∨ (x ∧ y)) = (z ∧ (x ∨ (y ∧ z))) ∨ (x ∧ (y ∨ z)) 21 (x ∧ (y ∨ (z ∧ x))) ∨ (y ∧ (z ∨ x)) = (y ∨ (z ∧ x)) ∧ (x ∨ (y ∧ z))

[flip 20]

23 A ∧ ((B ∨ C) ∧ (B ∨ D)) ≠ (A ∧ ((B ∨ C) ∧ (B ∨ D))) ∧ ((A∧ (B ∨ (C ∧ D))) ∨ ((A ∧ C) ∨ (A ∧ D)))

24 A ∧ ((B ∨ C) ∧ ((B ∨ D) ∧ ((A ∧ (B ∨ (C ∧ D))) ∨ ((A ∧ C)∨

(A ∧ D))))) ≠ A ∧ ((B ∨ C) ∧ (B ∨ D)) [copy,23 :11,11, flip]

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

x ∨ (y ∧ (z ∨ (x ∧ u)))  [flip 19]
26  x ∧ (y ∨ x) = x  [6 → 12]
28  (x ∨ y) ∧ x = x  [7 → 12]
30  x ∨ (y ∨ z) = y ∨ (x ∨ z)  [6 → 8 :9]
32,31  x ∨ (x ∨ y) = x ∨ y  [2 → 8, flip]
33  x ∨ (y ∨ z) = y ∨ (z ∨ x)  [6 → 8]
36  x ∨ (y ∨ z) = z ∨ (x ∨ y)  [flip 33]
40,39  x ∨ (y ∧ x) = x  [7 → 14]
43  (x ∧ y) ∨ x = x  [6 → 14]
45  x ∨ ((x ∧ y) ∨ z) = x ∨ z  [14 → 8, flip]
48,47  x ∧ (y ∧ x) = x ∧ y  [14 → 26 :11]
50,49  x ∧ (y ∨ (z ∨ x)) = x  [8 → 26]
51  (x ∨ y) ∧ y = y  [7 → 26]
55  x ∨ (y ∨ x) = x ∨ y  [28 → 14 :9]
59  (x ∧ y) ∨ y = y  [6 → 39]
62,61  x ∨ ((y ∧ x) ∨ z) = x ∨ z  [39 → 8, flip]
63  (x ∨ y) ∧ (x ∧ z) = x ∧ z  [28 → 10, flip]
69  x ∧ (y ∧ z) = y ∧ (x ∧ z)  [7 → 10 :11]

71,70  x ∧ (x ∧ y) = x ∧ y  [4 → 10, flip]
76  x ∧ (y ∧ z) = y ∧ (z ∧ x)  [7 → 10]
77  x ∧ (y ∧ z) = z ∧ (x ∧ y)  [flip 76]
78  x ∨ (y ∧ (z ∧ x)) = x  [10 → 39]
83,82  (x ∧ (y ∧ z)) ∨ (x ∧ y) = x ∧ y  [10 → 43]
86  (x ∨ (y ∨ z)) ∧ z = z  [8 → 51]
90  (x ∧ (y ∧ z)) ∨ z = z  [10 → 59]
92  (x ∧ y) ∨ (y ∨ z) = y ∨ z  [59 → 8, flip]

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

x ∧ (y ∨ (z ∧ (x ∨ u)))  [7 → 17]

112 (x ∧ (y ∨ (z ∨ (x ∧ u)))) ∨ (x ∧ ((x ∧ (y ∨ z)) ∨ (u ∧ v))) =

x ∧ (y ∨ (z ∨ (u ∧ (x ∨ v))))  [8 → 17 :9]

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

x ∧ (y ∨ (z ∧ (x ∨ u)))  [7 → 17]

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

x ∧ (y ∨ ((z ∨ u) ∧ (x ∨ u)))  [51 → 17]

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

[26 → 17 :50]
167,166  x ∧ (y ∧ (z ∧ x)) = x ∧ (y ∧ z)  [10 → 47]
168  (x ∧ y) ∨ (y ∧ x) = x ∧ y  [47 → 39]
175,174  x ∧ (y ∧ (x ∧ z)) = x ∧ (y ∧ z)  [47 → 10 :11,11, flip]
189,188  x ∧ (y ∧ (z ∨ x)) = x ∧ y  [14 → 49 :11]
192  x ∧ (y ∨ (x ∨ z)) = x  [6 → 49]
210  (x ∨ y) ∧ (y ∨ x) = x ∨ y  [55 → 26]
242,241  x ∨ (y ∧ (x ∧ z)) = x  [43 → 19 :11,15,40,11,13]
273  x ∨ (y ∨ (z ∧ x)) = x ∨ y  [12 → 78 :9]
295  (x ∨ (y ∨ z)) ∧ y = y  [6 → 86]
305  (x ∧ y) ∨ (z ∨ y) = z ∨ y  [26 → 90]

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

[43 → 21 :48,11,11,11,189,11,83,11,11,11,167,242,11,5]

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

[21 → 51 :11]

481,480  x ∨ (y ∨ (x ∧ z)) = y ∨ x  [14 → 30, flip]
487  x ∨ ((y ∧ (x ∨ z)) ∨ z) = x ∨ z  [59 → 30, flip]
527  x ∨ (y ∨ z) = z ∨ (y ∨ x)  [6 → 33]
576,575  x ∧ (y ∧ (x ∨ z)) = x ∧ y  [45 → 192 :11]
578,577  ((x ∧ y) ∨ z) ∧ (x ∨ z) = (x ∧ y) ∨ z  [45 → 26]
626  x ∨ (y ∧ ((x ∧ z) ∨ (x ∧ u))) = x  [14 → 25 :40,13, flip]

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

(x ∧ y) ∨ (x ∧ (z ∨ (x ∧ (y ∧ u))))  [43 → 25 :11]

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

z))) ∧ ((x ∧ y) ∨ (x ∧ (z ∨ u)))  [flip 644]
824,823  (x ∨ y) ∧ (z ∧ (x ∧ u)) = z ∧ (x ∧ u)  [63 → 69, flip]
835  x ∧ (((x ∧ y) ∨ z) ∧ y) = x ∧ y  [28 → 69, flip]
840  (x ∨ (y ∧ z)) ∧ (y ∧ (z ∨ x)) = y ∧ (z ∨ x)  [409 :824]

1109  x ∧ (y ∧ (z ∨ (y ∧ x))) = x ∧ y  [168 → 49 :11]
1121,1120 ((x ∧ y) ∨ z) ∧ (u ∧ (y ∨ z)) = ((x ∧ y) ∨ z) ∧ u  [61 → 188]
1123,1122 (x ∨ y) ∧ (z ∧ (y ∨ x)) = (x ∨ y) ∧ z  [55 → 188]
1129,1128 (x ∨ y) ∧ (z ∧ (y ∨ (u ∨ x))) = (x ∨ y) ∧ z  [36 → 188]
1156,1155 (x ∧ y) ∨ (y ∧ (z ∨ x)) = y ∧ (z ∨ x)  [188 → 59]
1271  x ∧ (y ∨ z) = (z ∨ y) ∧ x  [210 → 77 :1123]
1272  (x ∨ y) ∧ z = z ∧ (y ∨ x)  [flip 1271]
1341,1340 (x ∨ (y ∧ z)) ∧ (u ∧ (z ∨ x)) = (x ∨ (y ∧ z)) ∧ u  [273 → 188]
1351 (x ∨ (y ∧ z)) ∧ y = y ∧ (z ∨ x) [840 :1341]

1916 A ∧ ((B ∨ C) ∧ ((B ∨ D) ∧ ((A ∧ D) ∨ ((A ∧ C) ∨ (A ∧ (B∨

(C ∧ D))))))) ≠ A ∧ ((B ∨ C) ∧ (B ∨ D))  [527 → 24]
1971,1970 (x ∧ y) ∨ (z ∨ (y ∧ (x ∨ u))) = z ∨ (y ∧ (x ∨ u))  [575 → 305]
2231,2230 (x ∧ y) ∨ (x ∧ (z ∨ (y ∨ u))) = x ∧ (z ∨ (y ∨ u))  [295 → 82]
2243,2242 (x ∧ (y ∧ z)) ∨ (x ∧ (y ∨ u)) = x ∧ (y ∨ u)  [63 → 82]
2247,2246 (x ∧ y) ∨ (x ∧ (z ∨ y)) = x ∧ (z ∨ y)  [51 → 82]

3172,3171 (x ∧ y) ∨ (x ∧ ((x ∧ (y ∧ z)) ∨ (y ∧ u))) = x ∧ y

[82 → 104 :48,175,2243,576]

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

x ∧ (z ∨ (y ∧ (x ∨ u)))  [55 → 112 :1971]
4053,4052 (x ∧ (y ∨ (x ∧ z))) ∨ (x ∧ z) = (y ∨ (x ∧ z)) ∧ x  [51 → 361]

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

[126 → 273 :9,1971,9,1971]

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

[flip 5139]

5530,5529 x ∨ (y ∧ ((y ∧ x) ∨ z)) = x ∨ (y ∧ (x ∨ z))

[128 → 487 :578,62, flip]

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

[626 → 26 :11]
6072,6071 x ∧ (y ∧ ((x ∧ z) ∨ (x ∧ u)))=y ∧ ((x ∧ z) ∨ (x ∧ u)) [626 → 51]
6739,6738 (x ∨ (y ∧ (x ∨ z))) ∧ y = y ∧ (x ∨ z)  [92 → 132 :4053,32]

6830,6829 x ∧ (y ∨ (x ∧ (y ∨ z))) = x ∧ (y ∨ z)

[132 → 132 :71,9,2247,5530,71,4053,6739,9,2247,5530, flip]

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

((x ∧ y) ∨ z) ∧ x  [132 → 104 :1121,3172,9, flip]
7082,7081 (x ∧ y) ∨ (x ∧ ((x ∧ y) ∨ z)) = x ∧ ((x ∧ y) ∨ z)  [835 → 82]

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

x ∧ (z ∨ (y ∧ (x ∨ u)))  [3853 :7082]

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

(x ∧ (z ∨ u)))  [686 :7082,11,6072]
8277 (x ∧ y) ∨ (y ∧ (z ∨ (y ∧ x))) = y ∧ (z ∨ (y ∧ x)) [1109 → 59]
9238,9237 ((x ∧ y) ∨ z) ∧ x = x ∧ (y ∨ z)  [6 → 1351]
9241,9240 x ∧ ((x ∧ y) ∨ z) = x ∧ (y ∨ z)  [1272 → 1351]
9397,9396 x ∧ ((y ∧ z) ∨ (y ∧ u)) = x ∧ (y ∧ (z ∨ (y ∧ u))) [6026 :9238, flip]
9603,9602 x ∧ (y ∨ (z ∧ (x ∨ u))) = x ∧ (y ∨ z) [7141 :9241,9241,9,481, flip]

9965,9964 ((x ∧ y) ∨ z) ∧ (x ∧ (y ∨ (z ∨ u))) = x ∧ (y ∨ z)

[6857 :9241,9397,9,2231,6830,9238]

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

((x ∧ y) ∨ z) ∧ (x ∧ (y ∨ (x ∧ (z ∨ u))))  [7189 :9397]

10762,10761 (x ∧ y) ∨ (z ∧ (u ∨ (z ∧ x))) = (x ∧ y) ∨ (z ∧ (u ∨ x))

[5159 :9603]

10966,10965 x ∧ (y ∨ (x ∧ z)) = x ∧ (y ∨ z)  [8277 :10762,1156, flip]

11208,11207 (x ∧ y) ∨ (x ∧ (z ∨ (y ∧ u))) = x ∧ (y ∨ z)

[10254 :10966,10966,9965]

11311,11310 x ∧ ((y ∧ z) ∨ (y ∧ u)) = x ∧ (y ∧ (z ∨ u))  [9396 :10966]

11477 A ∧ ((B ∨ C) ∧ (B ∨ D)) ≠ A ∧ ((B ∨ C) ∧ (B ∨ D))

[1916 :11208,11311,1129,167]

11478  □  [11477,1]