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 29342939 

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

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

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

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

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 20792089 

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

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

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

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 21962209 

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

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

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

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

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

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

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

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

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


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 