No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24236-24246 | |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 24195-24206 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3392-3396 | |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1954-1954 | 整数 是 有理数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1960-1960 | 偶数 是 整数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1965-1965 | 奇整数 是 整数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1970-1970 | 素数 是 整数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1975-1975 | 非负整数 是 整数 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1985-1985 | 负整数 是 整数 的 subclass |