No TPTP formula. May not be expressible in strict first order. |
Military.kif 424-424 |
USMilitaryRankE7 est une instance de SeniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 437-437 |
USMilitaryRankE8 est une instance de SeniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 450-450 |
USMilitaryRankE9 est une instance de SeniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 471-471 |
USMilitaryRankE9special est une instance de SeniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52109-52109 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52108-52108 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52107-52107 |
|