No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14409-14409 |
无花植物 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 6295-6295 |
Cactus 是 开花植物 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 9356-9356 |
HerbaceousPlant 是 开花植物 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 6281-6281 |
Succulent 是 开花植物 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 6274-6274 |
Vine 是 开花植物 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 9364-9364 |
WoodyPlant 是 开花植物 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 966-966 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1139-1139 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 643-643 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 174-174 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 177-177 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2327-2327 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 595-595 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 211-211 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 664-664 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 178-178 |
|