No TPTP formula. May not be expressible in strict first order. 
Merge.kif 29722988 
A list is equal to the list composed of another list and a third list and the other list is not equal to null list and the third list is not equal to null list if and only if for all a positive integer and another positive integer 
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 62886292 
A quantity is an instance of the interval from a constant quantity to another constant quantity if and only if the quantity is greater than or equal to the constant quantity and the quantity is less than or equal to the other constant quantity 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 57275736 

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

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

No TPTP formula. May not be expressible in strict first order. 
Transportation.kif 14321443 

No TPTP formula. May not be expressible in strict first order. 
Transportation.kif 14141425 

No TPTP formula. May not be expressible in strict first order. 
Transportation.kif 13961407 

No TPTP formula. May not be expressible in strict first order. 
Weather.kif 528536 

No TPTP formula. May not be expressible in strict first order. 
Weather.kif 517526 

No TPTP formula. May not be expressible in strict first order. 
CountriesAndRegions.kif 5965 

No TPTP formula. May not be expressible in strict first order. 
Government.kif 10471054 

No TPTP formula. May not be expressible in strict first order. 
Government.kif 10361045 

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

No TPTP formula. May not be expressible in strict first order. 
Transportation.kif 447452 

No TPTP formula. May not be expressible in strict first order. 
Transportation.kif 430435 

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

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

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

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

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

No TPTP formula. May not be expressible in strict first order. 
Transportation.kif 710714 

No TPTP formula. May not be expressible in strict first order. 
Transportation.kif 733737 

No TPTP formula. May not be expressible in strict first order. 
Transportation.kif 756760 


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 