| 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 2855-2855 | Ternary relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2862-2862 | Quaternary relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2869-2869 | Quintary relation is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3340-3340 | Predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3351-3351 | Function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3360-3360 | Unary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3400-3400 | Binary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3452-3452 | Ternary function is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3463-3463 | Quaternary function is a subclass of inheritable 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 3491-3491 | Ternary predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3502-3502 | Quaternary predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3513-3513 | Quintary predicate is a subclass of inheritable relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3534-3534 | Relation extended to quantities is a subclass of inheritable relation |
|
|