No TPTP formula. May not be expressible in strict first order. | Merge.kif 1911-1911 | Rational number is a subclass of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1954-1954 | Integer is a subclass of rational number |