(set-option :produce-models true)
(set-option :pull-nested-quantifiers true)
(set-option :mbqi true)
(declare-const x (_ BitVec 80))
(declare-const y (_ BitVec 80))
(declare-const xs (_ BitVec 80))
; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\tcr.cnet--------
(declare-fun T ((_ BitVec 80) (_ BitVec 80) ) bool)
; -------------- Transition Relation: -----------------
(assert (forall ((x (_ BitVec 80)) (y (_ BitVec 80))
  )(= (T x y)
     (and (= (= ((_ extract 0 0) y) (_ bv1 1))
             (and (or (and (= ((_ extract 0 0) x) (_ bv1 1))))
                  (not (= ((_ extract 40 40) x) (_ bv1 1)))))
          (= (= ((_ extract 1 1) y) (_ bv1 1))
             (and (or (and (= ((_ extract 1 1) x) (_ bv1 1))))
                  (not (= ((_ extract 41 41) x) (_ bv1 1)))))
          (= (= ((_ extract 2 2) y) (_ bv1 1))
             (and (or (and (= ((_ extract 2 2) x) (_ bv1 1))))
                  (not (= ((_ extract 42 42) x) (_ bv1 1)))))
          (= (= ((_ extract 3 3) y) (_ bv1 1))
             (and (or (and (= ((_ extract 2 2) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1)))))
                  (not (= ((_ extract 43 43) x) (_ bv1 1)))))
          (= (= ((_ extract 4 4) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 3 3) x) (_ bv1 1))))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))))
                  (not (= ((_ extract 44 44) x) (_ bv1 1)))))
          (= (= ((_ extract 5 5) y) (_ bv1 1))
             (and (or (and (= ((_ extract 0 0) x) (_ bv1 1))
                           (= ((_ extract 1 1) x) (_ bv1 1))
                           (not (= ((_ extract 4 4) x) (_ bv1 1)))))
                  (not (= ((_ extract 45 45) x) (_ bv1 1)))))
          (= (= ((_ extract 6 6) y) (_ bv1 1))
             (and (or (and (= ((_ extract 0 0) x) (_ bv1 1))
                           (= ((_ extract 5 5) x) (_ bv1 1)))
                      (and (= ((_ extract 0 0) x) (_ bv1 1))
                           (= ((_ extract 3 3) x) (_ bv1 1))))
                  (not (= ((_ extract 46 46) x) (_ bv1 1)))))
          (= (= ((_ extract 7 7) y) (_ bv1 1))
             (and (or (and (= ((_ extract 5 5) x) (_ bv1 1))))
                  (not (= ((_ extract 47 47) x) (_ bv1 1)))))
          (= (= ((_ extract 8 8) y) (_ bv1 1))
             (and (or (and (= ((_ extract 3 3) x) (_ bv1 1))
                           (= ((_ extract 5 5) x) (_ bv1 1)))
                      (and (= ((_ extract 6 6) x) (_ bv1 1))))
                  (not (= ((_ extract 48 48) x) (_ bv1 1)))))
          (= (= ((_ extract 9 9) y) (_ bv1 1))
             (and (or (and (= ((_ extract 5 5) x) (_ bv1 1))
                           (= ((_ extract 8 8) x) (_ bv1 1))
                           (not (= ((_ extract 10 10) x) (_ bv1 1)))))
                  (not (= ((_ extract 49 49) x) (_ bv1 1)))))
          (= (= ((_ extract 10 10) y) (_ bv1 1))
             (and (or (and (= ((_ extract 9 9) x) (_ bv1 1))))
                  (not (= ((_ extract 50 50) x) (_ bv1 1)))))
          (= (= ((_ extract 11 11) y) (_ bv1 1))
             (and (or (and (= ((_ extract 9 9) x) (_ bv1 1))
                           (= ((_ extract 14 14) x) (_ bv1 1))))
                  (not (= ((_ extract 51 51) x) (_ bv1 1)))))
          (= (= ((_ extract 12 12) y) (_ bv1 1))
             (and (or (and (= ((_ extract 9 9) x) (_ bv1 1))))
                  (not (= ((_ extract 52 52) x) (_ bv1 1)))))
          (= (= ((_ extract 13 13) y) (_ bv1 1))
             (and (or (and (= ((_ extract 12 12) x) (_ bv1 1))))
                  (not (= ((_ extract 53 53) x) (_ bv1 1)))))
          (= (= ((_ extract 14 14) y) (_ bv1 1))
             (and (or (and (= ((_ extract 13 13) x) (_ bv1 1))))
                  (not (= ((_ extract 54 54) x) (_ bv1 1)))))
          (= (= ((_ extract 15 15) y) (_ bv1 1))
             (and (or (and (= ((_ extract 12 12) x) (_ bv1 1))))
                  (not (= ((_ extract 55 55) x) (_ bv1 1)))))
          (= (= ((_ extract 16 16) y) (_ bv1 1))
             (and (or (and (= ((_ extract 12 12) x) (_ bv1 1))))
                  (not (= ((_ extract 56 56) x) (_ bv1 1)))))
          (= (= ((_ extract 17 17) y) (_ bv1 1))
             (and (or (and (= ((_ extract 18 18) x) (_ bv1 1))))
                  (not (= ((_ extract 57 57) x) (_ bv1 1)))))
          (= (= ((_ extract 18 18) y) (_ bv1 1))
             (and (or (and (= ((_ extract 9 9) x) (_ bv1 1))
                           (= ((_ extract 11 11) x) (_ bv1 1))
                           (= ((_ extract 14 14) x) (_ bv1 1))
                           (= ((_ extract 15 15) x) (_ bv1 1)))
                      (and (= ((_ extract 7 7) x) (_ bv1 1))
                           (= ((_ extract 9 9) x) (_ bv1 1))
                           (= ((_ extract 14 14) x) (_ bv1 1))
                           (= ((_ extract 15 15) x) (_ bv1 1))))
                  (not (= ((_ extract 58 58) x) (_ bv1 1)))))
          (= (= ((_ extract 19 19) y) (_ bv1 1))
             (and (or (and (= ((_ extract 20 20) x) (_ bv1 1)))
                      (and (= ((_ extract 16 16) x) (_ bv1 1))))
                  (not (= ((_ extract 59 59) x) (_ bv1 1)))))
          (= (= ((_ extract 20 20) y) (_ bv1 1))
             (and (or (and (= ((_ extract 17 17) x) (_ bv1 1))
                           (= ((_ extract 21 21) x) (_ bv1 1))))
                  (not (= ((_ extract 60 60) x) (_ bv1 1)))))
          (= (= ((_ extract 21 21) y) (_ bv1 1))
             (and (or (and (= ((_ extract 17 17) x) (_ bv1 1))))
                  (not (= ((_ extract 61 61) x) (_ bv1 1)))))
          (= (= ((_ extract 22 22) y) (_ bv1 1))
             (and (or (and (= ((_ extract 18 18) x) (_ bv1 1))))
                  (not (= ((_ extract 62 62) x) (_ bv1 1)))))
          (= (= ((_ extract 23 23) y) (_ bv1 1))
             (and (or (and (= ((_ extract 19 19) x) (_ bv1 1))))
                  (not (= ((_ extract 63 63) x) (_ bv1 1)))))
          (= (= ((_ extract 24 24) y) (_ bv1 1))
             (and (or (and (= ((_ extract 23 23) x) (_ bv1 1))))
                  (not (= ((_ extract 64 64) x) (_ bv1 1)))))
          (= (= ((_ extract 25 25) y) (_ bv1 1))
             (and (or (and (= ((_ extract 22 22) x) (_ bv1 1))))
                  (not (= ((_ extract 65 65) x) (_ bv1 1)))))
          (= (= ((_ extract 26 26) y) (_ bv1 1))
             (and (or (and (= ((_ extract 24 24) x) (_ bv1 1))))
                  (not (= ((_ extract 66 66) x) (_ bv1 1)))))
          (= (= ((_ extract 27 27) y) (_ bv1 1))
             (and (or (and (= ((_ extract 21 21) x) (_ bv1 1))))
                  (not (= ((_ extract 67 67) x) (_ bv1 1)))))
          (= (= ((_ extract 28 28) y) (_ bv1 1))
             (and (or (and (= ((_ extract 21 21) x) (_ bv1 1))))
                  (not (= ((_ extract 68 68) x) (_ bv1 1)))))
          (= (= ((_ extract 29 29) y) (_ bv1 1))
             (and (or (and (= ((_ extract 25 25) x) (_ bv1 1))))
                  (not (= ((_ extract 69 69) x) (_ bv1 1)))))
          (= (= ((_ extract 30 30) y) (_ bv1 1))
             (and (or (and (= ((_ extract 26 26) x) (_ bv1 1))))
                  (not (= ((_ extract 70 70) x) (_ bv1 1)))))
          (= (= ((_ extract 31 31) y) (_ bv1 1))
             (and (or (and (= ((_ extract 26 26) x) (_ bv1 1))))
                  (not (= ((_ extract 71 71) x) (_ bv1 1)))))
          (= (= ((_ extract 32 32) y) (_ bv1 1))
             (and (or (and (= ((_ extract 27 27) x) (_ bv1 1))))
                  (not (= ((_ extract 72 72) x) (_ bv1 1)))))
          (= (= ((_ extract 33 33) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 28 28) x) (_ bv1 1)))))
                  (not (= ((_ extract 73 73) x) (_ bv1 1)))))
          (= (= ((_ extract 34 34) y) (_ bv1 1))
             (and (or (and (= ((_ extract 30 30) x) (_ bv1 1))))
                  (not (= ((_ extract 74 74) x) (_ bv1 1)))))
          (= (= ((_ extract 35 35) y) (_ bv1 1))
             (and (or (and (= ((_ extract 32 32) x) (_ bv1 1))))
                  (not (= ((_ extract 75 75) x) (_ bv1 1)))))
          (= (= ((_ extract 36 36) y) (_ bv1 1))
             (and (or (and (= ((_ extract 34 34) x) (_ bv1 1))))
                  (not (= ((_ extract 76 76) x) (_ bv1 1)))))
          (= (= ((_ extract 37 37) y) (_ bv1 1))
             (and (or (and (= ((_ extract 31 31) x) (_ bv1 1))
                           (= ((_ extract 35 35) x) (_ bv1 1))))
                  (not (= ((_ extract 77 77) x) (_ bv1 1)))))
          (= (= ((_ extract 38 38) y) (_ bv1 1))
             (and (or (and (not (= ((_ extract 33 33) x) (_ bv1 1)))))
                  (not (= ((_ extract 78 78) x) (_ bv1 1)))))
          (= (= ((_ extract 39 39) y) (_ bv1 1))
             (and (or (and (= ((_ extract 29 29) x) (_ bv1 1))))
                  (not (= ((_ extract 79 79) x) (_ bv1 1)))))
          (= (= ((_ extract 40 40) y) (_ bv1 1)) (= ((_ extract 40 40) x) (_ bv1 1)))
          (= (= ((_ extract 41 41) y) (_ bv1 1)) (= ((_ extract 41 41) x) (_ bv1 1)))
          (= (= ((_ extract 42 42) y) (_ bv1 1)) (= ((_ extract 42 42) x) (_ bv1 1)))
          (= (= ((_ extract 43 43) y) (_ bv1 1)) (= ((_ extract 43 43) x) (_ bv1 1)))
          (= (= ((_ extract 44 44) y) (_ bv1 1)) (= ((_ extract 44 44) x) (_ bv1 1)))
          (= (= ((_ extract 45 45) y) (_ bv1 1)) (= ((_ extract 45 45) x) (_ bv1 1)))
          (= (= ((_ extract 46 46) y) (_ bv1 1)) (= ((_ extract 46 46) x) (_ bv1 1)))
          (= (= ((_ extract 47 47) y) (_ bv1 1)) (= ((_ extract 47 47) x) (_ bv1 1)))
          (= (= ((_ extract 48 48) y) (_ bv1 1)) (= ((_ extract 48 48) x) (_ bv1 1)))
          (= (= ((_ extract 49 49) y) (_ bv1 1)) (= ((_ extract 49 49) x) (_ bv1 1)))
          (= (= ((_ extract 50 50) y) (_ bv1 1)) (= ((_ extract 50 50) x) (_ bv1 1)))
          (= (= ((_ extract 51 51) y) (_ bv1 1)) (= ((_ extract 51 51) x) (_ bv1 1)))
          (= (= ((_ extract 52 52) y) (_ bv1 1)) (= ((_ extract 52 52) x) (_ bv1 1)))
          (= (= ((_ extract 53 53) y) (_ bv1 1)) (= ((_ extract 53 53) x) (_ bv1 1)))
          (= (= ((_ extract 54 54) y) (_ bv1 1)) (= ((_ extract 54 54) x) (_ bv1 1)))
          (= (= ((_ extract 55 55) y) (_ bv1 1)) (= ((_ extract 55 55) x) (_ bv1 1)))
          (= (= ((_ extract 56 56) y) (_ bv1 1)) (= ((_ extract 56 56) x) (_ bv1 1)))
          (= (= ((_ extract 57 57) y) (_ bv1 1)) (= ((_ extract 57 57) x) (_ bv1 1)))
          (= (= ((_ extract 58 58) y) (_ bv1 1)) (= ((_ extract 58 58) x) (_ bv1 1)))
          (= (= ((_ extract 59 59) y) (_ bv1 1)) (= ((_ extract 59 59) x) (_ bv1 1)))
          (= (= ((_ extract 60 60) y) (_ bv1 1)) (= ((_ extract 60 60) x) (_ bv1 1)))
          (= (= ((_ extract 61 61) y) (_ bv1 1)) (= ((_ extract 61 61) x) (_ bv1 1)))
          (= (= ((_ extract 62 62) y) (_ bv1 1)) (= ((_ extract 62 62) x) (_ bv1 1)))
          (= (= ((_ extract 63 63) y) (_ bv1 1)) (= ((_ extract 63 63) x) (_ bv1 1)))
          (= (= ((_ extract 64 64) y) (_ bv1 1)) (= ((_ extract 64 64) x) (_ bv1 1)))
          (= (= ((_ extract 65 65) y) (_ bv1 1)) (= ((_ extract 65 65) x) (_ bv1 1)))
          (= (= ((_ extract 66 66) y) (_ bv1 1)) (= ((_ extract 66 66) x) (_ bv1 1)))
          (= (= ((_ extract 67 67) y) (_ bv1 1)) (= ((_ extract 67 67) x) (_ bv1 1)))
          (= (= ((_ extract 68 68) y) (_ bv1 1)) (= ((_ extract 68 68) x) (_ bv1 1)))
          (= (= ((_ extract 69 69) y) (_ bv1 1)) (= ((_ extract 69 69) x) (_ bv1 1)))
          (= (= ((_ extract 70 70) y) (_ bv1 1)) (= ((_ extract 70 70) x) (_ bv1 1)))
          (= (= ((_ extract 71 71) y) (_ bv1 1)) (= ((_ extract 71 71) x) (_ bv1 1)))
          (= (= ((_ extract 72 72) y) (_ bv1 1)) (= ((_ extract 72 72) x) (_ bv1 1)))
          (= (= ((_ extract 73 73) y) (_ bv1 1)) (= ((_ extract 73 73) x) (_ bv1 1)))
          (= (= ((_ extract 74 74) y) (_ bv1 1)) (= ((_ extract 74 74) x) (_ bv1 1)))
          (= (= ((_ extract 75 75) y) (_ bv1 1)) (= ((_ extract 75 75) x) (_ bv1 1)))
          (= (= ((_ extract 76 76) y) (_ bv1 1)) (= ((_ extract 76 76) x) (_ bv1 1)))
          (= (= ((_ extract 77 77) y) (_ bv1 1)) (= ((_ extract 77 77) x) (_ bv1 1)))
          (= (= ((_ extract 78 78) y) (_ bv1 1)) (= ((_ extract 78 78) x) (_ bv1 1)))
          (= (= ((_ extract 79 79) y) (_ bv1 1)) (= ((_ extract 79 79) x) (_ bv1 1)))))))
