represents |
No TPTP formula. May not be expressible in strict first order. | chinese_format.kif 228-228 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 49531-49531 | |
No TPTP formula. May not be expressible in strict first order. | domainEnglishFormat.kif 49530-49530 | |
No TPTP formula. May not be expressible in strict first order. | terms-de.txt 95-95 |