No TPTP formula. May not be expressible in strict first order. |
Merge.kif 1398-1398 |
语言式表达 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13280-13280 |
箭头图标 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13229-13229 |
蓝图 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13241-13241 |
图表 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
ComputerInput.kif 447-447 |
ComputerTouchscreenKeyboard 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13251-13251 |
旗 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
ComputingBrands.kif 2998-2998 |
资料夹 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 13284-13284 |
地图 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Merge.kif 15868-15868 |
代表性的艺术作品 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 29521-29521 |
TradingCard 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
ComputerInput.kif 842-842 |
UIElement 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
ComputerInput.kif 1181-1181 |
UserDirectAction 是 图标 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 836-836 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 874-874 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 512-512 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 44-44 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 47-47 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2197-2197 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 464-464 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 79-79 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 533-533 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 48-48 |
|