Challenge 3: Why X Stays Unbound After \+ flight(paris, X) — Possible Solution ==================================================================== flights.pl: flight(paris, london). flight(london, paris). flight(paris, rome). Query: ?- \+ flight(paris, X). false. ?- X == london. <-- would raise an "X is unbound" style issue; X was never bound by the query above -- Explanation -- -- -- \+ Goal is defined as Goal, !, fail. followed by a fallback clause -- that just succeeds -- notice neither clause ever unifies its own -- result with anything visible to the caller. When Goal (here, -- flight(paris, X)) succeeds internally -- for X = london, among -- others -- that internal proof triggers the cut and the fail, which -- discards the ENTIRE proof, bindings included, as part of forcing -- the failure. Prolog's backtracking then undoes whatever binding -- flight(paris, X) had produced for X, the same as it would for any -- other failed goal. And in the case where \+ Goal succeeds instead -- (Goal has no solutions at all), there was never any binding to -- expose in the first place, since Goal never succeeded even once. -- Either way -- whether \+ Goal succeeds or fails -- X comes back -- exactly as unbound as it started. \+ can only ever report a -- yes/no answer about provability; it was never designed to hand -- back the bindings that made a goal provable or not. WHY THIS WORKS AS AN ANSWER ------------------------------ This traces both possible outcomes of \+ flight(paris, X) (success and failure) back to the chapter's own Goal, !, fail definition, showing in both cases why any binding Goal might have produced internally is discarded rather than surfaced to the caller.