Theorem MFL-7. Simple basis with Moufang-3.

\{ \begin{matrix}1 · x = x \\ x′ · x = 1 \\ Moufang-3 \end{matrix} \} ⇒ \{Moufang-2\}.

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

1 x = x 3,2 1 · x = x 5,4 x′ · x = 1 7,6 ((x · y) · x) · z = x · (y · (x · z)) 8 ((A · B) · C) · B ≠ A · (B · (C · B))

9  x′ · (x · (x′ · y)) = x′ · y  [4 → 6 :3, flip]
12,11  (x · 1) · y = x · y  [2 → 6 :3,3]
13  (x · (y · (x · 1))) · z = x · (y · (x · z))  [6 → 11 :7]
17  (x · x) · y = x · (x · y)  [11 → 6 :3]
19  ((x · y) · (x · 1)) · z = x · (y · (x · z))  [11 → 6 :12,12]
34,33  (x · (x · 1)) · y = x · (x · y)  [11 → 17 :12,12]
38,37  x′ · (x · 1) = 1  [4 → 9 :5]
43  ((x · y) · x)′ · (x · (y · (x · 1))) = 1  [6 → 37]
51  x · (x′ · (x · y)) = x · y  [37 → 13 :12, flip]
53  (x · (y · (y · (x · 1)))) · z = x · (y · (y · (x · z)))  [33 → 13 :34]
61  x′ · (x′′ · 1) = 1  [37 → 51 :38]
128,127 x′′ · (x′ · (x′ · (x′′ · y))) = y  [61 → 53 :38,3, flip]
144,143 x′′ · (x′ · (x′ · 1)) = x′ · 1  [37 → 127]
146,145 x′ · (x′′ · y) = y  [9 → 127 :128, flip]
148,147 x′ · 1 = x′  [4 → 127 :144]
182,181 x′ · (x · y) = y  [145 → 9 :146]
185  (x · y′) · z = y′ · ((y′′ · x) · (y′ · z))  [145 → 19 :148]
188  x′ · ((x′′ · y) · (x′ · z)) = (y · x′) · z  [flip 185]
205  ((x · y) · x)′′ = x · (y · (x · 1))  [43 → 181 :148]
224,223 x′′ = x  [4 → 181 :148]
225  x′ · ((x · y) · (x′ · z)) = (y · x′) · z  [188 :224]
237  (x · y) · x = x · (y · (x · 1))  [205 :224]
245  x · (x′ · y) = y  [223 → 181]
248,247 x · 1 = x  [223 → 147 :224]
249 x · x′ = 1 [223 → 4]
252,251 (x · y) · x = x · (y · x)  [237 :248]
261  (x · (y · x)) · z = x · (y · (x · z))  [13 :248]
285  x · ((x′ · y) · (x · z)) = (y · x) · z  [223 → 225 :224,224]
286  (x · y′) · y = x  [249 → 225 :248,182,224, flip]
291  (x · y) · z = y · ((y′ · x) · (y · z))  [flip 285]
295  (x · y) · y′ = x  [223 → 286]
307  x · (y · x)′ = y′  [181 → 295]
314,313 (x · y)′ = y′ · x′  [295 → 307, flip]

562  (x · (y · (x · z))) · z′ = x · (y · x)  [261 → 295]^{843  B · (((B′ · A) · (B · C)) · B) ≠ A · (B · (C · B))  [291 → 8 :252]}^{1465  (x · (y · z)) · (z′ · x) = x · (y · x)  [245 → 562 :314,224]}^{1791  (x · y) · (z · x) = x · ((y · z) · x)  [295 → 1465 :224]}^{1824,1823 x · (((x′ · y) · z) · x) = y · (z · x)  [245 → 1791, flip]}^{1837  A · (B · (C · B)) ≠ A · (B · (C · B))  [843 :1824,252]}^{1838  □  [1837,1]}

2