No TPTP formula. May not be expressible in strict first order. | Merge.kif 2128-2128 | Set or class is a subclass of abstract |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2136-2136 | Class is a subclass of set or class |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2148-2148 | Set is a subclass of set or class |