Translate the following inference to logic notation: For all x, x_16 will climb a mountain if and only if x_16 will listen to a song. Sarah is not climbing a mountain. John is sad if and only if Sarah is not listening to a song. Therefore John is sad.
forall x: P(x) <-> Q(x). ~P(a). p <-> ~Q(a). Therefore p.