No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 2221522215 
abstract part is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 80428042 
before or equal is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
MilitaryProcesses.kif 16991699 
coordinates is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1755017550 
geometric part is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18141814 
greater than or equal to is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 32223222 
initial list is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 17971797 
less than or equal to is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 890890 
part is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 670670 
sub attribute is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 12411241 
sub collection is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Languages.kif 1447614476 
subLanguage is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 30473047 
sub list is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1646016460 
sub organization is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1001610016 
sub process is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 128128 
subclass is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 168168 
subrelation is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 44224422 
subsumes content class is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 44794479 
subsumes content instance is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 78357835 
temporal part is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 23142314 
Total ordering relation is a subclass of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
chinese_format.kif 901901 

No TPTP formula. May not be expressible in strict first order. 
english_format.kif 10091009 
