No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2902-2902 |
currencyType Japan and JapaneseYen |
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 2924-2924 |
currencyValue JapaneseYenCoin and JapaneseYen |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 31495-31495 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 31494-31494 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 31493-31493 |
|