| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14588-14588 |
广播节目 是 系列 的 subclass |
| No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 14673-14673 |
期刊 是 系列 的 subclass |
| 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 |
|
