Translate the following inference to logic notation: For all x, if x_10 were happy, then x_10 is listening to a song. John is not listening to a song. John is happy or Charles is driving a car. Therefore Charles is driving a car.
forall x: P(x) -> Q(x). ~Q(a). P(a) or p. Therefore p.