Let

P_{1}(x) = ∃y · (x_{1}x_{2} = y_{1}y_{2}) ∧ x ≠ y
P_{2}(x) = (∃y · (x_{1} + x_{2} = y_{1} + y_{2}) ∧ x ≠ y) ∧ (∀y · (x_{1} + x_{2} = y_{1} + y_{2}) ⇒ P_{1}(y))
P_{3}(x) = ∀y · ((x_{1}x_{2} = y_{1}y_{2}) ∧ P_{2}(y)) ⇒ x = y
P_{4}(x) = ∀y · ((x_{1} + x_{2} = y_{1} + y_{2}) ∧ P_{3}(y)) ⇒ x = y

Find (the unique) x such that

P_{1}(x) ∧ P_{2}(x) ∧ P_{3}(x) ∧ P_{4}(x)

Here all variables are quantified over unordered pairs of integers in the range [2, 99] (take x_{1} ≤ x_{2} say).