No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3406-3406 |
行星地球 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3414-3414 |
行星木星 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3412-3412 |
星球火星 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3408-3408 |
行星汞 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3418-3418 |
行星海王星 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3422-3422 |
行星冥王星 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3416-3416 |
行星土星 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3420-3420 |
行星天王星 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 3410-3410 |
行星金星 是 行星 的 instance |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 46034-46034 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 46033-46033 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 46032-46032 |
|