| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2159-2159 | Relation is a subclass of abstract |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2176-2176 | Single valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2194-2194 | Total valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2223-2223 | Partial valued relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2232-2232 | Binary relation is a subclass of relation |
| 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 2564-2564 | Probability relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2656-2656 | Spatial relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2663-2663 | Temporal relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2671-2671 | Intentional relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2854-2854 | Ternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2861-2861 | Quaternary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2868-2868 | Quintary relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3339-3339 | Predicate is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3522-3522 | Variable arity relation is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 3533-3533 | Relation extended to quantities is a subclass of relation |
| No TPTP formula. May not be expressible in strict first order. | Economy.kif 965-965 | PPP based economic valuation is a subclass of relation |
|
|