No TPTP formula. May not be expressible in strict first order. 
Geography.kif 44214429 
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 length measure and the length measure is greater than 5 nautical mile(s) 
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 17981802 
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 18501854 
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 73717379 
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 17071712 

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

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

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

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

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 803816 

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

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 1709417099 

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 25722588 

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 36073615 

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

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 