Quantifier Logic : Translation of sentence "All students have already done the exam for all course except course X" As the title said, what is the best translation for "All students have already done the exam for all course except course X"?
Me and my fellow students debated for quite a long time about this question. We use x is a domain of students and y is a domain of the courses, and Predicate P(x,y) is x already done exam course X. My answer is $$\forall x \forall y (P(x,y) \iff (y \neq Course X))$$
One of my friend answer is $$\forall x \forall y(P(x,y) \implies (y \neq Course X))$$
and the other answer is $$\forall x \forall y (P(x,y) \implies (y \neq Course X)) \land \exists x(\lnot P(x, Course X))$$
Which one do you think is right? And if none are right, what is the translation and why?
Consider $S$ be the domain of students.

And $C:$ be the domain of course tests.  

Let  $\text{X-Course}$ be the "name" of the course to be excluded (err, the course that no student has yet taken a test in).

Let $P(x, y)$ denote "$x$ has taken $y$."



$$\forall x \in S, \forall y \in C \Big((y \neq \text{X-Course})\to P(x, y) \Big)$$

Or we can say, $$\forall x \in S, \forall y \in (C\setminus \{\text{X-Course}\}) \Big(P(x, y)\Big)$$

where $C\setminus \{\text{X-Course}\}$ is the set of all course tests, except for the test for Course $X$.

$\Huge($ And if you insist on the fact that we are to assume that the domain for $x$ is "All students", and the domain for $y$ is "All courses", with $P(x, y)$ meaning $x$ has taken the test in course $y$, and $X$ the name for the course in which no test has yet been taken,

Then at its simplest, we have: $$\forall x, \forall y\Big(\big(y\neq X\big) \ \rightarrow P(x, y)\Big)\Huge)$$



Alternatively, let the domain $D$ of x, y, consist of all persons, places, things.  

Let $S(x)$ denote that element $x\in D$ is a student.

Let $C(x)$ denote that element $x \in D$ is a test for an academic course.

Let $P(x, y)$ denote "x has taken y".

Let $\text{X-Course }$ name the "not-yet-if-ever tested academic course X"

Then the sentence you are given can be translated as follows: 

$$ \forall x, \forall y\Big(\big(S(x) \land C(y) \land (y \neq \text{X-course})\big) \to P(x, y)\Big)$$
$\forall x,y (P(x,y) \iff (y \neq Course X))$ can also be accepted, meaning no one has done exam for $X$ but all did other exams

EDIT

$$\forall x \forall y ((y \neq Course X) \implies P(x,y)) \land \exists x(\lnot P(x, Course X))$$
So the other answer you provided is close to being right only it has to switch places in the implication. This means each exam not being $X$ has been done but also fact is that not everyone has done $X$, so there is someone who didn't do it