more pictures...
| AstronomicalBody(天文体)
more pictures... | |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Merge.kif 14023-14023 | 天文体 和 % 2 是 disjoint |
| 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 14024-14029 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8353-8353 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 8918-8918 | |
| 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. | Merge.kif 14022-14022 | 天文体 是 客体 的 subclass |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3436-3436 | 流星 是 天文体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3387-3387 | 天然卫星 是 天文体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3366-3366 | 卫星 是 天文体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Geography.kif 3350-3350 | 星 是 天文体 的 subclass |
| 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 157-157 | |
| 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 3374-3374 | 轨道 的 2 数量 是 天文体 的 instance |
| 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 3379-3384 |
|
|
|