41 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true)))) |
41 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true)))) |
42 (let ((@x45 (monotonicity @x42 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true))))) |
42 (let ((@x45 (monotonicity @x42 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true))))) |
43 (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false)))) |
43 (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false)))) |
44 (mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false))))))) |
44 (mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false))))))) |
45 |
45 |
|
46 6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0 |
|
47 unsat |
|
48 ((set-logic <null>) |
|
49 (proof |
|
50 (let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true))))) |
|
51 (let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false)))) |
|
52 (mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false))))) |
|
53 |
46 45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0 |
54 45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0 |
47 unsat |
55 unsat |
48 ((set-logic <null>) |
56 ((set-logic <null>) |
49 (proof |
57 (proof |
50 (let ((@x43 (monotonicity (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8))) (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8)))))) |
58 (let ((@x43 (monotonicity (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8))) (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8)))))) |
51 (let ((@x47 (trans @x43 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true)))) |
59 (let ((@x47 (trans @x43 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true)))) |
52 (let ((@x50 (monotonicity @x47 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true))))) |
60 (let ((@x50 (monotonicity @x47 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true))))) |
53 (let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false)))) |
61 (let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false)))) |
54 (mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false))))))) |
62 (mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false))))))) |
55 |
|
56 6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0 |
|
57 unsat |
|
58 ((set-logic <null>) |
|
59 (proof |
|
60 (let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true))))) |
|
61 (let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false)))) |
|
62 (mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false))))) |
|
63 |
63 |
64 00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0 |
64 00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0 |
65 unsat |
65 unsat |
66 ((set-logic <null>) |
66 ((set-logic <null>) |
67 (proof |
67 (proof |
140 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true)))) |
140 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true)))) |
141 (let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true))))) |
141 (let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true))))) |
142 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false)))) |
142 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false)))) |
143 (mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false))))))) |
143 (mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false))))))) |
144 |
144 |
145 3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0 |
|
146 unsat |
|
147 ((set-logic <null>) |
|
148 (proof |
|
149 (let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16)))))) |
|
150 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true)))) |
|
151 (let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false)))) |
|
152 (mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false)))))) |
|
153 |
|
154 14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0 |
145 14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0 |
155 unsat |
146 unsat |
156 ((set-logic <null>) |
147 ((set-logic <null>) |
157 (proof |
148 (proof |
158 (let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12)))))) |
149 (let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12)))))) |
159 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true)))) |
150 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true)))) |
160 (let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true))))) |
151 (let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true))))) |
161 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false)))) |
152 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false)))) |
162 (mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false))))))) |
153 (mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false))))))) |
163 |
154 |
|
155 3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0 |
|
156 unsat |
|
157 ((set-logic <null>) |
|
158 (proof |
|
159 (let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16)))))) |
|
160 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true)))) |
|
161 (let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false)))) |
|
162 (mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false)))))) |
|
163 |
|
164 8d29c9b5ef712a3d9d2db87383c9c25c0b553e01 8 0 |
|
165 unsat |
|
166 ((set-logic <null>) |
|
167 (proof |
|
168 (let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2)))))) |
|
169 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true)))) |
|
170 (let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false)))) |
|
171 (mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false)))))) |
|
172 |
164 880bee16a8f6469b14122277b92e87533ef6a071 9 0 |
173 880bee16a8f6469b14122277b92e87533ef6a071 9 0 |
165 unsat |
174 unsat |
166 ((set-logic <null>) |
175 ((set-logic <null>) |
167 (proof |
176 (proof |
168 (let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10)))))) |
177 (let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10)))))) |
169 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true)))) |
178 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true)))) |
170 (let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true))))) |
179 (let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true))))) |
171 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false)))) |
180 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false)))) |
172 (mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false))))))) |
181 (mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false))))))) |
173 |
182 |
174 6b4cf44be412b1ba63dbf9b301260e877097b1be 8 0 |
|
175 unsat |
|
176 ((set-logic <null>) |
|
177 (proof |
|
178 (let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2)))))) |
|
179 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true)))) |
|
180 (let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false)))) |
|
181 (mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false)))))) |
|
182 |
|
183 446b3cb9d63aa1f488dc092ed3fb111d2ad50b4e 9 0 |
183 446b3cb9d63aa1f488dc092ed3fb111d2ad50b4e 9 0 |
184 unsat |
184 unsat |
185 ((set-logic <null>) |
185 ((set-logic <null>) |
186 (proof |
186 (proof |
187 (let ((@x36 (monotonicity (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) (= (_ bv10 10) (_ bv10 10)))))) |
187 (let ((@x36 (monotonicity (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) (= (_ bv10 10) (_ bv10 10)))))) |
198 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true)))) |
198 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true)))) |
199 (let ((@x43 (monotonicity @x40 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true))))) |
199 (let ((@x43 (monotonicity @x40 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true))))) |
200 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false)))) |
200 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false)))) |
201 (mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x47 false))))))) |
201 (mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x47 false))))))) |
202 |
202 |
203 7a821bfbd2032abe40931e46e7875c58d78cac74 9 0 |
203 8e075e24ee51b2c8d282203ef406cf993a4d32e8 9 0 |
204 unsat |
204 unsat |
205 ((set-logic <null>) |
205 ((set-logic <null>) |
206 (proof |
206 (proof |
207 (let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8)))))) |
207 (let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8)))))) |
208 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true)))) |
208 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true)))) |
209 (let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true))))) |
209 (let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true))))) |
210 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false)))) |
210 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false)))) |
211 (mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false))))))) |
211 (mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false))))))) |
212 |
212 |
213 3a90f9cf3517f16b198f07da78a10c267f6ca981 9 0 |
213 e11f6641dec327aa96166093ca6eb62aa10965c0 9 0 |
214 unsat |
214 unsat |
215 ((set-logic <null>) |
215 ((set-logic <null>) |
216 (proof |
216 (proof |
217 (let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8)))))) |
217 (let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8)))))) |
218 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true)))) |
218 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true)))) |
219 (let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true))))) |
219 (let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true))))) |
220 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false)))) |
220 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false)))) |
221 (mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false))))))) |
221 (mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false))))))) |
222 |
222 |
223 512889429971c22172b835746742cd1214354685 9 0 |
223 f1f29c69ebfcb6af36e96ba5a738d9b0d7b31835 9 0 |
224 unsat |
224 unsat |
225 ((set-logic <null>) |
225 ((set-logic <null>) |
226 (proof |
226 (proof |
227 (let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8)))))) |
227 (let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8)))))) |
228 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true)))) |
228 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true)))) |
229 (let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true))))) |
229 (let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true))))) |
230 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false)))) |
230 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false)))) |
231 (mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false))))))) |
231 (mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false))))))) |
232 |
232 |
233 85eb639dc934d6e3f29fcc025e09dac5e8ec35be 9 0 |
233 d5599ccc28266367053026b485d411472eb0665c 9 0 |
234 unsat |
234 unsat |
235 ((set-logic <null>) |
235 ((set-logic <null>) |
236 (proof |
236 (proof |
237 (let ((@x36 (monotonicity (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) (= (_ bv9 4) (_ bv9 4)))))) |
237 (let ((@x36 (monotonicity (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) (= (_ bv9 4) (_ bv9 4)))))) |
238 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) true)))) |
238 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) true)))) |
239 (let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (not true))))) |
239 (let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (not true))))) |
240 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false)))) |
240 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false)))) |
241 (mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false))))))) |
241 (mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false))))))) |
242 |
|
243 072b118d30c575706ced09a142498447b46fa41f 9 0 |
|
244 unsat |
|
245 ((set-logic <null>) |
|
246 (proof |
|
247 (let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4)))))) |
|
248 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true)))) |
|
249 (let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true))))) |
|
250 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false)))) |
|
251 (mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false))))))) |
|
252 |
242 |
253 5c4e275bed2d91897e820ccd6744b0a775a6e26e 17 0 |
243 5c4e275bed2d91897e820ccd6744b0a775a6e26e 17 0 |
254 unsat |
244 unsat |
255 ((set-logic <null>) |
245 ((set-logic <null>) |
256 (proof |
246 (proof |
265 (let (($x52 (= x$ ?x32))) |
255 (let (($x52 (= x$ ?x32))) |
266 (let ((@x26 (true-axiom true))) |
256 (let ((@x26 (true-axiom true))) |
267 (let (($x53 (or $x52 false false false false false false false false false false false false false false false false))) |
257 (let (($x53 (or $x52 false false false false false false false false false false false false false false false false))) |
268 (let ((@x55 (unit-resolution ((_ th-lemma bv) $x53) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 $x52))) |
258 (let ((@x55 (unit-resolution ((_ th-lemma bv) $x53) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 $x52))) |
269 (unit-resolution @x55 @x63 false))))))))))))))) |
259 (unit-resolution @x55 @x63 false))))))))))))))) |
|
260 |
|
261 33a52e620069e1ecebbc00aa6b0099170558c111 9 0 |
|
262 unsat |
|
263 ((set-logic <null>) |
|
264 (proof |
|
265 (let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4)))))) |
|
266 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true)))) |
|
267 (let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true))))) |
|
268 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false)))) |
|
269 (mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false))))))) |
|
270 |
|
271 115ab22c9945d493b971e69a38d9e608c5b40a71 29 0 |
|
272 unsat |
|
273 ((set-logic <null>) |
|
274 (proof |
|
275 (let ((?x28 (bv2int$ (_ bv0 2)))) |
|
276 (let (($x183 (<= ?x28 0))) |
|
277 (let (($x184 (not $x183))) |
|
278 (let (($x175 (forall ((?v0 (_ BitVec 2)) )(!(let ((?x47 (bv2int$ ?v0))) |
|
279 (let (($x53 (<= ?x47 0))) |
|
280 (not $x53))) :pattern ( (bv2int$ ?v0) ))) |
|
281 )) |
|
282 (let (($x57 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0))) |
|
283 (let (($x53 (<= ?x47 0))) |
|
284 (not $x53)))) |
|
285 )) |
|
286 (let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) |
|
287 (let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) |
|
288 (let (($x49 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0))) |
|
289 (< 0 ?x47))) |
|
290 )) |
|
291 (let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0)))))) |
|
292 (let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57))) |
|
293 (let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175))) |
|
294 (let (($x187 (not $x175))) |
|
295 (let (($x188 (or $x187 $x184))) |
|
296 (let ((@x189 ((_ quant-inst (_ bv0 2)) $x188))) |
|
297 (let (($x29 (= ?x28 0))) |
|
298 (let ((@x30 (asserted $x29))) |
|
299 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false))))))))))))))))))) |
270 |
300 |
271 1d4a0e2a4449a8adbcf5a134bf7f2b0ee940d954 51 0 |
301 1d4a0e2a4449a8adbcf5a134bf7f2b0ee940d954 51 0 |
272 unsat |
302 unsat |
273 ((set-logic <null>) |
303 ((set-logic <null>) |
274 (proof |
304 (proof |
318 (let ((@x26 (true-axiom true))) |
348 (let ((@x26 (true-axiom true))) |
319 (let (($x312 (or $x300 false false false false false false false false $x74 $x75 $x76 $x77 $x78 $x79 $x80 $x81))) |
349 (let (($x312 (or $x300 false false false false false false false false $x74 $x75 $x76 $x77 $x78 $x79 $x80 $x81))) |
320 (let ((@x314 (unit-resolution ((_ th-lemma bv) $x312) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 (unit-resolution (def-axiom (or $x95 (not $x74))) @x303 (not $x74)) (unit-resolution (def-axiom (or $x95 (not $x75))) @x303 (not $x75)) (unit-resolution (def-axiom (or $x95 (not $x76))) @x303 (not $x76)) (unit-resolution (def-axiom (or $x95 (not $x77))) @x303 (not $x77)) (unit-resolution (def-axiom (or $x95 (not $x78))) @x303 (not $x78)) (unit-resolution (def-axiom (or $x95 (not $x79))) @x303 (not $x79)) (unit-resolution (def-axiom (or $x95 (not $x80))) @x303 (not $x80)) (unit-resolution (def-axiom (or $x95 $x264)) @x303 $x264) $x300))) |
350 (let ((@x314 (unit-resolution ((_ th-lemma bv) $x312) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 (unit-resolution (def-axiom (or $x95 (not $x74))) @x303 (not $x74)) (unit-resolution (def-axiom (or $x95 (not $x75))) @x303 (not $x75)) (unit-resolution (def-axiom (or $x95 (not $x76))) @x303 (not $x76)) (unit-resolution (def-axiom (or $x95 (not $x77))) @x303 (not $x77)) (unit-resolution (def-axiom (or $x95 (not $x78))) @x303 (not $x78)) (unit-resolution (def-axiom (or $x95 (not $x79))) @x303 (not $x79)) (unit-resolution (def-axiom (or $x95 (not $x80))) @x303 (not $x80)) (unit-resolution (def-axiom (or $x95 $x264)) @x303 $x264) $x300))) |
321 (unit-resolution @x314 @x322 false))))))))))))))))))))))))))))))))))))))))))))))))) |
351 (unit-resolution @x314 @x322 false))))))))))))))))))))))))))))))))))))))))))))))))) |
322 |
352 |
323 115ab22c9945d493b971e69a38d9e608c5b40a71 29 0 |
|
324 unsat |
|
325 ((set-logic <null>) |
|
326 (proof |
|
327 (let ((?x28 (bv2int$ (_ bv0 2)))) |
|
328 (let (($x183 (<= ?x28 0))) |
|
329 (let (($x184 (not $x183))) |
|
330 (let (($x175 (forall ((?v0 (_ BitVec 2)) )(!(let ((?x47 (bv2int$ ?v0))) |
|
331 (let (($x53 (<= ?x47 0))) |
|
332 (not $x53))) :pattern ( (bv2int$ ?v0) ))) |
|
333 )) |
|
334 (let (($x57 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0))) |
|
335 (let (($x53 (<= ?x47 0))) |
|
336 (not $x53)))) |
|
337 )) |
|
338 (let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) |
|
339 (let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0)))))) |
|
340 (let (($x49 (forall ((?v0 (_ BitVec 2)) )(let ((?x47 (bv2int$ ?v0))) |
|
341 (< 0 ?x47))) |
|
342 )) |
|
343 (let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0)))))) |
|
344 (let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57))) |
|
345 (let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175))) |
|
346 (let (($x187 (not $x175))) |
|
347 (let (($x188 (or $x187 $x184))) |
|
348 (let ((@x189 ((_ quant-inst (_ bv0 2)) $x188))) |
|
349 (let (($x29 (= ?x28 0))) |
|
350 (let ((@x30 (asserted $x29))) |
|
351 (unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false))))))))))))))))))) |
|
352 |
|
353 d14e7b8f0d1858316e700b4eb09e7d03e57cf9c3 16 0 |
353 d14e7b8f0d1858316e700b4eb09e7d03e57cf9c3 16 0 |
354 unsat |
354 unsat |
355 ((set-logic <null>) |
355 ((set-logic <null>) |
356 (proof |
356 (proof |
357 (let ((?x32 (p$ true))) |
357 (let ((?x32 (p$ true))) |