| No TPTP formula. May not be expressible in strict first order. | Military.kif 130-130 | 军车 是 军事平台 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 131-131 | 军车 是 车辆 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 145-145 | 军用坦克 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 156-156 | 军用飞机 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 195-195 | 军事支援车辆 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1571-1571 | APC 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1646-1646 | AAV 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1734-1734 | 鹞2 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1769-1769 | C h53 e 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1830-1830 | C h46 d 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1890-1890 | A h1 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1945-1945 | LCAC 是 军车 的 subclass |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 2128-2128 | AMEV 是 军车 的 subclass |
|
|