|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7316-7318 | 等於 測量 RealNumber and 蘭金度 and 測量 乘法 RealNumber and 1.8 and 凱文度 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7304-7306 | 等於 測量 RealNumber and 金屬塊 and 測量 乘法 RealNumber and 14593.90 and 公克 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7257-7259 | 等於 測量 RealNumber and 英國加侖 and 測量 乘法 RealNumber and 4.54609 and 升 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7391-7393 | 等於 測量 RealNumber and 美國分 and 測量 乘法 RealNumber and 0.01 and 美國美元 |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 7212-7214 | 等於 測量 RealNumber and 美國加侖 and 測量 乘法 RealNumber and 3.785411784 and 升 |
|
|
Sigma web home Suggested Upper Merged Ontology (SUMO) web home
Sigma version 3.0 is open source software produced by Articulate Software and its partners