No TPTP formula. May not be expressible in strict first order. 
Geography.kif 46104618 
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 nautical mile(s) and the real number is greater than 5.0 
No TPTP formula. May not be expressible in strict first order. 
People.kif 289310 
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 18251829 
A real number is greater than or equal to another real number if and only if the real number is equal to the other real number or the real number is greater than the other real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18771881 
A real number is an instance of positive real number if and only if the real number is greater than 0 and the real number is an instance of real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 76627670 
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 17571762 

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

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 11641179 

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

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

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

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 1817218177 

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

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

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

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

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

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

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

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

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

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


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 