No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12483-12483 |
Separating is disjoint from combining |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2472-2472 |
Acidifying is a subclass of combining |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 1896-1896 |
Aerating is a subclass of combining |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 12523-12523 |
Chemical synthesis is a subclass of combining |
No TPTP formula. May not be expressible in strict first order. |
Geography.kif 2893-2893 |
Salinifying is a subclass of combining |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17529-17529 |
Stirring is a subclass of 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 |
|