| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15349-15349 |
子類 NounPhrase and Phrase |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15370-15370 |
子類 PrepositionalPhrase and Phrase |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15338-15338 |
子類 VerbPhrase and Phrase |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1034-1034 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1280-1280 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 712-712 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 244-244 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 247-247 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2395-2395 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 664-664 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 249-249 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 282-282 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 733-733 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 248-248 |
|
Phrase