No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 3711-3711 |
家具 和 % 2 是 disjoint |
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 1784-1784 |
机器 是 机械制造业 的 industry 产品类别 |
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 2051-2051 |
AirConditioningCondenser 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 2075-2075 |
AirConditioningEvaporator 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 5176-5176 |
GasCompressor 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Cars.kif 1190-1190 |
Generator 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 25510-25510 |
IceMachine 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 5986-5986 |
车床 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
engineering.kif 742-742 |
发动机 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Economy.kif 6013-6013 |
刨床 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
Mid-level-ontology.kif 1954-1954 |
售货机 是 机器 的 subclass |
No TPTP formula. May not be expressible in strict first order. |
chinese_format.kif 1060-1060 |
|
No TPTP formula. May not be expressible in strict first order. |
english_format.kif 1331-1331 |
|
No TPTP formula. May not be expressible in strict first order. |
french_format.kif 738-738 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-hindi.txt 269-269 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-it.txt 272-272 |
|
No TPTP formula. May not be expressible in strict first order. |
japanese_format.kif 2422-2422 |
|
No TPTP formula. May not be expressible in strict first order. |
portuguese_format.kif 690-690 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cb.txt 274-274 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-cz.txt 308-308 |
|
No TPTP formula. May not be expressible in strict first order. |
relations-ro.kif 759-759 |
|
No TPTP formula. May not be expressible in strict first order. |
terms-tg.txt 273-273 |
|