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

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

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

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

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

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

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

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 16621674 

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 12351247 

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 11551167 

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 19001912 

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 11891201 

No TPTP formula. May not be expressible in strict first order. 
WMD.kif 205211 

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 18601872 

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 17881800 

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 17441756 

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 15421554 

No TPTP formula. May not be expressible in strict first order. 
WMD.kif 11791184 

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

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

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

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

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

No TPTP formula. May not be expressible in strict first order. 
MilitaryDevices.kif 121138 
 If a vehicle is maximum payload height width a real number an unit of measure(s) for another real number another unit of measure(s),
 then there don't exist a process, a self connected object,, , a third real number,, , the third real numberU,, , a fourth real number and the fourth real numberU such that the process is an instance of transportation and the vehicle is an instrument for the process and the self connected object is a patient of the process and the width of the self connected object is the third real number the third real numberU(s) and the height of the self connected object is the fourth real number the fourth real numberU(s) and the third real numberU is equal to the other unit of measure and the fourth real numberU is equal to the unit of measure and the third real number is greater than the other real number and the fourth real number is greater than the real number
