| MerchantMarineShip(merchant marine ship)
| | merchant_marine_ship, 商船海运, 商船海運 |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1011-1016 | |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 1846-1846 | "http://upload.wikimedia.org/wikipedia/commons/7/75/ Supertanker_AbQaiq.jpg" is a URL depicting merchant marine ship |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 2256-2256 | "http://upload.wikimedia.org/wikipedia/commons/e/e8/ Sabrina_I.jpg" is a URL depicting merchant marine ship |
| No TPTP formula. May not be expressible in strict first order. | pictureList.kif 2255-2255 | "http://upload.wikimedia.org/wikipedia/en/d/da/Knock_Nevis.jpg" is a URL depicting merchant marine ship |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1008-1008 | Merchant marine ship is a subclass of ship |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1010-1010 | Merchant marine ship has name "commercial vessel" |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1009-1009 | Merchant marine ship has name "merchant ship" |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37093-37093 | "商船海运" is the printable form of merchant marine ship in ChineseLanguage |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37092-37092 | "商船海運" is the printable form of merchant marine ship in ChineseTraditionalLanguage |
| No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 37091-37091 | "merchant marine ship" is the printable form of merchant marine ship in english language |
| antecedent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1018-1022 |
|
| consequent |
|
|
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 961-965 |
|
|
|
|