Theorem DUAL-BA-2. A basis for Boolean algebra (to show dependence).

\{ \begin{matrix}(x + y) · y = y \\ x · (y + z) = (x · y) + (x · z) \\ x + x′ = 1 \\ p(x, y, z) = (x · y′) + ((x · z) + (y′ · z)) \\ p(x, x, y) = y \\ p(x, y, y) = x \\ p(x, y, x) = x \end{matrix} \} .

We derive the “other half” of the 6-basis. The constant 0 is not explicit, so instead of x · x′ = 0, we show the existence of an element with that property, that is, x · x′ = y · y′.

(Otter’s original proof, which was found with the standard strategy with max_weight=28, is 135 steps and was found in 92 seconds. Larry Wos, starting with that proof, found the following 78-step proof by using the resonance strategy [?]).

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

1 x = x 2 A + (B · C) = (A + B) · (A + C), (A · B) + B = B,

B · B′ = A · A′ → □

3 (x + y) · y = y 5 x · (y + z) = (x · y) + (x · z)

7,6 (x · y) + (x · z) = x · (y + z) [flip 5]

9,8 x + x′ = 1 11,10 p(x, y, z) = (x · y′) + ((x · z) + (y′ · z)) 12 p(x, x, y) = y

13 (x · x′) + ((x · y) + (x′ · y)) = y [copy,12 :11]

15 p(x, y, y) = x

17,16  (x · y′) + ((x · y) + (y′ · y)) = x  [copy,15 :11]
22,21  1 · x′ = x′  [8 → 3]
23  x′ + (1 · y) = 1 · (x′ + y)  [21 → 6]
26,25  x + ((y + x) · z) = (y + x) · (x + z)  [3 → 6]
28,27  ((x + y) · z) + y = (x + y) · (z + y)  [3 → 6]
29  (x · (y + z)) · (x · z) = x · z  [6 → 3]
31  1 · (x′ + y′) = x′ + y′  [21 → 23, flip]
33  (x + y) · (y + y) = y + y  [3 → 25, flip]
35  ((x + y) · (z + y)) · y = y  [27 → 3]
38,37  1 · 1 = 1  [8 → 31 :9]
43  ((x + y′) · 1) · y′ = y′  [8 → 35]
45  1 · (x′ + 1) = x′ + 1  [37 → 23, flip]
48,47  (1 · (x + 1)) · 1 = 1  [37 → 29 :38]
49  (1 · x) + 1 = 1 · (x + 1)  [37 → 6]
52,51  1′ + (1 + (1′ · 1)) = 1  [37 → 13 :22]
55  x′ + (((y + x′) · x) + (x′ · x)) = y + x′  [3 → 16]

57  x′ · (x′ + (x + x)) = x′  [6 → 16 :7]

60,59 (x · y) + ((x · z) + (z′ · z)) = x · (y + ((x · z) + (z′ · z)))

[16 → 27 :17]
61  x · ((x · y) + (y′ · y)) = (x · y) + (y′ · y)  [16 → 3]
63  x · (y′ + ((x · y) + (y′ · y))) = x  [16 :60]
71  (1 · (x + 1)) · (1 + 1) = 1 + 1  [49 → 33]
74,73  (x′ · y) + x′ = x′ · (y + (x′ + (x + x)))  [57 → 6]
76,75  1 · (x + 1) = 1  [47 → 63 :52,48, flip]
78,77  1 + 1 = 1  [71 :76,76, flip]
82,81  x′ + 1 = 1  [45 :76, flip]
84,83  1′ · 1 = 1′  [77 → 57 :82]
86,85  (x + 1′) · 1 = x + 1′  [83 → 55 :28,9,26,82]
87  x · (1′ + ((x · 1) + 1′)) = x  [83 → 63]
90,89  x · ((x · 1) + 1′) = (x · 1) + 1′  [83 → 61 :84]
92,91  1′ + 1′ = 1′  [83 → 73 :78,82,78,84]
93  1′ · (x + 1′) = 1′ · (x + 1)  [83 → 59 :84,92,74,78,82,84,84,92, flip]
98,97  1′ + (x + 1′) = x + 1′  [85 → 25 :82,86]
100,99  (x · 1) + 1′ = x  [87 :98,90]
101  x · x = x  [89 :100,100]
104,103 x + 1 = 1  [3 → 99 :9, flip]
105 1′ · (x + 1′) = 1′ [93 :104,84]
108,107 1′ + x = x  [99 → 97 :100]
110,109 x · 1 = x  [99 → 85 :100]
112,111 x · 1′ = 1′  [99 → 43 :110]
114,113 x + 1′ = x  [99 :110]
116,115 1′ · x = 1′  [105 :114]
118,117 (x · y) + x = x · (y + x)  [101 → 6]
120,119 x + (x · y) = x · (x + y)  [101 → 6]
126,125 x · (y + x) = x  [109 → 6 :118,104,110]
127 x · (x + y) = x · (1 + y) [109 → 6 :120]
129,128 (x · y) + x = x  [117 :126]
130  x · x′ = 1′  [111 → 13 :112,114,114]
133  1′ = x · x′  [flip 130]
134  x′ · x = 1′  [61 → 115 :116,108]
138  x · ((y + x) + z) = x · (x + z)  [125 → 6 :120, flip]
140  x · (1 + x′) = x  [8 → 127 :110, flip]
143,142 x′′ = x  [130 → 13 :114,7,9,110, flip]
145,144 (x · y) + (x′ · y) = y  [130 → 13 :108]
148  x · x′ = y · y′  [133 → 133]
151  x′ · (y + x) = x′ · y  [134 → 6 :114, flip]
154,153 x′ · (x + y) = x′ · y  [134 → 6 :108, flip]
161 (x · (1 + y)) + (x′ · y) = x + y [127 → 144 :154]
167,166 1 + x = 1  [140 → 144 :143,126,9,143, flip]
169,168 x + (x′ · y) = x + y  [161 :167,110]
171,170 x · (x + y) = x  [127 :167,110]

173  x · ((y + x) + z) = x  [138 :171]
176,175 x + (x · y) = x  [119 :171]
180,179 x′ · ((y + x) + z) = x′ · (y + z)  [151 → 6 :7, flip]
189  x + (x + y) = x + y  [153 → 168 :169, flip]
197  (x + y) + z = y + (x + z)  [173 → 144 :180,169, flip]
200,199 (x · y) + y = y  [144 → 189 :145]
201  A + (B · C) = (A + B) · (A + C) → □  [2 :200 :1,148]
206  x + ((y · x) + z) = x + z  [199 → 197, flip]
213,212 x + (y · x) = x  [113 → 206 :114]
216  x + (y · (x + z)) = x + (y · z)  [6 → 206]
218  (x · y) + (y · z) = y · ((x · y) + z)  [212 → 25 :213]
220  (x · y) + (z · x) = x · (y + (z · x))  [212 → 27 :213]
223,222 x + ((x + y) · z) = (x + y) · (x + z)  [170 → 218 :171]
226 x · y = y · x [218 → 220 :129,176]
236,235 x + (y · z) = (x + z) · (x + y)  [226 → 216 :223, flip]
239  (A + C) · (A + B) = (A + B) · (A + C) → □  [201 :236]
240  □  [239,226]