| No TPTP formula. May not be expressible in strict first order. | Merge.kif 200-205 |
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2558-2558 | Inheritable relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2177-2177 | Single valued relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2195-2195 | Total valued relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2233-2233 | Binary relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2401-2401 | Case role is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2565-2565 | Probability relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2657-2657 | Spatial relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2664-2664 | Temporal relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2670-2670 | Intentional relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2696-2696 | Propositional attitude is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2709-2709 | Object attitude is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2856-2856 | Ternary relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2863-2863 | Quaternary relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2870-2870 | Quintary relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3341-3341 | Predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3352-3352 | Function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3361-3361 | Unary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3401-3401 | Binary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3453-3453 | Ternary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3464-3464 | Quaternary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3481-3481 | Binary predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3492-3492 | Ternary predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3503-3503 | Quaternary predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3514-3514 | Quintary predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3535-3535 | Relation extended to quantities is a subclass of inheritable relation |
|
|