| No TPTP formula. May not be expressible in strict first order. |
Food.kif 2311-2311 |
%每个 FleshOrPulp 是 水果或蔬菜 的 initially part |
| No TPTP formula. May not be expressible in strict first order. |
Food.kif 2596-2596 |
%每个 Juice 是 水果或蔬菜 的 initially part |
| No TPTP formula. May not be expressible in strict first order. |
Food.kif 2297-2297 |
%每个 PeelOrRind 是 水果或蔬菜 的 initially part |
| No TPTP formula. May not be expressible in strict first order. |
Food.kif 2391-2391 |
Broccoli 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4470-4470 |
食用坚果 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Food.kif 2175-2175 |
水果 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4486-4486 |
花生 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Food.kif 2154-2154 |
Herb 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4336-4336 |
豆科植物 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Food.kif 2684-2684 |
Mushroom 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4287-4287 |
根菜类 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Food.kif 3358-3358 |
Scallion 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4706-4706 |
茶树空中部分 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Economy.kif 4206-4206 |
蔬菜 是 水果或蔬菜 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1014-1014 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1240-1240 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 692-692 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 223-223 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 226-226 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2375-2375 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 644-644 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 261-261 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 713-713 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 227-227 |
|
|
| Display limited to 25 items. Show next 25 |
|
| Display limited to 25 items. Show next 25 |
