| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 496-496 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 495-495 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 494-494 |
|
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4709-4709 |
加法函数 是 交换函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4984-4984 |
较大值函数 是 交换函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 5010-5010 |
较小值函数 是 交换函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4696-4696 |
乘法函数 是 交换函数 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 922-922 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1051-1051 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 598-598 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 128-128 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 131-131 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2283-2283 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 550-550 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 165-165 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 619-619 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 132-132 |
|
