No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14720-14720 |
Carbohydrate is a subclass of nutrient |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14710-14710 |
Protein is a subclass of nutrient |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14726-14726 |
Vitamin is a subclass of nutrient |
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 |
|