Translate the following inference to logic notation: If Charles drives a car, then Susan is excited. If Susan were excited, then Charles is driving a car. For all x, x is excited or x will work. Charles is not driving a car. Therefore Susan is working.
p -> P(a). P(a) -> p. forall x: P(x) or Q(x). ~p. Therefore Q(a).