Past exam of the computer science course of the University of Oxford / 2015 / Logic and proof / 3 / a / C / Solution

The same person $y$ must both love $x$ and be loved by $x$:Equivalently, use $\forall x\forall y[(L(y,x)\wedge L(x,y))\to H(x)]$. There is no restriction that $x$ and $y$ be distinct; this matters when the later ground resolution proof considers Lucy loving herself.