Translate the following inference to logic notation: For all x, if x_12 were poor, then x_12 is rich. Charles is not poor. Charles is rich if and only if Charles is poor. Therefore Charles is not rich.
forall x: P(x) -> Q(x). ~P(a). Q(a) <-> P(a). Therefore ~Q(a).