No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 231-231 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 232-232 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 135-135 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-it.txt 255-255 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 1964-1964 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 87-87 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-de.txt 302-302 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-hindi.txt 292-292 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 154-154 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-sv.txt 140-140 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-tg.txt 447-447 |
|
No TPTP formula. May not be expressible in strict first order. |
Media.kif 3111-3111 |
title in language is a subrelation of represents in language |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 232-232 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 49544-49544 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 49543-49543 |
|
No TPTP formula. May not be expressible in strict first order. |
domainEnglishFormat.kif 49542-49542 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-de.txt 97-97 |
|