No TPTP formula. May not be expressible in strict first order. |
Military.kif 347-347 |
美国军衔e1 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 360-360 |
美国军衔e2 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 373-373 |
美国军衔e3 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 386-386 |
美国军衔e4 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 399-399 |
美国军衔e5 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 412-412 |
美国军衔e6 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 425-425 |
美国军衔e7 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 438-438 |
美国军衔e8 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 451-451 |
美国军衔e9 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 470-470 |
美国军衔e9特别 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 484-484 |
美国军衔o1 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 583-583 |
美军军衔o10 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 494-494 |
美国军衔o2 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 504-504 |
美国军衔o3 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 514-514 |
美国军衔o4 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 524-524 |
美国军衔o5 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 534-534 |
美国军衔o6 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 544-544 |
美国军衔o7 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 557-557 |
美国军衔o8 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 570-570 |
美国军衔o9 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 596-596 |
美国军衔特殊 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 627-627 |
美国军衔o 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 636-636 |
美国军衔o2 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 646-646 |
美军军衔W3 是 美国军衔 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 656-656 |
美军军衔o4 是 美国军衔 的 instance |
|
Display limited to 25 items. Show next 25 |
|
Display limited to 25 items. Show next 25 |