No TPTP formula. May not be expressible in strict first order. |
Military.kif 755-755 |
美国军衔o2 是 排 的 command 梯队等级 |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 492-492 |
美国军衔o1 是 美国军衔o2 的直接后续属性 |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 497-497 |
|
No TPTP formula. May not be expressible in strict first order. |
Military.kif 496-496 |
|
No TPTP formula. May not be expressible in strict first order. |
Military.kif 498-498 |
|
No TPTP formula. May not be expressible in strict first order. |
Military.kif 500-500 |
|
No TPTP formula. May not be expressible in strict first order. |
Military.kif 499-499 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 60970-60970 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 60969-60969 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 60968-60968 |
|