No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 2991-2991 |
Transit route is a subclass of region |
No TPTP formula. May not be expressible in strict first order. |
Transportation.kif 2924-2924 |
Transit stop is a subclass of region |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 14287-14287 |
Transitway is a subclass of region |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 17672-17672 |
Under water is a subclass of region |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 831-831 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 864-864 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 507-507 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 39-39 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 42-42 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2192-2192 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 459-459 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 74-74 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 528-528 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 43-43 |
|