No TPTP formula. May not be expressible in strict first order. 
Geography.kif 45064514 
Open sea is an attribute of an object if and only if the object is an instance of salt water area and the object is not an instance of landlocked water and the distance between a physical and the object is a real number NaticalMile(s) and the real number is greater than 5 
No TPTP formula. May not be expressible in strict first order. 
People.kif 285306 
A real number is an average of a list if and only if there exists another list such that length of the other list is equal to length of the list and 1th element of the other list is equal to 1th element of the list and for all a positive integer and a fourth positive integer is equal to length of the other list and the real number is equal to the fourth positive integerth element of the other list and the fourth positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 17971801 
A quantity is greater than or equal to another quantity if and only if the quantity is equal to the other quantity or the quantity is greater than the other quantity 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18491853 
A quantity is an instance of positive real number if and only if the quantity is greater than 0 and the quantity is an instance of real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 73847392 
An object is larger than another object if and only if for all a real number, another real number and an unit of measure 
No TPTP formula. May not be expressible in strict first order. 
Geography.kif 17251730 

No TPTP formula. May not be expressible in strict first order. 
Geography.kif 17371742 

No TPTP formula. May not be expressible in strict first order. 
Dining.kif 11181129 

No TPTP formula. May not be expressible in strict first order. 
ArabicCulture.kif 193212 

No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 11511166 

No TPTP formula. May not be expressible in strict first order. 
Economy.kif 15441548 

No TPTP formula. May not be expressible in strict first order. 
Cars.kif 809825 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1712517130 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1116411173 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1117411185 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1111911127 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1119311202 

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1710917114 

No TPTP formula. May not be expressible in strict first order. 
WMD.kif 816820 

No TPTP formula. May not be expressible in strict first order. 
Cars.kif 25992617 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1607016084 

No TPTP formula. May not be expressible in strict first order. 
FinancialOntology.kif 36493657 

No TPTP formula. May not be expressible in strict first order. 
Cars.kif 28982916 

No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 2883928860 

No TPTP formula. May not be expressible in strict first order. 
Economy.kif 15621566 


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 