No TPTP formula. May not be expressible in strict first order. |
Military.kif 306-306 |
NonCommissionedOfficerRank est disjointement decompos� en JuniorNCORank + SeniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 398-398 |
USMilitaryRankE5 est une instance de JuniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 411-411 |
USMilitaryRankE6 est une instance de JuniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 31921-31921 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 31920-31920 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 31919-31919 |
|