No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14677-14677 |
文章 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7863-7863 |
基督教圣经 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 26398-26398 |
GuideBook 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7878-7878 |
新约 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14945-14945 |
小说 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7874-7874 |
旧约 是 书 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14912-14912 |
参考书 是 书 的 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 |
|