| Star(star)
| | Aldebaran, Algol, Alpha_Centauri, Alpha_Crucis, Alpha_Orionis, Altair, Antares, Arcturus, Asterope, Beta_Centauri, Beta_Crucis, Beta_Orionis, Betelgeuse, Canicula, Canopus, Capella, Deneb, Denebola, Dog_Star, Epsilon_Aurigae, North_Star, Polaris, Pollux, Procyon, Proxima, Proxima_Centauri, Regulus, Rigel, Rigil, Rigil_Kent, Sirius, Sothis, Spica, Sterope, Vega, fixed_star, flare_star, giant, giant_star, loadstar, lodestar, neutron_star, nova, polar_star, pole_star, polestar, pulsar, red_dwarf, red_dwarf_star, red_giant... |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3351-3352 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 755-755 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 177-177 | |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3350-3350 | Star is a subclass of astronomical body |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3354-3354 | Sol is an instance of star |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55044-55044 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55043-55043 | |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 55042-55042 |
|
|
|