No TPTP formula. May not be expressible in strict first order. | Merge.kif 2128-2128 | 集或类 是 抽象体 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2136-2136 | 类 是 集或类 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2148-2148 | 集合 是 集或类 的 subclass |