| No TPTP formula. May not be expressible in strict first order. |
Military.kif 283-284 |
不相交分解 委任軍官級別, 國旗官員級別, 現場等級軍官等級 and 公司等級排名 |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 582-582 |
例 美軍軍銜o10 and 國旗官員級別 |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 543-543 |
例 美國軍銜o7 and 國旗官員級別 |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 556-556 |
例 美國軍銜o8 and 國旗官員級別 |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 569-569 |
例 美國軍銜o9 and 國旗官員級別 |
| No TPTP formula. May not be expressible in strict first order. |
Military.kif 595-595 |
例 美國軍銜特殊 and 國旗官員級別 |
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 24158-24158 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 24157-24157 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 24156-24156 |
|
