No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2334-2334 |
Transitive relation is disjoint from intransitive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 93-93 |
immediate instance is an instance of intransitive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 151-151 |
immediate subclass is an instance of intransitive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 108-108 |
inverse is an instance of intransitive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 8324-8324 |
meets temporally is an instance of intransitive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1278-1278 |
member is an instance of intransitive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16363-16363 |
parent is an instance of intransitive relation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4208-4208 |
penetrates is an instance of intransitive relation |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 900-900 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1007-1007 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 576-576 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 106-106 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 109-109 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2261-2261 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 528-528 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 143-143 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 597-597 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 110-110 |
|