| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1891-1891 | Numero Real e' uma sub-classe de Numero |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1911-1911 | Numero Racional e' uma sub-classe de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1916-1916 | Numero Irracional e' uma sub-classe de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1921-1921 | Numero Real nao-negativo e' uma sub-classe de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 1943-1943 | Numero Real negativo e' uma sub-classe de Numero Real |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 2003-2003 | Numero Binario e' uma sub-classe de Numero Real |
|
|