| No TPTP formula. May not be expressible in strict first order. | Military.kif 736-736 | CompanyMilitary est une sous-classe de MilitaryUnit |
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 483-483 | ArtilleryBattery est une sous-classe de CompanyMilitary |
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 501-501 | InfantryCompany est une sous-classe de CompanyMilitary |
| No TPTP formula. May not be expressible in strict first order. | MilitaryPersons.kif 563-563 | WeaponsCompany est une sous-classe de CompanyMilitary |
|
|