No TPTP formula. May not be expressible in strict first order. | Merge.kif 1943-1943 | Negative real number is a subclass of real number |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 1986-1986 | Negative integer is a subclass of negative real number |