No TPTP formula. May not be expressible in strict first order. |
Military.kif 306-306 |
非委任军官级别 分拆成不相交的 初级NCO排名 和 高级NCO排名 |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 398-398 |
美国军衔e5 是 初级NCO排名 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 411-411 |
美国军衔e6 是 初级NCO排名 的 instance |
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 |
|