more pictures...
| AstronomicalBody(astronomical body)
more pictures... | | Alpha_Geminorum, Andromeda, Antlia, Apollo_asteroid, Apus, Aquarius, Aquila, Ara, Aries, Auriga, Big_Dipper, Bootes, Caelum, Cancer, Canis_Major, Canis_Minor, Capricorn, Capricornus, Carina, Cassiopeia, Castor, Centaur, Centaurus, Cepheus, Ceres, Cetus, Chamaeleon, Chameleon, Charioteer, Charles's_Wain, Chiron, Circinus, Columba, Coma_Berenices, Copernican, Corona_Borealis, Corvus, Crab_Nebula, Crane, Crater, Crow, Crux, Crux_Australis, Cygnus, Delphinus, Dipper, Dorado, Dove, Draco, Dragon... |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13914-13914 | Astronomical body is disjoint from geographic area |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 1432-1434 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13915-13920 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8354-8354 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8919-8919 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8920-8920 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8921-8921 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8922-8922 | |
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 13913-13913 | Astronomical body is a subclass of object |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3362-3362 | Meteoroid is a subclass of astronomical body |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3313-3313 | Natural satellite is a subclass of astronomical body |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3292-3292 | Satellite is a subclass of astronomical body |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3276-3276 | Star is a subclass of astronomical body |
| No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 947-947 | |
| No TPTP formula. May not be expressible in strict first order. | english_format.kif 1101-1101 | |
| No TPTP formula. May not be expressible in strict first order. | french_format.kif 623-623 | |
| No TPTP formula. May not be expressible in strict first order. | terms-hindi.txt 154-154 | |
| No TPTP formula. May not be expressible in strict first order. | terms-it.txt 155-155 | |
| No TPTP formula. May not be expressible in strict first order. | japanese_format.kif 2308-2308 | |
| No TPTP formula. May not be expressible in strict first order. | portuguese_format.kif 575-575 | |
| No TPTP formula. May not be expressible in strict first order. | terms-cz.txt 191-191 | |
| No TPTP formula. May not be expressible in strict first order. | relations-ro.kif 644-644 | |
| No TPTP formula. May not be expressible in strict first order. | terms-tg.txt 158-158 |
| appearance as argument number 3 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3300-3300 | The number 2 argument of orbits is an instance of astronomical body |
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Weather.kif 22-27 |
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3305-3310 |
|
|
|
|