No TPTP formula. May not be expressible in strict first order. 
People.kif 357390 
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 exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other 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 403436 
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 exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other 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 310342 
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 exist a list, another integer,, , a symbolic string,, , an entity,, , another entity and a third entity such that the list is an instance of list and length of the list is an instance of the other 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 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. 
Music.kif 280287 

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

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

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

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

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

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

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

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 15151530 

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

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

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

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

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 48544859 

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

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

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 29402948 

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 