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

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

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

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

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

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

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

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. 
Geography.kif 562567 

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

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

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

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

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

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

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