No TPTP formula. May not be expressible in strict first order. 
Geography.kif 47114720 
Open sea is an attribute of an object if and only if there exist a physical and a real number such that the object is an instance of salt water area and the object is not an instance of landlocked water and the distance between the physical and the object is the 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 272293 
A real number is an average of a list if and only if there exist another list and a positive integer 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 another positive integer and the positive integer is equal to length of the other list and the real number is equal to the positive integerth element of the other list and the positive integer 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18851889 
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 19371941 
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 77947802 
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 17541759 

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

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

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

No TPTP formula. May not be expressible in strict first order. 
Medicine.kif 39844004 

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

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

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

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

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

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 1852518530 

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

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

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

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

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

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

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

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


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 