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