No TPTP formula. May not be expressible in strict first order. |
Languages.kif 6662-6662 |
例 san dionisio del mar huave 语 and huavean語言 |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 6672-6672 |
例 舊金山德爾馬爾韋夫語言 and huavean語言 |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 6685-6685 |
例 聖馬特奧-德爾韋韋語言 and huavean語言 |
No TPTP formula. May not be expressible in strict first order. |
Languages.kif 6697-6697 |
例 聖瑪麗亞德爾馬哈特語言 and huavean語言 |
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 28815-28815 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 28814-28814 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 28813-28813 |
|