(declare-fun b_1_2_4 () Bool)
(declare-fun b_1_1_4 () Bool)
(declare-fun b_1_0_4 () Bool)
(declare-fun b_0_2_4 () Bool)
(declare-fun b_0_1_4 () Bool)
(declare-fun b_0_0_4 () Bool)
(declare-fun |(switch_b_0_1 )_0| () Bool)
(declare-fun |(switch_b_0_2 )_0| () Bool)
(declare-fun b_0_0_0 () Bool)
(declare-fun |(switch_b_0_0 )_0| () Bool)
(declare-fun |(switch_b_0_0 )_1| () Bool)
(declare-fun b_0_1_0 () Bool)
(declare-fun |(switch_b_0_1 )_1| () Bool)
(declare-fun b_0_2_0 () Bool)
(declare-fun |(switch_b_0_2 )_1| () Bool)
(declare-fun |(switch_b_1_1 )_0| () Bool)
(declare-fun |(switch_b_1_2 )_0| () Bool)
(declare-fun b_1_0_0 () Bool)
(declare-fun |(switch_b_1_0 )_0| () Bool)
(declare-fun |(switch_b_1_0 )_1| () Bool)
(declare-fun b_1_1_0 () Bool)
(declare-fun |(switch_b_1_1 )_1| () Bool)
(declare-fun b_1_2_0 () Bool)
(declare-fun |(switch_b_1_2 )_1| () Bool)
(declare-fun b_0_0_1 () Bool)
(declare-fun |(switch_b_0_0 )_2| () Bool)
(declare-fun b_0_1_1 () Bool)
(declare-fun |(switch_b_0_1 )_2| () Bool)
(declare-fun b_0_2_1 () Bool)
(declare-fun |(switch_b_0_2 )_2| () Bool)
(declare-fun b_1_0_1 () Bool)
(declare-fun |(switch_b_1_0 )_2| () Bool)
(declare-fun b_1_1_1 () Bool)
(declare-fun |(switch_b_1_1 )_2| () Bool)
(declare-fun b_1_2_1 () Bool)
(declare-fun |(switch_b_1_2 )_2| () Bool)
(declare-fun b_0_0_2 () Bool)
(declare-fun |(switch_b_0_0 )_3| () Bool)
(declare-fun b_0_1_2 () Bool)
(declare-fun |(switch_b_0_1 )_3| () Bool)
(declare-fun b_0_2_2 () Bool)
(declare-fun |(switch_b_0_2 )_3| () Bool)
(declare-fun b_1_0_2 () Bool)
(declare-fun |(switch_b_1_0 )_3| () Bool)
(declare-fun b_1_1_2 () Bool)
(declare-fun |(switch_b_1_1 )_3| () Bool)
(declare-fun b_1_2_2 () Bool)
(declare-fun |(switch_b_1_2 )_3| () Bool)
(declare-fun b_0_0_3 () Bool)
(declare-fun |(switch_b_0_0 )_4| () Bool)
(declare-fun b_0_1_3 () Bool)
(declare-fun |(switch_b_0_1 )_4| () Bool)
(declare-fun b_0_2_3 () Bool)
(declare-fun |(switch_b_0_2 )_4| () Bool)
(declare-fun b_1_0_3 () Bool)
(declare-fun |(switch_b_1_0 )_4| () Bool)
(declare-fun b_1_1_3 () Bool)
(declare-fun |(switch_b_1_1 )_4| () Bool)
(declare-fun b_1_2_3 () Bool)
(declare-fun |(switch_b_1_2 )_4| () Bool)
(declare-fun |(switch_b_0_0 )_5| () Bool)
(declare-fun |(switch_b_0_1 )_5| () Bool)
(declare-fun |(switch_b_0_2 )_5| () Bool)
(declare-fun |(switch_b_1_0 )_5| () Bool)
(declare-fun |(switch_b_1_1 )_5| () Bool)
(declare-fun |(switch_b_1_2 )_5| () Bool)
(declare-fun cost_1_0 () Real)
(declare-fun cost_1_1 () Real)
(declare-fun cost_0_0 () Real)
(declare-fun cost_0_1 () Real)
(declare-fun cost_1_2 () Real)
(declare-fun cost_0_2 () Real)
(declare-fun cost_1_3 () Real)
(declare-fun cost_0_3 () Real)
(declare-fun cost_1_4 () Real)
(declare-fun cost_0_4 () Real)
(assert (and b_0_0_4 b_0_1_4 b_0_2_4 b_1_0_4 b_1_1_4 b_1_2_4))
(assert (=> |(switch_b_0_0 )_1|
    (or |(switch_b_0_0 )_0| b_0_0_0 |(switch_b_0_2 )_0| |(switch_b_0_1 )_0|)))
