No TPTP formula. May not be expressible in strict first order. 
People.kif 372405 
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 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. 
People.kif 418449 
The female life expectancy at birth of a geopolitical area and the year an integer 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 327357 
The life expectancy at birth of a geopolitical area and the year an integer 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. 
Music.kif 278285 

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

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

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. 
Merge.kif 48504860 

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

No TPTP formula. May not be expressible in strict first order. 
Music.kif 931941 

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

No TPTP formula. May not be expressible in strict first order. 
Media.kif 801812 

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

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

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

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

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

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

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

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

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

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

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

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


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 