|
|
  PlanetEarth
|
|
|
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3406-3406 | 例 行星地球 and 行星 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3407-3407 | 太陽 是 行星地球 的 orbits |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3399-3399 | 行星地球 是 地球月亮 的 orbits |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46038-46038 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46037-46037 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46036-46036 |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1462-1467 | 高度 飛機, SelfConnectedObject and 高度測量 表面 SelfConnectedObject and 行星地球 例 飛機 and 飛機 高度測量 是 absolute 飛機 的高度 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1488-1496 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3999-4010 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 2781-2786 | Object 是 LengthMeasure above 地表 SelfConnectedObject 高度 Object, SelfConnectedObject and LengthMeasure 表面 SelfConnectedObject and 行星地球 |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 1907-1912 | |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1441-1451 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3515-3517 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3468-3470 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3429-3433 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3991-3997 |
|
|
|
|