Translate the following inference to logic notation: For all x, y_4 will not drive a car. It is cloudy if and only if Thomas is driving a car. Therefore it is not cloudy.
forall x: ~P(x). p <-> P(a). Therefore ~p.