| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1793-1793 | 子類 動力車輛 and 車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1804-1804 | 子類 自供電公路車輛 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1887-1887 | 子類 緊急車輛 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 1893-1893 | 子類 緊急公路車輛 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2048-2048 | 子類 火車 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2111-2111 | 子類 機動鐵路車 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2116-2116 | 子類 機車 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2166-2166 | 子類 電氣化鐵路車 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2204-2204 | 子類 電動軌道車 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2583-2583 | 子類 飛機 and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1574-1574 | 子類 APC and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1649-1649 | 子類 AAV and 動力車輛 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1947-1947 | 子類 LCAC and 動力車輛 |
|
|