| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1177-1177 | AI m9 is a subclass of air-to-air missile |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1178-1178 | AI m9 is a subclass of infra redG missile |
|
|