No TPTP formula. May not be expressible in strict first order. |
Military.kif 513-513 |
美国军衔o4 是 现场等级军官等级 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 523-523 |
美国军衔o5 是 现场等级军官等级 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 533-533 |
美国军衔o6 是 现场等级军官等级 的 instance |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 23624-23624 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 23623-23623 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 23622-23622 |
|