Theorem PIX-1. Inconsistency of a Pixley polynomial with (gL). {p(y, y, x) = p(x, z, z) = p(x, u, x) = x} =(gL)⇒ {x = y}.

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

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

11,10  p(x, y, z) = x  [5 → 7 :(gL) :6,6]
12  x = y  [3 → 7 :(gL) :4,11,4]
13  □  [12,1]