; ------------------ END ------------------------------
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv1 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 0 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv2 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 1 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv4 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 2 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv8 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 3 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv16 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 4 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv32 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 5 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv64 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 6 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv128 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 7 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv256 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 8 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv512 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 9 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv1024 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 10 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv2048 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 11 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv4096 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 12 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv8192 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 13 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv16384 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 14 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv32768 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 15 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv65536 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 16 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv131072 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 17 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv262144 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 18 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv524288 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 19 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv1048576 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 20 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv2097152 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 21 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv4194304 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 22 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv8388608 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 23 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv16777216 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 24 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv33554432 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 25 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv67108864 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 26 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv134217728 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 27 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv268435456 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 28 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv536870912 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 29 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv1073741824 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 30 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv2147483648 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 31 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv4294967296 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 32 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv8589934592 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 33 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv17179869184 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 34 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv34359738368 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 35 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv68719476736 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 36 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv137438953472 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 37 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv274877906944 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 38 affect the stability of the system?")
(check-sat)
(pop)
(push)
(declare-const p10 (_ BitVec 80))
(declare-const p11 (_ BitVec 80))
(declare-const p12 (_ BitVec 80))
(declare-const p13 (_ BitVec 80))
(declare-const p14 (_ BitVec 80))
(declare-const p15 (_ BitVec 80))
(declare-const p16 (_ BitVec 80))
(declare-const p17 (_ BitVec 80))
(declare-const p18 (_ BitVec 80))
(declare-const p19 (_ BitVec 80))
(declare-const p110 (_ BitVec 80))
(declare-const p111 (_ BitVec 80))
(declare-const p112 (_ BitVec 80))
(declare-const p113 (_ BitVec 80))
(declare-const p114 (_ BitVec 80))
(declare-const p115 (_ BitVec 80))
(declare-const p116 (_ BitVec 80))
(declare-const p117 (_ BitVec 80))
(declare-const p118 (_ BitVec 80))
(declare-const p119 (_ BitVec 80))
(declare-const p120 (_ BitVec 80))
(declare-const p121 (_ BitVec 80))
(declare-const p122 (_ BitVec 80))
; ---------- 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)
     (T p118 p119)
     (T p119 p120)
     (T p120 p121)
     (T p121 p122)))
