No TPTP formula. May not be expressible in strict first order. | Military.kif 736-736 | Company- military is a subclass of military unit |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 483-483 | Artillery battery is a subclass of company- military |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 501-501 | Infantry company is a subclass of company- military |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 563-563 | Weapons company is a subclass of company- military |