No TPTP formula. May not be expressible in strict first order. 
People.kif 383416 
A year is an instance of the year the yearEAR and the male life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
No TPTP formula. May not be expressible in strict first order. 
People.kif 429462 
A year is an instance of the year an integer and the female life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
No TPTP formula. May not be expressible in strict first order. 
People.kif 336368 
A year is an instance of the year an integer and the life expectancy at birth of a geopolitical area and the year is equal to a real number if and only if there exists a list such that the list is an instance of list and length of the list is an instance of another integer and for all the listITEM and the real number is an average of the list 
No TPTP formula. May not be expressible in strict first order. 
People.kif 298319 
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 32143221 

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

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

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

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

No TPTP formula. May not be expressible in strict first order. 
UXExperimentalTerms.kif 39303948 

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

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

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

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

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

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

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