| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1891-1891 | 子類 RealNumber and Number |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1911-1911 | 子類 RationalNumber and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1916-1916 | 子類 IrrationalNumber and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1921-1921 | 子類 NonnegativeRealNumber and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1943-1943 | 子類 NegativeRealNumber and RealNumber |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2003-2003 | 子類 BinaryNumber and RealNumber |
|
|