[grubb]

Alternatively using z3 [0]:

  (declare-const a1 Bool)
  (declare-const a2 Bool)
  (declare-const a3 Bool)
  (declare-const a4 Bool)
  (declare-const a5 Bool)
  (declare-const a6 Bool)

  (assert (= a1 (and a2 (and a3 (and a4 (and a5 a6))))))
  (assert (= a2 (not (or a3 (or a4 (or a5 a6))))))
  (assert (= a3 (and a1 a2)))
  (assert (= a4 (or a1 (or a2 a3))))
  (assert (= a5 (not (or a1 (or a2 (or a3 a4))))))
  (assert (= a6 (not (or a1 (or a2 (or a3 (or a4 a5)))))))
  (assert (or a1 (or a2 (or a3 (or a4 (or a5 a6))))))

  (check-sat)
  (get-model)
  (exit)

The model is satisfiable where only a5 is true, anyone can run it themselves and play with it [1].

Additionally forcing a5 to be false by adding the following to the list of assertions:

  (assert (not a5))

And the model becomes unsatisfiable.

Edit: Finally, to make sure there's not some possible solution where a5 is true as well as another assertion you could alternatively add this assertion:

  (assert (and a5 (or a1 (or a2 (or a3 (or a4 (or a6)))))))

And the model also becomes unsatisfiable. So 5 only seems to be the correct answer.

[0] https://github.com/Z3Prover/z3

[1] https://rise4fun.com/Z3/1DMW

[Recursing]

I posted a solution using the python z3 library, which might be easier to use for people used to python, here: https://news.ycombinator.com/item?id=21545143

[Recursing]

That solution was not correct, see https://news.ycombinator.com/item?id=21568151