| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1106-1106 | 船舶登记 是 有内用物体 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1121-1121 | 国家船舶登记 是 船舶登记 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1168-1168 | 内部船舶登记 是 船舶登记 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1182-1182 | 海外船舶登记 是 船舶登记 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1198-1198 | 便利登记的旗帜 是 船舶登记 的 subclass |
|
|