No TPTP formula. May not be expressible in strict first order. | engineering.kif 767-767 | 变速器 是 工程组件 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 2339-2339 | AutomobileTransmission 是 变速器 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3963-3963 | SteeringBox 是 变速器 的 subclass |