No TPTP formula. May not be expressible in strict first order. | Cars.kif 4480-4480 | Unpowered device is a subclass of device |
No TPTP formula. May not be expressible in strict first order. | Cars.kif 4471-4471 | Hand tool is a subclass of unpowered device |