Theorem MFL-2. Moufang-2 ⇒ Moufang-3 in loops.

\{ \begin{matrix}loop \\ ((x · y) · z) · y = x · (y · (z · y)) \end{matrix} \} ⇒ \{((x · y) · x) · z = x · (y · (x · z))\}.

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

3,2 1 · x = x 4 x · 1 = x 8 x\(x · y) = y 11,10 (x/y) · y = x 12 (x · y)/y = x 14 x · R(x) = 1 18 ((x · y) · z) · y = x · (y · (z · y)) 20 ((A · B) · A) · C ≠ A · (B · (A · C))

30,29  x\1 = R(x)  [14 → 8]
32,31  x\x = 1  [4 → 8]
37  (x/y)\x = y  [10 → 8]
49  x · (R(x) · (y · R(x))) = y · R(x)  [14 → 18 :3, flip]
53,52  (x · y) · x = x · (y · x)  [2 → 18 :3]
54  x · (y · (R(x · y) · y)) = y  [14 → 18 :3, flip]
61  (A · (B · A)) · C ≠ A · (B · (A · C))  [20 :53]
68  x · (R(x) · x) = x  [14 → 52 :3, flip]
77,76  (x · (y · x))/x = x · y  [52 → 12]
84  R(x) · x = 1  [68 → 8 :32, flip]
93,92  R(R(x)) = x  [84 → 8 :30]
96  x · (R(x) · y) = y  [10 → 49 :11]
98  R(x) · (x · y) = y  [92 → 96]
102  x · (y · ((R(x · y) · z) · y)) = z · y  [96 → 18, flip]
109,108 x\y = R(x) · y  [96 → 8]
114  R(x/y) · x = y  [37 :109]
118  x/(y · x) = R(y)  [98 → 12]
136  (x · y) · z = R(z/x) · (z · (y · z))  [114 → 18]
138  R(x/y) · (x · (z · x)) = (y · z) · x  [flip 136]
154  x · R(y · x) = R(y)  [54 → 118 :77]
165,164 x/y = x · R(y)  [114 → 154 :93, flip]
172,171 R(x · R(y)) = y · R(x)  [10 → 154 :165, flip]
179 (x · R(y)) · (y · (z · y)) = (x · z) · y [138 :165,172]
203,202 R(x · y) = R(y) · R(x)  [154 → 98, flip]
204  x · (y · (((R(y) · R(x)) · z) · y)) = z · y  [102 :203]
236  (x · y) · ((R(y) · R(x)) · z) = z  [202 → 96]
374  (x · y) · ((R(y) · z) · x) = x · (z · x)  [179 → 236]
463,462 x · (((R(x) · y) · z) · x) = y · (z · x)  [204 → 96 :93, flip]
506  (x · (y · x)) · z = x · (y · (x · z))  [374 → 18 :463]
508  □  [506,61]