No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12483-12483 |
分开 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2472-2472 |
酸化 是 结合 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 1896-1896 |
曝气 是 结合 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12523-12523 |
化学合成 是 结合 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2893-2893 |
盐碱 是 结合 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17529-17529 |
搅拌 是 结合 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1167-1167 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1551-1551 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 845-845 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 377-377 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 380-380 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2529-2529 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 797-797 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 382-382 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 416-416 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 866-866 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 381-381 |
|