identity0:      integer(X) => X + 0 = X and X * 0 = 0;
identity1:      integer(X) => X * 1 = X;
commutativity:  integer(X) and integer(Y) => X * Y = Y * X;
associativity:  integer(X) and integer(Y) and integer(Z) =>
                X * (Y * Z) = (X * Y) * Z;
division:       integer(X) and integer(Y) and integer(Z) and                 not(X = 0) and X * Y = X * Z => Y = Z;
ordering:       integer(X) and integer(Y) =>
                X > Y xor X = Y xor Y > X;
magnitude1:     integer(X) and integer(Y) and integer(Z) and
                X * Y = Z and X > 1 and Z > 0 => Z > Y;
magnitude2:     integer(X) and integer(Y) and X * Y > 0 =>
                X > 0;
range_finite:   integer(X) and integer(Y) and integer(Z) and                 exists(X) and exists(Z) and
                X > Y and Y > Z => finite(Y);
factor:         factor(X,Y) <=> integer(X) and integer(Y) and
                integer(Z) and exists(Z) and X * Z = Y;
prime:          prime(X) => integer(X) and X > 1 and
                (factor(Y,X) and Y > 0 => Y=1 or Y=X);
prime_factor:   prime(X) and factor(X,Y*Z) =>
                factor(X,Y) or factor(X,Z);
prime2:         prime(2);
prove:          not (