Theorem DUAL-BA-3. A self-dual 2-basis for BA (Pixley reduction).

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

By duality, it is sufficient to derive either of the absorption laws.

(Otter’s original proof, which was found with the standard strategy with max_weight=28 and max_mem=28000, is 816 steps and was found in a few hours. We asked Larry Wos to try some of his new methods for shortening proofs by using the resonance strategy [?], and he found the following 99-step proof.) Proof

(found by Otter 3.0.4 on gyro at 8.56 seconds).

1 (A + B) · B ≠ B 2 x · (y + z) = (x · y) + (x · z) 3 x + (y · z) = (x + y) · (x + z) 4 x + x′ = 1 5 x · x′ = 0 7 x · (y + z) = (x · y) + (x · z)

8 (x · y) + (x · z) = x · (y + z) [flip 7]

11,10 x + (y · z) = (x + y) · (x + z) 13,12 x + x′ = 1 15,14 x · x′ = 0 16 (x · y′) + ((x · x) + (y′ · x)) = x 17 ((x · y′) + ((x · x) + y′)) · ((x · y′) + ((x · x) + x)) = x

[copy,16 :11,11]

19 (x · x′) + ((x · y) + (x′ · y)) = y

21,20 (0 + ((x · y) + x′)) · (0 + ((x · y) + y)) = y  [copy,19 :15,11,11]

22 (x · y′) + ((x · y) + (y′ · y)) = x 23 ((x · y′) + ((x · y) + y′)) · ((x · y′) + ((x · y) + y)) = x

[copy,22 :11,11]

25 (x + y′) · ((x + x) · (y′ + x)) = x 27 (x + x′) · ((x + y) · (x′ + y)) = y

28 1 · ((x + y) · (x′ + y)) = y [copy,27 :13]

31,30 (x + y′) · ((x + y) · (y′ + y)) = x

33,32 ((x · y) + x) · ((x · y) + z) = x · (y + z)  [8 :11]

35,34 (x + ((y · z) + y)) · (x + ((y · z) + u)) = (x + y) · (x + (z + u))

[32 → 10 :11, flip]

37,36 (x + y) · (x + (y′ + z)) = (x + (0 + y)) · (x + (0 + z))

[5 → 34 :15, flip]

38 x · (y + (x′ + z)) = ((x · y) + (0 + x)) · ((x · y) + (0 + z))

[32 → 36]

40 ((x · y) + (0 + x)) · ((x · y) + (0 + z)) = x · (y + (x′ + z))

[36 → 32]

42,41 (x + y) · (x + y′) = x + 0  [14 → 10, flip]
44,43 x · (x′ + y) = (0 + x) · (0 + y)  [14 → 32 :15, flip]
45  ((x + y) · (x + z)) · (x + (y · z)′) = x + 0  [3 → 41]
47  (x + x) · 1 = x + 0  [4 → 41]
48  (x + (y + z)) · (x + (y + z′)) = x + (y + 0)  [41 → 3, flip]
51,50 (x · y) + 0 = (x · (y + y)) · 1  [4 → 45 :33, flip]
52  x + 0 = (x + x) · 1  [flip 47]
53  x · (y + x′) = (x · (y + y)) · 1  [32 → 41 :51]
54  (x · (y + y)) · 1 = x · (y + x′)  [flip 53]
56,55 (x · (x + x)) · 1 = x · 1  [4 → 53, flip]
57  x · ((y · z) + x′) = (x · (y · (z + z))) · 1  [3 → 54 :33, flip]
60  x · (y + (x′ + x′)) = (x · y) + (0 + 0)  [40 → 48]
61  x + ((y · z) + (0 + 0)) = (x + y) · (x + (z + (y′ + y′)))  [60 → 3]

63,62 (x + (0 + y)) · (x + (0 + (y′ + y′))) = x + (0 + (0 + 0))

[5 → 61 :37, flip]

64  x′ · (x′ + (x′ + x′)) = x′  [34 → 17 :33]
66  (x + y′) · (x + (y′ + (y′ + y′))) = x + y′  [64 → 3, flip]
68  1 · (x + (x′ + (x′ + x′))) = 1  [4 → 66 :13]
71,70 (1 · 1) + (0 + (0 + 0)) = 1  [38 → 68 :63]
72  (0 + (0 + x′)) · (0 + (0 + x′)) = x′  [14 → 20 :15]
74  0′ = (0 + 1) · (0 + 1)  [4 → 72 :13, flip]
76  0 · ((0 + 1) · (0 + 1)) = 0  [74 → 5]
78  (x + 0) · ((x + (0 + 1)) · (x + (0 + 1))) = x + 0  [76 → 3 :11, flip]

80 (x + (0 + ((y · z) + y′))) · (x + (0 + ((y · z) + z))) = x + z

[20 → 10, flip]

83,82 1 · ((1 · 1) + (0 + 1)) = 1  [52 → 70 :11,11,71]
84 (x + 1) · (x + ((1 · 1) + (0 + 1))) = x + 1 [82 → 3, flip]

86 (0 + 1) · (0 + (1 + ((1 · 1) + (0 + 1)))) = (1 · 1) + (0 + 1)

[82 → 20 :83,13]

