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 2855-2855 | Ternary relation is a subclass of inheritable relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3399-3399 | Binary function is a subclass of ternary relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3490-3490 | Ternary predicate is a subclass of ternary relation |