No TPTP formula. May not be expressible in strict first order. 
Midlevelontology.kif 2223922239 
abstract part is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 80488048 
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 1756317563 
geometric part is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18201820 
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 32283228 
initial list is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 18031803 
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 896896 
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 12471247 
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 30533053 
sub list is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1647316473 
sub organization is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 1002210022 
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 44284428 
subsumes content class is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 44854485 
subsumes content instance is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 78417841 
temporal part is an instance of partial ordering relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 23202320 
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 
