| No TPTP formula. May not be expressible in strict first order. | Military.kif 736-736 | 子類 公司- 軍事 and 軍事單位 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 483-483 | 子類 砲兵電池 and 公司- 軍事 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 501-501 | 子類 步兵連 and 公司- 軍事 |
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 563-563 | 子類 武器公司 and 公司- 軍事 |
|
|