(assert (=> |(switch_b_0_1 )_1|
    (or |(switch_b_0_1 )_0| b_0_1_0 |(switch_b_0_2 )_0| |(switch_b_0_0 )_0|)))
(assert (=> |(switch_b_0_2 )_1|
    (or |(switch_b_0_2 )_0| b_0_2_0 |(switch_b_0_1 )_0| |(switch_b_0_0 )_0|)))
(assert (=> |(switch_b_1_0 )_1|
    (or |(switch_b_1_0 )_0| b_1_0_0 |(switch_b_1_2 )_0| |(switch_b_1_1 )_0|)))
(assert (=> |(switch_b_1_1 )_1|
    (or |(switch_b_1_1 )_0| b_1_1_0 |(switch_b_1_2 )_0| |(switch_b_1_0 )_0|)))
(assert (=> |(switch_b_1_2 )_1|
    (or |(switch_b_1_2 )_0| b_1_2_0 |(switch_b_1_1 )_0| |(switch_b_1_0 )_0|)))
(assert (=> |(switch_b_0_0 )_2|
    (or |(switch_b_0_0 )_1| b_0_0_1 |(switch_b_0_2 )_1| |(switch_b_0_1 )_1|)))
(assert (=> |(switch_b_0_1 )_2|
    (or |(switch_b_0_1 )_1| b_0_1_1 |(switch_b_0_2 )_1| |(switch_b_0_0 )_1|)))
(assert (=> |(switch_b_0_2 )_2|
    (or |(switch_b_0_2 )_1| b_0_2_1 |(switch_b_0_1 )_1| |(switch_b_0_0 )_1|)))
(assert (=> |(switch_b_1_0 )_2|
    (or |(switch_b_1_0 )_1| b_1_0_1 |(switch_b_1_2 )_1| |(switch_b_1_1 )_1|)))
(assert (=> |(switch_b_1_1 )_2|
    (or |(switch_b_1_1 )_1| b_1_1_1 |(switch_b_1_2 )_1| |(switch_b_1_0 )_1|)))
(assert (=> |(switch_b_1_2 )_2|
    (or |(switch_b_1_2 )_1| b_1_2_1 |(switch_b_1_1 )_1| |(switch_b_1_0 )_1|)))
(assert (=> |(switch_b_0_0 )_3|
    (or |(switch_b_0_0 )_2| b_0_0_2 |(switch_b_0_2 )_2| |(switch_b_0_1 )_2|)))
(assert (=> |(switch_b_0_1 )_3|
    (or |(switch_b_0_1 )_2| b_0_1_2 |(switch_b_0_2 )_2| |(switch_b_0_0 )_2|)))
(assert (=> |(switch_b_0_2 )_3|
    (or |(switch_b_0_2 )_2| b_0_2_2 |(switch_b_0_1 )_2| |(switch_b_0_0 )_2|)))
(assert (=> |(switch_b_1_0 )_3|
    (or |(switch_b_1_0 )_2| b_1_0_2 |(switch_b_1_2 )_2| |(switch_b_1_1 )_2|)))
(assert (=> |(switch_b_1_1 )_3|
    (or |(switch_b_1_1 )_2| b_1_1_2 |(switch_b_1_2 )_2| |(switch_b_1_0 )_2|)))
(assert (=> |(switch_b_1_2 )_3|
    (or |(switch_b_1_2 )_2| b_1_2_2 |(switch_b_1_1 )_2| |(switch_b_1_0 )_2|)))
