| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1767-1767 | 子類 C h53 e and 直升機 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1768-1768 | 子類 C h53 e and 乘用車 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1769-1769 | 子類 C h53 e and 軍車 |
|
|