| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3478-3478 | 子類 BinaryPredicate and Predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3479-3479 | 子類 BinaryPredicate and BinaryRelation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3480-3480 | 子類 BinaryPredicate and 可繼承的關係 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2400-2400 | 子類 CaseRole and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 643-643 | 子類 BinaryRelationExtendedToQuantities and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6406-6406 | 子類 SheddingPart and BinaryPredicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | 例 子類 and BinaryPredicate |
|
|