No TPTP formula. May not be expressible in strict first order. |
Merge.kif 2334-2334 |
不相交的 TransitiveRelation and IntransitiveRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 93-93 |
例 立即實例 and IntransitiveRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 151-151 |
例 直接子類 and IntransitiveRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 108-108 |
例 逆 and IntransitiveRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 8360-8360 |
例 短暫相遇 and IntransitiveRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1278-1278 |
例 會員 and IntransitiveRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 16434-16434 |
例 親 and IntransitiveRelation |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4209-4209 |
例 滲透 and IntransitiveRelation |
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 |
|