(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 6))
(declare-fun v1 () (_ BitVec 5))
(assert (let ((e2(_ bv81 7)))
(let ((e3(_ bv46 8)))
(let ((e4 ((_ sign_extend 2) v1)))
(let ((e5 (bvsrem e4 e2)))
(let ((e6 ((_ extract 0 0) e3)))
(let ((e7 (bvneg e4)))
(let ((e8 (bvadd e7 e7)))
(let ((e9 (bvurem e2 e2)))
(let ((e10 (bvxnor ((_ sign_extend 6) e6) e8)))
(let ((e11 (bvmul e7 e9)))
(let ((e12 (ite (bvuge e3 ((_ zero_extend 1) e4)) (_ bv1 1) (_ bv0 1))))
(let ((e13 ((_ zero_extend 1) e8)))
(let ((e14 (bvnand e10 e8)))
(let ((e15 (bvsub e10 e8)))
(let ((e16 (bvudiv ((_ zero_extend 1) e4) e13)))
(let ((e17 (bvnor e10 e14)))
(let ((e18 (bvsdiv e11 e10)))
(let ((e19 (ite (bvsge e14 ((_ sign_extend 2) v1)) (_ bv1 1) (_ bv0 1))))
(let ((e20 (ite (bvslt e13 ((_ zero_extend 1) e5)) (_ bv1 1) (_ bv0 1))))
(let ((e21 (bvsrem ((_ zero_extend 6) e20) e15)))
(let ((e22 (ite (bvugt e5 ((_ zero_extend 2) v1)) (_ bv1 1) (_ bv0 1))))
(let ((e23 (bvmul e14 e9)))
(let ((e24 (ite (bvult e8 e23) (_ bv1 1) (_ bv0 1))))
(let ((e25 (ite (distinct e14 e17) (_ bv1 1) (_ bv0 1))))
(let ((e26 (bvnand ((_ zero_extend 1) e2) e16)))
(let ((e27 ((_ extract 4 3) e9)))
(let ((e28 (ite (bvugt ((_ sign_extend 6) e6) e15) (_ bv1 1) (_ bv0 1))))
(let ((e29 (ite (= ((_ sign_extend 6) e12) e14) (_ bv1 1) (_ bv0 1))))
(let ((e30 (ite (bvule e18 e18) (_ bv1 1) (_ bv0 1))))
(let ((e31 (ite (bvsle e10 ((_ sign_extend 6) e22)) (_ bv1 1) (_ bv0 1))))
(let ((e32 (bvnor e24 e6)))
(let ((e33 (bvor ((_ zero_extend 2) v1) e2)))
(let ((e34 (bvor ((_ sign_extend 5) e25) v0)))
(let ((e35 (bvslt ((_ zero_extend 6) e28) e23)))
(let ((e36 (bvule e21 ((_ sign_extend 6) e22))))
(let ((e37 (bvule ((_ sign_extend 6) e19) e15)))
(let ((e38 (bvsgt e21 ((_ zero_extend 6) e32))))
(let ((e39 (bvsge ((_ sign_extend 6) e25) e15)))
(let ((e40 (= ((_ sign_extend 4) e24) v1)))
(let ((e41 (bvule ((_ zero_extend 7) e24) e16)))
(let ((e42 (distinct e4 ((_ zero_extend 2) v1))))
(let ((e43 (bvslt e16 e26)))
(let ((e44 (= e17 ((_ zero_extend 2) v1))))
(let ((e45 (bvugt ((_ zero_extend 6) e12) e14)))
(let ((e46 (distinct ((_ zero_extend 5) e27) e10)))
(let ((e47 (bvsge e23 e15)))
(let ((e48 (bvult e23 ((_ sign_extend 6) e29))))
(let ((e49 (distinct e7 ((_ sign_extend 6) e22))))
(let ((e50 (bvslt ((_ sign_extend 6) e28) e2)))
(let ((e51 (bvugt v0 ((_ zero_extend 5) e20))))
(let ((e52 (= e15 e4)))
(let ((e53 (bvult e2 e7)))
(let ((e54 (bvuge e4 e5)))
(let ((e55 (bvugt e14 e11)))
(let ((e56 (bvsle e5 ((_ zero_extend 6) e31))))
(let ((e57 (distinct e15 e11)))
(let ((e58 (bvsgt ((_ sign_extend 6) e25) e33)))
(let ((e59 (bvuge e14 e23)))
(let ((e60 (bvsge e4 ((_ zero_extend 5) e27))))
(let ((e61 (bvugt ((_ sign_extend 6) e32) e4)))
(let ((e62 (bvugt ((_ zero_extend 6) e22) e21)))
(let ((e63 (bvslt e22 e30)))
(let ((e64 (distinct ((_ zero_extend 6) e24) e8)))
(let ((e65 (bvugt e3 ((_ zero_extend 1) e23))))
(let ((e66 (bvult ((_ zero_extend 1) e14) e16)))
(let ((e67 (bvslt e26 ((_ zero_extend 7) e6))))
(let ((e68 (bvule ((_ sign_extend 5) e22) v0)))
(let ((e69 (= ((_ sign_extend 5) e6) e34)))
(let ((e70 (bvsgt e8 e9)))
(let ((e71 (distinct e2 e23)))
(let ((e72 (bvsle ((_ sign_extend 6) e12) e9)))
(let ((e73 (bvsle e26 ((_ sign_extend 7) e30))))
(let ((e74 (bvugt e8 ((_ zero_extend 6) e12))))
(let ((e75 (distinct ((_ zero_extend 1) e34) e15)))
(let ((e76 (= e13 e16)))
(let ((e77 (distinct e11 e7)))
(let ((e78 (bvule v0 ((_ zero_extend 5) e29))))
(let ((e79 (bvule e21 ((_ sign_extend 6) e29))))
(let ((e80 (bvsge e11 ((_ zero_extend 6) e25))))
(let ((e81 (bvsle e4 ((_ sign_extend 6) e24))))
(let ((e82 (bvuge e11 ((_ zero_extend 6) e22))))
(let ((e83 (bvsle ((_ zero_extend 6) e31) e4)))
(let ((e84 (= e10 ((_ zero_extend 6) e6))))
(let ((e85 (bvslt ((_ sign_extend 6) e22) e17)))
(let ((e86 (bvult ((_ sign_extend 6) e30) e33)))
(let ((e87 (distinct ((_ zero_extend 6) e25) e14)))
(let ((e88 (bvsge v0 ((_ sign_extend 5) e6))))
(let ((e89 (bvsle ((_ zero_extend 2) v1) e2)))
(let ((e90 (bvuge e33 e9)))
(let ((e91 (bvuge ((_ sign_extend 6) e28) e10)))
(let ((e92 (bvsgt e29 e29)))
(let ((e93 (= e11 e14)))
(let ((e94 (bvult e16 e3)))
(let ((e95 (bvult e9 e7)))
(let ((e96 (distinct ((_ zero_extend 6) e6) e14)))
(let ((e97 (= e23 e11)))
(let ((e98 (bvugt e4 e4)))
(let ((e99 (bvsle ((_ sign_extend 6) e31) e17)))
(let ((e100 (bvsle e30 e28)))
(let ((e101 (bvsge e10 e8)))
(let ((e102 (bvslt e9 ((_ sign_extend 2) v1))))
(let ((e103 (bvsle ((_ sign_extend 1) e15) e16)))
(let ((e104 (bvuge e17 ((_ zero_extend 6) e30))))
(let ((e105 (bvult ((_ zero_extend 6) e12) e10)))
(let ((e106 (bvslt ((_ zero_extend 2) v0) e3)))
(let ((e107 (bvuge e13 ((_ zero_extend 2) v0))))
(let ((e108 (bvsle e33 ((_ sign_extend 6) e32))))
(let ((e109 (bvult e14 ((_ zero_extend 6) e12))))
(let ((e110 (bvslt e11 e14)))
(let ((e111 (bvugt e6 e32)))
(let ((e112 (bvsgt e8 ((_ zero_extend 6) e31))))
(let ((e113 (bvule ((_ zero_extend 2) v0) e26)))
(let ((e114 (bvslt ((_ zero_extend 6) e24) e7)))
(let ((e115 (bvslt e2 ((_ sign_extend 6) e19))))
(let ((e116 (bvslt e24 e20)))
(let ((e117 (bvugt ((_ zero_extend 5) e31) v0)))
(let ((e118 (bvult e23 ((_ zero_extend 6) e29))))
(let ((e119 (bvule e6 e24)))
(let ((e120 (bvugt e15 ((_ sign_extend 6) e25))))
(let ((e121 (bvsgt ((_ zero_extend 1) e6) e27)))
(let ((e122 (bvsgt e25 e19)))
(let ((e123 (= e32 e19)))
(let ((e124 (bvult e4 ((_ zero_extend 6) e29))))
(let ((e125 (bvslt ((_ sign_extend 1) e28) e27)))
(let ((e126 (bvuge e4 e18)))
(let ((e127 (= e117 e98)))
(let ((e128 (xor e125 e94)))
(let ((e129 (=> e122 e70)))
(let ((e130 (or e62 e83)))
(let ((e131 (=> e116 e64)))
(let ((e132 (ite e91 e58 e95)))
(let ((e133 (= e85 e92)))
(let ((e134 (and e86 e87)))
(let ((e135 (ite e48 e134 e73)))
(let ((e136 (or e74 e35)))
(let ((e137 (xor e36 e115)))
(let ((e138 (and e55 e39)))
(let ((e139 (not e47)))
(let ((e140 (=> e112 e130)))
(let ((e141 (=> e139 e42)))
(let ((e142 (or e140 e49)))
(let ((e143 (or e66 e99)))
(let ((e144 (=> e119 e38)))
(let ((e145 (=> e138 e137)))
(let ((e146 (and e43 e126)))
(let ((e147 (= e101 e101)))
(let ((e148 (not e107)))
(let ((e149 (and e97 e77)))
(let ((e150 (or e100 e133)))
(let ((e151 (not e51)))
(let ((e152 (=> e143 e124)))
(let ((e153 (xor e109 e46)))
(let ((e154 (or e52 e50)))
(let ((e155 (xor e150 e120)))
(let ((e156 (=> e142 e65)))
(let ((e157 (and e144 e110)))
(let ((e158 (ite e108 e146 e57)))
(let ((e159 (= e151 e88)))
(let ((e160 (or e78 e131)))
(let ((e161 (=> e121 e44)))
(let ((e162 (xor e155 e154)))
(let ((e163 (and e156 e160)))
(let ((e164 (= e82 e145)))
(let ((e165 (= e45 e136)))
(let ((e166 (ite e61 e114 e61)))
(let ((e167 (or e53 e123)))
(let ((e168 (not e105)))
(let ((e169 (or e148 e166)))
(let ((e170 (= e72 e161)))
(let ((e171 (=> e96 e96)))
(let ((e172 (xor e90 e37)))
(let ((e173 (or e89 e153)))
(let ((e174 (= e67 e164)))
(let ((e175 (ite e69 e111 e171)))
(let ((e176 (not e129)))
(let ((e177 (or e103 e173)))
(let ((e178 (and e41 e147)))
(let ((e179 (=> e106 e167)))
(let ((e180 (=> e179 e162)))
(let ((e181 (not e175)))
(let ((e182 (=> e181 e127)))
(let ((e183 (= e163 e102)))
(let ((e184 (ite e169 e152 e176)))
(let ((e185 (and e76 e180)))
(let ((e186 (not e56)))
(let ((e187 (= e186 e113)))
(let ((e188 (and e40 e172)))
(let ((e189 (=> e63 e80)))
(let ((e190 (= e84 e81)))
(let ((e191 (xor e60 e71)))
(let ((e192 (and e118 e174)))
(let ((e193 (xor e54 e132)))
(let ((e194 (xor e75 e190)))
(let ((e195 (ite e178 e184 e68)))
(let ((e196 (and e183 e104)))
(let ((e197 (ite e195 e128 e141)))
(let ((e198 (or e188 e135)))
(let ((e199 (xor e93 e192)))
(let ((e200 (not e59)))
(let ((e201 (=> e79 e157)))
(let ((e202 (not e191)))
(let ((e203 (or e182 e197)))
(let ((e204 (not e168)))
(let ((e205 (and e159 e196)))
(let ((e206 (and e193 e177)))
(let ((e207 (and e199 e198)))
(let ((e208 (and e202 e203)))
(let ((e209 (xor e170 e194)))
(let ((e210 (= e206 e204)))
(let ((e211 (= e149 e208)))
(let ((e212 (not e158)))
(let ((e213 (xor e189 e189)))
(let ((e214 (and e165 e209)))
(let ((e215 (=> e210 e200)))
(let ((e216 (ite e212 e201 e185)))
(let ((e217 (not e187)))
(let ((e218 (not e207)))
(let ((e219 (and e216 e213)))
(let ((e220 (xor e217 e219)))
(let ((e221 (or e211 e218)))
(let ((e222 (ite e215 e205 e214)))
(let ((e223 (= e221 e220)))
(let ((e224 (xor e222 e222)))
(let ((e225 (= e223 e224)))
(let ((e226 (and e225 (not (= e2 (_ bv0 7))))))
(let ((e227 (and e226 (not (= e2 (bvnot (_ bv0 7)))))))
(let ((e228 (and e227 (not (= e10 (_ bv0 7))))))
(let ((e229 (and e228 (not (= e10 (bvnot (_ bv0 7)))))))
(let ((e230 (and e229 (not (= e15 (_ bv0 7))))))
(let ((e231 (and e230 (not (= e15 (bvnot (_ bv0 7)))))))
(let ((e232 (and e231 (not (= e13 (_ bv0 8))))))
e232
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)