|
| 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 升 |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31734-31739 | 等於 OrganismPopulationFn Organism and GeographicArea and 基數 卡帕 OrganismI and 例 OrganismI and Organism 位於 OrganismI and GeographicArea |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 31712-31717 | 等於 GeopoliticalArea 的 population and 基數 卡帕 SymbolicString and 例 SymbolicString and Human 棲息 SymbolicString and GeopoliticalArea |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 933-946 | 等於 GeopoliticalArea 和 年 每年的 reaching 軍事男性年齡 and 基數 卡帕 SymbolicString and 例 SymbolicString and Human attribute SymbolicString and 男 entity 是 GeopoliticalArea 的 military 年紀 等於 entity and 減法 entity and 1 持有期間 年 and 年齡 SymbolicString and entity 年齡 SymbolicString and entity 等於 entity and entity 棲息 SymbolicString and GeopoliticalArea |
| No TPTP formula. May not be expressible in strict first order. | ComputingBrands.kif 4534-4534 | 等於 AccountCreationRejected and FailureFn CreatingAnAccount |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 6976-6976 | 等於 美國國家 and StateOrProvince 所有的 instances 在 美國 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3681-3681 | 等於 AppleOrchard and 蘋果 在 的 farm |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 12637-12637 | 等於 Blood and food for Mosquito |
| No TPTP formula. May not be expressible in strict first order. | Medicine.kif 5188-5188 | 等於 BrainDead and DeadOrMissingBodyPartFn 腦 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1666-1666 | 等於 秋季 and 經常性時間間隔 September and November |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14873-14873 | 等於 Food and food for Human |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 4743-4743 | 等於 手套 and 對於 手 的 covering |
| No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 11411-11411 | 等於 Pericarditis and InflammationFn Pericardium |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1664-1664 | 等於 春暖花開的季節 and 經常性時間間隔 March and May |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3973-3973 | 等於 平方千米 and 千 儀表 的 square 單位 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3972-3972 | 等於 平方米 and 儀表 的 square 單位 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1665-1665 | 等於 夏季 and 經常性時間間隔 June and August |
| No TPTP formula. May not be expressible in strict first order. | QoSontology.kif 2143-2143 | 等於 unix時代 and 第二 0 and 分 0 and 小時 0 and 天 1 and 月 January and 年 1970 |
| No TPTP formula. May not be expressible in strict first order. | Food.kif 3685-3685 | 等於 Vineyard and 釀酒葡萄 在 的 farm |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1667-1667 | 等於 冬季 and 經常性時間間隔 December and February |
|
|
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