(set-option :produce-models true) (set-option :pull-nested-quantifiers true) (set-option :mbqi true) (declare-const x (_ BitVec 20)) (declare-const y (_ BitVec 20)) (declare-const xs (_ BitVec 20)) ; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\fission_yeast.cnet-------- (declare-fun T ((_ BitVec 20) (_ BitVec 20) ) bool) ; -------------- Transition Relation: ----------------- (assert (forall ((x (_ BitVec 20)) (y (_ BitVec 20)) )(= (T x y) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (and (or false) (not (= ((_ extract 10 10) x) (_ bv1 1))))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (and (or (and (= ((_ extract 0 0) x) (_ bv1 1)))) (not (= ((_ extract 11 11) x) (_ bv1 1))))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (and (or (and (not (= ((_ extract 1 1) x) (_ bv1 1))) (= ((_ extract 2 2) x) (_ bv1 1)) (not (= ((_ extract 3 3) x) (_ bv1 1))) (not (= ((_ extract 9 9) x) (_ bv1 1)))) (and (= ((_ extract 2 2) x) (_ bv1 1)) (not (= ((_ extract 3 3) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 9 9) x) (_ bv1 1)))) (and (not (= ((_ extract 1 1) x) (_ bv1 1))) (= ((_ extract 2 2) x) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 9 9) x) (_ bv1 1)))) (and (not (= ((_ extract 1 1) x) (_ bv1 1))) (= ((_ extract 2 2) x) (_ bv1 1)) (not (= ((_ extract 3 3) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1))) (and (not (= ((_ extract 1 1) x) (_ bv1 1))) (not (= ((_ extract 3 3) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 9 9) x) (_ bv1 1))))) (not (= ((_ extract 12 12) x) (_ bv1 1))))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (and (or (and (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 7 7) x) (_ bv1 1)))) (and (not (= ((_ extract 2 2) x) (_ bv1 1))) (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1)))) (and (not (= ((_ extract 2 2) x) (_ bv1 1))) (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 4 4) x) (_ bv1 1)))) (and (not (= ((_ extract 2 2) x) (_ bv1 1))) (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 7 7) x) (_ bv1 1))))) (not (= ((_ extract 13 13) x) (_ bv1 1))))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (and (or (and (not (= ((_ extract 3 3) x) (_ bv1 1))) (= ((_ extract 4 4) x) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (and (not (= ((_ extract 1 1) x) (_ bv1 1))) (not (= ((_ extract 3 3) x) (_ bv1 1))) (= ((_ extract 4 4) x) (_ bv1 1)) (not (= ((_ extract 9 9) x) (_ bv1 1)))) (and (not (= ((_ extract 1 1) x) (_ bv1 1))) (= ((_ extract 4 4) x) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 9 9) x) (_ bv1 1)))) (and (not (= ((_ extract 1 1) x) (_ bv1 1))) (not (= ((_ extract 3 3) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 9 9) x) (_ bv1 1))))) (not (= ((_ extract 14 14) x) (_ bv1 1))))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (and (or (and (= ((_ extract 7 7) x) (_ bv1 1)))) (not (= ((_ extract 15 15) x) (_ bv1 1))))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (and (or (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1))) (and (= ((_ extract 3 3) x) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (and (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 5 5) x) (_ bv1 1))))) (not (= ((_ extract 16 16) x) (_ bv1 1))))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (and (or (and (= ((_ extract 9 9) x) (_ bv1 1)))) (not (= ((_ extract 17 17) x) (_ bv1 1))))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (and (or (and (not (= ((_ extract 3 3) x) (_ bv1 1))) (= ((_ extract 8 8) x) (_ bv1 1))) (and (= ((_ extract 5 5) x) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (and (not (= ((_ extract 3 3) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)))) (not (= ((_ extract 18 18) x) (_ bv1 1))))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (and (or (and (not (= ((_ extract 2 2) x) (_ bv1 1))) (not (= ((_ extract 4 4) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 9 9) x) (_ bv1 1)))) (not (= ((_ extract 19 19) x) (_ bv1 1))))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))))))) ; ------------------ END ------------------------------ (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv1 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 0 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv2 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 1 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv4 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 2 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv8 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 3 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv16 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 4 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv32 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 5 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv64 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 6 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv128 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 7 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv256 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 8 affect the stability of the system?") (check-sat) (pop) (push) (declare-const p10 (_ BitVec 20)) (declare-const p11 (_ BitVec 20)) (declare-const p12 (_ BitVec 20)) (declare-const p13 (_ BitVec 20)) (declare-const p14 (_ BitVec 20)) (declare-const p15 (_ BitVec 20)) (declare-const p16 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p10 p11) (T p11 p12) (T p12 p13) (T p13 p14) (T p14 p15) (T p15 p16))) ; --------------- END (Path)------------------ (declare-const p20 (_ BitVec 20)) (declare-const p21 (_ BitVec 20)) (declare-const p22 (_ BitVec 20)) (declare-const p23 (_ BitVec 20)) (declare-const p24 (_ BitVec 20)) (declare-const p25 (_ BitVec 20)) (declare-const p26 (_ BitVec 20)) ; ---------- QFBV Path Correctness: --------------- (assert (and (T p20 p21) (T p21 p22) (T p22 p23) (T p23 p24) (T p24 p25) (T p25 p26))) ; --------------- END (Path)------------------ (assert (= ((_ extract 9 0) p10) ((_ extract 9 0) p20))) (assert (= ((_ extract 19 10) p10) (_ bv0 10))) (assert (= ((_ extract 19 10) p20) (_ bv512 10))) (assert (or (and (T p16 p16) (not (T p26 p26))) (and (not (T p16 p16)) (T p26 p26)))) (echo "Does gene 9 affect the stability of the system?") (check-sat) (pop) (get-info :all-statistics)