diff options
Diffstat (limited to 'test/regress/regress0/uflia/error1.smt')
-rw-r--r-- | test/regress/regress0/uflia/error1.smt | 701 |
1 files changed, 701 insertions, 0 deletions
diff --git a/test/regress/regress0/uflia/error1.smt b/test/regress/regress0/uflia/error1.smt new file mode 100644 index 000000000..7afffaa88 --- /dev/null +++ b/test/regress/regress0/uflia/error1.smt @@ -0,0 +1,701 @@ +(benchmark fuzzsmt +:logic QF_UFLIA +:status sat +:extrafuns ((f0 Int Int Int Int)) +:extrafuns ((f1 Int Int)) +:extrapreds ((p0 Int Int)) +:extrafuns ((v0 Int)) +:extrafuns ((v1 Int)) +:extrafuns ((v2 Int)) +:formula +(let (?e3 1) +(let (?e4 2) +(let (?e5 (f1 v1)) +(let (?e6 (+ v2 v2)) +(let (?e7 (ite (p0 ?e6 v1) 1 0)) +(let (?e8 (ite (p0 ?e5 v1) 1 0)) +(let (?e9 (+ ?e6 ?e8)) +(let (?e10 (ite (p0 v1 ?e6) 1 0)) +(let (?e11 (ite (p0 v2 ?e8) 1 0)) +(let (?e12 (* (~ ?e4) ?e6)) +(let (?e13 (+ v1 ?e5)) +(let (?e14 (* ?e4 ?e12)) +(let (?e15 (f0 v2 ?e5 v0)) +(let (?e16 (ite (p0 ?e5 ?e6) 1 0)) +(let (?e17 (+ ?e7 ?e16)) +(let (?e18 (+ ?e10 ?e12)) +(let (?e19 (- ?e13 ?e12)) +(let (?e20 (* ?e19 (~ ?e4))) +(let (?e21 (+ ?e13 ?e18)) +(let (?e22 (f0 ?e5 ?e17 ?e5)) +(let (?e23 (* ?e17 ?e4)) +(let (?e24 (ite (p0 ?e9 ?e19) 1 0)) +(let (?e25 (~ ?e6)) +(let (?e26 (f1 ?e6)) +(let (?e27 (* ?e25 (~ ?e3))) +(flet ($e28 (< ?e7 ?e6)) +(flet ($e29 (> ?e12 ?e10)) +(flet ($e30 (distinct ?e7 ?e9)) +(flet ($e31 (<= v2 v2)) +(flet ($e32 (>= ?e6 ?e27)) +(flet ($e33 (distinct ?e11 ?e20)) +(flet ($e34 (> ?e25 ?e23)) +(flet ($e35 (< ?e7 ?e22)) +(flet ($e36 (>= ?e24 ?e10)) +(flet ($e37 (>= ?e24 ?e23)) +(flet ($e38 (distinct ?e5 ?e25)) +(flet ($e39 (= ?e16 ?e27)) +(flet ($e40 (> ?e21 ?e16)) +(flet ($e41 (> ?e7 ?e12)) +(flet ($e42 (distinct ?e22 ?e22)) +(flet ($e43 (= v2 ?e16)) +(flet ($e44 (>= ?e23 ?e7)) +(flet ($e45 (= ?e12 ?e8)) +(flet ($e46 (<= ?e13 ?e12)) +(flet ($e47 (< ?e12 ?e24)) +(flet ($e48 (< ?e13 ?e6)) +(flet ($e49 (> ?e15 ?e19)) +(flet ($e50 (> ?e25 ?e18)) +(flet ($e51 (>= ?e15 ?e7)) +(flet ($e52 (distinct ?e8 ?e20)) +(flet ($e53 (= ?e18 ?e5)) +(flet ($e54 (> ?e13 ?e15)) +(flet ($e55 (= ?e14 ?e16)) +(flet ($e56 (>= v0 ?e21)) +(flet ($e57 (= v1 ?e10)) +(flet ($e58 (distinct ?e26 ?e22)) +(flet ($e59 (> ?e18 ?e5)) +(flet ($e60 (< ?e11 ?e10)) +(flet ($e61 (>= ?e8 ?e11)) +(flet ($e62 (distinct ?e23 ?e21)) +(flet ($e63 (p0 v1 ?e20)) +(flet ($e64 (< ?e8 ?e11)) +(flet ($e65 (<= ?e26 ?e12)) +(flet ($e66 (= ?e21 ?e6)) +(flet ($e67 (distinct ?e21 ?e21)) +(flet ($e68 (>= v1 ?e17)) +(let (?e69 (ite $e59 ?e16 ?e12)) +(let (?e70 (ite $e47 ?e9 ?e19)) +(let (?e71 (ite $e64 ?e9 ?e25)) +(let (?e72 (ite $e63 v2 ?e25)) +(let (?e73 (ite $e31 ?e22 ?e15)) +(let (?e74 (ite $e66 ?e23 ?e20)) +(let (?e75 (ite $e57 ?e15 ?e9)) +(let (?e76 (ite $e39 ?e21 ?e75)) +(let (?e77 (ite $e62 v0 ?e11)) +(let (?e78 (ite $e50 ?e17 ?e71)) +(let (?e79 (ite $e38 ?e6 v0)) +(let (?e80 (ite $e62 ?e18 v0)) +(let (?e81 (ite $e29 ?e70 ?e13)) +(let (?e82 (ite $e54 ?e19 ?e20)) +(let (?e83 (ite $e57 ?e19 ?e77)) +(let (?e84 (ite $e41 ?e79 v2)) +(let (?e85 (ite $e56 ?e84 v2)) +(let (?e86 (ite $e47 ?e7 ?e15)) +(let (?e87 (ite $e49 ?e27 ?e27)) +(let (?e88 (ite $e45 ?e14 ?e16)) +(let (?e89 (ite $e42 ?e26 ?e5)) +(let (?e90 (ite $e51 ?e10 ?e12)) +(let (?e91 (ite $e46 ?e26 ?e16)) +(let (?e92 (ite $e35 ?e24 v1)) +(let (?e93 (ite $e32 ?e8 ?e91)) +(let (?e94 (ite $e30 ?e80 ?e15)) +(let (?e95 (ite $e56 ?e75 ?e27)) +(let (?e96 (ite $e64 ?e79 ?e19)) +(let (?e97 (ite $e44 ?e77 ?e84)) +(let (?e98 (ite $e62 ?e25 ?e71)) +(let (?e99 (ite $e65 ?e91 ?e21)) +(let (?e100 (ite $e33 ?e97 ?e14)) +(let (?e101 (ite $e45 ?e90 ?e7)) +(let (?e102 (ite $e41 ?e78 ?e89)) +(let (?e103 (ite $e36 ?e7 ?e81)) +(let (?e104 (ite $e48 ?e74 ?e16)) +(let (?e105 (ite $e31 ?e24 ?e81)) +(let (?e106 (ite $e40 ?e83 ?e71)) +(let (?e107 (ite $e67 ?e11 ?e10)) +(let (?e108 (ite $e52 ?e104 ?e76)) +(let (?e109 (ite $e55 ?e14 ?e14)) +(let (?e110 (ite $e61 ?e102 ?e80)) +(let (?e111 (ite $e34 ?e74 v2)) +(let (?e112 (ite $e54 ?e21 ?e106)) +(let (?e113 (ite $e28 ?e93 ?e20)) +(let (?e114 (ite $e37 ?e8 ?e83)) +(let (?e115 (ite $e55 ?e113 ?e89)) +(let (?e116 (ite $e58 ?e7 ?e25)) +(let (?e117 (ite $e60 ?e7 ?e75)) +(let (?e118 (ite $e43 ?e75 ?e16)) +(let (?e119 (ite $e53 ?e74 ?e26)) +(let (?e120 (ite $e68 ?e76 ?e25)) +(flet ($e121 (< ?e90 ?e9)) +(flet ($e122 (distinct ?e99 v0)) +(flet ($e123 (= ?e116 ?e23)) +(flet ($e124 (= ?e86 ?e99)) +(flet ($e125 (>= ?e78 ?e18)) +(flet ($e126 (> ?e99 ?e75)) +(flet ($e127 (<= ?e84 ?e107)) +(flet ($e128 (>= ?e9 ?e69)) +(flet ($e129 (= ?e95 ?e79)) +(flet ($e130 (p0 ?e103 ?e16)) +(flet ($e131 (<= ?e83 ?e104)) +(flet ($e132 (p0 ?e119 ?e97)) +(flet ($e133 (p0 ?e96 ?e89)) +(flet ($e134 (<= ?e100 ?e21)) +(flet ($e135 (= ?e102 ?e18)) +(flet ($e136 (<= ?e81 ?e16)) +(flet ($e137 (distinct ?e70 ?e94)) +(flet ($e138 (= ?e114 ?e112)) +(flet ($e139 (= ?e107 ?e89)) +(flet ($e140 (p0 ?e110 v2)) +(flet ($e141 (< ?e21 ?e114)) +(flet ($e142 (p0 ?e20 v2)) +(flet ($e143 (< ?e100 ?e94)) +(flet ($e144 (distinct ?e94 ?e26)) +(flet ($e145 (= ?e109 ?e88)) +(flet ($e146 (= ?e16 ?e100)) +(flet ($e147 (= ?e99 ?e87)) +(flet ($e148 (<= ?e87 ?e86)) +(flet ($e149 (p0 ?e73 ?e96)) +(flet ($e150 (> ?e12 ?e94)) +(flet ($e151 (distinct ?e95 ?e71)) +(flet ($e152 (distinct ?e19 ?e101)) +(flet ($e153 (p0 ?e84 ?e96)) +(flet ($e154 (= ?e99 ?e111)) +(flet ($e155 (p0 ?e14 ?e118)) +(flet ($e156 (<= ?e70 ?e25)) +(flet ($e157 (= ?e19 ?e98)) +(flet ($e158 (< ?e99 ?e90)) +(flet ($e159 (>= ?e14 ?e15)) +(flet ($e160 (<= v2 ?e120)) +(flet ($e161 (<= ?e21 ?e75)) +(flet ($e162 (< ?e114 ?e6)) +(flet ($e163 (> ?e99 ?e116)) +(flet ($e164 (<= ?e89 ?e11)) +(flet ($e165 (distinct ?e9 ?e10)) +(flet ($e166 (> ?e27 ?e97)) +(flet ($e167 (< ?e119 ?e10)) +(flet ($e168 (< ?e69 ?e79)) +(flet ($e169 (<= ?e22 ?e7)) +(flet ($e170 (= ?e117 ?e17)) +(flet ($e171 (>= ?e72 ?e16)) +(flet ($e172 (>= ?e12 ?e114)) +(flet ($e173 (distinct ?e119 ?e27)) +(flet ($e174 (<= ?e72 ?e119)) +(flet ($e175 (= ?e119 ?e118)) +(flet ($e176 (distinct ?e80 ?e73)) +(flet ($e177 (> ?e10 ?e18)) +(flet ($e178 (> ?e115 ?e15)) +(flet ($e179 (= ?e13 ?e72)) +(flet ($e180 (>= ?e110 ?e111)) +(flet ($e181 (< v0 ?e87)) +(flet ($e182 (< ?e72 ?e70)) +(flet ($e183 (<= ?e13 ?e9)) +(flet ($e184 (>= ?e7 ?e20)) +(flet ($e185 (<= ?e77 ?e23)) +(flet ($e186 (< ?e105 ?e102)) +(flet ($e187 (<= ?e78 ?e109)) +(flet ($e188 (distinct ?e89 ?e97)) +(flet ($e189 (p0 ?e118 ?e97)) +(flet ($e190 (> ?e81 ?e111)) +(flet ($e191 (> ?e14 ?e78)) +(flet ($e192 (< ?e101 ?e97)) +(flet ($e193 (distinct ?e12 ?e16)) +(flet ($e194 (< ?e113 ?e92)) +(flet ($e195 (>= ?e100 ?e87)) +(flet ($e196 (>= ?e103 ?e12)) +(flet ($e197 (p0 ?e116 ?e13)) +(flet ($e198 (>= ?e85 ?e13)) +(flet ($e199 (p0 ?e107 ?e120)) +(flet ($e200 (> ?e96 ?e74)) +(flet ($e201 (<= ?e113 ?e113)) +(flet ($e202 (>= ?e16 ?e103)) +(flet ($e203 (>= ?e72 ?e11)) +(flet ($e204 (> ?e27 ?e25)) +(flet ($e205 (distinct ?e25 ?e15)) +(flet ($e206 (distinct v1 ?e85)) +(flet ($e207 (p0 ?e95 ?e75)) +(flet ($e208 (< ?e92 ?e84)) +(flet ($e209 (< ?e91 ?e115)) +(flet ($e210 (distinct ?e13 ?e75)) +(flet ($e211 (= ?e91 ?e69)) +(flet ($e212 (p0 ?e13 ?e23)) +(flet ($e213 (>= ?e96 ?e100)) +(flet ($e214 (>= ?e72 ?e111)) +(flet ($e215 (p0 ?e97 ?e112)) +(flet ($e216 (>= ?e78 ?e98)) +(flet ($e217 (= ?e120 ?e101)) +(flet ($e218 (<= ?e72 ?e71)) +(flet ($e219 (p0 ?e90 ?e103)) +(flet ($e220 (< ?e117 ?e113)) +(flet ($e221 (>= ?e118 ?e84)) +(flet ($e222 (> ?e11 ?e104)) +(flet ($e223 (< ?e77 ?e111)) +(flet ($e224 (<= ?e21 ?e7)) +(flet ($e225 (>= ?e16 ?e74)) +(flet ($e226 (<= ?e91 ?e74)) +(flet ($e227 (p0 v2 ?e70)) +(flet ($e228 (p0 ?e101 ?e83)) +(flet ($e229 (>= ?e10 ?e8)) +(flet ($e230 (> ?e110 ?e72)) +(flet ($e231 (< ?e84 ?e20)) +(flet ($e232 (p0 ?e79 ?e26)) +(flet ($e233 (= ?e113 ?e81)) +(flet ($e234 (p0 ?e14 ?e90)) +(flet ($e235 (distinct ?e96 ?e15)) +(flet ($e236 (distinct ?e96 ?e7)) +(flet ($e237 (p0 ?e87 ?e104)) +(flet ($e238 (= ?e110 ?e71)) +(flet ($e239 (< ?e70 ?e7)) +(flet ($e240 (>= ?e13 ?e112)) +(flet ($e241 (p0 ?e24 ?e93)) +(flet ($e242 (<= ?e102 ?e87)) +(flet ($e243 (p0 ?e73 ?e25)) +(flet ($e244 (distinct ?e24 ?e116)) +(flet ($e245 (< ?e84 ?e78)) +(flet ($e246 (<= ?e104 ?e100)) +(flet ($e247 (= ?e18 ?e74)) +(flet ($e248 (< ?e16 ?e8)) +(flet ($e249 (< ?e93 ?e25)) +(flet ($e250 (>= ?e88 ?e81)) +(flet ($e251 (>= ?e98 ?e109)) +(flet ($e252 (>= ?e21 ?e13)) +(flet ($e253 (p0 v2 ?e74)) +(flet ($e254 (distinct ?e24 ?e27)) +(flet ($e255 (>= ?e120 ?e111)) +(flet ($e256 (>= ?e81 ?e14)) +(flet ($e257 (<= ?e87 ?e21)) +(flet ($e258 (p0 ?e74 ?e12)) +(flet ($e259 (distinct ?e5 ?e9)) +(flet ($e260 (>= ?e105 ?e79)) +(flet ($e261 (<= v2 ?e108)) +(flet ($e262 (= ?e96 ?e6)) +(flet ($e263 (= ?e5 ?e77)) +(flet ($e264 (>= v0 ?e23)) +(flet ($e265 (= ?e107 ?e72)) +(flet ($e266 (= ?e110 ?e95)) +(flet ($e267 (< ?e90 ?e117)) +(flet ($e268 (= v2 ?e23)) +(flet ($e269 (<= ?e77 ?e12)) +(flet ($e270 (<= ?e104 ?e111)) +(flet ($e271 (= ?e93 ?e14)) +(flet ($e272 (p0 ?e72 ?e79)) +(flet ($e273 (distinct ?e8 ?e20)) +(flet ($e274 (p0 ?e96 ?e112)) +(flet ($e275 (= ?e92 ?e24)) +(flet ($e276 (>= ?e16 ?e22)) +(flet ($e277 (= ?e19 ?e10)) +(flet ($e278 (<= ?e20 ?e86)) +(flet ($e279 (< ?e116 ?e118)) +(flet ($e280 (>= ?e74 ?e5)) +(flet ($e281 (<= ?e79 ?e105)) +(flet ($e282 (< ?e115 ?e70)) +(flet ($e283 (<= ?e13 ?e103)) +(flet ($e284 (p0 ?e27 ?e87)) +(flet ($e285 (p0 v0 ?e88)) +(flet ($e286 (<= ?e81 ?e104)) +(flet ($e287 (= ?e6 ?e99)) +(flet ($e288 (= ?e114 ?e87)) +(flet ($e289 (distinct ?e77 ?e71)) +(flet ($e290 (distinct ?e15 ?e15)) +(flet ($e291 (< ?e79 ?e72)) +(flet ($e292 (< ?e19 ?e8)) +(flet ($e293 (p0 ?e109 ?e5)) +(flet ($e294 (p0 v1 ?e19)) +(flet ($e295 (p0 ?e75 ?e104)) +(flet ($e296 (>= ?e100 ?e110)) +(flet ($e297 (>= ?e101 ?e23)) +(flet ($e298 (distinct ?e21 ?e107)) +(flet ($e299 (= ?e27 ?e101)) +(flet ($e300 (distinct ?e116 v1)) +(flet ($e301 (> ?e22 ?e5)) +(flet ($e302 (distinct ?e102 ?e80)) +(flet ($e303 (p0 ?e112 ?e84)) +(flet ($e304 (<= ?e111 ?e78)) +(flet ($e305 (= ?e75 ?e9)) +(flet ($e306 (= ?e80 ?e20)) +(flet ($e307 (< ?e80 ?e80)) +(flet ($e308 (distinct ?e13 ?e9)) +(flet ($e309 (p0 ?e6 ?e14)) +(flet ($e310 (> ?e70 ?e91)) +(flet ($e311 (> ?e16 ?e8)) +(flet ($e312 (<= ?e13 ?e95)) +(flet ($e313 (> ?e92 ?e95)) +(flet ($e314 (< ?e96 ?e87)) +(flet ($e315 (= ?e91 ?e92)) +(flet ($e316 (>= ?e120 ?e117)) +(flet ($e317 (p0 ?e13 ?e93)) +(flet ($e318 (distinct ?e120 ?e24)) +(flet ($e319 (>= ?e15 ?e86)) +(flet ($e320 (> ?e94 ?e84)) +(flet ($e321 (> ?e20 ?e99)) +(flet ($e322 (< ?e23 ?e71)) +(flet ($e323 (= ?e119 ?e73)) +(flet ($e324 (<= ?e82 ?e94)) +(flet ($e325 (<= ?e108 ?e107)) +(flet ($e326 (p0 ?e13 ?e80)) +(flet ($e327 (<= ?e87 ?e102)) +(flet ($e328 (<= ?e74 ?e89)) +(flet ($e329 (= ?e73 ?e11)) +(flet ($e330 (distinct ?e15 ?e106)) +(flet ($e331 (<= ?e115 ?e110)) +(flet ($e332 (p0 v0 ?e69)) +(flet ($e333 (>= v1 ?e9)) +(flet ($e334 (> v1 v2)) +(flet ($e335 (< ?e80 ?e95)) +(flet ($e336 (>= ?e114 ?e69)) +(flet ($e337 (distinct ?e80 ?e118)) +(flet ($e338 (p0 ?e16 ?e91)) +(flet ($e339 (p0 ?e100 ?e85)) +(flet ($e340 (= ?e13 ?e73)) +(flet ($e341 (= ?e92 ?e12)) +(flet ($e342 (p0 ?e100 ?e72)) +(flet ($e343 (= ?e26 ?e119)) +(flet ($e344 (< ?e20 ?e20)) +(flet ($e345 (<= ?e100 ?e94)) +(flet ($e346 (> ?e114 ?e116)) +(flet ($e347 (p0 ?e102 ?e19)) +(flet ($e348 (= ?e113 ?e13)) +(flet ($e349 (distinct ?e108 ?e5)) +(flet ($e350 (< ?e14 ?e118)) +(flet ($e351 (< ?e72 ?e110)) +(flet ($e352 (> ?e83 ?e114)) +(flet ($e353 (distinct ?e106 ?e24)) +(flet ($e354 (<= ?e24 ?e83)) +(flet ($e355 (p0 ?e116 ?e101)) +(flet ($e356 (< ?e110 ?e96)) +(flet ($e357 (= ?e12 v0)) +(flet ($e358 (p0 ?e108 ?e113)) +(flet ($e359 (>= ?e27 ?e81)) +(flet ($e360 (<= ?e109 ?e75)) +(flet ($e361 (= ?e102 ?e26)) +(flet ($e362 (distinct ?e108 ?e104)) +(flet ($e363 (<= ?e108 ?e26)) +(flet ($e364 (<= ?e114 ?e69)) +(flet ($e365 (>= ?e113 ?e82)) +(flet ($e366 (= ?e115 v1)) +(flet ($e367 (= ?e25 ?e27)) +(flet ($e368 (p0 ?e27 ?e91)) +(flet ($e369 (<= ?e13 ?e116)) +(flet ($e370 (<= ?e87 ?e114)) +(flet ($e371 (< ?e25 ?e108)) +(flet ($e372 (= ?e108 ?e9)) +(flet ($e373 (p0 ?e89 ?e117)) +(flet ($e374 (<= ?e13 ?e19)) +(flet ($e375 (p0 ?e12 ?e26)) +(flet ($e376 (< ?e20 ?e91)) +(flet ($e377 (distinct ?e107 ?e76)) +(flet ($e378 (if_then_else $e180 $e123 $e342)) +(flet ($e379 (if_then_else $e151 $e330 $e232)) +(flet ($e380 (if_then_else $e136 $e175 $e130)) +(flet ($e381 (if_then_else $e362 $e250 $e56)) +(flet ($e382 (not $e337)) +(flet ($e383 (xor $e194 $e150)) +(flet ($e384 (iff $e44 $e65)) +(flet ($e385 (xor $e300 $e160)) +(flet ($e386 (xor $e158 $e241)) +(flet ($e387 (not $e286)) +(flet ($e388 (and $e168 $e55)) +(flet ($e389 (or $e143 $e153)) +(flet ($e390 (not $e289)) +(flet ($e391 (or $e191 $e235)) +(flet ($e392 (and $e42 $e184)) +(flet ($e393 (not $e170)) +(flet ($e394 (iff $e35 $e356)) +(flet ($e395 (xor $e128 $e207)) +(flet ($e396 (implies $e394 $e208)) +(flet ($e397 (not $e354)) +(flet ($e398 (not $e201)) +(flet ($e399 (if_then_else $e176 $e169 $e331)) +(flet ($e400 (and $e217 $e172)) +(flet ($e401 (and $e324 $e178)) +(flet ($e402 (iff $e387 $e279)) +(flet ($e403 (or $e204 $e374)) +(flet ($e404 (iff $e323 $e334)) +(flet ($e405 (xor $e302 $e247)) +(flet ($e406 (iff $e288 $e125)) +(flet ($e407 (or $e375 $e227)) +(flet ($e408 (and $e127 $e378)) +(flet ($e409 (iff $e58 $e284)) +(flet ($e410 (implies $e181 $e52)) +(flet ($e411 (implies $e166 $e385)) +(flet ($e412 (and $e41 $e306)) +(flet ($e413 (xor $e268 $e361)) +(flet ($e414 (and $e47 $e32)) +(flet ($e415 (iff $e228 $e339)) +(flet ($e416 (implies $e292 $e199)) +(flet ($e417 (implies $e252 $e39)) +(flet ($e418 (or $e37 $e351)) +(flet ($e419 (and $e209 $e49)) +(flet ($e420 (implies $e263 $e197)) +(flet ($e421 (if_then_else $e349 $e312 $e287)) +(flet ($e422 (implies $e353 $e249)) +(flet ($e423 (not $e388)) +(flet ($e424 (and $e296 $e310)) +(flet ($e425 (xor $e309 $e59)) +(flet ($e426 (and $e240 $e242)) +(flet ($e427 (if_then_else $e45 $e163 $e411)) +(flet ($e428 (not $e364)) +(flet ($e429 (if_then_else $e144 $e267 $e293)) +(flet ($e430 (if_then_else $e173 $e238 $e126)) +(flet ($e431 (implies $e338 $e48)) +(flet ($e432 (iff $e156 $e383)) +(flet ($e433 (or $e68 $e391)) +(flet ($e434 (xor $e262 $e304)) +(flet ($e435 (not $e318)) +(flet ($e436 (iff $e29 $e155)) +(flet ($e437 (not $e121)) +(flet ($e438 (implies $e389 $e36)) +(flet ($e439 (iff $e234 $e174)) +(flet ($e440 (iff $e253 $e314)) +(flet ($e441 (if_then_else $e137 $e278 $e355)) +(flet ($e442 (xor $e131 $e64)) +(flet ($e443 (or $e377 $e124)) +(flet ($e444 (implies $e346 $e122)) +(flet ($e445 (iff $e212 $e372)) +(flet ($e446 (implies $e195 $e277)) +(flet ($e447 (not $e430)) +(flet ($e448 (not $e192)) +(flet ($e449 (implies $e196 $e177)) +(flet ($e450 (or $e190 $e257)) +(flet ($e451 (iff $e215 $e412)) +(flet ($e452 (implies $e274 $e418)) +(flet ($e453 (if_then_else $e336 $e322 $e149)) +(flet ($e454 (if_then_else $e447 $e189 $e269)) +(flet ($e455 (not $e218)) +(flet ($e456 (xor $e152 $e224)) +(flet ($e457 (not $e358)) +(flet ($e458 (not $e60)) +(flet ($e459 (not $e424)) +(flet ($e460 (not $e398)) +(flet ($e461 (if_then_else $e380 $e291 $e453)) +(flet ($e462 (iff $e305 $e271)) +(flet ($e463 (if_then_else $e408 $e417 $e148)) +(flet ($e464 (not $e270)) +(flet ($e465 (and $e261 $e51)) +(flet ($e466 (or $e450 $e299)) +(flet ($e467 (iff $e301 $e154)) +(flet ($e468 (iff $e200 $e460)) +(flet ($e469 (and $e343 $e129)) +(flet ($e470 (iff $e313 $e400)) +(flet ($e471 (or $e433 $e347)) +(flet ($e472 (not $e451)) +(flet ($e473 (iff $e266 $e317)) +(flet ($e474 (and $e273 $e390)) +(flet ($e475 (and $e406 $e440)) +(flet ($e476 (implies $e223 $e233)) +(flet ($e477 (if_then_else $e298 $e185 $e344)) +(flet ($e478 (xor $e462 $e426)) +(flet ($e479 (and $e368 $e28)) +(flet ($e480 (implies $e319 $e466)) +(flet ($e481 (not $e348)) +(flet ($e482 (not $e134)) +(flet ($e483 (xor $e145 $e471)) +(flet ($e484 (xor $e439 $e171)) +(flet ($e485 (if_then_else $e369 $e198 $e295)) +(flet ($e486 (xor $e329 $e405)) +(flet ($e487 (iff $e290 $e221)) +(flet ($e488 (if_then_else $e373 $e415 $e219)) +(flet ($e489 (iff $e50 $e244)) +(flet ($e490 (and $e363 $e403)) +(flet ($e491 (or $e402 $e431)) +(flet ($e492 (not $e229)) +(flet ($e493 (implies $e470 $e280)) +(flet ($e494 (or $e489 $e220)) +(flet ($e495 (and $e188 $e67)) +(flet ($e496 (or $e53 $e165)) +(flet ($e497 (and $e427 $e206)) +(flet ($e498 (iff $e307 $e333)) +(flet ($e499 (if_then_else $e186 $e487 $e281)) +(flet ($e500 (iff $e360 $e442)) +(flet ($e501 (iff $e490 $e357)) +(flet ($e502 (iff $e392 $e211)) +(flet ($e503 (xor $e210 $e410)) +(flet ($e504 (iff $e239 $e486)) +(flet ($e505 (implies $e248 $e54)) +(flet ($e506 (implies $e465 $e492)) +(flet ($e507 (and $e494 $e255)) +(flet ($e508 (or $e285 $e352)) +(flet ($e509 (if_then_else $e264 $e399 $e316)) +(flet ($e510 (if_then_else $e34 $e508 $e448)) +(flet ($e511 (not $e203)) +(flet ($e512 (not $e246)) +(flet ($e513 (and $e366 $e371)) +(flet ($e514 (xor $e367 $e311)) +(flet ($e515 (iff $e141 $e226)) +(flet ($e516 (iff $e455 $e484)) +(flet ($e517 (iff $e164 $e62)) +(flet ($e518 (iff $e140 $e294)) +(flet ($e519 (and $e345 $e222)) +(flet ($e520 (xor $e135 $e519)) +(flet ($e521 (implies $e216 $e315)) +(flet ($e522 (or $e260 $e446)) +(flet ($e523 (xor $e520 $e522)) +(flet ($e524 (iff $e407 $e46)) +(flet ($e525 (xor $e275 $e256)) +(flet ($e526 (and $e420 $e423)) +(flet ($e527 (not $e61)) +(flet ($e528 (implies $e297 $e488)) +(flet ($e529 (or $e231 $e332)) +(flet ($e530 (and $e482 $e66)) +(flet ($e531 (and $e518 $e245)) +(flet ($e532 (not $e183)) +(flet ($e533 (and $e382 $e236)) +(flet ($e534 (iff $e456 $e422)) +(flet ($e535 (if_then_else $e413 $e524 $e379)) +(flet ($e536 (and $e436 $e401)) +(flet ($e537 (xor $e475 $e475)) +(flet ($e538 (implies $e437 $e498)) +(flet ($e539 (implies $e485 $e477)) +(flet ($e540 (implies $e504 $e474)) +(flet ($e541 (xor $e272 $e445)) +(flet ($e542 (implies $e393 $e438)) +(flet ($e543 (xor $e139 $e205)) +(flet ($e544 (implies $e414 $e386)) +(flet ($e545 (if_then_else $e214 $e321 $e544)) +(flet ($e546 (xor $e449 $e265)) +(flet ($e547 (and $e533 $e187)) +(flet ($e548 (xor $e530 $e506)) +(flet ($e549 (or $e258 $e283)) +(flet ($e550 (iff $e326 $e500)) +(flet ($e551 (if_then_else $e535 $e359 $e537)) +(flet ($e552 (iff $e479 $e469)) +(flet ($e553 (xor $e531 $e521)) +(flet ($e554 (xor $e435 $e43)) +(flet ($e555 (not $e162)) +(flet ($e556 (and $e525 $e454)) +(flet ($e557 (xor $e501 $e514)) +(flet ($e558 (implies $e179 $e138)) +(flet ($e559 (xor $e404 $e365)) +(flet ($e560 (not $e540)) +(flet ($e561 (xor $e513 $e546)) +(flet ($e562 (implies $e503 $e308)) +(flet ($e563 (if_then_else $e541 $e561 $e434)) +(flet ($e564 (not $e335)) +(flet ($e565 (not $e341)) +(flet ($e566 (if_then_else $e564 $e551 $e511)) +(flet ($e567 (or $e523 $e496)) +(flet ($e568 (and $e534 $e159)) +(flet ($e569 (if_then_else $e555 $e562 $e497)) +(flet ($e570 (xor $e457 $e225)) +(flet ($e571 (or $e161 $e251)) +(flet ($e572 (implies $e556 $e559)) +(flet ($e573 (iff $e483 $e370)) +(flet ($e574 (if_then_else $e237 $e432 $e213)) +(flet ($e575 (and $e147 $e528)) +(flet ($e576 (xor $e376 $e552)) +(flet ($e577 (and $e463 $e542)) +(flet ($e578 (not $e548)) +(flet ($e579 (implies $e468 $e560)) +(flet ($e580 (or $e557 $e495)) +(flet ($e581 (if_then_else $e327 $e478 $e472)) +(flet ($e582 (implies $e254 $e572)) +(flet ($e583 (and $e491 $e543)) +(flet ($e584 (implies $e527 $e243)) +(flet ($e585 (if_then_else $e428 $e142 $e566)) +(flet ($e586 (xor $e429 $e133)) +(flet ($e587 (not $e202)) +(flet ($e588 (iff $e481 $e550)) +(flet ($e589 (iff $e33 $e441)) +(flet ($e590 (or $e547 $e532)) +(flet ($e591 (and $e538 $e57)) +(flet ($e592 (not $e230)) +(flet ($e593 (or $e576 $e592)) +(flet ($e594 (iff $e505 $e578)) +(flet ($e595 (and $e350 $e580)) +(flet ($e596 (or $e443 $e574)) +(flet ($e597 (or $e579 $e575)) +(flet ($e598 (or $e132 $e38)) +(flet ($e599 (implies $e303 $e146)) +(flet ($e600 (if_then_else $e598 $e499 $e419)) +(flet ($e601 (and $e558 $e473)) +(flet ($e602 (or $e590 $e529)) +(flet ($e603 (if_then_else $e591 $e182 $e40)) +(flet ($e604 (iff $e596 $e571)) +(flet ($e605 (iff $e328 $e588)) +(flet ($e606 (and $e397 $e594)) +(flet ($e607 (or $e593 $e502)) +(flet ($e608 (or $e516 $e539)) +(flet ($e609 (iff $e573 $e193)) +(flet ($e610 (not $e549)) +(flet ($e611 (not $e563)) +(flet ($e612 (xor $e30 $e606)) +(flet ($e613 (if_then_else $e467 $e609 $e581)) +(flet ($e614 (not $e526)) +(flet ($e615 (if_then_else $e517 $e602 $e610)) +(flet ($e616 (implies $e464 $e396)) +(flet ($e617 (not $e425)) +(flet ($e618 (or $e452 $e611)) +(flet ($e619 (xor $e416 $e63)) +(flet ($e620 (iff $e545 $e565)) +(flet ($e621 (xor $e603 $e458)) +(flet ($e622 (if_then_else $e536 $e476 $e567)) +(flet ($e623 (or $e515 $e157)) +(flet ($e624 (iff $e510 $e493)) +(flet ($e625 (or $e600 $e599)) +(flet ($e626 (iff $e553 $e619)) +(flet ($e627 (or $e586 $e625)) +(flet ($e628 (not $e621)) +(flet ($e629 (not $e509)) +(flet ($e630 (xor $e617 $e582)) +(flet ($e631 (implies $e480 $e630)) +(flet ($e632 (implies $e421 $e340)) +(flet ($e633 (iff $e577 $e612)) +(flet ($e634 (iff $e512 $e627)) +(flet ($e635 (if_then_else $e632 $e444 $e583)) +(flet ($e636 (not $e569)) +(flet ($e637 (implies $e629 $e276)) +(flet ($e638 (and $e633 $e620)) +(flet ($e639 (and $e461 $e381)) +(flet ($e640 (iff $e597 $e395)) +(flet ($e641 (implies $e637 $e639)) +(flet ($e642 (and $e640 $e320)) +(flet ($e643 (or $e607 $e259)) +(flet ($e644 (if_then_else $e384 $e584 $e325)) +(flet ($e645 (implies $e626 $e608)) +(flet ($e646 (xor $e585 $e631)) +(flet ($e647 (or $e616 $e167)) +(flet ($e648 (or $e568 $e644)) +(flet ($e649 (or $e589 $e614)) +(flet ($e650 (and $e641 $e642)) +(flet ($e651 (xor $e554 $e650)) +(flet ($e652 (implies $e635 $e595)) +(flet ($e653 (or $e618 $e636)) +(flet ($e654 (and $e645 $e282)) +(flet ($e655 (not $e648)) +(flet ($e656 (or $e649 $e652)) +(flet ($e657 (iff $e31 $e409)) +(flet ($e658 (iff $e634 $e651)) +(flet ($e659 (xor $e601 $e605)) +(flet ($e660 (not $e628)) +(flet ($e661 (xor $e587 $e622)) +(flet ($e662 (not $e459)) +(flet ($e663 (or $e656 $e638)) +(flet ($e664 (not $e646)) +(flet ($e665 (or $e623 $e653)) +(flet ($e666 (implies $e663 $e663)) +(flet ($e667 (implies $e570 $e507)) +(flet ($e668 (xor $e647 $e658)) +(flet ($e669 (not $e661)) +(flet ($e670 (iff $e660 $e657)) +(flet ($e671 (not $e655)) +(flet ($e672 (if_then_else $e615 $e615 $e624)) +(flet ($e673 (iff $e665 $e643)) +(flet ($e674 (xor $e662 $e669)) +(flet ($e675 (not $e671)) +(flet ($e676 (and $e674 $e675)) +(flet ($e677 (implies $e670 $e676)) +(flet ($e678 (iff $e668 $e604)) +(flet ($e679 (not $e659)) +(flet ($e680 (or $e672 $e666)) +(flet ($e681 (xor $e679 $e678)) +(flet ($e682 (not $e667)) +(flet ($e683 (and $e677 $e681)) +(flet ($e684 (xor $e680 $e680)) +(flet ($e685 (not $e683)) +(flet ($e686 (if_then_else $e664 $e684 $e685)) +(flet ($e687 (iff $e654 $e686)) +(flet ($e688 (if_then_else $e687 $e613 $e613)) +(flet ($e689 (and $e682 $e688)) +(flet ($e690 (implies $e673 $e689)) +$e690 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |