Theorem MED-1. Cancellative median algebras. The type is ⟨2, 0⟩ with constant e.

\{ \begin{matrix}· is cancellative \\ (xy)(zu) = (xz)(yu) \\ ee = e \end{matrix} \} ⇒ \{(x(yz))((uv)w) = (x(uz))((yv)w)\}.

Proof (found by Otter 3.0.4 on gyro^{1} at 142.15 seconds).

1 x = x 2 x · y = z, x · u = z → y = u 3 x · y = z, u · y = z → x = u 4 (x · y) · (z · u) = (x · z) · (y · u) 5 e · e = e 7 (A · (D · C)) · ((B · E) · F) = (A · (B · C)) · ((D · E) · F) → □

8  ((x · y) · (z · u)) · (v · w) = ((x · z) · v) · ((y · u) · w)  [4 → 4]
9  (x · y) · ((z · u) · (v · w)) = (x · (z · v)) · (y · (u · w))  [4 → 4]
10  ((x · y) · z) · ((u · v) · w) = ((x · u) · (y · v)) · (z · w)  [flip 8]
13,12 (x · e) · (y · e) = (x · y) · e  [5 → 4, flip]
15,14 (e · x) · (e · y) = e · (x · y)  [5 → 4, flip]
16  (e · x) · e = e · (x · e)  [5 → 12, flip]
27  ((e · x) · y) · (e · z) = (e · (x · e)) · (y · z)  [16 → 4, flip]
30  (x · (e · y)) · (z · (e · u)) = (x · z) · (e · (y · u))  [14 → 4, flip]
33,32 ((e · x) · y) · ((e · z) · u) = (e · (x · z)) · (y · u)  [14 → 4, flip]
74  ((x · y) · (z · u)) · e = ((x · z) · (y · u)) · e  [5 → 8 :13]
81  (e · (x · e)) · ((e · y) · z) = e · ((x · y) · z)  [14 → 27 :15, flip]
147  (x · ((y · z) · (u · v))) · e = (x · ((y · u) · (z · v))) · e  [74 → 12 :13]
193  (e · (x · y)) · ((z · u) · v) = (e · (z · y)) · ((x · u) · v)  [14 → 10 :33]
238,237 (x · (y · e)) · ((e · z) · (u · v)) = (x · (y · u)) · (e · (z · v))  [9 → 30]
306 x · ((y · z) · (u · v)) = x · ((y · u) · (z · v)) [3,1,147]

369 e · ((x · (y · z)) · ((u · v) · w)) = e · ((x · (y · v)) · ((u · z) · w))

[193 → 81 :238,15]

485  (x · (y · z)) · ((u · v) · w) = (x · (u · z)) · ((y · v) · w)  [2,306,369]
486  □  [485,7]

1gyro is a 486 DX2/66 computer with 40 megabytes of RAM running the Linux (a UNIX clone) operating system. It runs Otter and MACE about 1.4 times faster than a Sun SPARCstation 2.