No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14678-14678 |
文章 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7864-7864 |
基督教圣经 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 26410-26410 |
GuideBook 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7879-7879 |
新约 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14946-14946 |
小说 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7875-7875 |
旧约 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14913-14913 |
参考书 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1040-1040 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1291-1291 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 718-718 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 20-20 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 22-22 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2402-2402 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 670-670 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 23-23 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 288-288 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 739-739 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 23-23 |
|