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 | 子類 Integer and RationalNumber |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1960-1960 | 子類 EvenInteger and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1965-1965 | 子類 OddInteger and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1970-1970 | 子類 PrimeNumber and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1975-1975 | 子類 NonnegativeInteger and Integer |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1985-1985 | 子類 NegativeInteger and Integer |