Sigma KB Term Intersection

No TPTP formula. May not be expressible in strict first order.	Merge.kif 3320-3324	If a function is an instance of sequence function and the range of the function is an instance of a class, then the class is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1894-1894	Integer is a subclass of rational number
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1900-1900	Even integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1905-1905	Odd integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1910-1910	Prime number is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1915-1915	Nonnegative integer is a subclass of integer
No TPTP formula. May not be expressible in strict first order.	Merge.kif 1925-1925	Negative integer is a subclass of integer