| Planet(planet)
| | Jovian_planet, gas_giant, inferior_planet, major_planet, outer_planet, planet, planetal, planetary, superior_planet, terrestrial_planet |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3391-3392 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 1496-1496 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3390-3390 | Planet is a subclass of natural satellite |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3394-3394 | Planet earth is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3402-3402 | Planet jupiter is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3400-3400 | Planet mars is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3396-3396 | Planet mercury is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3406-3406 | Planet neptune is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3410-3410 | Planet pluto is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3404-3404 | Planet saturn is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3408-3408 | Planet uranus is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3398-3398 | Planet venus is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46063-46063 | Planet venus is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46062-46062 | Planet venus is an instance of planet |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 46061-46061 | Planet venus is an instance of planet |
|
|
|