Translate the following inference to logic notation: For all x, x_17 is poor or x_17 will drink water. Mary is not poor. Thomas is a server if and only if Mary is drinking water. Therefore Thomas is a server.
forall x: P(x) or Q(x). ~P(a). p <-> Q(a). Therefore p.