No TPTP formula. May not be expressible in strict first order. |
Military.kif 424-424 |
美国军衔e7 是 高级NCO排名 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 437-437 |
美国军衔e8 是 高级NCO排名 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 450-450 |
美国军衔e9 是 高级NCO排名 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 471-471 |
美国军衔e9特别 是 高级NCO排名 的 instance |
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 |
|