(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :mbqi true)
(declare-const x (_ BitVec 30))
(declare-const y (_ BitVec 30))
(declare-const xs (_ BitVec 30))
; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\arabidopsis.cnet--------
(declare-fun T ((_ BitVec 30) (_ BitVec 30) ) bool)
; -------------- Transition Relation: -----------------
(assert (forall ((x (_ BitVec 30)) (y (_ BitVec 30))
  )(= (T x y)
     (and (= (= ((_ extract 0 0) y) (_ bv1 1))
             (and (or (and (= ((_ extract 9 9) x) (_ bv1 1))
                           (= ((_ extract 13 13) x) (_ bv1 1))
                           (= ((_ extract 14 14) x) (_ bv1 1))
                           (= ((_ extract 0 0) x) (_ bv1 1)))
                      (and (= ((_ extract 4 4) x) (_ bv1 1))
                           (= ((_ extract 13 13) x) (_ bv1 1))
                           (= ((_ extract 14 14) x) (_ bv1 1))
                           (= ((_ extract 0 0) x) (_ bv1 1)))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 1 1) x) (_ bv1 1))))
                  (not (= ((_ extract 15 15) x) (_ bv1 1)))))
          (= (= ((_ extract 1 1) y) (_ bv1 1))
             (and (or (and (= ((_ extract 1 1) x) (_ bv1 1))))
                  (not (= ((_ extract 16 16) x) (_ bv1 1)))))
          (= (= ((_ extract 2 2) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (not (= ((_ extract 12 12) x) (_ bv1 1)))))
                  (not (= ((_ extract 17 17) x) (_ bv1 1)))))
          (= (= ((_ extract 3 3) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 5 5) x) (_ bv1 1)))))
                  (not (= ((_ extract 18 18) x) (_ bv1 1)))))
          (= (= ((_ extract 4 4) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 9 9) x) (_ bv1 1)))
                           (not (= ((_ extract 12 12) x) (_ bv1 1))))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 9 9) x) (_ bv1 1))))
                      (and (= ((_ extract 3 3) x) (_ bv1 1))
                           (not (= ((_ extract 9 9) x) (_ bv1 1)))))
                  (not (= ((_ extract 19 19) x) (_ bv1 1)))))
          (= (= ((_ extract 5 5) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 6 6) x) (_ bv1 1)))))
                  (not (= ((_ extract 20 20) x) (_ bv1 1)))))
          (= (= ((_ extract 6 6) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 12 12) x) (_ bv1 1))))
                      (and (not (= ((_ extract 5 5) x) (_ bv1 1)))))
                  (not (= ((_ extract 21 21) x) (_ bv1 1)))))
          (= (= ((_ extract 7 7) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 12 12) x) (_ bv1 1)))))
                  (not (= ((_ extract 22 22) x) (_ bv1 1)))))
          (= (= ((_ extract 8 8) y) (_ bv1 1))
             (and (or (and (= ((_ extract 8 8) x) (_ bv1 1))
                           (not (= ((_ extract 14 14) x) (_ bv1 1))))
                      (and (= ((_ extract 8 8) x) (_ bv1 1))
                           (not (= ((_ extract 9 9) x) (_ bv1 1)))))
                  (not (= ((_ extract 23 23) x) (_ bv1 1)))))
          (= (= ((_ extract 9 9) y) (_ bv1 1))
             (and (or (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1))
                           (= ((_ extract 14 14) x) (_ bv1 1)))
                      (and (not (= ((_ extract 7 7) x) (_ bv1 1)))
                           (not (= ((_ extract 12 12) x) (_ bv1 1))))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 11 11) x) (_ bv1 1))))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1))))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 8 8) x) (_ bv1 1)))
                      (and (not (= ((_ extract 4 4) x) (_ bv1 1)))
                           (= ((_ extract 6 6) x) (_ bv1 1)))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (not (= ((_ extract 7 7) x) (_ bv1 1)))))
                  (not (= ((_ extract 24 24) x) (_ bv1 1)))))
          (= (= ((_ extract 10 10) y) (_ bv1 1))
             (and (or true) (not (= ((_ extract 25 25) x) (_ bv1 1)))))
          (= (= ((_ extract 11 11) y) (_ bv1 1))
             (and (or true) (not (= ((_ extract 26 26) x) (_ bv1 1)))))
          (= (= ((_ extract 12 12) 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 27 27) x) (_ bv1 1)))))
          (= (= ((_ extract 13 13) y) (_ bv1 1))
             (and (or (and (= ((_ extract 4 4) x) (_ bv1 1))
                           (= ((_ extract 13 13) x) (_ bv1 1))
                           (= ((_ extract 14 14) x) (_ bv1 1))
                           (= ((_ extract 0 0) x) (_ bv1 1)))
                      (and (= ((_ extract 9 9) x) (_ bv1 1))
                           (= ((_ extract 13 13) x) (_ bv1 1))
                           (= ((_ extract 14 14) x) (_ bv1 1))
                           (= ((_ extract 0 0) x) (_ bv1 1)))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1)))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))
                           (= ((_ extract 0 0) x) (_ bv1 1))))
                  (not (= ((_ extract 28 28) x) (_ bv1 1)))))
          (= (= ((_ extract 14 14) y) (_ bv1 1))
             (and (or (and (= ((_ extract 6 6) x) (_ bv1 1))))
                  (not (= ((_ extract 29 29) 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)))
          (= (= ((_ extract 24 24) y) (_ bv1 1)) (= ((_ extract 24 24) x) (_ bv1 1)))
          (= (= ((_ extract 25 25) y) (_ bv1 1)) (= ((_ extract 25 25) x) (_ bv1 1)))
          (= (= ((_ extract 26 26) y) (_ bv1 1)) (= ((_ extract 26 26) x) (_ bv1 1)))
          (= (= ((_ extract 27 27) y) (_ bv1 1)) (= ((_ extract 27 27) x) (_ bv1 1)))
          (= (= ((_ extract 28 28) y) (_ bv1 1)) (= ((_ extract 28 28) x) (_ bv1 1)))
          (= (= ((_ extract 29 29) y) (_ bv1 1)) (= ((_ extract 29 29) x) (_ bv1 1)))))))
