Why this first-order logic formula is not correct?

Question

I'm studing computer science at university, in specific Artificial Intelligence. We are using Otter as Theorem prover.

I'm having some problems formalizing this:

"John, Mary and Derek are three people. They work as cook, waiter or manager, but the order is unknown. John, a friend of Mary's brother, is younger than Mary. John's eyes are black. The waiter's eyes are blue. The manager has no brother or sister and he's the oldest. Use Otter to find the correct work of each one."

In particular, formalizing the younger-older relationship, I tried to write it like this:

But when I write it in otter, the solver starts to loop and never find the solution. Example:

set(auto).

formula_list(usable).
all x y (younger(x, y) & x != y <-> -younger(y, x)).
younger(A, B).

end_of_list.

Answer 1

Try implementing something like: $$ \forall x ~ [isOldest(x) \iff \forall y ~ [\neg isYounger(x,y)]] $$

---

From the information, we are given that $isYounger(John, Mary)$. Now consider $x = John$. Observe that we have found some $y$ (namely $y = Mary$) such that $isYounger(x,y)$. Hence, by the above rule, it follows that $\neg isOldest(John)$. But since the oldest person is male and the only other male is Derek, we must have that $isOldest(Derek)$ so that Derek is the manager.

Answer 2

Shouldn't it be

all x y (younger(x, y) & x != y <-> -younger(y, x) & x!= y)

?