diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
commit | 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch) | |
tree | 040efec36cde7775b5c19eb43fcdd60cbeb61f9e /test/regress/regress0/bv/fuzz07.smt | |
parent | 4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff) |
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally
* added more bv regressions
Diffstat (limited to 'test/regress/regress0/bv/fuzz07.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz07.smt | 395 |
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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |