No TPTP formula. May not be expressible in strict first order. | Merge.kif 5819-5819 | 图元素 是 命题 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5832-5832 | 图节点 是 图元素 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 5842-5842 | 图弧 是 图元素 的 subclass |