| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2365-2365 | 子類 PartialOrderingRelation and TransitiveRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2366-2366 | 子類 PartialOrderingRelation and AntisymmetricRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2367-2367 | 子類 PartialOrderingRelation and ReflexiveRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2368-2368 | 子類 PartialOrderingRelation and TotalValuedRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2374-2374 | 子類 TotalOrderingRelation and PartialOrderingRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 130-130 | 例 子類 and PartialOrderingRelation |
|
|