(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :mbqi true)
; Note that, since no compartments are needed, this solution uses many aux. variables instead of building a transition relation.
(declare-const dev0 bool)
(declare-const dev1 bool)
(declare-const dev2 bool)
(declare-const dev3 bool)
(declare-const dev4 bool)
(declare-const in0 bool)
(declare-const out0 bool)
(assert (and (implies (= in0 true) (not (and (= dev0 false) (= dev3 false))))
     (implies (not (and (= dev0 false) (= dev3 false))) (= in0 true))))
(assert (= out0 false))
(declare-const in1 bool)
(declare-const out1 bool)
(assert (and (implies (= in1 true) (not (and (= dev1 false) (= dev3 false))))
     (implies (not (and (= dev1 false) (= dev3 false))) (= in1 true))))
(assert (and (implies (= out1 true) (not (and (= dev0 false) (= dev4 false))))
     (implies (not (and (= dev0 false) (= dev4 false))) (= out1 true))))
(declare-const in2 bool)
(declare-const out2 bool)
(assert (= in2 false))
(assert (and (implies (= out2 true) (not (and (= dev1 false) (= dev4 false))))
     (implies (not (and (= dev1 false) (= dev4 false))) (= out2 true))))
(declare-const in3 bool)
(declare-const out3 bool)
(assert (and (implies (= in3 true) (not (and (= dev4 false))))
     (implies (not (and (= dev4 false))) (= in3 true))))
(assert (and (implies (= out3 true) (not (and (= dev3 false))))
     (implies (not (and (= dev3 false))) (= out3 true))))
(declare-const in4 bool)
(declare-const out4 bool)
(assert (and (implies (= in4 true) (not (and (= dev2 false))))
     (implies (not (and (= dev2 false))) (= in4 true))))
(assert (and (implies (= out4 true) (not (and (= dev3 false))))
     (implies (not (and (= dev3 false))) (= out4 true))))
(declare-const in5 bool)
(declare-const out5 bool)
(assert (and (implies (= in5 true) (not (and (= dev4 false))))
     (implies (not (and (= dev4 false))) (= in5 true))))
(assert (and (implies (= out5 true) (not (and (= dev2 false))))
     (implies (not (and (= dev2 false))) (= out5 true))))
(assert (and (not (and dev0 dev4))
     (not (and dev1 dev4))
     (not (and dev4 dev0))
     (not (and dev4 dev1))
     (= out2 true)
     (= in0 true)
     (implies (= in1 true) (= out1 true))
     (implies (= in2 true) (= out2 true))
     (implies (= in3 true) (= out3 true))
     (implies (= in4 true) (= out4 true))
     (implies (= in5 true) (= out5 true))
     (implies (= out0 true) (= in0 true))
     (implies (= out1 true) (= in1 true))
     (implies (= out3 true) (= in3 true))
     (implies (= out4 true) (= in4 true))
     (implies (= out5 true) (= in5 true))))

(echo "Are there additional solutions?")
(check-sat)
(echo "Enabled devices:")
(eval dev0)
(eval dev1)
(eval dev2)
(eval dev3)
(eval dev4)

(echo "Are there additional solutions?")
(assert (not (and (= dev0 false)
          (= dev1 false)
          (= dev2 true)
          (= dev3 true)
          (= dev4 true))))
(check-sat)
(echo "Enabled devices:")
(eval dev0)
(eval dev1)
(eval dev2)
(eval dev3)
(eval dev4)

(echo "Are there additional solutions?")
(assert (not (and (= dev0 true)
          (= dev1 true)
          (= dev2 false)
          (= dev3 false)
          (= dev4 false))))
(check-sat)
(get-info :all-statistics)