; --------------- END (Path)------------------
(declare-const p20 (_ BitVec 80))
(declare-const p21 (_ BitVec 80))
(declare-const p22 (_ BitVec 80))
(declare-const p23 (_ BitVec 80))
(declare-const p24 (_ BitVec 80))
(declare-const p25 (_ BitVec 80))
(declare-const p26 (_ BitVec 80))
(declare-const p27 (_ BitVec 80))
(declare-const p28 (_ BitVec 80))
(declare-const p29 (_ BitVec 80))
(declare-const p210 (_ BitVec 80))
(declare-const p211 (_ BitVec 80))
(declare-const p212 (_ BitVec 80))
(declare-const p213 (_ BitVec 80))
(declare-const p214 (_ BitVec 80))
(declare-const p215 (_ BitVec 80))
(declare-const p216 (_ BitVec 80))
(declare-const p217 (_ BitVec 80))
(declare-const p218 (_ BitVec 80))
(declare-const p219 (_ BitVec 80))
(declare-const p220 (_ BitVec 80))
(declare-const p221 (_ BitVec 80))
(declare-const p222 (_ BitVec 80))
; ---------- 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)
     (T p218 p219)
     (T p219 p220)
     (T p220 p221)
     (T p221 p222)))
; --------------- END (Path)------------------
(assert (= ((_ extract 39 0) p10) ((_ extract 39 0) p20)))
(assert (= ((_ extract 79 40) p10) (_ bv0 40)))
(assert (= ((_ extract 79 40) p20) (_ bv549755813888 40)))
(assert (or (and (T p122 p122) (not (T p222 p222)))
    (and (not (T p122 p122)) (T p222 p222))))
(echo "Does gene 39 affect the stability of the system?")
(check-sat)
(pop)
(get-info :all-statistics)