Theorem MAJ-1. Inconsistency of a majority polynomial with (gL). {p(x, x, y) = p(x, y, x) = p(y, x, x) = x} =(gL)⇒ {x = y}.

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

1 B ≠ A 3 p(x, x, y) = x 4 p(x, y, x) = x 5 p(x, y, y) = y

11  p(x, y, z) = p(x, y, u)  [3 → 3 :(gL)]
41  p(x, y, z) = x  [4 → 11, flip]
53  p(x, y, z) = p(u, y, z)  [5 → 5 :(gL)]
65  p(x, y, z) = u  [53 → 41]
66  x = y  [65 → 65]
67  □  [66,1]