88  1 · (x + ((1 · 1) + (0 + 1))) = (1 · x) + 1  [32 → 84]
89  x + ((1 · y) + 1) = (x + 1) · (x + (y + ((1 · 1) + (0 + 1))))  [88 → 3]
90  (x + 1) · (x + (y + ((1 · 1) + (0 + 1)))) = x + ((1 · y) + 1)  [flip 89]
92,91 (1 · 1) + (0 + 1) = 0 + ((1 · 1) + 1)  [86 → 90]
93  x′ · (x′ + (x + x)) = x′  [34 → 23 :33]
95  (x + y′) · (x + (y′ + (y + y))) = x + y′  [93 → 3, flip]
97  1 · (x + (x′ + (x + x))) = 1  [4 → 95 :13]
100,99 (1 · 1) · ((0 + 1) · (0 + (1 + 1))) = 1 · 1  [91 → 78 :51,56,92,35,51,56]
102,101 (0 + ((1 · 1) + 1)) · ((1 · 1) + (0 + (1 + 1))) = 1  [38 → 97 :92]

103 (x + (0 + 1)) · (x + (0 + (1 + 1))) = (x + (0 + 1)) · (x + (0 + 1))

[99 → 80 :100,13,11,92,102,11, flip]

106,105 (0 + 1) · (0 + (1 + 1)) = (0 + 1) · (0 + 1)

[99 → 20 :100,13,11,92,102, flip]
108,107 (0 + 1) · (0 + 1) = 1  [91 → 103 :102,92,92,35,106, flip]
109 (0 + 1) · (0 + (1 + 1)) = 1 [105 :108]
112,111 0 · 1 = 0  [76 :108]

114,113 0′ = 1  [74 :108]
115 (x + 0) · (x + 1) = x + 0 [111 → 3, flip]
118,117 0 + 1 = 1  [113 → 4]
119 1 · (0 + (1 + 1)) = 1 [109 :118]
122,121 1 · 1 = 1  [107 :118,118]
124,123 0 + (1 + 1) = 1 + 1  [91 :122,118,122, flip]
126,125 (x + 1) · (x + (1 + 1)) = x + 1  [119 → 3 :124, flip]
128,127 1 + 1 = 1  [101 :122,124,122,124,126]
129 1 + (0 + (0 + 0)) = 1 [70 :122]
132,131 x · (0 + x′) = (x · 0) · 1  [111 → 57 :128,112]
134,133 0 + 0 = 0  [111 → 50 :128,112,112]
136,135 1 + 0 = 1  [129 :134,134]

137 ((x · y) + z′) · ((x · (y + y)) · ((z′ + x) · (z′ + y))) = x · y

[10 → 25 :33,11]

139 1 · ((x · (y + y)) · (((x · y)′ + x) · ((x · y)′ + y))) = x · y [4 → 137]
142,141 1 · 0 = 0  [5 → 139 :44,42,134,114,15,114,42,136,112,15]
147 1 · (1 · (x′ + x′)) = x′ [12 → 28]
150,149 1′ = 0  [53 → 147 :44,118,132,142,112,112,142, flip]
152,151 (x + 0) · ((x + 1) · 1) = x  [149 → 30 :150,118]

154,153 (x + (y + z′)) · ((x + (y + z)) · (x + (z′ + z))) = x + y

[30 → 10 :11, flip]

155 1 · (((x + y′) · ((x + y) · ((y′ + y) + (y′ + y)))) · (x′ + x)) = x

[30 → 139 :11,33,31,11,154,31]

157 x · (y + x′) = (x · y) · 1 [151 → 57 :11,33,128,152]
160,159 x + 0 = x · 1  [151 → 50 :11,33,128,152]
162,161 (x · x) · 1 = x · 1  [4 → 157, flip]
164,163 (x · 1) · ((x + 1) · 1) = x  [151 :160]
166,165 (x · 1) · (x + 1) = x · 1  [115 :160,160]
168,167 (x + x) · 1 = x · 1  [52 :160, flip]
170,169 (x + y) · (x + y′) = x · 1  [41 :160]
171 x · (x′ · 1) = (0 + x) · 0 [159 → 43 :160,112]

173 (x · 1) · ((x + 1) + y) = (x · 1) · ((x · 1) + y)

[165 → 32 :166,11,33,128, flip]

176,175 (x · 1) · ((x · 1) · 1) = x  [159 → 173 :164,160, flip]
178,177 x + x = x  [167 → 175 :168,176, flip]
180,179 x · x = x  [161 → 175 :162,176, flip]
182,181 1 · (0 + x) = x  [155 :178,31,44,180]
184,183 x′ · (x′ + x) = x′  [93 :178]
188,187 (x · y) + x = x · (y + x)  [32 → 179, flip]
189 x′ + (x′ + x) = x′ + x [183 → 20 :184,13,118,182]
192,191 0 + (0 + x) = 0 + x  [189 → 38 :44,180,15,15,180, flip]
194,193 0 + x = x  [191 → 80 :192,21, flip]
195 ((x · y) + x′) · ((x · y) + y) = y [191 → 80 :194,194,194,194]
198,197 1 · x = x  [191 → 181 :194,194]

201 (x + y′) · (x + y) = x · 1

[191 → 153 :194,194,194,194,194,37,194,194,180,160]

203 x · (x′ · 1) = x · 0 [171 :194]
206,205 x · 1 = x  [4 → 201 :178,198, flip]
207  (x + y) · x = x  [203 → 3 :11,160,206,206,170,206]
209  ((x + y) · (x + z)) · x = x  [3 → 207]
211  x + 1 = 1  [205 → 195 :13,206,198]
214,213 x · (y + x) = x  [211 → 2 :206,206,188, flip]
219  x · (y · x) = y · x  [195 → 209]
221  (x + y) · y = y  [213 → 219 :214]
223  □  [221,1]