| PrivateRank(private rank) | | buck_private, common_soldier, private |
| appearance as argument number 1 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Military.kif 315-317 | |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 314-314 | Private rank is a subclass of enlisted soldier rank |
| appearance as argument number 2 |
|
|
| No TPTP formula. May not be expressible in strict first order. | Military.kif 269-269 | Enlisted soldier rank is disjointly decomposed into private rank and non commissioned officer rank |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 346-346 | US military rank e1 is an instance of private rank |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 359-359 | US military rank e2 is an instance of private rank |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 372-372 | US military rank e3 is an instance of private rank |
| No TPTP formula. May not be expressible in strict first order. | Military.kif 385-385 | US military rank e4 is an instance of private rank |
| 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 |
|
|
|