| No TPTP formula. May not be expressible in strict first order. |
Food.kif 1237-1237 |
mixtureRatio 是 五元关系 的 instance |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3462-3462 |
四元函数 是 五元关系 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 3512-3512 |
五元谓语 是 五元关系 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 912-912 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1031-1031 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 588-588 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 118-118 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 121-121 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2273-2273 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 540-540 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 155-155 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 609-609 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 122-122 |
|
QuintaryRelation