Alternatively using z3 [0]: (declare-const a1 Bool) (declare-const a2 Bool) (declare-const a3 Bool) (declare-const a4 Bool) (declare-const a5 Bool)

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 https://github.com/Z3Prover/z3 [1] https://rise4fun.com/Z3/1DMW https://rise4fun.com/Z3/1DMW