|
1 8e6fd56de8adc20c29f4bdb8c2c55e63988185a8 8 0 |
|
2 unsat |
|
3 ((set-logic <null>) |
|
4 (proof |
|
5 (let ((@x38 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4)))))) |
|
6 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true)))) |
|
7 (let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false)))) |
|
8 (mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false)))))) |
|
9 |
|
10 aa1cdd144e99278cb2bdb51d68a75ec8d25b433d 7 0 |
|
11 unsat |
|
12 ((set-logic <null>) |
|
13 (proof |
|
14 (let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true))))) |
|
15 (let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false)))) |
|
16 (mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false))))) |
|
17 |
|
18 a14afea8a52a1586ff44eff03b88f1717144d17a 7 0 |
|
19 unsat |
|
20 ((set-logic <null>) |
|
21 (proof |
|
22 (let ((@x38 (monotonicity (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) true)) (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true))))) |
|
23 (let ((@x42 (trans @x38 (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false)))) |
|
24 (mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x42 false))))) |
|
25 |
|
26 282d94be68c87485ea9ec13e80f6f2a51b18f5bd 9 0 |
|
27 unsat |
|
28 ((set-logic <null>) |
|
29 (proof |
|
30 (let ((@x38 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5)))))) |
|
31 (let ((@x42 (trans @x38 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true)))) |
|
32 (let ((@x45 (monotonicity @x42 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true))))) |
|
33 (let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false)))) |
|
34 (mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x49 false))))))) |
|
35 |
|
36 4df99826f79b2c96079a4c58ea51a58b8cc6199c 9 0 |
|
37 unsat |
|
38 ((set-logic <null>) |
|
39 (proof |
|
40 (let ((@x38 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8)))))) |
|
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))))) |
|
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))))))) |
|
45 |
|
46 45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0 |
|
47 unsat |
|
48 ((set-logic <null>) |
|
49 (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)))))) |
|
51 (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))))) |
|
53 (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))))))) |
|
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 |
|
64 00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0 |
|
65 unsat |
|
66 ((set-logic <null>) |
|
67 (proof |
|
68 (let ((@x42 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7)))))) |
|
69 (let ((@x47 (trans @x42 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7))))) |
|
70 (let ((@x52 (monotonicity @x47 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7)))))) |
|
71 (let ((@x56 (trans @x52 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true)))) |
|
72 (let ((@x59 (monotonicity @x56 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true))))) |
|
73 (let ((@x63 (trans @x59 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false)))) |
|
74 (mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x63 false))))))))) |
|
75 |
|
76 9673ca576ccae343db48aa68f876fd3a2515cc33 19 0 |
|
77 unsat |
|
78 ((set-logic <null>) |
|
79 (proof |
|
80 (let ((?x35 (bvadd b$ c$))) |
|
81 (let ((?x36 (bvadd ?x35 a$))) |
|
82 (let ((?x30 (bvmul (_ bv2 32) b$))) |
|
83 (let ((?x31 (bvadd a$ ?x30))) |
|
84 (let ((?x33 (bvadd ?x31 c$))) |
|
85 (let ((?x34 (bvsub ?x33 b$))) |
|
86 (let (($x37 (= ?x34 ?x36))) |
|
87 (let (($x38 (not $x37))) |
|
88 (let ((@x58 (rewrite (= (= (bvadd a$ b$ c$) (bvadd a$ b$ c$)) true)))) |
|
89 (let ((@x48 (rewrite (= (bvsub (bvadd a$ ?x30 c$) b$) (bvadd a$ b$ c$))))) |
|
90 (let ((@x46 (monotonicity (rewrite (= ?x33 (bvadd a$ ?x30 c$))) (= ?x34 (bvsub (bvadd a$ ?x30 c$) b$))))) |
|
91 (let ((@x56 (monotonicity (trans @x46 @x48 (= ?x34 (bvadd a$ b$ c$))) (rewrite (= ?x36 (bvadd a$ b$ c$))) (= $x37 (= (bvadd a$ b$ c$) (bvadd a$ b$ c$)))))) |
|
92 (let ((@x63 (monotonicity (trans @x56 @x58 (= $x37 true)) (= $x38 (not true))))) |
|
93 (let ((@x67 (trans @x63 (rewrite (= (not true) false)) (= $x38 false)))) |
|
94 (mp (asserted $x38) @x67 false))))))))))))))))) |
|
95 |
|
96 b4600e6d14c88b633ac7bcc5b2e24af8539b0218 18 0 |
|
97 unsat |
|
98 ((set-logic <null>) |
|
99 (proof |
|
100 (let ((?x31 (bvmul (_ bv4 4) x$))) |
|
101 (let (($x32 (= ?x31 (_ bv4 4)))) |
|
102 (let (($x43 (= (_ bv5 4) x$))) |
|
103 (let (($x56 (not (or (not $x43) (= (_ bv4 4) ?x31))))) |
|
104 (let ((@x48 (monotonicity (rewrite (= (= x$ (_ bv5 4)) $x43)) (= (not (= x$ (_ bv5 4))) (not $x43))))) |
|
105 (let ((@x55 (monotonicity @x48 (rewrite (= $x32 (= (_ bv4 4) ?x31))) (= (or (not (= x$ (_ bv5 4))) $x32) (or (not $x43) (= (_ bv4 4) ?x31)))))) |
|
106 (let (($x34 (not (=> (= x$ (_ bv5 4)) $x32)))) |
|
107 (let ((@x39 (rewrite (= (=> (= x$ (_ bv5 4)) $x32) (or (not (= x$ (_ bv5 4))) $x32))))) |
|
108 (let ((@x60 (trans (monotonicity @x39 (= $x34 (not (or (not (= x$ (_ bv5 4))) $x32)))) (monotonicity @x55 (= (not (or (not (= x$ (_ bv5 4))) $x32)) $x56)) (= $x34 $x56)))) |
|
109 (let ((@x67 (monotonicity (not-or-elim (mp (asserted $x34) @x60 $x56) $x43) (= ?x31 (bvmul (_ bv4 4) (_ bv5 4)))))) |
|
110 (let ((@x73 (monotonicity (trans @x67 (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x32) (= (= (_ bv4 4) ?x31) (= (_ bv4 4) (_ bv4 4)))))) |
|
111 (let ((@x77 (trans @x73 (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= (= (_ bv4 4) ?x31) true)))) |
|
112 (let ((@x84 (trans (monotonicity @x77 (= (not (= (_ bv4 4) ?x31)) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv4 4) ?x31)) false)))) |
|
113 (mp (not-or-elim (mp (asserted $x34) @x60 $x56) (not (= (_ bv4 4) ?x31))) @x84 false)))))))))))))))) |
|
114 |
|
115 d150015a66b6757a72346710966844993c0f3c27 9 0 |
|
116 unsat |
|
117 ((set-logic <null>) |
|
118 (proof |
|
119 (let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32)))))) |
|
120 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true)))) |
|
121 (let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true))))) |
|
122 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false)))) |
|
123 (mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false))))))) |
|
124 |
|
125 d7cc0827eb340c29b0f489145022e4b3e3610818 9 0 |
|
126 unsat |
|
127 ((set-logic <null>) |
|
128 (proof |
|
129 (let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8)))))) |
|
130 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true)))) |
|
131 (let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true))))) |
|
132 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false)))) |
|
133 (mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false))))))) |
|
134 |
|
135 200e29aa9f19844d244c5c9755155eb956c5cf7c 9 0 |
|
136 unsat |
|
137 ((set-logic <null>) |
|
138 (proof |
|
139 (let ((@x37 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8)))))) |
|
140 (let ((@x41 (trans @x37 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true)))) |
|
141 (let ((@x44 (monotonicity @x41 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true))))) |
|
142 (let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false)))) |
|
143 (mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x48 false))))))) |
|
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 |
|
155 unsat |
|
156 ((set-logic <null>) |
|
157 (proof |
|
158 (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)))) |
|
160 (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)))) |
|
162 (mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false))))))) |
|
163 |
|
164 880bee16a8f6469b14122277b92e87533ef6a071 9 0 |
|
165 unsat |
|
166 ((set-logic <null>) |
|
167 (proof |
|
168 (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)))) |
|
170 (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)))) |
|
172 (mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false))))))) |
|
173 |
|
174 9e2fe3c1b368a228c2dbf7cde7085d55a48a6d7d 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 |
|
184 unsat |
|
185 ((set-logic <null>) |
|
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)))))) |
|
188 (let ((@x40 (trans @x36 (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) true)))) |
|
189 (let ((@x43 (monotonicity @x40 (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (not true))))) |
|
190 (let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) false)))) |
|
191 (mp (asserted (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) @x47 false))))))) |
|
192 |
|
193 956d8b6229140c8c4aa869ab0f3765697ab8ff25 9 0 |
|
194 unsat |
|
195 ((set-logic <null>) |
|
196 (proof |
|
197 (let ((@x36 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6)))))) |
|
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))))) |
|
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))))))) |
|
202 |
|
203 78062d69d2e39df30e3b96bcc1dc2b4cf4d9ba20 9 0 |
|
204 unsat |
|
205 ((set-logic <null>) |
|
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)))))) |
|
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))))) |
|
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))))))) |
|
212 |
|
213 33b517e5a63a8909bf9a8a46d6f37ecff561f0d3 9 0 |
|
214 unsat |
|
215 ((set-logic <null>) |
|
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)))))) |
|
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))))) |
|
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))))))) |
|
222 |
|
223 792dc8efc6a11427de36bb71a1584a02ba01edfb 9 0 |
|
224 unsat |
|
225 ((set-logic <null>) |
|
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)))))) |
|
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))))) |
|
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))))))) |
|
232 |
|
233 3ac6376c7c9d58e3d8cdda57bbb72d26bd0754d2 9 0 |
|
234 unsat |
|
235 ((set-logic <null>) |
|
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)))))) |
|
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))))) |
|
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))))))) |
|
242 |
|
243 4817b51a29a8c19d79a235020826dd105db2dcf1 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 |
|
253 5c4e275bed2d91897e820ccd6744b0a775a6e26e 17 0 |
|
254 unsat |
|
255 ((set-logic <null>) |
|
256 (proof |
|
257 (let ((?x31 (bvand x$ (_ bv255 16)))) |
|
258 (let ((?x29 (bvand x$ (_ bv65280 16)))) |
|
259 (let ((?x32 (bvor ?x29 ?x31))) |
|
260 (let (($x33 (= ?x32 x$))) |
|
261 (let (($x34 (not $x33))) |
|
262 (let ((@x59 (symm (commutativity (= (= x$ ?x32) $x33)) (= $x33 (= x$ ?x32))))) |
|
263 (let ((@x35 (asserted $x34))) |
|
264 (let ((@x63 (mp @x35 (monotonicity @x59 (= $x34 (not (= x$ ?x32)))) (not (= x$ ?x32))))) |
|
265 (let (($x52 (= x$ ?x32))) |
|
266 (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))) |
|
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))) |
|
269 (unit-resolution @x55 @x63 false))))))))))))))) |
|
270 |
|
271 1d4a0e2a4449a8adbcf5a134bf7f2b0ee940d954 51 0 |
|
272 unsat |
|
273 ((set-logic <null>) |
|
274 (proof |
|
275 (let ((?x31 (bvand w$ (_ bv255 16)))) |
|
276 (let (($x32 (= ?x31 w$))) |
|
277 (let (($x64 (not $x32))) |
|
278 (let ((@x318 (symm (commutativity (= (= w$ ?x31) $x32)) (= $x32 (= w$ ?x31))))) |
|
279 (let (($x57 (not (or (bvule (_ bv256 16) w$) $x32)))) |
|
280 (let ((@x49 (monotonicity (rewrite (= (bvult w$ (_ bv256 16)) (not (bvule (_ bv256 16) w$)))) (= (not (bvult w$ (_ bv256 16))) (not (not (bvule (_ bv256 16) w$))))))) |
|
281 (let ((@x53 (trans @x49 (rewrite (= (not (not (bvule (_ bv256 16) w$))) (bvule (_ bv256 16) w$))) (= (not (bvult w$ (_ bv256 16))) (bvule (_ bv256 16) w$))))) |
|
282 (let ((@x56 (monotonicity @x53 (= (or (not (bvult w$ (_ bv256 16))) $x32) (or (bvule (_ bv256 16) w$) $x32))))) |
|
283 (let ((@x59 (monotonicity @x56 (= (not (or (not (bvult w$ (_ bv256 16))) $x32)) $x57)))) |
|
284 (let (($x34 (not (=> (bvult w$ (_ bv256 16)) $x32)))) |
|
285 (let ((@x39 (rewrite (= (=> (bvult w$ (_ bv256 16)) $x32) (or (not (bvult w$ (_ bv256 16))) $x32))))) |
|
286 (let ((@x42 (monotonicity @x39 (= $x34 (not (or (not (bvult w$ (_ bv256 16))) $x32)))))) |
|
287 (let ((@x65 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x64))) |
|
288 (let ((@x322 (mp @x65 (monotonicity @x318 (= $x64 (not (= w$ ?x31)))) (not (= w$ ?x31))))) |
|
289 (let (($x300 (= w$ ?x31))) |
|
290 (let (($x81 (= ((_ extract 15 15) w$) (_ bv1 1)))) |
|
291 (let (($x264 (not $x81))) |
|
292 (let (($x74 (= ((_ extract 8 8) w$) (_ bv1 1)))) |
|
293 (let (($x75 (= ((_ extract 9 9) w$) (_ bv1 1)))) |
|
294 (let (($x82 (and $x75 $x74))) |
|
295 (let (($x83 (or $x75 $x74 $x82))) |
|
296 (let (($x76 (= ((_ extract 10 10) w$) (_ bv1 1)))) |
|
297 (let (($x84 (and $x76 $x83))) |
|
298 (let (($x85 (or $x76 $x75 $x74 $x82 $x84))) |
|
299 (let (($x77 (= ((_ extract 11 11) w$) (_ bv1 1)))) |
|
300 (let (($x86 (and $x77 $x85))) |
|
301 (let (($x87 (or $x77 $x76 $x75 $x74 $x82 $x84 $x86))) |
|
302 (let (($x78 (= ((_ extract 12 12) w$) (_ bv1 1)))) |
|
303 (let (($x88 (and $x78 $x87))) |
|
304 (let (($x89 (or $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88))) |
|
305 (let (($x79 (= ((_ extract 13 13) w$) (_ bv1 1)))) |
|
306 (let (($x90 (and $x79 $x89))) |
|
307 (let (($x91 (or $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90))) |
|
308 (let (($x80 (= ((_ extract 14 14) w$) (_ bv1 1)))) |
|
309 (let (($x92 (and $x80 $x91))) |
|
310 (let (($x93 (or $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92))) |
|
311 (let (($x94 (and $x81 $x93))) |
|
312 (let (($x95 (or $x81 $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92 $x94))) |
|
313 (let (($x297 (not $x95))) |
|
314 (let (($x43 (bvule (_ bv256 16) w$))) |
|
315 (let (($x44 (not $x43))) |
|
316 (let ((@x63 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x44))) |
|
317 (let ((@x303 (unit-resolution ((_ th-lemma bv) (or $x43 $x297)) @x63 $x297))) |
|
318 (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))) |
|
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))) |
|
321 (unit-resolution @x314 @x322 false))))))))))))))))))))))))))))))))))))))))))))))))) |
|
322 |
|
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 |
|
354 unsat |
|
355 ((set-logic <null>) |
|
356 (proof |
|
357 (let ((?x32 (p$ true))) |
|
358 (let (($x29 (bvule (_ bv0 4) a$))) |
|
359 (let (($x30 (ite $x29 true false))) |
|
360 (let ((?x31 (p$ $x30))) |
|
361 (let (($x33 (= ?x31 ?x32))) |
|
362 (let (($x34 (not $x33))) |
|
363 (let ((@x52 (monotonicity (monotonicity (rewrite (= $x29 true)) (= (p$ $x29) ?x32)) (= (= (p$ $x29) ?x32) (= ?x32 ?x32))))) |
|
364 (let ((@x56 (trans @x52 (rewrite (= (= ?x32 ?x32) true)) (= (= (p$ $x29) ?x32) true)))) |
|
365 (let ((@x63 (trans (monotonicity @x56 (= (not (= (p$ $x29) ?x32)) (not true))) (rewrite (= (not true) false)) (= (not (= (p$ $x29) ?x32)) false)))) |
|
366 (let ((@x43 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= ?x31 (p$ $x29))) (= $x33 (= (p$ $x29) ?x32))))) |
|
367 (let ((@x46 (monotonicity @x43 (= $x34 (not (= (p$ $x29) ?x32)))))) |
|
368 (mp (asserted $x34) (trans @x46 @x63 (= $x34 false)) false)))))))))))))) |
|
369 |