No TPTP formula. May not be expressible in strict first order. |
Military.kif 269-269 |
不相交分解 士兵軍銜, 私人排名 and 非委任軍官級別 |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 346-346 |
例 美國軍銜e1 and 私人排名 |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 359-359 |
例 美國軍銜e2 and 私人排名 |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 372-372 |
例 美國軍銜e3 and 私人排名 |
No TPTP formula. May not be expressible in strict first order. |
Military.kif 385-385 |
例 美國軍銜e4 and 私人排名 |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 47468-47468 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 47467-47467 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 47466-47466 |
|