| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3478-3478 | Binary predicate is a subclass of predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3479-3479 | Binary predicate is a subclass of binary relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3480-3480 | Binary predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2400-2400 | Case role is a subclass of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 643-643 | Binary relation extended to quantities is a subclass of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6406-6406 | Shedding part is a subclass of binary predicate |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 129-129 | subclass is an instance of binary predicate |
|
|