(set-option :produce-models true) (set-option :pull-nested-quantifiers true) (set-option :mbqi true) (declare-const x (_ BitVec 23)) (declare-const y (_ BitVec 23)) (declare-const xs (_ BitVec 23)) ; --- Parsed BLIF network from Z:\Projects\Z3 4Biology\Code\v0.1\models\thelper.cnet-------- (declare-fun T ((_ BitVec 23) (_ BitVec 23) ) bool) ; -------------- Transition Relation: ----------------- (assert (forall ((x (_ BitVec 23)) (y (_ BitVec 23)) )(= (T x y) (and (or (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (or false)) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (or (and (= ((_ extract 0 0) x) (_ bv1 1))))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (or false)) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (or (and (= ((_ extract 2 2) x) (_ bv1 1))))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (or false)) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (or (and (= ((_ extract 4 4) x) (_ bv1 1)) (not (= ((_ extract 18 18) x) (_ bv1 1)))))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (or (and (= ((_ extract 5 5) x) (_ bv1 1))))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (or (and (= ((_ extract 15 15) x) (_ bv1 1))) (and (= ((_ extract 11 11) x) (_ bv1 1))))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (or false)) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (or (and (= ((_ extract 8 8) x) (_ bv1 1)) (not (= ((_ extract 18 18) x) (_ bv1 1)))))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (or (and (= ((_ extract 9 9) x) (_ bv1 1)) (not (= ((_ extract 19 19) x) (_ bv1 1)))))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (or (and (= ((_ extract 15 15) x) (_ bv1 1)) (not (= ((_ extract 19 19) x) (_ bv1 1)))) (and (= ((_ extract 11 11) x) (_ bv1 1)) (not (= ((_ extract 19 19) x) (_ bv1 1)))))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (or (and (= ((_ extract 11 11) x) (_ bv1 1)) (not (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= ((_ extract 10 10) x) (_ bv1 1)) (not (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= ((_ extract 6 6) x) (_ bv1 1)) (not (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= ((_ extract 1 1) x) (_ bv1 1)) (not (= ((_ extract 22 22) x) (_ bv1 1)))))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (or (and (= ((_ extract 12 12) x) (_ bv1 1))))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (or (and (= ((_ extract 13 13) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1)))))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (or (and (= ((_ extract 14 14) x) (_ bv1 1))) (and (= ((_ extract 3 3) x) (_ bv1 1))))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (or (and (= ((_ extract 19 19) x) (_ bv1 1)) (not (= ((_ extract 15 15) x) (_ bv1 1)))))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (or (and (= ((_ extract 16 16) x) (_ bv1 1)) (not (= ((_ extract 7 7) x) (_ bv1 1)))))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (or (and (= ((_ extract 17 17) x) (_ bv1 1))))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (or (and (= ((_ extract 19 19) x) (_ bv1 1)) (not (= ((_ extract 11 11) x) (_ bv1 1)))) (and (= ((_ extract 18 18) x) (_ bv1 1)) (not (= ((_ extract 11 11) x) (_ bv1 1)))))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (or (and (= ((_ extract 19 19) x) (_ bv1 1))))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (or (and (= ((_ extract 20 20) x) (_ bv1 1))))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (= ((_ extract 22 22) x) (_ bv1 1)))) (and (= (= ((_ extract 0 0) y) (_ bv1 1)) (= ((_ extract 0 0) x) (_ bv1 1))) (= (= ((_ extract 1 1) y) (_ bv1 1)) (= ((_ extract 1 1) x) (_ bv1 1))) (= (= ((_ extract 2 2) y) (_ bv1 1)) (= ((_ extract 2 2) x) (_ bv1 1))) (= (= ((_ extract 3 3) y) (_ bv1 1)) (= ((_ extract 3 3) x) (_ bv1 1))) (= (= ((_ extract 4 4) y) (_ bv1 1)) (= ((_ extract 4 4) x) (_ bv1 1))) (= (= ((_ extract 5 5) y) (_ bv1 1)) (= ((_ extract 5 5) x) (_ bv1 1))) (= (= ((_ extract 6 6) y) (_ bv1 1)) (= ((_ extract 6 6) x) (_ bv1 1))) (= (= ((_ extract 7 7) y) (_ bv1 1)) (= ((_ extract 7 7) x) (_ bv1 1))) (= (= ((_ extract 8 8) y) (_ bv1 1)) (= ((_ extract 8 8) x) (_ bv1 1))) (= (= ((_ extract 9 9) y) (_ bv1 1)) (= ((_ extract 9 9) x) (_ bv1 1))) (= (= ((_ extract 10 10) y) (_ bv1 1)) (= ((_ extract 10 10) x) (_ bv1 1))) (= (= ((_ extract 11 11) y) (_ bv1 1)) (= ((_ extract 11 11) x) (_ bv1 1))) (= (= ((_ extract 12 12) y) (_ bv1 1)) (= ((_ extract 12 12) x) (_ bv1 1))) (= (= ((_ extract 13 13) y) (_ bv1 1)) (= ((_ extract 13 13) x) (_ bv1 1))) (= (= ((_ extract 14 14) y) (_ bv1 1)) (= ((_ extract 14 14) x) (_ bv1 1))) (= (= ((_ extract 15 15) y) (_ bv1 1)) (= ((_ extract 15 15) x) (_ bv1 1))) (= (= ((_ extract 16 16) y) (_ bv1 1)) (= ((_ extract 16 16) x) (_ bv1 1))) (= (= ((_ extract 17 17) y) (_ bv1 1)) (= ((_ extract 17 17) x) (_ bv1 1))) (= (= ((_ extract 18 18) y) (_ bv1 1)) (= ((_ extract 18 18) x) (_ bv1 1))) (= (= ((_ extract 19 19) y) (_ bv1 1)) (= ((_ extract 19 19) x) (_ bv1 1))) (= (= ((_ extract 20 20) y) (_ bv1 1)) (= ((_ extract 20 20) x) (_ bv1 1))) (= (= ((_ extract 21 21) y) (_ bv1 1)) (= ((_ extract 21 21) x) (_ bv1 1))) (= (= ((_ extract 22 22) y) (_ bv1 1)) (or (and (= ((_ extract 21 21) x) (_ bv1 1))))))))))) ; ------------------ END ------------------------------ (get-info :all-statistics)