(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :mbqi true)
(declare-const x (_ BitVec 24))
(declare-const y (_ BitVec 24))
(declare-const xs (_ BitVec 24))
; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\budding_yeast.cnet--------
(declare-fun T ((_ BitVec 24) (_ BitVec 24) ) bool)
; -------------- Transition Relation: -----------------
(assert (forall ((x (_ BitVec 24)) (y (_ BitVec 24))
  )(= (T x y)
     (and (= (= ((_ extract 0 0) y) (_ bv1 1))
             (and (or false) (not (= ((_ extract 12 12) x) (_ bv1 1)))))
          (= (= ((_ extract 1 1) y) (_ bv1 1))
             (and (or (and (= ((_ extract 0 0) x) (_ bv1 1))))
                  (not (= ((_ extract 13 13) x) (_ bv1 1)))))
          (= (= ((_ extract 2 2) y) (_ bv1 1))
             (and (or (and (= ((_ extract 2 2) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1))))
                      (and (= ((_ extract 1 1) x) (_ bv1 1))
                           (= ((_ extract 2 2) x) (_ bv1 1)))
                      (and (= ((_ extract 1 1) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))))
                  (not (= ((_ extract 14 14) x) (_ bv1 1)))))
          (= (= ((_ extract 3 3) y) (_ bv1 1))
             (and (or (and (= ((_ extract 3 3) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1))))
                      (and (= ((_ extract 1 1) x) (_ bv1 1))
                           (= ((_ extract 3 3) x) (_ bv1 1)))
                      (and (= ((_ extract 1 1) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))))
                  (not (= ((_ extract 15 15) x) (_ bv1 1)))))
          (= (= ((_ extract 4 4) y) (_ bv1 1))
             (and (or (and (= ((_ extract 2 2) x) (_ bv1 1))))
                  (not (= ((_ extract 16 16) x) (_ bv1 1)))))
          (= (= ((_ extract 5 5) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (not (= ((_ extract 8 8) x) (_ bv1 1))))
                      (and (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1)))
                      (and (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (= ((_ extract 5 5) x) (_ bv1 1))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (= ((_ extract 5 5) x) (_ bv1 1))
                           (= ((_ extract 10 10) x) (_ bv1 1))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1))
                           (= ((_ extract 11 11) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1))))
                  (not (= ((_ extract 17 17) x) (_ bv1 1)))))
          (= (= ((_ extract 6 6) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (= ((_ extract 3 3) x) (_ bv1 1))
                           (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (= ((_ extract 3 3) x) (_ bv1 1))
                           (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1)))
                      (and (= ((_ extract 3 3) x) (_ bv1 1))
                           (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (not (= ((_ extract 10 10) x) (_ bv1 1)))))
                  (not (= ((_ extract 18 18) x) (_ bv1 1)))))
          (= (= ((_ extract 7 7) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (= ((_ extract 7 7) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1))))
                      (and (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (= ((_ extract 7 7) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (= ((_ extract 7 7) x) (_ bv1 1))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (= ((_ extract 7 7) x) (_ bv1 1))
                           (= ((_ extract 10 10) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (not (= ((_ extract 6 6) x) (_ bv1 1)))
                           (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1))))
                  (not (= ((_ extract 19 19) x) (_ bv1 1)))))
          (= (= ((_ extract 8 8) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 8 8) x) (_ bv1 1)))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1)))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1)))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1)))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 9 9) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 9 9) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (= ((_ extract 9 9) x) (_ bv1 1))))
                  (not (= ((_ extract 20 20) x) (_ bv1 1)))))
          (= (= ((_ extract 9 9) y) (_ bv1 1))
             (and (or (and (= ((_ extract 8 8) x) (_ bv1 1)))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))))
                  (not (= ((_ extract 21 21) x) (_ bv1 1)))))
          (= (= ((_ extract 10 10) y) (_ bv1 1))
             (and (or (and (= ((_ extract 9 9) x) (_ bv1 1)))
                      (and (= ((_ extract 8 8) x) (_ bv1 1))))
                  (not (= ((_ extract 22 22) x) (_ bv1 1)))))
          (= (= ((_ extract 11 11) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 10 10) x) (_ bv1 1)))
                      (and (= ((_ extract 9 9) x) (_ bv1 1))
                           (= ((_ extract 10 10) x) (_ bv1 1)))
                      (and (not (= ((_ extract 8 8) x) (_ bv1 1)))
                           (= ((_ extract 9 9) x) (_ bv1 1))))
                  (not (= ((_ extract 23 23) x) (_ bv1 1)))))
          (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1)))
          (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1)))
          (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1)))
          (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1)))
          (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1)))
          (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1)))
          (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1)))
          (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1)))
          (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1)))
          (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1)))
          (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))
          (= (= ((_ extract 23 23) y) (_ bv1 1)) (= ((_ extract 23 23) x) (_ bv1 1)))))))
