No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14744-14744 |
碳水化物 是 营养 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14734-14734 |
蛋白质 是 营养 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14750-14750 |
维生素 是 营养 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1005-1005 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1222-1222 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 682-682 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 213-213 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 216-216 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2366-2366 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 634-634 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 250-250 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 703-703 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 217-217 |
|