| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1106-1106 | 子類 船舶登記 and ContentBearingObject |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1121-1121 | 子類 國家船舶登記 and 船舶登記 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1168-1168 | 子類 內部船舶登記 and 船舶登記 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1182-1182 | 子類 海外船舶登記 and 船舶登記 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1198-1198 | 子類 便利登記的旗幟 and 船舶登記 |
|
|