| No TPTP formula. May not be expressible in strict first order. |
Military.kif 283-284 |
委任军官级别 分拆成不相交的 国旗官员级别, 现场等级军官等级, 和 公司等级排名 |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 582-582 |
美军军衔o10 是 国旗官员级别 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 543-543 |
美国军衔o7 是 国旗官员级别 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 556-556 |
美国军衔o8 是 国旗官员级别 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 569-569 |
美国军衔o9 是 国旗官员级别 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 595-595 |
美国军衔特殊 是 国旗官员级别 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 24158-24158 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 24157-24157 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 24156-24156 |
|
