No TPTP formula. May not be expressible in strict first order. |
Government.kif 3435-3435 |
"ICRC" is an abbreviation of international committee of the red cross |
No TPTP formula. May not be expressible in strict first order. |
Government.kif 3434-3434 |
International committee of the red cross is a conventional long name of "International Committee of the Red Cross" |
No TPTP formula. May not be expressible in strict first order. |
Government.kif 3436-3436 |
International committee of the red cross is a conventional short name of "Red Cross" |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 30535-30535 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 30534-30534 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 30533-30533 |
|