No TPTP formula. May not be expressible in strict first order. | Military.kif 732-732 | 子類 營 and 軍事單位 |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 539-539 | 子類 LAR營 and 營 |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 650-650 | 子類 AssaultAmphibianBatallion and 營 |