| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2309-2309 | 子類 客船 and 船 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2432-2432 | 子類 客貨船 and 客船 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2434-2434 | 子類 近海客船 and 客船 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2467-2467 | 子類 遊輪 and 客船 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2482-2482 | 子類 遠洋班輪 and 客船 |
|
|