| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1811-1811 | 子類 代理動力車輛 and 車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1924-1924 | 子類 週期 and 代理動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1945-1945 | 子類 摩托車 and 代理動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2500-2500 | 子類 獨木舟 and 代理動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2503-2503 | 子類 皮艇 and 代理動力車輛 |
|
|