(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]. (assert (not a5))
And the model becomes unsatisfiable. (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.
I don't have a ton of experience with Western Governor's, but the fact that unlike many online universities they are nonprofit is a good sign. Of course, whether they have access to quality instructors is an unknown to me.
[1]: https://finserve.byu.edu/students-parents/tuition-fees-deadl...