No TPTP formula. May not be expressible in strict first order. | Cars.kif 4572-4572 | EightCylinderEngine 是 IntermittentCombustionEngine 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 4720-4720 | RoverV8Engine 是 EightCylinderEngine 的 subclass |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 5122-5122 | GMLs1V8engine 是 EightCylinderEngine 的 subclass |