No TPTP formula. May not be expressible in strict first order. 
People.kif 257281 
The deaths per thousand live births of a geopolitical area and the year an integer is equal to a real number if and only if another integer is equal to the number of instances in the class described by a symbolic string and the other integer and 1000 is equal to another real number and a third integer is equal to the number of instances in the class described by another symbolic string and the third integer and the other real number is equal to the real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18661870 
A real number is an instance of negative real number if and only if the real number is less than 0 and the real number is an instance of real number 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 17851789 
A real number is less than or equal to another real number if and only if the real number is equal to the other real number or the real number is less than the other real number 
No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 1805218061 

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

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

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

No TPTP formula. May not be expressible in strict first order. 
Dining.kif 11011109 

No TPTP formula. May not be expressible in strict first order. 
FinancialOntology.kif 36563664 

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

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

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

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

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

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

No TPTP formula. May not be expressible in strict first order. 
Dining.kif 725748 

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

No TPTP formula. May not be expressible in strict first order. 
Geography.kif 19351949 

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

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

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

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

No TPTP formula. May not be expressible in strict first order. 
QoSontology.kif 19321946 

No TPTP formula. May not be expressible in strict first order. 
Dining.kif 507516 

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


Display limited to 25 items. Show next 25 

Display limited to 25 items. Show next 25 