| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15328-15328 |
名词短语 和 % 2 是 disjoint |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15302-15302 |
短语 分拆成不相交的 动词短语, 名词短语, 和 介词短语 |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1035-1035 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1282-1282 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 713-713 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 245-245 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 248-248 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2396-2396 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 665-665 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 250-250 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 283-283 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 734-734 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 249-249 |
|
VerbPhrase