Prove:

not (

Given:

integer(X) => X + 0 = X and X * 0 = 0

and:

integer(X) => X * 1 = X

and:

integer(X) and integer(Y) => X * Y = Y * X

and:

integer(X) and integer(Y) and integer(Z) =>
X * (Y * Z) = (X * Y) * Z

and:

integer(X) and integer(Y) and integer(Z) and                 not(X = 0) and X * Y = X * Z => Y = Z

and:

integer(X) and integer(Y) =>
X > Y xor X = Y xor Y > X

and:

integer(X) and integer(Y) and integer(Z) and
X * Y = Z and X > 1 and Z > 0 => Z > Y

and:

integer(X) and integer(Y) and X * Y > 0 =>
X > 0

and:

integer(X) and integer(Y) and integer(Z) and                 exists(X) and exists(Z) and
X > Y and Y > Z => finite(Y)

and:

factor(X,Y) <=> integer(X) and integer(Y) and
integer(Z) and exists(Z) and X * Z = Y

and:

prime(X) => integer(X) and X > 1 and
(factor(Y,X) and Y > 0 => Y=1 or Y=X)

and:

prime(X) and factor(X,Y*Z) =>
factor(X,Y) or factor(X,Z)

and:

prime(2)

Test as a text file.