; ------------------ END ------------------------------
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv1 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 0 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv2 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 1 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv4 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 2 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv8 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 3 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv16 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 4 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv32 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 5 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv64 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 6 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv128 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 7 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv256 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 8 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv512 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 9 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv1024 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 10 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 24))
(declare-const p11 (_ BitVec 24))
(declare-const p12 (_ BitVec 24))
(declare-const p13 (_ BitVec 24))
(declare-const p14 (_ BitVec 24))
(declare-const p15 (_ BitVec 24))
(declare-const p16 (_ BitVec 24))
(declare-const p17 (_ BitVec 24))
(declare-const p18 (_ BitVec 24))
(declare-const p19 (_ BitVec 24))
(declare-const p110 (_ BitVec 24))
(declare-const p111 (_ BitVec 24))
(declare-const p112 (_ BitVec 24))
(declare-const p113 (_ BitVec 24))
(declare-const p114 (_ BitVec 24))
(declare-const p115 (_ BitVec 24))
(declare-const p116 (_ BitVec 24))
(declare-const p117 (_ BitVec 24))
(declare-const p118 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p10 p11)
     (T p11 p12)
     (T p12 p13)
     (T p13 p14)
     (T p14 p15)
     (T p15 p16)
     (T p16 p17)
     (T p17 p18)
     (T p18 p19)
     (T p19 p110)
     (T p110 p111)
     (T p111 p112)
     (T p112 p113)
     (T p113 p114)
     (T p114 p115)
     (T p115 p116)
     (T p116 p117)
     (T p117 p118)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 24))
(declare-const p21 (_ BitVec 24))
(declare-const p22 (_ BitVec 24))
(declare-const p23 (_ BitVec 24))
(declare-const p24 (_ BitVec 24))
(declare-const p25 (_ BitVec 24))
(declare-const p26 (_ BitVec 24))
(declare-const p27 (_ BitVec 24))
(declare-const p28 (_ BitVec 24))
(declare-const p29 (_ BitVec 24))
(declare-const p210 (_ BitVec 24))
(declare-const p211 (_ BitVec 24))
(declare-const p212 (_ BitVec 24))
(declare-const p213 (_ BitVec 24))
(declare-const p214 (_ BitVec 24))
(declare-const p215 (_ BitVec 24))
(declare-const p216 (_ BitVec 24))
(declare-const p217 (_ BitVec 24))
(declare-const p218 (_ BitVec 24))
; ---------- QFBV Path Correctness: ---------------
(assert (and (T p20 p21)
     (T p21 p22)
     (T p22 p23)
     (T p23 p24)
     (T p24 p25)
     (T p25 p26)
     (T p26 p27)
     (T p27 p28)
     (T p28 p29)
     (T p29 p210)
     (T p210 p211)
     (T p211 p212)
     (T p212 p213)
     (T p213 p214)
     (T p214 p215)
     (T p215 p216)
     (T p216 p217)
     (T p217 p218)))
; --------------- END (Path)------------------
(assert (= ((_ extract 11 0) p10) ((_ extract 11 0) p20)))
(assert (= ((_ extract 23 12) p10) (_ bv0 12)))
(assert (= ((_ extract 23 12) p20) (_ bv2048 12)))
(assert (or (and (T p118 p118) (not (T p218 p218)))
    (and (not (T p118 p118)) (T p218 p218))))
(echo "Does gene 11 affect the stability of the system?")
(check-sat)
(pop)
(get-info :all-statistics)