One interesting aspect of this concrete example is that even though the two statements seem contradictory at first sight, there are in fact two assignments of t

One interesting aspect of this concrete example is that even though the two statements seem contradictory at first sight, there are in fact two assignments of truth values to statements so that no contradiction arises. For instance, using Scryer Prolog and its SAT solver to model the situation: ?- sat(S1 =:= (S2 =:= 0)), sat(S2 =:= (S1 =:= 0)). As answer, we get a symbolic expression that compactly captures all concrete solutions: clpb:sat(S1=\=S2) This means that as long as the truth value of S1 is different from that of S2, the puzzle is solved. This is intuitively admissible, because if one of the statements is false, then the other is true. It would be different if for example Statement 1 said “Statement 1 is false”, because then there is no satisfiable assignment at all: ?- sat(S1 =:= (S1 =:= 0)). false.