| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 207-207 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 208-208 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 123-123 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-it.txt 98-98 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1952-1952 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 75-75 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-de.txt 266-266 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-hindi.txt 138-138 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 142-142 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-sv.txt 128-128 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 208-208 |
|
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4551-4551 |
内容等效实例 和 内容等效类 是 内部相关 |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 208-208 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 22366-22366 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 22365-22365 |
|
| No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 22364-22364 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-de.txt 85-85 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 209-209 |
|
equivalentContentClass