Translate the following inference to logic notation: For all x, if x_14 plays a game, then x_14 is listening to a song. Charles is not listening to a song. John is a taxi driver. Therefore John is a taxi driver and Charles is not playing a game.
forall x: P(x) -> Q(x). ~Q(a). p. Therefore p and ~P(a).