No TPTP formula. May not be expressible in strict first order. |
Military.kif 424-424 |
USMilitaryRankE7 e' uma instancia de SeniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 437-437 |
USMilitaryRankE8 e' uma instancia de SeniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 450-450 |
USMilitaryRankE9 e' uma instancia de SeniorNCORank |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 471-471 |
USMilitaryRankE9special e' uma instancia 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 |
|