1 files changed, 0 insertions, 411 deletions
diff --git a/test/regress/regress0/aufbv/fuzz02.smt b/test/regress/regress0/aufbv/fuzz02.smt
deleted file mode 100644
index 2ada96dab..000000000
--- a/test/regress/regress0/aufbv/fuzz02.smt
+++ /dev/null
@@ -1,411 +0,0 @@
-(benchmark fuzzsmt
-:logic QF_AUFBV
-:status sat
-:extrafuns ((v0 BitVec[14]))
-:extrafuns ((v1 BitVec[10]))
-:extrafuns ((v2 BitVec[10]))
-:extrafuns ((v3 BitVec[8]))
-:extrafuns ((v4 BitVec[11]))
-:extrafuns ((a5 Array[5:13]))
-:extrafuns ((a6 Array[15:15]))
-:extrafuns ((a7 Array[3:1]))
-:extrafuns ((a8 Array[8:14]))
-:extrafuns ((a9 Array[6:16]))
-:extrafuns ((a10 Array[13:9]))
-:extrafuns ((a11 Array[3:14]))
-:extrafuns ((a12 Array[1:3]))
-:formula
-(let (?e13 bv37[10])
-(let (?e14 bv27[6])
-(let (?e15 bv60[7])
-(let (?e16 bv486[9])
-(let (?e17 bv7[5])
-(let (?e18 (ite (bvsle v4 (sign_extend[6] ?e17)) bv1[1] bv0[1]))
-(let (?e19 (ite (bvsge v0 (zero_extend[4] ?e13)) bv1[1] bv0[1]))
-(let (?e20 (bvneg v3))
-(let (?e21 (rotate_left[5] v1))
-(let (?e22 (ite (bvsge v4 v4) bv1[1] bv0[1]))
-(let (?e23 (ite (= (zero_extend[4] ?e14) ?e13) bv1[1] bv0[1]))
-(let (?e24 (sign_extend[4] v2))
-(let (?e25 (bvneg ?e16))
-(let (?e26 (bvashr ?e15 (zero_extend[6] ?e23)))
-(let (?e27 (store a12 (extract[6:6] ?e21) (extract[13:11] v0)))
-(let (?e28 (store a10 (sign_extend[5] v3) (extract[9:1] v0)))
-(let (?e29 (store a12 (extract[5:5] ?e16) (extract[9:7] ?e21)))
-(let (?e30 (store a11 (extract[9:7] v0) (sign_extend[4] v1)))
-(let (?e31 (store a5 (extract[5:1] ?e14) (zero_extend[12] ?e22)))
-(let (?e32 (ite (= ?e30 ?e30) bv1[1] bv0[1]))
-(let (?e33 (select a10 (extract[13:1] v0)))
-(let (?e34 (select ?e29 (extract[2:2] ?e17)))
-(let (?e35 (select ?e30 ?e34))
-(let (?e36 (select a8 (extract[13:6] ?e35)))
-(let (?e37 (select ?e31 (extract[4:0] ?e15)))
-(let (?e38 (select a9 (extract[9:4] v1)))
-(let (?e39 (select a8 (zero_extend[1] ?e26)))
-(let (?e40 (store a7 (extract[2:0] ?e24) ?e18))
-(let (?e41 (store ?e31 (extract[11:7] ?e24) (sign_extend[12] ?e23)))
-(let (?e42 (store a8 (zero_extend[7] ?e23) ?e36))
-(let (?e43 (select ?e42 (zero_extend[1] ?e26)))
-(let (?e44 (select ?e29 (extract[6:6] v2)))
-(let (?e45 (select a5 (zero_extend[4] ?e32)))
-(let (?e46 (store a6 (sign_extend[14] ?e23) (zero_extend[1] v0)))
-(let (?e47 (select ?e27 ?e18))
-(let (?e48 (select ?e40 (extract[13:11] ?e43)))
-(let (?e49 (store a6 (zero_extend[1] ?e39) (sign_extend[14] ?e23)))
-(let (?e50 (select ?e27 (extract[10:10] ?e36)))
-(let (?e51 (bvnot ?e15))
-(let (?e52 (repeat[2] v3))
-(let (?e53 (bvmul (zero_extend[10] ?e34) ?e37))
-(let (?e54 (bvsub ?e21 (zero_extend[3] ?e15)))
-(let (?e55 (bvneg ?e39))
-(let (?e56 (bvsub (zero_extend[8] ?e17) ?e37))
-(let (?e57 (ite (bvsgt ?e24 (sign_extend[7] ?e26)) bv1[1] bv0[1]))
-(let (?e58 (bvcomp (sign_extend[9] ?e32) ?e13))
-(let (?e59 (rotate_left[3] ?e33))
-(let (?e60 (bvadd ?e37 (sign_extend[8] ?e17)))
-(let (?e61 (rotate_right[0] ?e44))
-(let (?e62 (ite (bvsgt (zero_extend[6] ?e13) ?e52) bv1[1] bv0[1]))
-(let (?e63 (ite (bvsle ?e38 (zero_extend[6] v2)) bv1[1] bv0[1]))
-(let (?e64 (ite (bvuge (zero_extend[15] ?e23) ?e52) bv1[1] bv0[1]))
-(let (?e65 (bvlshr (zero_extend[10] ?e47) ?e45))
-(let (?e66 (bvnand ?e18 ?e23))
-(let (?e67 (bvashr ?e36 (zero_extend[13] ?e58)))
-(let (?e68 (bvxnor (zero_extend[6] ?e50) ?e25))
-(let (?e69 (ite (bvugt ?e55 (sign_extend[4] v2)) bv1[1] bv0[1]))
-(let (?e70 (bvshl (zero_extend[13] ?e19) ?e35))
-(let (?e71 (bvashr (zero_extend[2] ?e23) ?e61))
-(let (?e72 (bvcomp (sign_extend[3] v2) ?e65))
-(let (?e73 (ite (bvugt ?e56 (sign_extend[7] ?e14)) bv1[1] bv0[1]))
-(let (?e74 (bvneg ?e70))
-(let (?e75 (bvsub ?e16 ?e59))
-(let (?e76 (ite (bvsgt (sign_extend[5] ?e57) ?e14) bv1[1] bv0[1]))
-(let (?e77 (repeat[3] ?e22))
-(let (?e78 (bvcomp ?e65 ?e65))
-(let (?e79 (bvneg ?e48))
-(let (?e80 (ite (bvsge (zero_extend[8] ?e20) ?e38) bv1[1] bv0[1]))
-(let (?e81 (ite (bvult (zero_extend[4] ?e68) ?e45) bv1[1] bv0[1]))
-(let (?e82 (sign_extend[1] v1))
-(let (?e83 (bvor (sign_extend[2] ?e33) v4))
-(let (?e84 (bvshl v0 ?e39))
-(let (?e85 (ite (bvugt (sign_extend[9] ?e62) v2) bv1[1] bv0[1]))
-(let (?e86 (bvnot ?e43))
-(flet ($e87 (bvsge (zero_extend[11] ?e50) ?e86))
-(flet ($e88 (bvsle ?e73 ?e76))
-(flet ($e89 (bvult ?e50 (zero_extend[2] ?e76)))
-(flet ($e90 (= ?e63 ?e79))
-(flet ($e91 (bvsgt (zero_extend[13] ?e72) ?e84))
-(flet ($e92 (bvsle (sign_extend[13] ?e44) ?e52))
-(flet ($e93 (distinct ?e32 ?e76))
-(flet ($e94 (bvult (sign_extend[8] ?e78) ?e33))
-(flet ($e95 (bvuge (sign_extend[11] ?e71) ?e35))
-(flet ($e96 (bvule (zero_extend[15] ?e72) ?e38))
-(flet ($e97 (bvsge ?e65 (zero_extend[2] ?e82)))
-(flet ($e98 (bvuge v0 (sign_extend[5] ?e33)))
-(flet ($e99 (distinct (sign_extend[2] ?e25) v4))
-(flet ($e100 (bvsge ?e33 (zero_extend[8] ?e58)))
-(flet ($e101 (bvsge ?e35 (zero_extend[11] ?e44)))
-(flet ($e102 (= ?e53 (zero_extend[12] ?e57)))
-(flet ($e103 (bvugt ?e39 (zero_extend[4] v1)))
-(flet ($e104 (bvult (zero_extend[11] ?e34) ?e24))
-(flet ($e105 (bvuge ?e47 (sign_extend[2] ?e32)))
-(flet ($e106 (bvsgt ?e84 (sign_extend[1] ?e56)))
-(flet ($e107 (bvsle ?e17 (sign_extend[4] ?e85)))
-(flet ($e108 (bvsle ?e56 (zero_extend[10] ?e61)))
-(flet ($e109 (bvsle (zero_extend[11] ?e47) ?e35))
-(flet ($e110 (bvslt ?e67 v0))
-(flet ($e111 (bvsgt (zero_extend[13] ?e69) ?e74))
-(flet ($e112 (bvslt ?e36 v0))
-(flet ($e113 (bvsge (zero_extend[3] ?e61) ?e14))
-(flet ($e114 (bvsgt (zero_extend[11] ?e61) ?e36))
-(flet ($e115 (bvsge (zero_extend[8] ?e22) ?e25))
-(flet ($e116 (bvuge ?e33 ?e59))
-(flet ($e117 (bvuge (zero_extend[5] ?e23) ?e14))
-(flet ($e118 (bvugt (sign_extend[6] ?e85) ?e51))
-(flet ($e119 (distinct (zero_extend[2] ?e69) ?e34))
-(flet ($e120 (bvugt (zero_extend[8] ?e19) ?e59))
-(flet ($e121 (distinct (zero_extend[8] ?e72) ?e75))
-(flet ($e122 (distinct v1 (zero_extend[7] ?e77)))
-(flet ($e123 (distinct ?e21 (zero_extend[3] ?e15)))
-(flet ($e124 (bvult ?e86 (zero_extend[11] ?e44)))
-(flet ($e125 (bvslt ?e60 (zero_extend[4] ?e68)))
-(flet ($e126 (distinct ?e66 ?e72))
-(flet ($e127 (bvslt v1 (sign_extend[9] ?e64)))
-(flet ($e128 (bvult (zero_extend[8] ?e23) ?e68))
-(flet ($e129 (bvult (zero_extend[1] v3) ?e33))
-(flet ($e130 (= (sign_extend[6] ?e32) ?e26))
-(flet ($e131 (bvsgt ?e84 (zero_extend[13] ?e76)))
-(flet ($e132 (bvslt ?e24 (sign_extend[6] v3)))
-(flet ($e133 (bvugt ?e33 (zero_extend[6] ?e34)))
-(flet ($e134 (bvsgt ?e68 (sign_extend[8] ?e57)))
-(flet ($e135 (bvult ?e84 (zero_extend[11] ?e44)))
-(flet ($e136 (bvsle (zero_extend[10] ?e50) ?e53))
-(flet ($e137 (bvuge v2 (zero_extend[1] ?e68)))
-(flet ($e138 (bvsle (sign_extend[11] ?e44) ?e39))
-(flet ($e139 (bvule (sign_extend[4] ?e13) ?e36))
-(flet ($e140 (bvslt ?e38 (zero_extend[15] ?e64)))
-(flet ($e141 (bvsge (sign_extend[5] ?e64) ?e14))
-(flet ($e142 (bvsge (sign_extend[10] ?e61) ?e65))
-(flet ($e143 (bvslt (zero_extend[3] ?e51) ?e13))
-(flet ($e144 (distinct ?e83 (sign_extend[10] ?e81)))
-(flet ($e145 (bvsle (zero_extend[10] ?e66) ?e83))
-(flet ($e146 (bvule (sign_extend[8] ?e61) ?e83))
-(flet ($e147 (bvule (zero_extend[5] ?e16) ?e55))
-(flet ($e148 (bvuge ?e83 (sign_extend[2] ?e25)))
-(flet ($e149 (bvule ?e50 (sign_extend[2] ?e32)))
-(flet ($e150 (= (sign_extend[1] ?e37) v0))
-(flet ($e151 (bvugt (sign_extend[5] v3) ?e45))
-(flet ($e152 (bvugt ?e55 (sign_extend[8] ?e14)))
-(flet ($e153 (bvsle (zero_extend[13] ?e78) ?e74))
-(flet ($e154 (bvule ?e61 (sign_extend[2] ?e73)))
-(flet ($e155 (bvule ?e22 ?e57))
-(flet ($e156 (bvugt ?e78 ?e32))
-(flet ($e157 (bvuge ?e65 ?e60))
-(flet ($e158 (distinct ?e52 (sign_extend[10] ?e14)))
-(flet ($e159 (bvsge ?e24 ?e43))
-(flet ($e160 (bvsge ?e25 (sign_extend[2] ?e26)))
-(flet ($e161 (bvsgt v0 (zero_extend[9] ?e17)))
-(flet ($e162 (bvult ?e18 ?e72))
-(flet ($e163 (bvsgt ?e53 (sign_extend[3] ?e21)))
-(flet ($e164 (bvsgt ?e77 (sign_extend[2] ?e85)))
-(flet ($e165 (distinct (sign_extend[15] ?e62) ?e38))
-(flet ($e166 (bvsle ?e50 ?e44))
-(flet ($e167 (bvuge ?e39 (zero_extend[1] ?e65)))
-(flet ($e168 (bvsgt v4 (sign_extend[10] ?e85)))
-(flet ($e169 (= (sign_extend[5] ?e68) ?e55))
-(flet ($e170 (= (zero_extend[5] ?e16) ?e67))
-(flet ($e171 (distinct ?e53 (sign_extend[12] ?e32)))
-(flet ($e172 (bvule ?e58 ?e72))
-(flet ($e173 (bvsgt v2 (sign_extend[9] ?e32)))
-(flet ($e174 (bvuge ?e59 (sign_extend[2] ?e15)))
-(flet ($e175 (distinct (zero_extend[8] ?e63) ?e25))
-(flet ($e176 (bvslt (sign_extend[4] ?e59) ?e45))
-(flet ($e177 (bvule v0 (zero_extend[5] ?e25)))
-(flet ($e178 (bvslt ?e25 (zero_extend[4] ?e17)))
-(flet ($e179 (bvule (sign_extend[13] ?e85) ?e70))
-(flet ($e180 (bvsge ?e26 ?e26))
-(flet ($e181 (bvsgt ?e86 (zero_extend[4] ?e54)))
-(flet ($e182 (bvsle (sign_extend[9] ?e57) v2))
-(flet ($e183 (bvuge ?e86 (sign_extend[13] ?e80)))
-(flet ($e184 (distinct ?e38 (sign_extend[2] ?e43)))
-(flet ($e185 (bvugt ?e74 ?e39))
-(flet ($e186 (bvsge ?e56 (sign_extend[3] ?e13)))
-(flet ($e187 (bvsge ?e32 ?e76))
-(flet ($e188 (bvugt ?e36 ?e36))
-(flet ($e189 (distinct (zero_extend[6] ?e17) ?e82))
-(flet ($e190 (bvsle ?e67 (zero_extend[5] ?e59)))
-(flet ($e191 (bvugt ?e51 (zero_extend[2] ?e17)))
-(flet ($e192 (= ?e51 (sign_extend[6] ?e18)))
-(flet ($e193 (bvsge ?e81 ?e32))
-(flet ($e194 (bvuge (zero_extend[4] v2) ?e84))
-(flet ($e195 (= ?e43 (zero_extend[9] ?e17)))
-(flet ($e196 (bvsgt ?e74 (zero_extend[11] ?e77)))
-(flet ($e197 (bvugt ?e83 (sign_extend[10] ?e78)))
-(flet ($e198 (bvsgt ?e25 (zero_extend[1] v3)))
-(flet ($e199 (bvsge (sign_extend[7] ?e32) v3))
-(flet ($e200 (bvuge ?e39 (zero_extend[13] ?e64)))
-(flet ($e201 (bvsgt ?e65 (sign_extend[12] ?e32)))
-(flet ($e202 (bvuge ?e45 ?e60))
-(flet ($e203 (distinct ?e59 (sign_extend[8] ?e62)))
-(flet ($e204 (bvsle (sign_extend[4] ?e47) ?e15))
-(flet ($e205 (bvsle (zero_extend[8] ?e81) ?e16))
-(flet ($e206 (bvugt ?e16 (sign_extend[4] ?e17)))
-(flet ($e207 (bvule ?e77 (zero_extend[2] ?e64)))
-(flet ($e208 (bvule ?e64 ?e19))
-(flet ($e209 (bvule ?e86 ?e43))
-(flet ($e210 (bvsgt (zero_extend[1] ?e60) ?e55))
-(flet ($e211 (bvsle (sign_extend[2] ?e19) ?e47))
-(flet ($e212 (bvuge v0 (sign_extend[1] ?e65)))
-(flet ($e213 (bvult (zero_extend[9] ?e18) ?e13))
-(flet ($e214 (distinct ?e35 (sign_extend[13] ?e32)))
-(flet ($e215 (distinct (zero_extend[2] ?e58) ?e47))
-(flet ($e216 (bvsge (zero_extend[1] ?e56) ?e43))
-(flet ($e217 (bvslt ?e81 ?e19))
-(flet ($e218 (distinct (sign_extend[6] ?e20) ?e35))
-(flet ($e219 (bvsgt (sign_extend[2] ?e67) ?e52))
-(flet ($e220 (bvsgt (zero_extend[2] ?e82) ?e56))
-(flet ($e221 (bvule ?e77 (zero_extend[2] ?e19)))
-(flet ($e222 (bvuge ?e65 (zero_extend[6] ?e51)))
-(flet ($e223 (bvuge ?e47 ?e34))
-(flet ($e224 (bvult ?e38 (sign_extend[15] ?e85)))
-(flet ($e225 (bvsgt v4 (zero_extend[10] ?e78)))
-(flet ($e226 (bvugt (sign_extend[11] ?e17) ?e38))
-(flet ($e227 (bvult (zero_extend[2] ?e69) ?e77))
-(flet ($e228 (bvuge ?e39 (sign_extend[13] ?e63)))
-(flet ($e229 (distinct (zero_extend[13] ?e85) ?e39))
-(flet ($e230 (bvsgt (zero_extend[12] ?e57) ?e60))
-(flet ($e231 (bvugt ?e71 (sign_extend[2] ?e18)))
-(flet ($e232 (= (zero_extend[4] ?e50) ?e26))
-(flet ($e233 (bvuge ?e70 (zero_extend[13] ?e22)))
-(flet ($e234 (bvsgt v2 (sign_extend[9] ?e19)))
-(flet ($e235 (bvuge (sign_extend[13] ?e22) ?e39))
-(flet ($e236 (bvuge (sign_extend[7] ?e51) ?e70))
-(flet ($e237 (bvslt ?e18 ?e73))
-(flet ($e238 (bvult ?e54 (sign_extend[9] ?e78)))
-(flet ($e239 (bvuge v2 (sign_extend[1] ?e25)))
-(flet ($e240 (= ?e21 (sign_extend[9] ?e85)))
-(flet ($e241 (bvsle v3 (zero_extend[7] ?e62)))
-(flet ($e242 (= ?e71 (sign_extend[2] ?e63)))
-(flet ($e243 (bvsgt ?e45 (zero_extend[12] ?e85)))
-(flet ($e244 (bvsle ?e55 (zero_extend[13] ?e48)))
-(flet ($e245 (= ?e30 ?e30))
-(flet ($e246 (and $e97 $e119))
-(flet ($e247 (if_then_else $e217 $e186 $e127))
-(flet ($e248 (iff $e99 $e89))
-(flet ($e249 (implies $e241 $e226))
-(flet ($e250 (implies $e102 $e114))
-(flet ($e251 (if_then_else $e236 $e117 $e184))
-(flet ($e252 (if_then_else $e111 $e138 $e219))
-(flet ($e253 (or $e227 $e135))
-(flet ($e254 (xor $e93 $e221))
-(flet ($e255 (and $e104 $e210))
-(flet ($e256 (if_then_else $e158 $e238 $e172))
-(flet ($e257 (and $e113 $e136))
-(flet ($e258 (not $e190))
-(flet ($e259 (implies $e163 $e94))
-(flet ($e260 (iff $e243 $e228))
-(flet ($e261 (not $e155))
-(flet ($e262 (if_then_else $e147 $e141 $e216))
-(flet ($e263 (xor $e194 $e160))
-(flet ($e264 (or $e103 $e233))
-(flet ($e265 (and $e179 $e140))
-(flet ($e266 (if_then_else $e173 $e198 $e150))
-(flet ($e267 (xor $e167 $e231))
-(flet ($e268 (if_then_else $e223 $e252 $e258))
-(flet ($e269 (iff $e177 $e200))
-(flet ($e270 (or $e245 $e132))
-(flet ($e271 (implies $e148 $e218))
-(flet ($e272 (or $e265 $e195))
-(flet ($e273 (not $e96))
-(flet ($e274 (or $e123 $e182))
-(flet ($e275 (if_then_else $e239 $e193 $e178))
-(flet ($e276 (xor $e249 $e110))
-(flet ($e277 (xor $e251 $e264))
-(flet ($e278 (if_then_else $e181 $e222 $e244))
-(flet ($e279 (if_then_else $e207 $e128 $e152))
-(flet ($e280 (not $e274))
-(flet ($e281 (if_then_else $e92 $e255 $e214))
-(flet ($e282 (iff $e234 $e115))
-(flet ($e283 (xor $e260 $e209))
-(flet ($e284 (and $e191 $e180))
-(flet ($e285 (or $e183 $e95))
-(flet ($e286 (or $e259 $e100))
-(flet ($e287 (if_then_else $e273 $e153 $e101))
-(flet ($e288 (not $e188))
-(flet ($e289 (not $e229))
-(flet ($e290 (iff $e284 $e268))
-(flet ($e291 (or $e269 $e124))
-(flet ($e292 (or $e202 $e145))
-(flet ($e293 (or $e169 $e129))
-(flet ($e294 (iff $e204 $e142))
-(flet ($e295 (and $e271 $e146))
-(flet ($e296 (implies $e185 $e144))
-(flet ($e297 (iff $e118 $e143))
-(flet ($e298 (and $e242 $e263))
-(flet ($e299 (or $e283 $e125))
-(flet ($e300 (xor $e130 $e168))
-(flet ($e301 (if_then_else $e213 $e257 $e293))
-(flet ($e302 (xor $e277 $e280))
-(flet ($e303 (or $e199 $e187))
-(flet ($e304 (and $e109 $e237))
-(flet ($e305 (implies $e165 $e205))
-(flet ($e306 (xor $e91 $e299))
-(flet ($e307 (or $e246 $e175))
-(flet ($e308 (implies $e133 $e302))
-(flet ($e309 (xor $e307 $e174))
-(flet ($e310 (or $e261 $e298))
-(flet ($e311 (iff $e297 $e122))
-(flet ($e312 (xor $e267 $e170))
-(flet ($e313 (iff $e292 $e300))
-(flet ($e314 (implies $e256 $e287))
-(flet ($e315 (and $e201 $e120))
-(flet ($e316 (and $e106 $e304))
-(flet ($e317 (or $e126 $e290))
-(flet ($e318 (implies $e262 $e108))
-(flet ($e319 (and $e107 $e310))
-(flet ($e320 (implies $e220 $e206))
-(flet ($e321 (iff $e196 $e225))
-(flet ($e322 (xor $e295 $e294))
-(flet ($e323 (xor $e87 $e321))
-(flet ($e324 (and $e240 $e151))
-(flet ($e325 (xor $e121 $e161))
-(flet ($e326 (iff $e90 $e319))
-(flet ($e327 (iff $e215 $e248))
-(flet ($e328 (xor $e285 $e288))
-(flet ($e329 (or $e232 $e98))
-(flet ($e330 (not $e317))
-(flet ($e331 (and $e315 $e270))
-(flet ($e332 (iff $e318 $e279))
-(flet ($e333 (or $e328 $e253))
-(flet ($e334 (xor $e276 $e306))
-(flet ($e335 (iff $e88 $e235))
-(flet ($e336 (xor $e211 $e313))
-(flet ($e337 (iff $e286 $e324))
-(flet ($e338 (implies $e266 $e166))
-(flet ($e339 (if_then_else $e250 $e312 $e212))
-(flet ($e340 (not $e131))
-(flet ($e341 (xor $e329 $e275))
-(flet ($e342 (iff $e208 $e289))
-(flet ($e343 (and $e338 $e154))
-(flet ($e344 (not $e149))
-(flet ($e345 (and $e134 $e272))
-(flet ($e346 (implies $e301 $e322))
-(flet ($e347 (and $e346 $e176))
-(flet ($e348 (not $e343))
-(flet ($e349 (xor $e316 $e308))
-(flet ($e350 (or $e281 $e281))
-(flet ($e351 (not $e333))
-(flet ($e352 (implies $e351 $e327))
-(flet ($e353 (xor $e345 $e112))
-(flet ($e354 (xor $e311 $e157))
-(flet ($e355 (implies $e350 $e341))
-(flet ($e356 (implies $e344 $e171))
-(flet ($e357 (implies $e326 $e347))
-(flet ($e358 (implies $e332 $e162))
-(flet ($e359 (iff $e320 $e342))
-(flet ($e360 (iff $e159 $e339))
-(flet ($e361 (if_then_else $e337 $e334 $e358))
-(flet ($e362 (iff $e116 $e224))
-(flet ($e363 (or $e278 $e197))
-(flet ($e364 (if_then_else $e137 $e362 $e296))
-(flet ($e365 (or $e336 $e323))
-(flet ($e366 (and $e356 $e330))
-(flet ($e367 (implies $e230 $e348))
-(flet ($e368 (not $e365))
-(flet ($e369 (iff $e352 $e353))
-(flet ($e370 (or $e189 $e354))
-(flet ($e371 (and $e331 $e139))
-(flet ($e372 (not $e254))
-(flet ($e373 (implies $e370 $e291))
-(flet ($e374 (xor $e349 $e367))
-(flet ($e375 (iff $e305 $e361))
-(flet ($e376 (not $e364))
-(flet ($e377 (if_then_else $e314 $e340 $e309))
-(flet ($e378 (iff $e335 $e357))
-(flet ($e379 (xor $e355 $e366))
-(flet ($e380 (or $e359 $e359))
-(flet ($e381 (implies $e375 $e105))
-(flet ($e382 (if_then_else $e203 $e380 $e164))
-(flet ($e383 (implies $e371 $e325))
-(flet ($e384 (implies $e282 $e360))
-(flet ($e385 (xor $e376 $e373))
-(flet ($e386 (not $e363))
-(flet ($e387 (implies $e247 $e383))
-(flet ($e388 (implies $e378 $e156))
-(flet ($e389 (implies $e382 $e369))
-(flet ($e390 (not $e386))
-(flet ($e391 (not $e389))
-(flet ($e392 (implies $e379 $e384))
-(flet ($e393 (iff $e381 $e192))
-(flet ($e394 (if_then_else $e385 $e388 $e374))
-(flet ($e395 (not $e377))
-(flet ($e396 (if_then_else $e390 $e387 $e387))
-(flet ($e397 (if_then_else $e394 $e396 $e396))
-(flet ($e398 (implies $e303 $e392))
-(flet ($e399 (or $e397 $e398))
-(flet ($e400 (implies $e399 $e368))
-(flet ($e401 (implies $e391 $e372))
-(flet ($e402 (and $e400 $e393))
-(flet ($e403 (if_then_else $e401 $e395 $e402))
-$e403
-))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
-