; ------------------ END ------------------------------
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv1 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 0 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv2 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 1 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv4 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 2 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv8 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 3 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv16 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 4 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv32 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 5 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv64 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 6 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv128 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 7 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv256 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 8 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv512 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 9 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv1024 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 10 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv2048 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 11 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv4096 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 12 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv8192 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 13 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 30))
(declare-const p11 (_ BitVec 30))
(declare-const p12 (_ BitVec 30))
(declare-const p13 (_ BitVec 30))
(declare-const p14 (_ BitVec 30))
(declare-const p15 (_ BitVec 30))
(declare-const p16 (_ BitVec 30))
(declare-const p17 (_ BitVec 30))
(declare-const p18 (_ BitVec 30))
(declare-const p19 (_ BitVec 30))
(declare-const p110 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 30))
(declare-const p21 (_ BitVec 30))
(declare-const p22 (_ BitVec 30))
(declare-const p23 (_ BitVec 30))
(declare-const p24 (_ BitVec 30))
(declare-const p25 (_ BitVec 30))
(declare-const p26 (_ BitVec 30))
(declare-const p27 (_ BitVec 30))
(declare-const p28 (_ BitVec 30))
(declare-const p29 (_ BitVec 30))
(declare-const p210 (_ BitVec 30))
; ---------- 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)))
; --------------- END (Path)------------------
(assert (= ((_ extract 14 0) p10) ((_ extract 14 0) p20)))
(assert (= ((_ extract 29 15) p10) (_ bv0 15)))
(assert (= ((_ extract 29 15) p20) (_ bv16384 15)))
(assert (or (and (T p110 p110) (not (T p210 p210)))
    (and (not (T p110 p110)) (T p210 p210))))
(echo "Does gene 14 affect the stability of the system?")
(check-sat)
(pop)
(get-info :all-statistics)