No TPTP formula. May not be expressible in strict first order. | Merge.kif 2854-2854 | 子類 TernaryRelation and Relation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2855-2855 | 子類 TernaryRelation and 可繼承的關係 |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3399-3399 | 子類 BinaryFunction and TernaryRelation |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3490-3490 | 子類 TernaryPredicate and TernaryRelation |