No TPTP formula. May not be expressible in strict first order. | engineering.kif 767-767 | Gearbox is a subclass of engineering component |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 2339-2339 | Transmission is a subclass of gearbox |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 3963-3963 | Steering box is a subclass of gearbox |