(assert (=> |(switch_b_0_0 )_4|
    (or |(switch_b_0_0 )_3| b_0_0_3 |(switch_b_0_2 )_3| |(switch_b_0_1 )_3|)))
(assert (=> |(switch_b_0_1 )_4|
    (or |(switch_b_0_1 )_3| b_0_1_3 |(switch_b_0_2 )_3| |(switch_b_0_0 )_3|)))
(assert (=> |(switch_b_0_2 )_4|
    (or |(switch_b_0_2 )_3| b_0_2_3 |(switch_b_0_1 )_3| |(switch_b_0_0 )_3|)))
(assert (=> |(switch_b_1_0 )_4|
    (or |(switch_b_1_0 )_3| b_1_0_3 |(switch_b_1_2 )_3| |(switch_b_1_1 )_3|)))
(assert (=> |(switch_b_1_1 )_4|
    (or |(switch_b_1_1 )_3| b_1_1_3 |(switch_b_1_2 )_3| |(switch_b_1_0 )_3|)))
(assert (=> |(switch_b_1_2 )_4|
    (or |(switch_b_1_2 )_3| b_1_2_3 |(switch_b_1_1 )_3| |(switch_b_1_0 )_3|)))
(assert (=> |(switch_b_0_0 )_5|
    (or |(switch_b_0_0 )_4| b_0_0_4 |(switch_b_0_2 )_4| |(switch_b_0_1 )_4|)))
(assert (=> |(switch_b_0_1 )_5|
    (or |(switch_b_0_1 )_4| b_0_1_4 |(switch_b_0_2 )_4| |(switch_b_0_0 )_4|)))
(assert (=> |(switch_b_0_2 )_5|
    (or |(switch_b_0_2 )_4| b_0_2_4 |(switch_b_0_1 )_4| |(switch_b_0_0 )_4|)))
(assert (=> |(switch_b_1_0 )_5|
    (or |(switch_b_1_0 )_4| b_1_0_4 |(switch_b_1_2 )_4| |(switch_b_1_1 )_4|)))
(assert (=> |(switch_b_1_1 )_5|
    (or |(switch_b_1_1 )_4| b_1_1_4 |(switch_b_1_2 )_4| |(switch_b_1_0 )_4|)))
(assert (=> |(switch_b_1_2 )_5|
    (or |(switch_b_1_2 )_4| b_1_2_4 |(switch_b_1_1 )_4| |(switch_b_1_0 )_4|)))
(assert (=> (and (not b_1_1_0) b_1_1_1) (or |(switch_b_1_1 )_0|)))
(assert (=> (and b_1_1_0 (not b_1_1_1)) (or |(switch_b_1_2 )_0|)))
(assert (=> (and (not b_0_1_0) b_0_1_1) (or |(switch_b_0_1 )_0|)))
(assert (=> (and b_0_1_0 (not b_0_1_1)) (or |(switch_b_0_2 )_0|)))
(assert (=> (and (not b_1_2_0) b_1_2_1) (or |(switch_b_1_2 )_0|)))
(assert (=> (and (not b_0_0_0) b_0_0_1) (or |(switch_b_0_0 )_0|)))
(assert (=> (and b_0_0_0 (not b_0_0_1)) (or |(switch_b_0_1 )_0| |(switch_b_0_2 )_0|)))
(assert (=> (and (not b_1_0_0) b_1_0_1) (or |(switch_b_1_0 )_0|)))
(assert (=> (and b_1_0_0 (not b_1_0_1)) (or |(switch_b_1_1 )_0| |(switch_b_1_2 )_0|)))
(assert (=> (and (not b_0_2_0) b_0_2_1) (or |(switch_b_0_2 )_0|)))
(assert (or (= cost_1_1 cost_1_0)
    |(switch_b_1_0 )_0|
    |(switch_b_1_1 )_0|
    |(switch_b_1_2 )_0|))
(assert (or (= cost_0_1 cost_0_0)
    |(switch_b_0_0 )_0|
    |(switch_b_0_1 )_0|
    |(switch_b_0_2 )_0|))
