No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 208-208 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 207-207 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 206-206 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4708-4708 |
加法函数 是 结合函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4983-4983 |
较大值函数 是 结合函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5009-5009 |
较小值函数 是 结合函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4695-4695 |
乘法函数 是 结合函数 的 instance |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 921-921 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1049-1049 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 597-597 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 127-127 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 130-130 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2282-2282 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 549-549 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 164-164 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 618-618 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 131-131 |
|