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