No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 3281-3281 |
子屬性 首席管家 and 船友 |
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 3280-3280 |
子屬性 大副 and 船友 |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52677-52677 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52676-52676 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52675-52675 |
|