fof(at_least_four, axiom, ? [A,B,C,D] : ((A != B) & (A != C) & (B != C) & (B != D) & (C != D) & (D != A))).

fof (zero, axiom, ! [X] :
	(zero (X) <=> ~one(X))
).

fof (one, axiom, ! [X] :
	(one (X) <=> ~zero (X))
).

fof (less, axiom, ! [X,Y,Z] : (
    ( ~less(X,X) => ( (less(X,Y) & less (Y,Z)) => less(X,Z))))).

fof(is_binary, axiom, ! [X] : (zero(X) | one(X))).

fof (four_binaries, axiom, ? [W,X,Y,Z] : (
    (is_binary (W) & is_binary (X) & is_binary(Y) & is_binary(Z))) &
	(less (W,X) | less (X,Y) | less(Y,Z) | less(W,Y) | less (X,Z) | less (Z,W)) ).