(assert (=> (and (not b_1_1_1) b_1_1_2) (or |(switch_b_1_1 )_1|)))
(assert (=> (and b_1_1_1 (not b_1_1_2)) (or |(switch_b_1_2 )_1|)))
(assert (=> (and (not b_0_1_1) b_0_1_2) (or |(switch_b_0_1 )_1|)))
(assert (=> (and b_0_1_1 (not b_0_1_2)) (or |(switch_b_0_2 )_1|)))
(assert (=> (and (not b_1_2_1) b_1_2_2) (or |(switch_b_1_2 )_1|)))
(assert (=> (and (not b_0_0_1) b_0_0_2) (or |(switch_b_0_0 )_1|)))
(assert (=> (and b_0_0_1 (not b_0_0_2)) (or |(switch_b_0_1 )_1| |(switch_b_0_2 )_1|)))
(assert (=> (and (not b_1_0_1) b_1_0_2) (or |(switch_b_1_0 )_1|)))
(assert (=> (and b_1_0_1 (not b_1_0_2)) (or |(switch_b_1_1 )_1| |(switch_b_1_2 )_1|)))
(assert (=> (and (not b_0_2_1) b_0_2_2) (or |(switch_b_0_2 )_1|)))
(assert (or (= cost_1_2 cost_1_1)
    |(switch_b_1_0 )_1|
    |(switch_b_1_1 )_1|
    |(switch_b_1_2 )_1|))
(assert (or (= cost_0_2 cost_0_1)
    |(switch_b_0_0 )_1|
    |(switch_b_0_1 )_1|
    |(switch_b_0_2 )_1|))
(assert (=> (and (not b_1_1_2) b_1_1_3) (or |(switch_b_1_1 )_2|)))
(assert (=> (and b_1_1_2 (not b_1_1_3)) (or |(switch_b_1_2 )_2|)))
(assert (=> (and (not b_0_1_2) b_0_1_3) (or |(switch_b_0_1 )_2|)))
(assert (=> (and b_0_1_2 (not b_0_1_3)) (or |(switch_b_0_2 )_2|)))
(assert (=> (and (not b_1_2_2) b_1_2_3) (or |(switch_b_1_2 )_2|)))
(assert (=> (and (not b_0_0_2) b_0_0_3) (or |(switch_b_0_0 )_2|)))
(assert (=> (and b_0_0_2 (not b_0_0_3)) (or |(switch_b_0_1 )_2| |(switch_b_0_2 )_2|)))
(assert (=> (and (not b_1_0_2) b_1_0_3) (or |(switch_b_1_0 )_2|)))
(assert (=> (and b_1_0_2 (not b_1_0_3)) (or |(switch_b_1_1 )_2| |(switch_b_1_2 )_2|)))
(assert (=> (and (not b_0_2_2) b_0_2_3) (or |(switch_b_0_2 )_2|)))
(assert (or (= cost_1_3 cost_1_2)
    |(switch_b_1_0 )_2|
    |(switch_b_1_1 )_2|
    |(switch_b_1_2 )_2|))
(assert (or (= cost_0_3 cost_0_2)
    |(switch_b_0_0 )_2|
    |(switch_b_0_1 )_2|
    |(switch_b_0_2 )_2|))
(assert (=> (and (not b_1_1_3) b_1_1_4) (or |(switch_b_1_1 )_3|)))
(assert (=> (and b_1_1_3 (not b_1_1_4)) (or |(switch_b_1_2 )_3|)))
(assert (=> (and (not b_0_1_3) b_0_1_4) (or |(switch_b_0_1 )_3|)))
(assert (=> (and b_0_1_3 (not b_0_1_4)) (or |(switch_b_0_2 )_3|)))
(assert (=> (and (not b_1_2_3) b_1_2_4) (or |(switch_b_1_2 )_3|)))
(assert (=> (and (not b_0_0_3) b_0_0_4) (or |(switch_b_0_0 )_3|)))
(assert (=> (and b_0_0_3 (not b_0_0_4)) (or |(switch_b_0_1 )_3| |(switch_b_0_2 )_3|)))
(assert (=> (and (not b_1_0_3) b_1_0_4) (or |(switch_b_1_0 )_3|)))
(assert (=> (and b_1_0_3 (not b_1_0_4)) (or |(switch_b_1_1 )_3| |(switch_b_1_2 )_3|)))
(assert (=> (and (not b_0_2_3) b_0_2_4) (or |(switch_b_0_2 )_3|)))
(assert (or (= cost_1_4 cost_1_3)
    |(switch_b_1_0 )_3|
    |(switch_b_1_1 )_3|
    |(switch_b_1_2 )_3|))
