No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 239-239 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 240-240 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 137-137 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-it.txt 282-282 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1968-1968 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 89-89 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-de.txt 308-308 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-hindi.txt 319-319 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 156-156 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-sv.txt 142-142 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 474-474 |
|
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 4578-4578 |
subsumes content instance is internally related to subsumes content class |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 240-240 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 55817-55817 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 55816-55816 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-de.txt 99-99 |
|