Prove:

true=> prime(2)

Given:

AxiomDefinition
division integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and true and true and true and not X = 0 and X * Y = X * Z=> Y = Z ;
ordering integer(X) and any(X) and integer(Y) and any(Y) and true and true=> X > Y xor X = Y xor Y > X ;
magnitude1 integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and true and true and true and X * Y = Z and X > 1 and Z > 0=> Z > Y ;
magnitude2 integer(X) and any(X) and integer(Y) and any(Y) and true and true and X * Y > 0 and X > 0=> Y > 0 ;
times_range1 integer(X) and any(X) and integer(Y) and any(Y) and true and true and X > 0 and X * Y > 0=> Y > 0 ;
times_range2 integer(X) and any(X) and integer(Y) and any(Y) and integer(Z) and any(Z) and true and true and true and X * Y = Z and X > 0 and Z > 0=> not Y > Z ;
factor factor(X,Y)<=> (true) and (true) and (true) and (true) and (X * Z = Y) ;
prime prime(X)<=> (true) and (X > 1) and (integer(X) and any(X) and integer(Y) and any(Y) and (factor(Y,X)) and Y > 0=> Y = 1 or Y = X ) ;