(assert (or (= cost_0_4 cost_0_3)
    |(switch_b_0_0 )_3|
    |(switch_b_0_1 )_3|
    |(switch_b_0_2 )_3|))
(assert (= cost_0_0 0.0))
(assert (= cost_1_0 0.0))
(assert (not b_1_2_0))
(assert (not b_1_0_0))
(assert (not b_1_1_0))
(assert (not b_0_2_0))
(assert (not b_0_1_0))
(assert (not b_0_0_0))
(assert (=> |(switch_b_0_0 )_0| (not b_0_0_0)))
(assert (=> |(switch_b_0_0 )_0| b_0_0_1))
(assert (=> |(switch_b_0_0 )_0| (= cost_0_1 (+ cost_0_0 1.0))))
(assert (=> |(switch_b_0_1 )_0| (not b_0_1_0)))
(assert (=> |(switch_b_0_1 )_0| b_0_1_1))
(assert (=> |(switch_b_0_1 )_0| (not b_0_0_1)))
(assert (=> |(switch_b_0_1 )_0| (= cost_0_1 (+ cost_0_0 2.0))))
(assert (=> |(switch_b_0_2 )_0| (not b_0_2_0)))
(assert (=> |(switch_b_0_2 )_0| b_0_2_1))
(assert (=> |(switch_b_0_2 )_0| (not b_0_0_1)))
(assert (=> |(switch_b_0_2 )_0| (not b_0_1_1)))
(assert (=> |(switch_b_0_2 )_0| (= cost_0_1 (+ cost_0_0 4.0))))
(assert (=> |(switch_b_1_0 )_0| (not b_1_0_0)))
(assert (=> |(switch_b_1_0 )_0| b_1_0_1))
(assert (=> |(switch_b_1_0 )_0| (= cost_1_1 (+ cost_1_0 1.0))))
(assert (=> |(switch_b_1_1 )_0| (not b_1_1_0)))
(assert (=> |(switch_b_1_1 )_0| b_1_1_1))
(assert (=> |(switch_b_1_1 )_0| (not b_1_0_1)))
(assert (=> |(switch_b_1_1 )_0| (= cost_1_1 (+ cost_1_0 2.0))))
(assert (=> |(switch_b_1_2 )_0| (not b_1_2_0)))
(assert (=> |(switch_b_1_2 )_0| b_1_2_1))
(assert (=> |(switch_b_1_2 )_0| (not b_1_0_1)))
(assert (=> |(switch_b_1_2 )_0| (not b_1_1_1)))
(assert (=> |(switch_b_1_2 )_0| (= cost_1_1 (+ cost_1_0 4.0))))
(assert (=> |(switch_b_0_0 )_1| (not b_0_0_1)))
(assert (=> |(switch_b_0_0 )_1| b_0_0_2))
(assert (=> |(switch_b_0_0 )_1| (= cost_0_2 (+ cost_0_1 1.0))))
(assert (=> |(switch_b_0_1 )_1| (not b_0_1_1)))
(assert (=> |(switch_b_0_1 )_1| b_0_1_2))
(assert (=> |(switch_b_0_1 )_1| (not b_0_0_2)))
(assert (=> |(switch_b_0_1 )_1| (= cost_0_2 (+ cost_0_1 2.0))))
(assert (=> |(switch_b_0_2 )_1| (not b_0_2_1)))
(assert (=> |(switch_b_0_2 )_1| b_0_2_2))
(assert (=> |(switch_b_0_2 )_1| (not b_0_0_2)))
(assert (=> |(switch_b_0_2 )_1| (not b_0_1_2)))
(assert (=> |(switch_b_0_2 )_1| (= cost_0_2 (+ cost_0_1 4.0))))
(assert (=> |(switch_b_1_0 )_1| (not b_1_0_1)))
(assert (=> |(switch_b_1_0 )_1| b_1_0_2))
(assert (=> |(switch_b_1_0 )_1| (= cost_1_2 (+ cost_1_1 1.0))))
(assert (=> |(switch_b_1_1 )_1| (not b_1_1_1)))
(assert (=> |(switch_b_1_1 )_1| b_1_1_2))
(assert (=> |(switch_b_1_1 )_1| (not b_1_0_2)))
(assert (=> |(switch_b_1_1 )_1| (= cost_1_2 (+ cost_1_1 2.0))))
(assert (=> |(switch_b_1_2 )_1| (not b_1_2_1)))
(assert (=> |(switch_b_1_2 )_1| b_1_2_2))
(assert (=> |(switch_b_1_2 )_1| (not b_1_0_2)))
(assert (=> |(switch_b_1_2 )_1| (not b_1_1_2)))
(assert (=> |(switch_b_1_2 )_1| (= cost_1_2 (+ cost_1_1 4.0))))
(assert (=> |(switch_b_0_0 )_2| (not b_0_0_2)))
(assert (=> |(switch_b_0_0 )_2| b_0_0_3))
(assert (=> |(switch_b_0_0 )_2| (= cost_0_3 (+ cost_0_2 1.0))))
(assert (=> |(switch_b_0_1 )_2| (not b_0_1_2)))
(assert (=> |(switch_b_0_1 )_2| b_0_1_3))
(assert (=> |(switch_b_0_1 )_2| (not b_0_0_3)))
(assert (=> |(switch_b_0_1 )_2| (= cost_0_3 (+ cost_0_2 2.0))))
(assert (=> |(switch_b_0_2 )_2| (not b_0_2_2)))
(assert (=> |(switch_b_0_2 )_2| b_0_2_3))
(assert (=> |(switch_b_0_2 )_2| (not b_0_0_3)))
(assert (=> |(switch_b_0_2 )_2| (not b_0_1_3)))
(assert (=> |(switch_b_0_2 )_2| (= cost_0_3 (+ cost_0_2 4.0))))
(assert (=> |(switch_b_1_0 )_2| (not b_1_0_2)))
(assert (=> |(switch_b_1_0 )_2| b_1_0_3))
(assert (=> |(switch_b_1_0 )_2| (= cost_1_3 (+ cost_1_2 1.0))))
(assert (=> |(switch_b_1_1 )_2| (not b_1_1_2)))
(assert (=> |(switch_b_1_1 )_2| b_1_1_3))
(assert (=> |(switch_b_1_1 )_2| (not b_1_0_3)))
(assert (=> |(switch_b_1_1 )_2| (= cost_1_3 (+ cost_1_2 2.0))))
(assert (=> |(switch_b_1_2 )_2| (not b_1_2_2)))
(assert (=> |(switch_b_1_2 )_2| b_1_2_3))
(assert (=> |(switch_b_1_2 )_2| (not b_1_0_3)))
(assert (=> |(switch_b_1_2 )_2| (not b_1_1_3)))
(assert (=> |(switch_b_1_2 )_2| (= cost_1_3 (+ cost_1_2 4.0))))
(assert (=> |(switch_b_0_0 )_3| (not b_0_0_3)))
(assert (=> |(switch_b_0_0 )_3| b_0_0_4))
(assert (=> |(switch_b_0_0 )_3| (= cost_0_4 (+ cost_0_3 1.0))))
(assert (=> |(switch_b_0_1 )_3| (not b_0_1_3)))
(assert (=> |(switch_b_0_1 )_3| b_0_1_4))
(assert (=> |(switch_b_0_1 )_3| (not b_0_0_4)))
(assert (=> |(switch_b_0_1 )_3| (= cost_0_4 (+ cost_0_3 2.0))))
(assert (=> |(switch_b_0_2 )_3| (not b_0_2_3)))
(assert (=> |(switch_b_0_2 )_3| b_0_2_4))
(assert (=> |(switch_b_0_2 )_3| (not b_0_0_4)))
(assert (=> |(switch_b_0_2 )_3| (not b_0_1_4)))
(assert (=> |(switch_b_0_2 )_3| (= cost_0_4 (+ cost_0_3 4.0))))
(assert (=> |(switch_b_1_0 )_3| (not b_1_0_3)))
(assert (=> |(switch_b_1_0 )_3| b_1_0_4))
(assert (=> |(switch_b_1_0 )_3| (= cost_1_4 (+ cost_1_3 1.0))))
(assert (=> |(switch_b_1_1 )_3| (not b_1_1_3)))
(assert (=> |(switch_b_1_1 )_3| b_1_1_4))
(assert (=> |(switch_b_1_1 )_3| (not b_1_0_4)))
(assert (=> |(switch_b_1_1 )_3| (= cost_1_4 (+ cost_1_3 2.0))))
(assert (=> |(switch_b_1_2 )_3| (not b_1_2_3)))
(assert (=> |(switch_b_1_2 )_3| b_1_2_4))
(assert (=> |(switch_b_1_2 )_3| (not b_1_0_4)))
(assert (=> |(switch_b_1_2 )_3| (not b_1_1_4)))
(assert (=> |(switch_b_1_2 )_3| (= cost_1_4 (+ cost_1_3 4.0))))
(assert (or (not |(switch_b_0_1 )_0|) (not |(switch_b_0_2 )_0|)))
(assert (or (not |(switch_b_1_2 )_0|) (not |(switch_b_1_1 )_0|)))
(assert (or (not |(switch_b_1_2 )_0|) (not |(switch_b_1_0 )_0|)))
(assert (or (not |(switch_b_0_0 )_0|) (not |(switch_b_0_2 )_0|)))
(assert (or (not |(switch_b_0_0 )_0|) (not |(switch_b_0_1 )_0|)))
(assert (or (not |(switch_b_1_1 )_0|) (not |(switch_b_1_0 )_0|)))
(assert (or (not |(switch_b_0_1 )_1|) (not |(switch_b_0_2 )_1|)))
(assert (or (not |(switch_b_1_2 )_1|) (not |(switch_b_1_1 )_1|)))
(assert (or (not |(switch_b_1_2 )_1|) (not |(switch_b_1_0 )_1|)))
(assert (or (not |(switch_b_0_0 )_1|) (not |(switch_b_0_2 )_1|)))
(assert (or (not |(switch_b_0_0 )_1|) (not |(switch_b_0_1 )_1|)))
(assert (or (not |(switch_b_1_1 )_1|) (not |(switch_b_1_0 )_1|)))
(assert (or (not |(switch_b_0_1 )_2|) (not |(switch_b_0_2 )_2|)))
(assert (or (not |(switch_b_1_2 )_2|) (not |(switch_b_1_1 )_2|)))
(assert (or (not |(switch_b_1_2 )_2|) (not |(switch_b_1_0 )_2|)))
(assert (or (not |(switch_b_0_0 )_2|) (not |(switch_b_0_2 )_2|)))
(assert (or (not |(switch_b_0_0 )_2|) (not |(switch_b_0_1 )_2|)))
(assert (or (not |(switch_b_1_1 )_2|) (not |(switch_b_1_0 )_2|)))
(assert (or (not |(switch_b_0_1 )_3|) (not |(switch_b_0_2 )_3|)))
(assert (or (not |(switch_b_1_2 )_3|) (not |(switch_b_1_1 )_3|)))
(assert (or (not |(switch_b_1_2 )_3|) (not |(switch_b_1_0 )_3|)))
(assert (or (not |(switch_b_0_0 )_3|) (not |(switch_b_0_2 )_3|)))
(assert (or (not |(switch_b_0_0 )_3|) (not |(switch_b_0_1 )_3|)))
(assert (or (not |(switch_b_1_1 )_3|) (not |(switch_b_1_0 )_3|)))
(minimize (+ cost_1_4 cost_0_4))
(check-sat)
(get-objectives)
(get-model)