No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14678-14678 |
Article is disjoint from book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7864-7864 |
Christian bible is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 26410-26410 |
Guide book is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7879-7879 |
New testament is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14946-14946 |
Novel is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 7875-7875 |
Old testament is a subclass of book |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14913-14913 |
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 |
|