No TPTP formula. May not be expressible in strict first order. 
chinese_format.kif 13671369 

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

No TPTP formula. May not be expressible in strict first order. 
Merge.kif 110110 
The number 1 argument of inverse is an instance of binary relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 111111 
The number 2 argument of inverse is an instance of binary relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 105105 
inverse is an instance of binary predicate 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 107107 
inverse is an instance of intransitive relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 106106 
inverse is an instance of irreflexive relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 109109 
inverse is an instance of partial valued relation 
No TPTP formula. May not be expressible in strict first order. 
Merge.kif 108108 
inverse is an instance of symmetric relation 