| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1123-1123 | 子類 AG m and 空中發射導彈 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1124-1124 | 子類 AG m and 地面攻擊導彈 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1136-1136 | 子類 AG m65 and AG m |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1203-1203 | 子類 AG m114 and AG m |
|
|