No TPTP formula. May not be expressible in strict first order. 
People.kif 411442 
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 221238 
The male to female ratio of a geopolitical area is equal to a real number if and only if an integer is equal to the number of instances in the class described by a symbolic string and another integer is equal to the number of instances in the class described by another symbolic string and the integer and the other integer is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1671316717 
An object is an instance of female cow if and only if the object is an instance of cow and female is an attribute of the object 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1672716731 
An object is an instance of hen if and only if the object is an instance of chicken and female is an attribute of the object 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1685016855 

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

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

No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 12081219 

No TPTP formula. May not be expressible in strict first order. 
Hotel.kif 10071015 

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

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

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

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

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