No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3436-3436 |
Meteoroid is a subclass of astronomical body |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3387-3387 |
Natural satellite is a subclass of astronomical body |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3366-3366 |
Satellite is a subclass of astronomical body |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3350-3350 |
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 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 |
|