| No TPTP formula. May not be expressible in strict first order. | Military.kif 130-130 | Military vehicle is a subclass of military platform |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 131-131 | Military vehicle is a subclass of vehicle |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 145-145 | Military tank is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 156-156 | Military aircraft is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 195-195 | Military support vehicle is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1571-1571 | APC is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1646-1646 | Amphibious Assault Vehicle is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1734-1734 | Harrier2 is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1769-1769 | C h53 e is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1830-1830 | C h46 d is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1890-1890 | A h1 is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1945-1945 | LCAC is a subclass of military vehicle |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2128-2128 | M113A4 Armored Medical Evacuation Vehicle is a subclass of military vehicle |
|
|