| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13603-13603 |
例 聽得見 and SoundAttribute |
| No TPTP formula. May not be expressible in strict first order. |
Merge.kif 13604-13604 |
例 Inaudible and SoundAttribute |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 19434-19434 |
例 強調 and SoundAttribute |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1255-1255 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1731-1731 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 933-933 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 468-468 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 471-471 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2617-2617 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 885-885 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 473-473 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 507-507 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 954-954 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 472-472 |
|
