jhoechtl

An expert system answer (Prolog, CLIPS) would be cool to see here.

tephra

Using the clpb library [0]:

  solution([A1,A2,A3,A4,A5,A6]) :-
        sat(A1 =:= A2*A3*A4*A5*A6),
        sat(A2 =:= ~(A3+A4+A5+A6)),
        sat(A3 =:= A1*A2),
        sat(A4 =:= A1+A2+A3),
        sat(A5 =:= ~(A1+A2+A3+A4)),
        sat(A6 =:= ~(A1+A2+A3+A4+A5)).
[0] https://www.metalevel.at/prolog/puzzles
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