1 files changed, 395 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz07.smt b/test/regress/regress0/bv/fuzz07.smt
new file mode 100644
index 000000000..c813a31be
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz07.smt
@@ -0,0 +1,395 @@
+(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
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+