Agree with John, absolutely. The ATPL questions are really about the mathematical manipulation of the formula, not about the real world. Don't get me going on this, I have real problems trying to juggle truth with exams. As Goedel said, to every w-consistent class k of formulae there correspond recursive class signs r, such that neither v Gen r nor negative (v Gen r) belongs to Flg k (where v is the free variable of r).
Or, truth is a more powerful concept than proof.
Dick W