| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12505-12505 |
不相交的 Separating and Combining |
| No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2472-2472 |
子類 酸化 and Combining |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 1896-1896 |
子類 曝氣 and Combining |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12545-12545 |
子類 ChemicalSynthesis and Combining |
| No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2893-2893 |
子類 鹽鹼 and Combining |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17528-17528 |
子類 攪拌 and Combining |
| 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 |
|
Combining