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 52107-52107 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52106-52106 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 52105-52105 |
|