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

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

fof (less, axiom, ! [A,B] :
	(
		less (A, B)
	)
		<=>
	(
		! [C] :
			((less (A, B) & less (B, C)) => less (A, C))
	)
).