No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 509-509 | LARUnit est une sous-classe de MilitaryUnit |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 540-540 | LARBattalion est une sous-classe de LARUnit |
No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 546-546 | LARPlatoon est une sous-classe de LARUnit |