No TPTP formula. May not be expressible in strict first order. | Merge.kif 2067-2067 | 时间单位 是 恒量 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2073-2073 | 持续时间 是 时间单位 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 2078-2078 | 时间位置 是 时间单位 的 subclass |