No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3062-3062 | 车灯 是 灯具 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3074-3074 | 车灯 是 车灯 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Mid-level-ontology.kif 3085-3085 | 尾灯 是 车灯 的 subclass |