| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3375-3375 | 子類 VehicleSafetyDevice and SafetyDevice |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3624-3624 | 子類 AutoAirbag and VehicleSafetyDevice |
| No TPTP formula. May not be expressible in strict first order. | Cars.kif 3658-3658 | 子類 SeatBelt and VehicleSafetyDevice |
|
|