| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2582-2582 | 子類 飛機 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. | Transportation.kif 2589-2589 | 子類 螺旋槳飛機 and 飛機 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2590-2590 | 子類 噴氣式飛機 and 飛機 |
| No TPTP formula. May not be expressible in strict first order. | Transportation.kif 2591-2591 | 子類 螺旋槳噴氣機 and 飛機 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1708-1708 | 子類 VSTOL and 飛機 |
|
|