| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5143-5143 | Light bulb is a subclass of electric light fixture |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5155-5155 | LE d is a subclass of light bulb |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5159-5159 | Fluorescent light bulb is a subclass of light bulb |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 5162-5162 | Light bulb is a subclass of light bulb |
|
|