| No TPTP formula. May not be expressible in strict first order. | WMD.kif 130-130 | 子類 核武器 and 爆炸裝置 |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 131-131 | 子類 核武器 and Weapon |
| No TPTP formula. May not be expressible in strict first order. | WMD.kif 134-134 | 子類 核武器 and 放射性武器 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryDevices.kif 1391-1391 | 子類 絕對的啞彈 and 核武器 |
|
|