| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14587-14587 |
子類 廣播節目 and Series |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14672-14672 |
子類 Periodical and Series |
| No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1042-1042 |
|
| No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1295-1295 |
|
| No TPTP formula. May not be expressible in strict first order. |
french_format.kif 720-720 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 251-251 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 254-254 |
|
| No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2404-2404 |
|
| No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 672-672 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 256-256 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 290-290 |
|
| No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 741-741 |
|
| No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 255-255 |
|
