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 3099631001 

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

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

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

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

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 38133817 

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

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

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

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
