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 29262931 

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

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

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

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

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

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

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. 
Media.kif 20912101 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 