No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14705-14705 |
Article is disjoint from book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7891-7891 |
Christian bible is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 26443-26443 |
Guide book is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7906-7906 |
New testament is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14973-14973 |
Novel is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7902-7902 |
Old testament is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14940-14940 |
Reference book is a subclass of book |
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 |
|