Logic puzzle: which answer is correct?

which_answer.v

(**
  
Which answer is correct?
 1. All of the below.
 2. None of the below.
 3. All of the above.
 4. At least one of the above.
 5. None of the above.
 6. None of the above.

**)

Require Import Bool.
Notation "-- a" := (negb a) (at level 10).
Notation " a <--> b" := (eqb a b) (at level 100).
Definition puzzle a1 a2 a3 a4 a5 a6 :=
  (a1 <--> (a2 && a3 && a4 && a5 && a6))   &&
  (a2 <--> --(a3||a4||a5||a6))  &&
  (a3 <--> (a1&&a2))         &&
  (a4 <--> (a1||a2||a3))        &&
  (a5 <--> -- (a1||a2||a3||a4))  &&
  (a6 <--> -- (a1||a2||a3||a4||a5)).

Goal exists a1 a2 a3 a4 a5 a6, puzzle a1 a2 a3 a4 a5 a6 = true.
  assert ( forall a1 a2 a3 a4 a5 a6, puzzle a1 a2 a3 a4 a5 a6 = false).
  (* to get rid of all the failed cases with auto, and only keep the good ones *)
  intros a1 a2 a3 a4 a5 a6;
    remember (a1,a2,a3,a4,a5,a6) as Q;
    destruct a1,a2,a3,a4,a5,a6; simpl; auto.
  (* now we have the good ones left. see what we have in Q and use that *)
  Restart.
  now exists false, false, false, false, true, false.
Qed.

(* show it is the only answer *)
Goal forall a1 a2 a3 a4 a5 a6,
    puzzle a1 a2 a3 a4 a5 a6 = true <->
    ( a1, a2, a3, a4, a5, a6) = (false, false, false, false, true, false).
  split.
  now destruct a1,a2,a3,a4,a5,a6; compute; inversion 1.
  now inversion 1.
Qed.