Adding a couple of example from fuzzsmt to regress1.

3 files changed, 734 insertions, 1 deletions

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