PrivateRank |
appearance as argument number 1 |
No TPTP formula. May not be expressible in strict first order. | Military.kif 315-317 | |
No TPTP formula. May not be expressible in strict first order. | Military.kif 314-314 | PrivateRank est une sous-classe de EnlistedSoldierRank |
appearance as argument number 2 |
No TPTP formula. May not be expressible in strict first order. | Military.kif 269-269 | EnlistedSoldierRank est disjointement decompos� en PrivateRank + NonCommissionedOfficerRank |
No TPTP formula. May not be expressible in strict first order. | Military.kif 346-346 | USMilitaryRankE1 est une instance de PrivateRank |
No TPTP formula. May not be expressible in strict first order. | Military.kif 359-359 | USMilitaryRankE2 est une instance de PrivateRank |
No TPTP formula. May not be expressible in strict first order. | Military.kif 372-372 | USMilitaryRankE3 est une instance de PrivateRank |
No TPTP formula. May not be expressible in strict first order. | Military.kif 385-385 | USMilitaryRankE4 est une instance de PrivateRank |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 47470-47470 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 47469-47469 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 47468-47468 |