Translate the following inference to logic notation: For all x, x_7 will sleep or x_7 will not play tennis. John is playing tennis. Therefore John is sleeping.
forall x: P(x) or ~Q(x). Q(a). Therefore P(a).