(set-option :produce-models true) (set-option :pull-nested-quantifiers true) (set-option :mbqi true) (declare-const x (_ BitVec 12)) (declare-const y (_ BitVec 12)) (declare-const xs (_ BitVec 12)) ; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\budding_yeast.cnet-------- (declare-fun T ((_ BitVec 12) (_ BitVec 12) ) bool) ; -------------- Transition Relation: ----------------- (assert (forall ((x (_ BitVec 12)) (y (_ BitVec 12)) )(= (T x y) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (or false)) (= (= ((_ extract 1 1) y) (_ bv1 1)) (or (and (= ((_ extract 0 0) x) (_ bv1 1))))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (or (and (= ((_ extract 2 2) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1)))) (and (= ((_ extract 1 1) x) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (and (= ((_ extract 1 1) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1)))))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (or (and (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1)))) (and (= ((_ extract 1 1) x) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (and (= ((_ extract 1 1) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1)))))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (or (and (= ((_ extract 2 2) x) (_ bv1 1))))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (or (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 6 6) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1)))) (and (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 6 6) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 6 6) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1))) (and (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 6 6) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 11 11) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 11 11) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 6 6) x) (_ bv1 1))) (= ((_ extract 11 11) x) (_ bv1 1))) (and (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (and (= ((_ extract 5 5) x) (_ bv1 1)) (not (= ((_ extract 6 6) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (= ((_ extract 5 5) x) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 6 6) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 11 11) x) (_ bv1 1))) (and (not (= ((_ extract 6 6) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 6 6) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 6 6) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1))))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (or (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (= ((_ extract 3 3) x) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1))) (and (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 5 5) x) (_ bv1 1))) (not (= ((_ extract 10 10) x) (_ bv1 1)))))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (or (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 6 6) x) (_ bv1 1))) (= ((_ extract 7 7) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1)))) (and (not (= ((_ extract 6 6) x) (_ bv1 1))) (= ((_ extract 7 7) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (= ((_ extract 7 7) x) (_ bv1 1)) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 6 6) x) (_ bv1 1))) (= ((_ extract 7 7) x) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (and (not (= ((_ extract 4 4) x) (_ bv1 1))) (not (= ((_ extract 6 6) x) (_ bv1 1))) (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1))))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (or (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 8 8) x) (_ bv1 1))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 8 8) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (and (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 8 8) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 8 8) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 8 8) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 8 8) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 8 8) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 10 10) x) (_ bv1 1)))) (and (not (= ((_ extract 5 5) x) (_ bv1 1))) (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1))) (= ((_ extract 9 9) x) (_ bv1 1))))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (or (and (= ((_ extract 8 8) x) (_ bv1 1))) (and (= ((_ extract 6 6) x) (_ bv1 1))))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (or (and (= ((_ extract 9 9) x) (_ bv1 1))) (and (= ((_ extract 8 8) x) (_ bv1 1))))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (or (and (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 10 10) x) (_ bv1 1))) (and (= ((_ extract 9 9) x) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (and (not (= ((_ extract 8 8) x) (_ bv1 1))) (= ((_ extract 9 9) x) (_ bv1 1))))))))) ; ------------------ END ------------------------------ (echo "Testing the stability of model budding_yeast") (echo "-----------------------------------------------------------") (echo "Is the system non-deterministic?") (push) (assert (and (T x y) (T x xs) (not (= y xs)))) (check-sat) (pop) (declare-const p0 (_ BitVec 12)) (declare-const p1 (_ BitVec 12)) (assert (T p0 p1)) (echo "Is oscillation possible (k=1)?") (push) (assert (not (T p1 p1))) (check-sat) (pop) (echo "Is stabilization possible (k=1)?") (push) (assert (T p1 p1)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=1)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p2 (_ BitVec 12)) (assert (T p1 p2)) (echo "Is oscillation possible (k=2)?") (push) (assert (not (T p2 p2))) (check-sat) (pop) (echo "Is stabilization possible (k=2)?") (push) (assert (T p2 p2)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=2)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p3 (_ BitVec 12)) (assert (T p2 p3)) (echo "Is oscillation possible (k=3)?") (push) (assert (not (T p3 p3))) (check-sat) (pop) (echo "Is stabilization possible (k=3)?") (push) (assert (T p3 p3)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=3)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p4 (_ BitVec 12)) (assert (T p3 p4)) (echo "Is oscillation possible (k=4)?") (push) (assert (not (T p4 p4))) (check-sat) (pop) (echo "Is stabilization possible (k=4)?") (push) (assert (T p4 p4)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=4)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p5 (_ BitVec 12)) (assert (T p4 p5)) (echo "Is oscillation possible (k=5)?") (push) (assert (not (T p5 p5))) (check-sat) (pop) (echo "Is stabilization possible (k=5)?") (push) (assert (T p5 p5)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=5)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p6 (_ BitVec 12)) (assert (T p5 p6)) (echo "Is oscillation possible (k=6)?") (push) (assert (not (T p6 p6))) (check-sat) (pop) (echo "Is stabilization possible (k=6)?") (push) (assert (T p6 p6)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=6)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p7 (_ BitVec 12)) (assert (T p6 p7)) (echo "Is oscillation possible (k=7)?") (push) (assert (not (T p7 p7))) (check-sat) (pop) (echo "Is stabilization possible (k=7)?") (push) (assert (T p7 p7)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=7)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p8 (_ BitVec 12)) (assert (T p7 p8)) (echo "Is oscillation possible (k=8)?") (push) (assert (not (T p8 p8))) (check-sat) (pop) (echo "Is stabilization possible (k=8)?") (push) (assert (T p8 p8)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=8)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p9 (_ BitVec 12)) (assert (T p8 p9)) (echo "Is oscillation possible (k=9)?") (push) (assert (not (T p9 p9))) (check-sat) (pop) (echo "Is stabilization possible (k=9)?") (push) (assert (T p9 p9)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=9)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p10 (_ BitVec 12)) (assert (T p9 p10)) (echo "Is oscillation possible (k=10)?") (push) (assert (not (T p10 p10))) (check-sat) (pop) (echo "Is stabilization possible (k=10)?") (push) (assert (T p10 p10)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=10)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))) (and (not (= p10 p0)) (not (= p10 p1)) (not (= p10 p2)) (not (= p10 p3)) (not (= p10 p4)) (not (= p10 p5)) (not (= p10 p6)) (not (= p10 p7)) (not (= p10 p8)) (not (= p10 p9))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p11 (_ BitVec 12)) (assert (T p10 p11)) (echo "Is oscillation possible (k=11)?") (push) (assert (not (T p11 p11))) (check-sat) (pop) (echo "Is stabilization possible (k=11)?") (push) (assert (T p11 p11)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=11)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))) (and (not (= p10 p0)) (not (= p10 p1)) (not (= p10 p2)) (not (= p10 p3)) (not (= p10 p4)) (not (= p10 p5)) (not (= p10 p6)) (not (= p10 p7)) (not (= p10 p8)) (not (= p10 p9))) (and (not (= p11 p0)) (not (= p11 p1)) (not (= p11 p2)) (not (= p11 p3)) (not (= p11 p4)) (not (= p11 p5)) (not (= p11 p6)) (not (= p11 p7)) (not (= p11 p8)) (not (= p11 p9)) (not (= p11 p10))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p12 (_ BitVec 12)) (assert (T p11 p12)) (echo "Is oscillation possible (k=12)?") (push) (assert (not (T p12 p12))) (check-sat) (pop) (echo "Is stabilization possible (k=12)?") (push) (assert (T p12 p12)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=12)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))) (and (not (= p10 p0)) (not (= p10 p1)) (not (= p10 p2)) (not (= p10 p3)) (not (= p10 p4)) (not (= p10 p5)) (not (= p10 p6)) (not (= p10 p7)) (not (= p10 p8)) (not (= p10 p9))) (and (not (= p11 p0)) (not (= p11 p1)) (not (= p11 p2)) (not (= p11 p3)) (not (= p11 p4)) (not (= p11 p5)) (not (= p11 p6)) (not (= p11 p7)) (not (= p11 p8)) (not (= p11 p9)) (not (= p11 p10))) (and (not (= p12 p0)) (not (= p12 p1)) (not (= p12 p2)) (not (= p12 p3)) (not (= p12 p4)) (not (= p12 p5)) (not (= p12 p6)) (not (= p12 p7)) (not (= p12 p8)) (not (= p12 p9)) (not (= p12 p10)) (not (= p12 p11))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p13 (_ BitVec 12)) (assert (T p12 p13)) (echo "Is oscillation possible (k=13)?") (push) (assert (not (T p13 p13))) (check-sat) (pop) (echo "Is stabilization possible (k=13)?") (push) (assert (T p13 p13)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=13)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))) (and (not (= p10 p0)) (not (= p10 p1)) (not (= p10 p2)) (not (= p10 p3)) (not (= p10 p4)) (not (= p10 p5)) (not (= p10 p6)) (not (= p10 p7)) (not (= p10 p8)) (not (= p10 p9))) (and (not (= p11 p0)) (not (= p11 p1)) (not (= p11 p2)) (not (= p11 p3)) (not (= p11 p4)) (not (= p11 p5)) (not (= p11 p6)) (not (= p11 p7)) (not (= p11 p8)) (not (= p11 p9)) (not (= p11 p10))) (and (not (= p12 p0)) (not (= p12 p1)) (not (= p12 p2)) (not (= p12 p3)) (not (= p12 p4)) (not (= p12 p5)) (not (= p12 p6)) (not (= p12 p7)) (not (= p12 p8)) (not (= p12 p9)) (not (= p12 p10)) (not (= p12 p11))) (and (not (= p13 p0)) (not (= p13 p1)) (not (= p13 p2)) (not (= p13 p3)) (not (= p13 p4)) (not (= p13 p5)) (not (= p13 p6)) (not (= p13 p7)) (not (= p13 p8)) (not (= p13 p9)) (not (= p13 p10)) (not (= p13 p11)) (not (= p13 p12))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p14 (_ BitVec 12)) (assert (T p13 p14)) (echo "Is oscillation possible (k=14)?") (push) (assert (not (T p14 p14))) (check-sat) (pop) (echo "Is stabilization possible (k=14)?") (push) (assert (T p14 p14)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=14)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))) (and (not (= p10 p0)) (not (= p10 p1)) (not (= p10 p2)) (not (= p10 p3)) (not (= p10 p4)) (not (= p10 p5)) (not (= p10 p6)) (not (= p10 p7)) (not (= p10 p8)) (not (= p10 p9))) (and (not (= p11 p0)) (not (= p11 p1)) (not (= p11 p2)) (not (= p11 p3)) (not (= p11 p4)) (not (= p11 p5)) (not (= p11 p6)) (not (= p11 p7)) (not (= p11 p8)) (not (= p11 p9)) (not (= p11 p10))) (and (not (= p12 p0)) (not (= p12 p1)) (not (= p12 p2)) (not (= p12 p3)) (not (= p12 p4)) (not (= p12 p5)) (not (= p12 p6)) (not (= p12 p7)) (not (= p12 p8)) (not (= p12 p9)) (not (= p12 p10)) (not (= p12 p11))) (and (not (= p13 p0)) (not (= p13 p1)) (not (= p13 p2)) (not (= p13 p3)) (not (= p13 p4)) (not (= p13 p5)) (not (= p13 p6)) (not (= p13 p7)) (not (= p13 p8)) (not (= p13 p9)) (not (= p13 p10)) (not (= p13 p11)) (not (= p13 p12))) (and (not (= p14 p0)) (not (= p14 p1)) (not (= p14 p2)) (not (= p14 p3)) (not (= p14 p4)) (not (= p14 p5)) (not (= p14 p6)) (not (= p14 p7)) (not (= p14 p8)) (not (= p14 p9)) (not (= p14 p10)) (not (= p14 p11)) (not (= p14 p12)) (not (= p14 p13))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p15 (_ BitVec 12)) (assert (T p14 p15)) (echo "Is oscillation possible (k=15)?") (push) (assert (not (T p15 p15))) (check-sat) (pop) (echo "Is stabilization possible (k=15)?") (push) (assert (T p15 p15)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=15)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))) (and (not (= p10 p0)) (not (= p10 p1)) (not (= p10 p2)) (not (= p10 p3)) (not (= p10 p4)) (not (= p10 p5)) (not (= p10 p6)) (not (= p10 p7)) (not (= p10 p8)) (not (= p10 p9))) (and (not (= p11 p0)) (not (= p11 p1)) (not (= p11 p2)) (not (= p11 p3)) (not (= p11 p4)) (not (= p11 p5)) (not (= p11 p6)) (not (= p11 p7)) (not (= p11 p8)) (not (= p11 p9)) (not (= p11 p10))) (and (not (= p12 p0)) (not (= p12 p1)) (not (= p12 p2)) (not (= p12 p3)) (not (= p12 p4)) (not (= p12 p5)) (not (= p12 p6)) (not (= p12 p7)) (not (= p12 p8)) (not (= p12 p9)) (not (= p12 p10)) (not (= p12 p11))) (and (not (= p13 p0)) (not (= p13 p1)) (not (= p13 p2)) (not (= p13 p3)) (not (= p13 p4)) (not (= p13 p5)) (not (= p13 p6)) (not (= p13 p7)) (not (= p13 p8)) (not (= p13 p9)) (not (= p13 p10)) (not (= p13 p11)) (not (= p13 p12))) (and (not (= p14 p0)) (not (= p14 p1)) (not (= p14 p2)) (not (= p14 p3)) (not (= p14 p4)) (not (= p14 p5)) (not (= p14 p6)) (not (= p14 p7)) (not (= p14 p8)) (not (= p14 p9)) (not (= p14 p10)) (not (= p14 p11)) (not (= p14 p12)) (not (= p14 p13))) (and (not (= p15 p0)) (not (= p15 p1)) (not (= p15 p2)) (not (= p15 p3)) (not (= p15 p4)) (not (= p15 p5)) (not (= p15 p6)) (not (= p15 p7)) (not (= p15 p8)) (not (= p15 p9)) (not (= p15 p10)) (not (= p15 p11)) (not (= p15 p12)) (not (= p15 p13)) (not (= p15 p14))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p16 (_ BitVec 12)) (assert (T p15 p16)) (echo "Is oscillation possible (k=16)?") (push) (assert (not (T p16 p16))) (check-sat) (pop) (echo "Is stabilization possible (k=16)?") (push) (assert (T p16 p16)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=16)?") ; ---------- Loop Free: --------------- (assert (and (and (not (= p1 p0))) (and (not (= p2 p0)) (not (= p2 p1))) (and (not (= p3 p0)) (not (= p3 p1)) (not (= p3 p2))) (and (not (= p4 p0)) (not (= p4 p1)) (not (= p4 p2)) (not (= p4 p3))) (and (not (= p5 p0)) (not (= p5 p1)) (not (= p5 p2)) (not (= p5 p3)) (not (= p5 p4))) (and (not (= p6 p0)) (not (= p6 p1)) (not (= p6 p2)) (not (= p6 p3)) (not (= p6 p4)) (not (= p6 p5))) (and (not (= p7 p0)) (not (= p7 p1)) (not (= p7 p2)) (not (= p7 p3)) (not (= p7 p4)) (not (= p7 p5)) (not (= p7 p6))) (and (not (= p8 p0)) (not (= p8 p1)) (not (= p8 p2)) (not (= p8 p3)) (not (= p8 p4)) (not (= p8 p5)) (not (= p8 p6)) (not (= p8 p7))) (and (not (= p9 p0)) (not (= p9 p1)) (not (= p9 p2)) (not (= p9 p3)) (not (= p9 p4)) (not (= p9 p5)) (not (= p9 p6)) (not (= p9 p7)) (not (= p9 p8))) (and (not (= p10 p0)) (not (= p10 p1)) (not (= p10 p2)) (not (= p10 p3)) (not (= p10 p4)) (not (= p10 p5)) (not (= p10 p6)) (not (= p10 p7)) (not (= p10 p8)) (not (= p10 p9))) (and (not (= p11 p0)) (not (= p11 p1)) (not (= p11 p2)) (not (= p11 p3)) (not (= p11 p4)) (not (= p11 p5)) (not (= p11 p6)) (not (= p11 p7)) (not (= p11 p8)) (not (= p11 p9)) (not (= p11 p10))) (and (not (= p12 p0)) (not (= p12 p1)) (not (= p12 p2)) (not (= p12 p3)) (not (= p12 p4)) (not (= p12 p5)) (not (= p12 p6)) (not (= p12 p7)) (not (= p12 p8)) (not (= p12 p9)) (not (= p12 p10)) (not (= p12 p11))) (and (not (= p13 p0)) (not (= p13 p1)) (not (= p13 p2)) (not (= p13 p3)) (not (= p13 p4)) (not (= p13 p5)) (not (= p13 p6)) (not (= p13 p7)) (not (= p13 p8)) (not (= p13 p9)) (not (= p13 p10)) (not (= p13 p11)) (not (= p13 p12))) (and (not (= p14 p0)) (not (= p14 p1)) (not (= p14 p2)) (not (= p14 p3)) (not (= p14 p4)) (not (= p14 p5)) (not (= p14 p6)) (not (= p14 p7)) (not (= p14 p8)) (not (= p14 p9)) (not (= p14 p10)) (not (= p14 p11)) (not (= p14 p12)) (not (= p14 p13))) (and (not (= p15 p0)) (not (= p15 p1)) (not (= p15 p2)) (not (= p15 p3)) (not (= p15 p4)) (not (= p15 p5)) (not (= p15 p6)) (not (= p15 p7)) (not (= p15 p8)) (not (= p15 p9)) (not (= p15 p10)) (not (= p15 p11)) (not (= p15 p12)) (not (= p15 p13)) (not (= p15 p14))) (and (not (= p16 p0)) (not (= p16 p1)) (not (= p16 p2)) (not (= p16 p3)) (not (= p16 p4)) (not (= p16 p5)) (not (= p16 p6)) (not (= p16 p7)) (not (= p16 p8)) (not (= p16 p9)) (not (= p16 p10)) (not (= p16 p11)) (not (= p16 p12)) (not (= p16 p13)) (not (= p16 p14)) (not (= p16 p15))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p17 (_ BitVec 12)) (assert (T p16 p17)) (echo "Is oscillation possible (k=17)?") (push) (assert (not (T p17 p17))) (check-sat) (pop) (get-info :all-statistics)