(set-option :produce-models true) (set-option :pull-nested-quantifiers true) (set-option :mbqi true) (declare-const x (_ BitVec 52)) (declare-const y (_ BitVec 52)) (declare-const xs (_ BitVec 52)) ; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\drosophila4.cnet-------- (declare-fun T ((_ BitVec 52) (_ BitVec 52) ) bool) ; -------------- Transition Relation: ----------------- (assert (forall ((x (_ BitVec 52)) (y (_ BitVec 52)) )(= (T x y) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (or false)) (= (= ((_ extract 1 1) y) (_ bv1 1)) (or false)) (= (= ((_ extract 2 2) y) (_ bv1 1)) (or true)) (= (= ((_ extract 3 3) y) (_ bv1 1)) (or true)) (= (= ((_ extract 4 4) y) (_ bv1 1)) (or (and (= ((_ extract 44 44) x) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1)) (not (= ((_ extract 48 48) x) (_ bv1 1)))) (and (= ((_ extract 4 4) x) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1)) (not (= ((_ extract 48 48) x) (_ bv1 1)))) (and (= ((_ extract 4 4) x) (_ bv1 1)) (= ((_ extract 44 44) x) (_ bv1 1)) (not (= ((_ extract 48 48) x) (_ bv1 1)))))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (or (and (= ((_ extract 45 45) x) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1)) (not (= ((_ extract 49 49) x) (_ bv1 1)))) (and (= ((_ extract 5 5) x) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1)) (not (= ((_ extract 49 49) x) (_ bv1 1)))) (and (= ((_ extract 5 5) x) (_ bv1 1)) (= ((_ extract 45 45) x) (_ bv1 1)) (not (= ((_ extract 49 49) x) (_ bv1 1)))))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (or (and (= ((_ extract 46 46) x) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1)) (not (= ((_ extract 50 50) x) (_ bv1 1)))) (and (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1)) (not (= ((_ extract 50 50) x) (_ bv1 1)))) (and (= ((_ extract 6 6) x) (_ bv1 1)) (= ((_ extract 46 46) x) (_ bv1 1)) (not (= ((_ extract 50 50) x) (_ bv1 1)))))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (or (and (= ((_ extract 47 47) x) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 51 51) x) (_ bv1 1)))) (and (= ((_ extract 7 7) x) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1)) (not (= ((_ extract 51 51) x) (_ bv1 1)))) (and (= ((_ extract 7 7) x) (_ bv1 1)) (= ((_ extract 47 47) x) (_ bv1 1)) (not (= ((_ extract 51 51) x) (_ bv1 1)))))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (or (and (= ((_ extract 4 4) x) (_ bv1 1))))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (or (and (= ((_ extract 5 5) x) (_ bv1 1))))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (or (and (= ((_ extract 6 6) x) (_ bv1 1))))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (or (and (= ((_ extract 7 7) x) (_ bv1 1))))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (or (and (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 0 0) x) (_ bv1 1)))))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (or (and (= ((_ extract 10 10) x) (_ bv1 1)) (not (= ((_ extract 1 1) x) (_ bv1 1)))) (and (= ((_ extract 8 8) x) (_ bv1 1)) (not (= ((_ extract 1 1) x) (_ bv1 1)))))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (or (and (= ((_ extract 11 11) x) (_ bv1 1)) (not (= ((_ extract 2 2) x) (_ bv1 1)))) (and (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 2 2) x) (_ bv1 1)))))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (or (and (= ((_ extract 10 10) x) (_ bv1 1)) (not (= ((_ extract 3 3) x) (_ bv1 1)))))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (or (and (= ((_ extract 12 12) x) (_ bv1 1))))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (or (and (= ((_ extract 13 13) x) (_ bv1 1))))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (or (and (= ((_ extract 14 14) x) (_ bv1 1))))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (or (and (= ((_ extract 15 15) x) (_ bv1 1))))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (or (and (= ((_ extract 16 16) x) (_ bv1 1)) (not (= ((_ extract 48 48) x) (_ bv1 1)))))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (or (and (= ((_ extract 17 17) x) (_ bv1 1)) (not (= ((_ extract 49 49) x) (_ bv1 1)))))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (or (and (= ((_ extract 18 18) x) (_ bv1 1)) (not (= ((_ extract 50 50) x) (_ bv1 1)))))) (= (= ((_ extract 23 23) y) (_ bv1 1)) (or (and (= ((_ extract 19 19) x) (_ bv1 1)) (not (= ((_ extract 51 51) x) (_ bv1 1)))))) (= (= ((_ extract 24 24) y) (_ bv1 1)) (or (and (= ((_ extract 20 20) x) (_ bv1 1))))) (= (= ((_ extract 25 25) y) (_ bv1 1)) (or (and (= ((_ extract 21 21) x) (_ bv1 1))))) (= (= ((_ extract 26 26) y) (_ bv1 1)) (or (and (= ((_ extract 22 22) x) (_ bv1 1))))) (= (= ((_ extract 27 27) y) (_ bv1 1)) (or (and (= ((_ extract 23 23) x) (_ bv1 1))))) (= (= ((_ extract 28 28) y) (_ bv1 1)) (or (and (= ((_ extract 44 44) x) (_ bv1 1)) (not (= ((_ extract 16 16) x) (_ bv1 1))) (not (= ((_ extract 48 48) x) (_ bv1 1)))))) (= (= ((_ extract 29 29) y) (_ bv1 1)) (or (and (= ((_ extract 45 45) x) (_ bv1 1)) (not (= ((_ extract 17 17) x) (_ bv1 1))) (not (= ((_ extract 49 49) x) (_ bv1 1)))))) (= (= ((_ extract 30 30) y) (_ bv1 1)) (or (and (= ((_ extract 46 46) x) (_ bv1 1)) (not (= ((_ extract 18 18) x) (_ bv1 1))) (not (= ((_ extract 50 50) x) (_ bv1 1)))))) (= (= ((_ extract 31 31) y) (_ bv1 1)) (or (and (= ((_ extract 47 47) x) (_ bv1 1)) (not (= ((_ extract 19 19) x) (_ bv1 1))) (not (= ((_ extract 51 51) x) (_ bv1 1)))))) (= (= ((_ extract 32 32) y) (_ bv1 1)) (or (and (= ((_ extract 32 32) x) (_ bv1 1)) (not (= ((_ extract 25 25) x) (_ bv1 1)))) (and (= ((_ extract 28 28) x) (_ bv1 1))))) (= (= ((_ extract 33 33) y) (_ bv1 1)) (or (and (= ((_ extract 33 33) x) (_ bv1 1)) (not (= ((_ extract 24 24) x) (_ bv1 1))) (not (= ((_ extract 26 26) x) (_ bv1 1)))) (and (= ((_ extract 29 29) x) (_ bv1 1))))) (= (= ((_ extract 34 34) y) (_ bv1 1)) (or (and (= ((_ extract 34 34) x) (_ bv1 1)) (not (= ((_ extract 25 25) x) (_ bv1 1))) (not (= ((_ extract 27 27) x) (_ bv1 1)))) (and (= ((_ extract 30 30) x) (_ bv1 1))))) (= (= ((_ extract 35 35) y) (_ bv1 1)) (or (and (= ((_ extract 35 35) x) (_ bv1 1)) (not (= ((_ extract 26 26) x) (_ bv1 1)))) (and (= ((_ extract 31 31) x) (_ bv1 1))))) (= (= ((_ extract 36 36) y) (_ bv1 1)) (or (and (not (= ((_ extract 16 16) x) (_ bv1 1)))))) (= (= ((_ extract 37 37) y) (_ bv1 1)) (or (and (not (= ((_ extract 17 17) x) (_ bv1 1)))))) (= (= ((_ extract 38 38) y) (_ bv1 1)) (or (and (not (= ((_ extract 18 18) x) (_ bv1 1)))))) (= (= ((_ extract 39 39) y) (_ bv1 1)) (or (and (not (= ((_ extract 19 19) x) (_ bv1 1)))))) (= (= ((_ extract 40 40) y) (_ bv1 1)) (or (and (= ((_ extract 36 36) x) (_ bv1 1))))) (= (= ((_ extract 41 41) y) (_ bv1 1)) (or (and (= ((_ extract 37 37) x) (_ bv1 1))))) (= (= ((_ extract 42 42) y) (_ bv1 1)) (or (and (= ((_ extract 38 38) x) (_ bv1 1))))) (= (= ((_ extract 43 43) y) (_ bv1 1)) (or (and (= ((_ extract 39 39) x) (_ bv1 1))))) (= (= ((_ extract 44 44) y) (_ bv1 1)) (or (and (= ((_ extract 40 40) x) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (and (= ((_ extract 40 40) x) (_ bv1 1)) (= ((_ extract 25 25) x) (_ bv1 1))) (and (= ((_ extract 40 40) x) (_ bv1 1)) (not (= ((_ extract 32 32) x) (_ bv1 1)))))) (= (= ((_ extract 45 45) y) (_ bv1 1)) (or (and (= ((_ extract 41 41) x) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1))) (and (= ((_ extract 41 41) x) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (and (= ((_ extract 41 41) x) (_ bv1 1)) (= ((_ extract 26 26) x) (_ bv1 1))) (and (= ((_ extract 41 41) x) (_ bv1 1)) (= ((_ extract 24 24) x) (_ bv1 1))) (and (= ((_ extract 41 41) x) (_ bv1 1)) (not (= ((_ extract 33 33) x) (_ bv1 1)))))) (= (= ((_ extract 46 46) y) (_ bv1 1)) (or (and (= ((_ extract 42 42) x) (_ bv1 1)) (= ((_ extract 23 23) x) (_ bv1 1))) (and (= ((_ extract 42 42) x) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (and (= ((_ extract 42 42) x) (_ bv1 1)) (= ((_ extract 27 27) x) (_ bv1 1))) (and (= ((_ extract 42 42) x) (_ bv1 1)) (= ((_ extract 25 25) x) (_ bv1 1))) (and (= ((_ extract 42 42) x) (_ bv1 1)) (not (= ((_ extract 34 34) x) (_ bv1 1)))))) (= (= ((_ extract 47 47) y) (_ bv1 1)) (or (and (= ((_ extract 43 43) x) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1))) (and (= ((_ extract 43 43) x) (_ bv1 1)) (= ((_ extract 26 26) x) (_ bv1 1))) (and (= ((_ extract 43 43) x) (_ bv1 1)) (not (= ((_ extract 35 35) x) (_ bv1 1)))))) (= (= ((_ extract 48 48) y) (_ bv1 1)) (or (and (= ((_ extract 40 40) x) (_ bv1 1)) (= ((_ extract 32 32) x) (_ bv1 1)) (not (= ((_ extract 25 25) x) (_ bv1 1))) (not (= ((_ extract 21 21) x) (_ bv1 1)))))) (= (= ((_ extract 49 49) y) (_ bv1 1)) (or (and (= ((_ extract 41 41) x) (_ bv1 1)) (= ((_ extract 33 33) x) (_ bv1 1)) (not (= ((_ extract 24 24) x) (_ bv1 1))) (not (= ((_ extract 26 26) x) (_ bv1 1))) (not (= ((_ extract 20 20) x) (_ bv1 1))) (not (= ((_ extract 22 22) x) (_ bv1 1)))))) (= (= ((_ extract 50 50) y) (_ bv1 1)) (or (and (= ((_ extract 42 42) x) (_ bv1 1)) (= ((_ extract 34 34) x) (_ bv1 1)) (not (= ((_ extract 25 25) x) (_ bv1 1))) (not (= ((_ extract 27 27) x) (_ bv1 1))) (not (= ((_ extract 21 21) x) (_ bv1 1))) (not (= ((_ extract 23 23) x) (_ bv1 1)))))) (= (= ((_ extract 51 51) y) (_ bv1 1)) (or (and (= ((_ extract 43 43) x) (_ bv1 1)) (= ((_ extract 35 35) x) (_ bv1 1)) (not (= ((_ extract 26 26) x) (_ bv1 1))) (not (= ((_ extract 22 22) x) (_ bv1 1)))))))))) ; ------------------ END ------------------------------ (echo "Testing the stability of model drosophila4") (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 52)) (declare-const p1 (_ BitVec 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (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 52)) (assert (T p16 p17)) (echo "Is oscillation possible (k=17)?") (push) (assert (not (T p17 p17))) (check-sat) (pop) (echo "Is stabilization possible (k=17)?") (push) (assert (T p17 p17)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=17)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p18 (_ BitVec 52)) (assert (T p17 p18)) (echo "Is oscillation possible (k=18)?") (push) (assert (not (T p18 p18))) (check-sat) (pop) (echo "Is stabilization possible (k=18)?") (push) (assert (T p18 p18)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=18)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p19 (_ BitVec 52)) (assert (T p18 p19)) (echo "Is oscillation possible (k=19)?") (push) (assert (not (T p19 p19))) (check-sat) (pop) (echo "Is stabilization possible (k=19)?") (push) (assert (T p19 p19)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=19)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p20 (_ BitVec 52)) (assert (T p19 p20)) (echo "Is oscillation possible (k=20)?") (push) (assert (not (T p20 p20))) (check-sat) (pop) (echo "Is stabilization possible (k=20)?") (push) (assert (T p20 p20)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=20)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p21 (_ BitVec 52)) (assert (T p20 p21)) (echo "Is oscillation possible (k=21)?") (push) (assert (not (T p21 p21))) (check-sat) (pop) (echo "Is stabilization possible (k=21)?") (push) (assert (T p21 p21)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=21)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p22 (_ BitVec 52)) (assert (T p21 p22)) (echo "Is oscillation possible (k=22)?") (push) (assert (not (T p22 p22))) (check-sat) (pop) (echo "Is stabilization possible (k=22)?") (push) (assert (T p22 p22)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=22)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p23 (_ BitVec 52)) (assert (T p22 p23)) (echo "Is oscillation possible (k=23)?") (push) (assert (not (T p23 p23))) (check-sat) (pop) (echo "Is stabilization possible (k=23)?") (push) (assert (T p23 p23)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=23)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p24 (_ BitVec 52)) (assert (T p23 p24)) (echo "Is oscillation possible (k=24)?") (push) (assert (not (T p24 p24))) (check-sat) (pop) (echo "Is stabilization possible (k=24)?") (push) (assert (T p24 p24)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=24)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p25 (_ BitVec 52)) (assert (T p24 p25)) (echo "Is oscillation possible (k=25)?") (push) (assert (not (T p25 p25))) (check-sat) (pop) (echo "Is stabilization possible (k=25)?") (push) (assert (T p25 p25)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=25)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))) (and (not (= p25 p0)) (not (= p25 p1)) (not (= p25 p2)) (not (= p25 p3)) (not (= p25 p4)) (not (= p25 p5)) (not (= p25 p6)) (not (= p25 p7)) (not (= p25 p8)) (not (= p25 p9)) (not (= p25 p10)) (not (= p25 p11)) (not (= p25 p12)) (not (= p25 p13)) (not (= p25 p14)) (not (= p25 p15)) (not (= p25 p16)) (not (= p25 p17)) (not (= p25 p18)) (not (= p25 p19)) (not (= p25 p20)) (not (= p25 p21)) (not (= p25 p22)) (not (= p25 p23)) (not (= p25 p24))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p26 (_ BitVec 52)) (assert (T p25 p26)) (echo "Is oscillation possible (k=26)?") (push) (assert (not (T p26 p26))) (check-sat) (pop) (echo "Is stabilization possible (k=26)?") (push) (assert (T p26 p26)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=26)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))) (and (not (= p25 p0)) (not (= p25 p1)) (not (= p25 p2)) (not (= p25 p3)) (not (= p25 p4)) (not (= p25 p5)) (not (= p25 p6)) (not (= p25 p7)) (not (= p25 p8)) (not (= p25 p9)) (not (= p25 p10)) (not (= p25 p11)) (not (= p25 p12)) (not (= p25 p13)) (not (= p25 p14)) (not (= p25 p15)) (not (= p25 p16)) (not (= p25 p17)) (not (= p25 p18)) (not (= p25 p19)) (not (= p25 p20)) (not (= p25 p21)) (not (= p25 p22)) (not (= p25 p23)) (not (= p25 p24))) (and (not (= p26 p0)) (not (= p26 p1)) (not (= p26 p2)) (not (= p26 p3)) (not (= p26 p4)) (not (= p26 p5)) (not (= p26 p6)) (not (= p26 p7)) (not (= p26 p8)) (not (= p26 p9)) (not (= p26 p10)) (not (= p26 p11)) (not (= p26 p12)) (not (= p26 p13)) (not (= p26 p14)) (not (= p26 p15)) (not (= p26 p16)) (not (= p26 p17)) (not (= p26 p18)) (not (= p26 p19)) (not (= p26 p20)) (not (= p26 p21)) (not (= p26 p22)) (not (= p26 p23)) (not (= p26 p24)) (not (= p26 p25))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p27 (_ BitVec 52)) (assert (T p26 p27)) (echo "Is oscillation possible (k=27)?") (push) (assert (not (T p27 p27))) (check-sat) (pop) (echo "Is stabilization possible (k=27)?") (push) (assert (T p27 p27)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=27)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))) (and (not (= p25 p0)) (not (= p25 p1)) (not (= p25 p2)) (not (= p25 p3)) (not (= p25 p4)) (not (= p25 p5)) (not (= p25 p6)) (not (= p25 p7)) (not (= p25 p8)) (not (= p25 p9)) (not (= p25 p10)) (not (= p25 p11)) (not (= p25 p12)) (not (= p25 p13)) (not (= p25 p14)) (not (= p25 p15)) (not (= p25 p16)) (not (= p25 p17)) (not (= p25 p18)) (not (= p25 p19)) (not (= p25 p20)) (not (= p25 p21)) (not (= p25 p22)) (not (= p25 p23)) (not (= p25 p24))) (and (not (= p26 p0)) (not (= p26 p1)) (not (= p26 p2)) (not (= p26 p3)) (not (= p26 p4)) (not (= p26 p5)) (not (= p26 p6)) (not (= p26 p7)) (not (= p26 p8)) (not (= p26 p9)) (not (= p26 p10)) (not (= p26 p11)) (not (= p26 p12)) (not (= p26 p13)) (not (= p26 p14)) (not (= p26 p15)) (not (= p26 p16)) (not (= p26 p17)) (not (= p26 p18)) (not (= p26 p19)) (not (= p26 p20)) (not (= p26 p21)) (not (= p26 p22)) (not (= p26 p23)) (not (= p26 p24)) (not (= p26 p25))) (and (not (= p27 p0)) (not (= p27 p1)) (not (= p27 p2)) (not (= p27 p3)) (not (= p27 p4)) (not (= p27 p5)) (not (= p27 p6)) (not (= p27 p7)) (not (= p27 p8)) (not (= p27 p9)) (not (= p27 p10)) (not (= p27 p11)) (not (= p27 p12)) (not (= p27 p13)) (not (= p27 p14)) (not (= p27 p15)) (not (= p27 p16)) (not (= p27 p17)) (not (= p27 p18)) (not (= p27 p19)) (not (= p27 p20)) (not (= p27 p21)) (not (= p27 p22)) (not (= p27 p23)) (not (= p27 p24)) (not (= p27 p25)) (not (= p27 p26))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p28 (_ BitVec 52)) (assert (T p27 p28)) (echo "Is oscillation possible (k=28)?") (push) (assert (not (T p28 p28))) (check-sat) (pop) (echo "Is stabilization possible (k=28)?") (push) (assert (T p28 p28)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=28)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))) (and (not (= p25 p0)) (not (= p25 p1)) (not (= p25 p2)) (not (= p25 p3)) (not (= p25 p4)) (not (= p25 p5)) (not (= p25 p6)) (not (= p25 p7)) (not (= p25 p8)) (not (= p25 p9)) (not (= p25 p10)) (not (= p25 p11)) (not (= p25 p12)) (not (= p25 p13)) (not (= p25 p14)) (not (= p25 p15)) (not (= p25 p16)) (not (= p25 p17)) (not (= p25 p18)) (not (= p25 p19)) (not (= p25 p20)) (not (= p25 p21)) (not (= p25 p22)) (not (= p25 p23)) (not (= p25 p24))) (and (not (= p26 p0)) (not (= p26 p1)) (not (= p26 p2)) (not (= p26 p3)) (not (= p26 p4)) (not (= p26 p5)) (not (= p26 p6)) (not (= p26 p7)) (not (= p26 p8)) (not (= p26 p9)) (not (= p26 p10)) (not (= p26 p11)) (not (= p26 p12)) (not (= p26 p13)) (not (= p26 p14)) (not (= p26 p15)) (not (= p26 p16)) (not (= p26 p17)) (not (= p26 p18)) (not (= p26 p19)) (not (= p26 p20)) (not (= p26 p21)) (not (= p26 p22)) (not (= p26 p23)) (not (= p26 p24)) (not (= p26 p25))) (and (not (= p27 p0)) (not (= p27 p1)) (not (= p27 p2)) (not (= p27 p3)) (not (= p27 p4)) (not (= p27 p5)) (not (= p27 p6)) (not (= p27 p7)) (not (= p27 p8)) (not (= p27 p9)) (not (= p27 p10)) (not (= p27 p11)) (not (= p27 p12)) (not (= p27 p13)) (not (= p27 p14)) (not (= p27 p15)) (not (= p27 p16)) (not (= p27 p17)) (not (= p27 p18)) (not (= p27 p19)) (not (= p27 p20)) (not (= p27 p21)) (not (= p27 p22)) (not (= p27 p23)) (not (= p27 p24)) (not (= p27 p25)) (not (= p27 p26))) (and (not (= p28 p0)) (not (= p28 p1)) (not (= p28 p2)) (not (= p28 p3)) (not (= p28 p4)) (not (= p28 p5)) (not (= p28 p6)) (not (= p28 p7)) (not (= p28 p8)) (not (= p28 p9)) (not (= p28 p10)) (not (= p28 p11)) (not (= p28 p12)) (not (= p28 p13)) (not (= p28 p14)) (not (= p28 p15)) (not (= p28 p16)) (not (= p28 p17)) (not (= p28 p18)) (not (= p28 p19)) (not (= p28 p20)) (not (= p28 p21)) (not (= p28 p22)) (not (= p28 p23)) (not (= p28 p24)) (not (= p28 p25)) (not (= p28 p26)) (not (= p28 p27))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p29 (_ BitVec 52)) (assert (T p28 p29)) (echo "Is oscillation possible (k=29)?") (push) (assert (not (T p29 p29))) (check-sat) (pop) (echo "Is stabilization possible (k=29)?") (push) (assert (T p29 p29)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=29)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))) (and (not (= p25 p0)) (not (= p25 p1)) (not (= p25 p2)) (not (= p25 p3)) (not (= p25 p4)) (not (= p25 p5)) (not (= p25 p6)) (not (= p25 p7)) (not (= p25 p8)) (not (= p25 p9)) (not (= p25 p10)) (not (= p25 p11)) (not (= p25 p12)) (not (= p25 p13)) (not (= p25 p14)) (not (= p25 p15)) (not (= p25 p16)) (not (= p25 p17)) (not (= p25 p18)) (not (= p25 p19)) (not (= p25 p20)) (not (= p25 p21)) (not (= p25 p22)) (not (= p25 p23)) (not (= p25 p24))) (and (not (= p26 p0)) (not (= p26 p1)) (not (= p26 p2)) (not (= p26 p3)) (not (= p26 p4)) (not (= p26 p5)) (not (= p26 p6)) (not (= p26 p7)) (not (= p26 p8)) (not (= p26 p9)) (not (= p26 p10)) (not (= p26 p11)) (not (= p26 p12)) (not (= p26 p13)) (not (= p26 p14)) (not (= p26 p15)) (not (= p26 p16)) (not (= p26 p17)) (not (= p26 p18)) (not (= p26 p19)) (not (= p26 p20)) (not (= p26 p21)) (not (= p26 p22)) (not (= p26 p23)) (not (= p26 p24)) (not (= p26 p25))) (and (not (= p27 p0)) (not (= p27 p1)) (not (= p27 p2)) (not (= p27 p3)) (not (= p27 p4)) (not (= p27 p5)) (not (= p27 p6)) (not (= p27 p7)) (not (= p27 p8)) (not (= p27 p9)) (not (= p27 p10)) (not (= p27 p11)) (not (= p27 p12)) (not (= p27 p13)) (not (= p27 p14)) (not (= p27 p15)) (not (= p27 p16)) (not (= p27 p17)) (not (= p27 p18)) (not (= p27 p19)) (not (= p27 p20)) (not (= p27 p21)) (not (= p27 p22)) (not (= p27 p23)) (not (= p27 p24)) (not (= p27 p25)) (not (= p27 p26))) (and (not (= p28 p0)) (not (= p28 p1)) (not (= p28 p2)) (not (= p28 p3)) (not (= p28 p4)) (not (= p28 p5)) (not (= p28 p6)) (not (= p28 p7)) (not (= p28 p8)) (not (= p28 p9)) (not (= p28 p10)) (not (= p28 p11)) (not (= p28 p12)) (not (= p28 p13)) (not (= p28 p14)) (not (= p28 p15)) (not (= p28 p16)) (not (= p28 p17)) (not (= p28 p18)) (not (= p28 p19)) (not (= p28 p20)) (not (= p28 p21)) (not (= p28 p22)) (not (= p28 p23)) (not (= p28 p24)) (not (= p28 p25)) (not (= p28 p26)) (not (= p28 p27))) (and (not (= p29 p0)) (not (= p29 p1)) (not (= p29 p2)) (not (= p29 p3)) (not (= p29 p4)) (not (= p29 p5)) (not (= p29 p6)) (not (= p29 p7)) (not (= p29 p8)) (not (= p29 p9)) (not (= p29 p10)) (not (= p29 p11)) (not (= p29 p12)) (not (= p29 p13)) (not (= p29 p14)) (not (= p29 p15)) (not (= p29 p16)) (not (= p29 p17)) (not (= p29 p18)) (not (= p29 p19)) (not (= p29 p20)) (not (= p29 p21)) (not (= p29 p22)) (not (= p29 p23)) (not (= p29 p24)) (not (= p29 p25)) (not (= p29 p26)) (not (= p29 p27)) (not (= p29 p28))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p30 (_ BitVec 52)) (assert (T p29 p30)) (echo "Is oscillation possible (k=30)?") (push) (assert (not (T p30 p30))) (check-sat) (pop) (echo "Is stabilization possible (k=30)?") (push) (assert (T p30 p30)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=30)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))) (and (not (= p25 p0)) (not (= p25 p1)) (not (= p25 p2)) (not (= p25 p3)) (not (= p25 p4)) (not (= p25 p5)) (not (= p25 p6)) (not (= p25 p7)) (not (= p25 p8)) (not (= p25 p9)) (not (= p25 p10)) (not (= p25 p11)) (not (= p25 p12)) (not (= p25 p13)) (not (= p25 p14)) (not (= p25 p15)) (not (= p25 p16)) (not (= p25 p17)) (not (= p25 p18)) (not (= p25 p19)) (not (= p25 p20)) (not (= p25 p21)) (not (= p25 p22)) (not (= p25 p23)) (not (= p25 p24))) (and (not (= p26 p0)) (not (= p26 p1)) (not (= p26 p2)) (not (= p26 p3)) (not (= p26 p4)) (not (= p26 p5)) (not (= p26 p6)) (not (= p26 p7)) (not (= p26 p8)) (not (= p26 p9)) (not (= p26 p10)) (not (= p26 p11)) (not (= p26 p12)) (not (= p26 p13)) (not (= p26 p14)) (not (= p26 p15)) (not (= p26 p16)) (not (= p26 p17)) (not (= p26 p18)) (not (= p26 p19)) (not (= p26 p20)) (not (= p26 p21)) (not (= p26 p22)) (not (= p26 p23)) (not (= p26 p24)) (not (= p26 p25))) (and (not (= p27 p0)) (not (= p27 p1)) (not (= p27 p2)) (not (= p27 p3)) (not (= p27 p4)) (not (= p27 p5)) (not (= p27 p6)) (not (= p27 p7)) (not (= p27 p8)) (not (= p27 p9)) (not (= p27 p10)) (not (= p27 p11)) (not (= p27 p12)) (not (= p27 p13)) (not (= p27 p14)) (not (= p27 p15)) (not (= p27 p16)) (not (= p27 p17)) (not (= p27 p18)) (not (= p27 p19)) (not (= p27 p20)) (not (= p27 p21)) (not (= p27 p22)) (not (= p27 p23)) (not (= p27 p24)) (not (= p27 p25)) (not (= p27 p26))) (and (not (= p28 p0)) (not (= p28 p1)) (not (= p28 p2)) (not (= p28 p3)) (not (= p28 p4)) (not (= p28 p5)) (not (= p28 p6)) (not (= p28 p7)) (not (= p28 p8)) (not (= p28 p9)) (not (= p28 p10)) (not (= p28 p11)) (not (= p28 p12)) (not (= p28 p13)) (not (= p28 p14)) (not (= p28 p15)) (not (= p28 p16)) (not (= p28 p17)) (not (= p28 p18)) (not (= p28 p19)) (not (= p28 p20)) (not (= p28 p21)) (not (= p28 p22)) (not (= p28 p23)) (not (= p28 p24)) (not (= p28 p25)) (not (= p28 p26)) (not (= p28 p27))) (and (not (= p29 p0)) (not (= p29 p1)) (not (= p29 p2)) (not (= p29 p3)) (not (= p29 p4)) (not (= p29 p5)) (not (= p29 p6)) (not (= p29 p7)) (not (= p29 p8)) (not (= p29 p9)) (not (= p29 p10)) (not (= p29 p11)) (not (= p29 p12)) (not (= p29 p13)) (not (= p29 p14)) (not (= p29 p15)) (not (= p29 p16)) (not (= p29 p17)) (not (= p29 p18)) (not (= p29 p19)) (not (= p29 p20)) (not (= p29 p21)) (not (= p29 p22)) (not (= p29 p23)) (not (= p29 p24)) (not (= p29 p25)) (not (= p29 p26)) (not (= p29 p27)) (not (= p29 p28))) (and (not (= p30 p0)) (not (= p30 p1)) (not (= p30 p2)) (not (= p30 p3)) (not (= p30 p4)) (not (= p30 p5)) (not (= p30 p6)) (not (= p30 p7)) (not (= p30 p8)) (not (= p30 p9)) (not (= p30 p10)) (not (= p30 p11)) (not (= p30 p12)) (not (= p30 p13)) (not (= p30 p14)) (not (= p30 p15)) (not (= p30 p16)) (not (= p30 p17)) (not (= p30 p18)) (not (= p30 p19)) (not (= p30 p20)) (not (= p30 p21)) (not (= p30 p22)) (not (= p30 p23)) (not (= p30 p24)) (not (= p30 p25)) (not (= p30 p26)) (not (= p30 p27)) (not (= p30 p28)) (not (= p30 p29))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p31 (_ BitVec 52)) (assert (T p30 p31)) (echo "Is oscillation possible (k=31)?") (push) (assert (not (T p31 p31))) (check-sat) (pop) (echo "Is stabilization possible (k=31)?") (push) (assert (T p31 p31)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=31)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))) (and (not (= p25 p0)) (not (= p25 p1)) (not (= p25 p2)) (not (= p25 p3)) (not (= p25 p4)) (not (= p25 p5)) (not (= p25 p6)) (not (= p25 p7)) (not (= p25 p8)) (not (= p25 p9)) (not (= p25 p10)) (not (= p25 p11)) (not (= p25 p12)) (not (= p25 p13)) (not (= p25 p14)) (not (= p25 p15)) (not (= p25 p16)) (not (= p25 p17)) (not (= p25 p18)) (not (= p25 p19)) (not (= p25 p20)) (not (= p25 p21)) (not (= p25 p22)) (not (= p25 p23)) (not (= p25 p24))) (and (not (= p26 p0)) (not (= p26 p1)) (not (= p26 p2)) (not (= p26 p3)) (not (= p26 p4)) (not (= p26 p5)) (not (= p26 p6)) (not (= p26 p7)) (not (= p26 p8)) (not (= p26 p9)) (not (= p26 p10)) (not (= p26 p11)) (not (= p26 p12)) (not (= p26 p13)) (not (= p26 p14)) (not (= p26 p15)) (not (= p26 p16)) (not (= p26 p17)) (not (= p26 p18)) (not (= p26 p19)) (not (= p26 p20)) (not (= p26 p21)) (not (= p26 p22)) (not (= p26 p23)) (not (= p26 p24)) (not (= p26 p25))) (and (not (= p27 p0)) (not (= p27 p1)) (not (= p27 p2)) (not (= p27 p3)) (not (= p27 p4)) (not (= p27 p5)) (not (= p27 p6)) (not (= p27 p7)) (not (= p27 p8)) (not (= p27 p9)) (not (= p27 p10)) (not (= p27 p11)) (not (= p27 p12)) (not (= p27 p13)) (not (= p27 p14)) (not (= p27 p15)) (not (= p27 p16)) (not (= p27 p17)) (not (= p27 p18)) (not (= p27 p19)) (not (= p27 p20)) (not (= p27 p21)) (not (= p27 p22)) (not (= p27 p23)) (not (= p27 p24)) (not (= p27 p25)) (not (= p27 p26))) (and (not (= p28 p0)) (not (= p28 p1)) (not (= p28 p2)) (not (= p28 p3)) (not (= p28 p4)) (not (= p28 p5)) (not (= p28 p6)) (not (= p28 p7)) (not (= p28 p8)) (not (= p28 p9)) (not (= p28 p10)) (not (= p28 p11)) (not (= p28 p12)) (not (= p28 p13)) (not (= p28 p14)) (not (= p28 p15)) (not (= p28 p16)) (not (= p28 p17)) (not (= p28 p18)) (not (= p28 p19)) (not (= p28 p20)) (not (= p28 p21)) (not (= p28 p22)) (not (= p28 p23)) (not (= p28 p24)) (not (= p28 p25)) (not (= p28 p26)) (not (= p28 p27))) (and (not (= p29 p0)) (not (= p29 p1)) (not (= p29 p2)) (not (= p29 p3)) (not (= p29 p4)) (not (= p29 p5)) (not (= p29 p6)) (not (= p29 p7)) (not (= p29 p8)) (not (= p29 p9)) (not (= p29 p10)) (not (= p29 p11)) (not (= p29 p12)) (not (= p29 p13)) (not (= p29 p14)) (not (= p29 p15)) (not (= p29 p16)) (not (= p29 p17)) (not (= p29 p18)) (not (= p29 p19)) (not (= p29 p20)) (not (= p29 p21)) (not (= p29 p22)) (not (= p29 p23)) (not (= p29 p24)) (not (= p29 p25)) (not (= p29 p26)) (not (= p29 p27)) (not (= p29 p28))) (and (not (= p30 p0)) (not (= p30 p1)) (not (= p30 p2)) (not (= p30 p3)) (not (= p30 p4)) (not (= p30 p5)) (not (= p30 p6)) (not (= p30 p7)) (not (= p30 p8)) (not (= p30 p9)) (not (= p30 p10)) (not (= p30 p11)) (not (= p30 p12)) (not (= p30 p13)) (not (= p30 p14)) (not (= p30 p15)) (not (= p30 p16)) (not (= p30 p17)) (not (= p30 p18)) (not (= p30 p19)) (not (= p30 p20)) (not (= p30 p21)) (not (= p30 p22)) (not (= p30 p23)) (not (= p30 p24)) (not (= p30 p25)) (not (= p30 p26)) (not (= p30 p27)) (not (= p30 p28)) (not (= p30 p29))) (and (not (= p31 p0)) (not (= p31 p1)) (not (= p31 p2)) (not (= p31 p3)) (not (= p31 p4)) (not (= p31 p5)) (not (= p31 p6)) (not (= p31 p7)) (not (= p31 p8)) (not (= p31 p9)) (not (= p31 p10)) (not (= p31 p11)) (not (= p31 p12)) (not (= p31 p13)) (not (= p31 p14)) (not (= p31 p15)) (not (= p31 p16)) (not (= p31 p17)) (not (= p31 p18)) (not (= p31 p19)) (not (= p31 p20)) (not (= p31 p21)) (not (= p31 p22)) (not (= p31 p23)) (not (= p31 p24)) (not (= p31 p25)) (not (= p31 p26)) (not (= p31 p27)) (not (= p31 p28)) (not (= p31 p29)) (not (= p31 p30))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p32 (_ BitVec 52)) (assert (T p31 p32)) (echo "Is oscillation possible (k=32)?") (push) (assert (not (T p32 p32))) (check-sat) (pop) (echo "Is stabilization possible (k=32)?") (push) (assert (T p32 p32)) (check-sat) (pop) (push) (echo "Can a simple path be generated (k=32)?") ; ---------- 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))) (and (not (= p17 p0)) (not (= p17 p1)) (not (= p17 p2)) (not (= p17 p3)) (not (= p17 p4)) (not (= p17 p5)) (not (= p17 p6)) (not (= p17 p7)) (not (= p17 p8)) (not (= p17 p9)) (not (= p17 p10)) (not (= p17 p11)) (not (= p17 p12)) (not (= p17 p13)) (not (= p17 p14)) (not (= p17 p15)) (not (= p17 p16))) (and (not (= p18 p0)) (not (= p18 p1)) (not (= p18 p2)) (not (= p18 p3)) (not (= p18 p4)) (not (= p18 p5)) (not (= p18 p6)) (not (= p18 p7)) (not (= p18 p8)) (not (= p18 p9)) (not (= p18 p10)) (not (= p18 p11)) (not (= p18 p12)) (not (= p18 p13)) (not (= p18 p14)) (not (= p18 p15)) (not (= p18 p16)) (not (= p18 p17))) (and (not (= p19 p0)) (not (= p19 p1)) (not (= p19 p2)) (not (= p19 p3)) (not (= p19 p4)) (not (= p19 p5)) (not (= p19 p6)) (not (= p19 p7)) (not (= p19 p8)) (not (= p19 p9)) (not (= p19 p10)) (not (= p19 p11)) (not (= p19 p12)) (not (= p19 p13)) (not (= p19 p14)) (not (= p19 p15)) (not (= p19 p16)) (not (= p19 p17)) (not (= p19 p18))) (and (not (= p20 p0)) (not (= p20 p1)) (not (= p20 p2)) (not (= p20 p3)) (not (= p20 p4)) (not (= p20 p5)) (not (= p20 p6)) (not (= p20 p7)) (not (= p20 p8)) (not (= p20 p9)) (not (= p20 p10)) (not (= p20 p11)) (not (= p20 p12)) (not (= p20 p13)) (not (= p20 p14)) (not (= p20 p15)) (not (= p20 p16)) (not (= p20 p17)) (not (= p20 p18)) (not (= p20 p19))) (and (not (= p21 p0)) (not (= p21 p1)) (not (= p21 p2)) (not (= p21 p3)) (not (= p21 p4)) (not (= p21 p5)) (not (= p21 p6)) (not (= p21 p7)) (not (= p21 p8)) (not (= p21 p9)) (not (= p21 p10)) (not (= p21 p11)) (not (= p21 p12)) (not (= p21 p13)) (not (= p21 p14)) (not (= p21 p15)) (not (= p21 p16)) (not (= p21 p17)) (not (= p21 p18)) (not (= p21 p19)) (not (= p21 p20))) (and (not (= p22 p0)) (not (= p22 p1)) (not (= p22 p2)) (not (= p22 p3)) (not (= p22 p4)) (not (= p22 p5)) (not (= p22 p6)) (not (= p22 p7)) (not (= p22 p8)) (not (= p22 p9)) (not (= p22 p10)) (not (= p22 p11)) (not (= p22 p12)) (not (= p22 p13)) (not (= p22 p14)) (not (= p22 p15)) (not (= p22 p16)) (not (= p22 p17)) (not (= p22 p18)) (not (= p22 p19)) (not (= p22 p20)) (not (= p22 p21))) (and (not (= p23 p0)) (not (= p23 p1)) (not (= p23 p2)) (not (= p23 p3)) (not (= p23 p4)) (not (= p23 p5)) (not (= p23 p6)) (not (= p23 p7)) (not (= p23 p8)) (not (= p23 p9)) (not (= p23 p10)) (not (= p23 p11)) (not (= p23 p12)) (not (= p23 p13)) (not (= p23 p14)) (not (= p23 p15)) (not (= p23 p16)) (not (= p23 p17)) (not (= p23 p18)) (not (= p23 p19)) (not (= p23 p20)) (not (= p23 p21)) (not (= p23 p22))) (and (not (= p24 p0)) (not (= p24 p1)) (not (= p24 p2)) (not (= p24 p3)) (not (= p24 p4)) (not (= p24 p5)) (not (= p24 p6)) (not (= p24 p7)) (not (= p24 p8)) (not (= p24 p9)) (not (= p24 p10)) (not (= p24 p11)) (not (= p24 p12)) (not (= p24 p13)) (not (= p24 p14)) (not (= p24 p15)) (not (= p24 p16)) (not (= p24 p17)) (not (= p24 p18)) (not (= p24 p19)) (not (= p24 p20)) (not (= p24 p21)) (not (= p24 p22)) (not (= p24 p23))) (and (not (= p25 p0)) (not (= p25 p1)) (not (= p25 p2)) (not (= p25 p3)) (not (= p25 p4)) (not (= p25 p5)) (not (= p25 p6)) (not (= p25 p7)) (not (= p25 p8)) (not (= p25 p9)) (not (= p25 p10)) (not (= p25 p11)) (not (= p25 p12)) (not (= p25 p13)) (not (= p25 p14)) (not (= p25 p15)) (not (= p25 p16)) (not (= p25 p17)) (not (= p25 p18)) (not (= p25 p19)) (not (= p25 p20)) (not (= p25 p21)) (not (= p25 p22)) (not (= p25 p23)) (not (= p25 p24))) (and (not (= p26 p0)) (not (= p26 p1)) (not (= p26 p2)) (not (= p26 p3)) (not (= p26 p4)) (not (= p26 p5)) (not (= p26 p6)) (not (= p26 p7)) (not (= p26 p8)) (not (= p26 p9)) (not (= p26 p10)) (not (= p26 p11)) (not (= p26 p12)) (not (= p26 p13)) (not (= p26 p14)) (not (= p26 p15)) (not (= p26 p16)) (not (= p26 p17)) (not (= p26 p18)) (not (= p26 p19)) (not (= p26 p20)) (not (= p26 p21)) (not (= p26 p22)) (not (= p26 p23)) (not (= p26 p24)) (not (= p26 p25))) (and (not (= p27 p0)) (not (= p27 p1)) (not (= p27 p2)) (not (= p27 p3)) (not (= p27 p4)) (not (= p27 p5)) (not (= p27 p6)) (not (= p27 p7)) (not (= p27 p8)) (not (= p27 p9)) (not (= p27 p10)) (not (= p27 p11)) (not (= p27 p12)) (not (= p27 p13)) (not (= p27 p14)) (not (= p27 p15)) (not (= p27 p16)) (not (= p27 p17)) (not (= p27 p18)) (not (= p27 p19)) (not (= p27 p20)) (not (= p27 p21)) (not (= p27 p22)) (not (= p27 p23)) (not (= p27 p24)) (not (= p27 p25)) (not (= p27 p26))) (and (not (= p28 p0)) (not (= p28 p1)) (not (= p28 p2)) (not (= p28 p3)) (not (= p28 p4)) (not (= p28 p5)) (not (= p28 p6)) (not (= p28 p7)) (not (= p28 p8)) (not (= p28 p9)) (not (= p28 p10)) (not (= p28 p11)) (not (= p28 p12)) (not (= p28 p13)) (not (= p28 p14)) (not (= p28 p15)) (not (= p28 p16)) (not (= p28 p17)) (not (= p28 p18)) (not (= p28 p19)) (not (= p28 p20)) (not (= p28 p21)) (not (= p28 p22)) (not (= p28 p23)) (not (= p28 p24)) (not (= p28 p25)) (not (= p28 p26)) (not (= p28 p27))) (and (not (= p29 p0)) (not (= p29 p1)) (not (= p29 p2)) (not (= p29 p3)) (not (= p29 p4)) (not (= p29 p5)) (not (= p29 p6)) (not (= p29 p7)) (not (= p29 p8)) (not (= p29 p9)) (not (= p29 p10)) (not (= p29 p11)) (not (= p29 p12)) (not (= p29 p13)) (not (= p29 p14)) (not (= p29 p15)) (not (= p29 p16)) (not (= p29 p17)) (not (= p29 p18)) (not (= p29 p19)) (not (= p29 p20)) (not (= p29 p21)) (not (= p29 p22)) (not (= p29 p23)) (not (= p29 p24)) (not (= p29 p25)) (not (= p29 p26)) (not (= p29 p27)) (not (= p29 p28))) (and (not (= p30 p0)) (not (= p30 p1)) (not (= p30 p2)) (not (= p30 p3)) (not (= p30 p4)) (not (= p30 p5)) (not (= p30 p6)) (not (= p30 p7)) (not (= p30 p8)) (not (= p30 p9)) (not (= p30 p10)) (not (= p30 p11)) (not (= p30 p12)) (not (= p30 p13)) (not (= p30 p14)) (not (= p30 p15)) (not (= p30 p16)) (not (= p30 p17)) (not (= p30 p18)) (not (= p30 p19)) (not (= p30 p20)) (not (= p30 p21)) (not (= p30 p22)) (not (= p30 p23)) (not (= p30 p24)) (not (= p30 p25)) (not (= p30 p26)) (not (= p30 p27)) (not (= p30 p28)) (not (= p30 p29))) (and (not (= p31 p0)) (not (= p31 p1)) (not (= p31 p2)) (not (= p31 p3)) (not (= p31 p4)) (not (= p31 p5)) (not (= p31 p6)) (not (= p31 p7)) (not (= p31 p8)) (not (= p31 p9)) (not (= p31 p10)) (not (= p31 p11)) (not (= p31 p12)) (not (= p31 p13)) (not (= p31 p14)) (not (= p31 p15)) (not (= p31 p16)) (not (= p31 p17)) (not (= p31 p18)) (not (= p31 p19)) (not (= p31 p20)) (not (= p31 p21)) (not (= p31 p22)) (not (= p31 p23)) (not (= p31 p24)) (not (= p31 p25)) (not (= p31 p26)) (not (= p31 p27)) (not (= p31 p28)) (not (= p31 p29)) (not (= p31 p30))) (and (not (= p32 p0)) (not (= p32 p1)) (not (= p32 p2)) (not (= p32 p3)) (not (= p32 p4)) (not (= p32 p5)) (not (= p32 p6)) (not (= p32 p7)) (not (= p32 p8)) (not (= p32 p9)) (not (= p32 p10)) (not (= p32 p11)) (not (= p32 p12)) (not (= p32 p13)) (not (= p32 p14)) (not (= p32 p15)) (not (= p32 p16)) (not (= p32 p17)) (not (= p32 p18)) (not (= p32 p19)) (not (= p32 p20)) (not (= p32 p21)) (not (= p32 p22)) (not (= p32 p23)) (not (= p32 p24)) (not (= p32 p25)) (not (= p32 p26)) (not (= p32 p27)) (not (= p32 p28)) (not (= p32 p29)) (not (= p32 p30)) (not (= p32 p31))))) ; --------------- END (Loop free)------------------ (check-sat) (pop) (declare-const p33 (_ BitVec 52)) (assert (T p32 p33)) (echo "Is oscillation possible (k=33)?") (push) (assert (not (T p33 p33))) (check-sat) (pop) (get-info :all-statistics)