diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-01-05 03:21:35 +0000 |
| commit | f9a4fe48a4ec2355f8fec93d3f47242577df2511 (patch) | |
| tree | eb49b7760b16aa17666d59464c96979b445fbcc8 /test/regress | |
| parent | eecc1e4f301711dbb2bf1508ea0ba6cd20acd593 (diff) | |
Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 36 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0100_10_10.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0100_10_11.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0100_10_15.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0100_10_16.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0100_10_19.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0200_10_22.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0200_10_25.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0200_10_26.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0200_10_27.smt | 126 | ||||
| -rw-r--r-- | test/regress/regress0/uflra/pb_real_10_0200_10_29.smt | 126 |
12 files changed, 1297 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 6ce2468b8..383cb01cb 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf bv lemmas push-pop +SUBDIRS = . arith precedence uf uflra bv lemmas push-pop TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 MAKEFLAGS = -k diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am new file mode 100644 index 000000000..3ebd95257 --- /dev/null +++ b/test/regress/regress0/uflra/Makefile.am @@ -0,0 +1,36 @@ +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" + +# Regression tests for SMT inputs +SMT_TESTS = pb_real_10_0100_10_10.smt \ + pb_real_10_0100_10_11.smt \ + pb_real_10_0100_10_15.smt \ + pb_real_10_0100_10_16.smt \ + pb_real_10_0100_10_19.smt \ + pb_real_10_0200_10_22.smt \ + pb_real_10_0200_10_26.smt \ + pb_real_10_0200_10_29.smt + + +# Regression tests for SMT2 inputs +SMT2_TESTS = + +# Regression tests for PL inputs +CVC_TESTS = + +# Regression tests derived from bug reports +BUG_TESTS = + +TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/uflra/pb_real_10_0100_10_10.smt b/test/regress/regress0/uflra/pb_real_10_0100_10_10.smt new file mode 100644 index 000000000..b6e7253b3 --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0100_10_10.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status sat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (- (+ (* (- 0 16) x4) (* 19 x9)) (* 28 x6))) +(let (?x11 (- (+ (* 28 x2) (* 29 x2)) (* 4 x6))) +(let (?x12 (f1_1 x1)) +(let (?x13 (f1_2 x3 x5)) +(let (?x14 (f1_1 x1)) +(let (?x15 (f0_2 x2 x9)) +(let (?x16 (f0_2 x8 x8)) +(let (?x17 (- (- (* (- 0 18) x9) (* 24 x4)) (* 27 x2))) +(let (?x18 (f1_1 x8)) +(let (?x19 (f0_1 x1)) +(let (?x20 (f1_1 x0)) +(let (?x21 (f0_1 x9)) +(let (?x22 (f1_2 x1 x2)) +(let (?x23 (- (- (* 5 x3) (* 29 x6)) (* 19 x9))) +(let (?x24 (+ (+ (* 16 x4) (* 4 x2)) (* 25 x0))) +(let (?x25 (f0_1 x7)) +(let (?x26 (f0_1 x9)) +(let (?x27 (+ (- (* (- 0 12) x9) (* 6 x1)) (* 10 x2))) +(let (?x28 (f0_2 x3 x6)) +(let (?x29 (f0_1 x0)) +(let (?x30 (+ (- (* (- 0 4) x9) (* 29 x3)) (* 14 x0))) +(let (?x31 (f1_2 x3 ?x19)) +(let (?x32 (f1_2 ?x15 x8)) +(let (?x33 (+ (+ (* (- 0 16) x4) (* 14 x2)) (* 7 x8))) +(let (?x34 (f1_2 x0 x0)) +(let (?x35 (f0_1 x8)) +(let (?x36 (f1_2 x7 x4)) +(let (?x37 (f1_2 ?x33 ?x13)) +(let (?x38 (- (- (* 7 x2) (* 28 x6)) (* 12 x7))) +(let (?x39 (f0_2 x2 x6)) +(let (?x40 (- (+ (* 22 x4) (* 4 x9)) (* 1 x7))) +(let (?x41 (f0_2 x5 x9)) +(let (?x42 (- (- (* 25 ?x33) (* 22 x8)) (* 23 x0))) +(let (?x43 (f1_2 x5 ?x21)) +(let (?x44 (- (+ (* (- 0 15) ?x19) (* 10 ?x13)) (* 24 ?x37))) +(let (?x45 (- (+ (* 22 x0) (* 5 x5)) (* 17 x3))) +(let (?x46 (f1_1 ?x44)) +(let (?x47 (- (- (* (- 0 28) x8) (* 22 x6)) (* 4 x7))) +(let (?x48 (f1_1 ?x32)) +(let (?x49 (+ (- (* 22 x8) (* 23 x7)) (* 9 x3))) +(flet ($P10 (= ?x20 ?x10)) +(flet ($P11 (< ?x44 (- 0 18))) +(flet ($P12 (< ?x23 (- 0 7))) +(flet ($P13 (< ?x34 28)) +(flet ($P14 (< ?x18 9)) +(flet ($P15 (< ?x43 24)) +(flet ($P16 (< x5 27)) +(flet ($P17 (< x7 11)) +(flet ($P18 (< ?x35 (- 0 7))) +(flet ($P19 (< ?x43 5)) +(flet ($P20 (< x3 (- 0 20))) +(flet ($P21 (< ?x25 (- 0 8))) +(flet ($P22 (= ?x21 ?x11)) +(flet ($P23 (< ?x46 2)) +(flet ($P24 (< x4 19)) +(flet ($P25 (< ?x49 11)) +(flet ($P26 (= ?x49 x9)) +(flet ($P27 (= ?x46 ?x38)) +(flet ($P28 (< ?x22 (- 0 22))) +(flet ($P29 (< ?x37 (- 0 4))) +(flet ($P30 (< x1 29)) +(flet ($P31 (< ?x36 (- 0 28))) +(flet ($P32 (< ?x30 13)) +(flet ($P33 (< ?x24 5)) +(flet ($P34 (= ?x16 ?x22)) +(flet ($P35 (< ?x49 (- 0 16))) +(flet ($P36 (< ?x31 (- 0 23))) +(flet ($P37 (< ?x34 1)) +(flet ($P38 (< ?x42 0)) +(flet ($P39 (< x2 (- 0 3))) +(flet ($P40 (< x3 (- 0 16))) +(flet ($P41 (< ?x25 9)) +(flet ($P42 (< ?x29 (- 0 4))) +(flet ($P43 (< x6 (- 0 29))) +(flet ($P44 (< ?x42 (- 0 1))) +(flet ($P45 (< ?x30 16)) +(flet ($P46 (= ?x15 ?x21)) +(flet ($P47 (< ?x12 28)) +(flet ($P48 (= ?x23 ?x28)) +(flet ($P49 (< ?x35 (- 0 12))) +(flet ($P50 (< ?x37 14)) +(flet ($P51 (< ?x42 (- 0 12))) +(flet ($P52 (< ?x44 13)) +(flet ($P53 (< x9 4)) +(flet ($P54 (< ?x23 12)) +(flet ($P55 (< x4 29)) +(flet ($P56 (= ?x21 ?x22)) +(flet ($P57 (< ?x46 (- 0 7))) +(flet ($P58 (< ?x14 15)) +(flet ($P59 (< ?x18 29)) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or $P55 (not $P53)) $P20) (or (or $P38 (not $P29)) P6)) (or (or $P12 (not $P41)) (not $P47))) (or (or (not $P23) (not P9)) $P57)) (or (or $P19 $P32) $P10)) (or (or (not $P54) $P33) P1)) (or (or (not $P50) $P39) (not P6))) (or (or $P19 $P21) $P58)) (or (or $P13 (not $P25)) (not $P54))) (or (or (not $P21) $P39) $P14)) (or (or (not P0) (not $P32)) $P37)) (or (or P3 (not $P44)) (not $P30))) (or (or (not $P17) $P39) (not $P23))) (or (or (not $P45) (not P7)) (not $P18))) (or (or $P50 $P57) (not $P59))) (or (or $P32 (not $P47)) $P51)) (or (or $P17 (not P8)) (not $P24))) (or (or (not $P39) (not $P47)) (not $P31))) (or (or (not $P25) $P57) $P35)) (or (or (not $P39) $P18) P3)) (or (or (not $P31) $P35) (not P4))) (or (or (not $P46) (not $P22)) $P45)) (or (or P3 $P11) (not $P53))) (or (or (not $P58) (not $P20)) $P41)) (or (or $P42 $P57) P2)) (or (or (not $P10) P1) $P50)) (or (or (not $P49) (not $P58)) $P36)) (or (or $P23 (not $P19)) $P36)) (or (or $P39 (not $P40)) (not $P50))) (or (or P6 (not $P40)) (not $P47))) (or (or (not $P28) (not $P23)) (not $P46))) (or (or (not $P18) (not $P27)) (not $P19))) (or (or (not $P43) P2) $P20)) (or (or (not P3) (not $P44)) (not $P34))) (or (or (not P8) (not $P22)) $P35)) (or (or $P46 $P44) (not $P50))) (or (or $P16 $P50) P7)) (or (or $P34 (not P4)) $P25)) (or (or (not $P31) $P48) $P27)) (or (or $P31 (not P5)) $P22)) (or (or $P22 (not $P39)) (not $P11))) (or (or $P59 (not $P50)) (not $P25))) (or (or (not $P43) (not P6)) $P30)) (or (or (not P8) (not $P40)) $P12)) (or (or (not $P26) $P52) (not $P35))) (or (or $P29 P1) $P34)) (or (or P6 $P30) $P19)) (or (or $P36 $P14) $P19)) (or (or $P38 $P35) (not $P44))) (or (or (not P1) $P13) $P15)) (or (or $P33 (not $P31)) (not $P10))) (or (or (not $P59) (not $P45)) $P47)) (or (or $P52 (not P5)) (not $P50))) (or (or $P45 (not $P33)) (not $P14))) (or (or P3 $P18) $P58)) (or (or $P47 $P44) (not $P55))) (or (or (not $P35) (not $P11)) $P16)) (or (or $P23 $P34) $P11)) (or (or $P52 (not $P18)) (not $P50))) (or (or $P32 (not $P13)) (not $P43))) (or (or (not $P15) (not $P29)) (not $P45))) (or (or $P17 (not $P36)) (not $P21))) (or (or $P32 (not $P31)) (not $P20))) (or (or $P28 (not $P46)) $P27)) (or (or $P19 P8) $P44)) (or (or (not $P21) $P39) $P16)) (or (or (not $P18) $P17) (not $P10))) (or (or $P47 (not $P47)) $P28)) (or (or (not $P57) P5) (not $P18))) (or (or $P33 $P44) (not $P49))) (or (or $P25 (not $P18)) (not P1))) (or (or (not $P47) $P17) $P42)) (or (or (not $P59) $P21) (not $P42))) (or (or (not $P14) $P52) $P51)) (or (or $P20 (not $P30)) $P28)) (or (or (not $P50) (not P1)) $P49)) (or (or $P47 $P17) $P41)) (or (or (not $P35) (not $P18)) (not $P33))) (or (or (not $P16) $P16) $P22)) (or (or P6 $P42) P2)) (or (or (not $P15) (not $P45)) (not $P28))) (or (or (not $P51) $P58) (not $P20))) (or (or $P28 (not P8)) (not $P18))) (or (or (not $P38) P4) (not $P55))) (or (or $P13 $P53) $P56)) (or (or (not $P16) P2) $P38)) (or (or (not P1) P1) $P55)) (or (or (not $P39) $P54) $P34)) (or (or $P50 (not $P30)) (not $P27))) (or (or (not $P50) P9) $P42)) (or (or (not $P26) (not $P12)) $P14)) (or (or (not $P15) (not $P32)) (not $P17))) (or (or $P50 $P59) $P39)) (or (or (not P0) (not $P36)) $P57)) (or (or (not $P56) $P10) (not P6))) (or (or $P52 $P41) $P37)) (or (or $P51 (not $P11)) (not $P33))) (or (or $P18 $P24) $P19)) (or (or $P52 (not $P54)) $P32)) (or (or (not $P36) $P18) $P50))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0100_10_11.smt b/test/regress/regress0/uflra/pb_real_10_0100_10_11.smt new file mode 100644 index 000000000..39b7ed9b1 --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0100_10_11.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status sat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (f1_1 x4)) +(let (?x11 (f1_1 x6)) +(let (?x12 (- (+ (* 4 x1) (* 29 x9)) (* 21 x7))) +(let (?x13 (- (+ (* (- 0 17) x5) (* 27 x1)) (* 12 x3))) +(let (?x14 (- (+ (* (- 0 10) x3) (* 13 x7)) (* 5 x1))) +(let (?x15 (f0_1 x9)) +(let (?x16 (f0_1 x1)) +(let (?x17 (+ (+ (* 17 ?x15) (* 24 x5)) (* 23 ?x16))) +(let (?x18 (f0_2 x6 x5)) +(let (?x19 (f1_2 x0 x0)) +(let (?x20 (- (+ (* (- 0 19) x5) (* 26 x2)) (* 21 ?x12))) +(let (?x21 (f1_2 x7 x8)) +(let (?x22 (- (+ (* 10 ?x18) (* 23 x2)) (* 11 x8))) +(let (?x23 (f0_2 x9 x3)) +(let (?x24 (f1_2 x1 x9)) +(let (?x25 (f0_2 x5 x8)) +(let (?x26 (f1_1 x1)) +(let (?x27 (f0_2 x4 x7)) +(let (?x28 (f1_1 x7)) +(let (?x29 (f1_2 x6 ?x18)) +(let (?x30 (- (- (* (- 0 12) x8) (* 1 x5)) (* 16 x7))) +(let (?x31 (+ (- (* (- 0 29) ?x28) (* 7 ?x19)) (* 7 ?x11))) +(let (?x32 (f1_1 x3)) +(let (?x33 (+ (+ (* (- 0 23) x0) (* 17 x2)) (* 7 x4))) +(let (?x34 (- (+ (* (- 0 21) ?x27) (* 17 x8)) (* 6 ?x23))) +(let (?x35 (+ (+ (* (- 0 14) ?x20) (* 16 ?x30)) (* 8 ?x18))) +(let (?x36 (f0_2 x5 x7)) +(let (?x37 (f1_2 x9 x8)) +(let (?x38 (f1_2 x1 ?x12)) +(let (?x39 (f0_1 x3)) +(let (?x40 (- (- (* (- 0 24) x4) (* 21 x2)) (* 9 x5))) +(let (?x41 (+ (- (* 1 ?x35) (* 3 ?x14)) (* 12 ?x18))) +(let (?x42 (- (+ (* (- 0 11) x9) (* 16 x7)) (* 4 x1))) +(let (?x43 (f1_2 ?x15 ?x14)) +(let (?x44 (f1_2 ?x43 ?x18)) +(let (?x45 (f0_1 x5)) +(let (?x46 (f0_1 x2)) +(let (?x47 (f0_1 x5)) +(let (?x48 (+ (- (* (- 0 8) x2) (* 19 x6)) (* 8 x1))) +(let (?x49 (f1_2 x9 x0)) +(flet ($P10 (= ?x38 ?x18)) +(flet ($P11 (< ?x12 (- 0 20))) +(flet ($P12 (< ?x11 8)) +(flet ($P13 (< ?x39 (- 0 24))) +(flet ($P14 (< x2 (- 0 18))) +(flet ($P15 (= ?x18 x8)) +(flet ($P16 (= ?x37 ?x34)) +(flet ($P17 (< ?x14 (- 0 24))) +(flet ($P18 (= ?x26 ?x33)) +(flet ($P19 (= ?x18 ?x15)) +(flet ($P20 (< ?x35 (- 0 22))) +(flet ($P21 (= ?x41 ?x13)) +(flet ($P22 (< x1 (- 0 27))) +(flet ($P23 (< ?x47 (- 0 27))) +(flet ($P24 (< ?x45 (- 0 10))) +(flet ($P25 (= ?x13 ?x35)) +(flet ($P26 (< ?x17 (- 0 1))) +(flet ($P27 (< x8 3)) +(flet ($P28 (< x7 23)) +(flet ($P29 (< ?x27 (- 0 28))) +(flet ($P30 (< ?x35 (- 0 1))) +(flet ($P31 (< ?x11 15)) +(flet ($P32 (< ?x39 (- 0 17))) +(flet ($P33 (< ?x40 (- 0 28))) +(flet ($P34 (< ?x15 (- 0 8))) +(flet ($P35 (< ?x33 19)) +(flet ($P36 (= ?x41 x6)) +(flet ($P37 (< ?x48 26)) +(flet ($P38 (< ?x46 0)) +(flet ($P39 (< ?x42 9)) +(flet ($P40 (= ?x43 x6)) +(flet ($P41 (< x8 (- 0 13))) +(flet ($P42 (< ?x17 (- 0 26))) +(flet ($P43 (= x4 x5)) +(flet ($P44 (< ?x11 17)) +(flet ($P45 (< ?x12 15)) +(flet ($P46 (< ?x19 1)) +(flet ($P47 (< ?x49 9)) +(flet ($P48 (< x0 (- 0 14))) +(flet ($P49 (< ?x27 22)) +(flet ($P50 (< x6 18)) +(flet ($P51 (< x0 (- 0 15))) +(flet ($P52 (< ?x13 17)) +(flet ($P53 (< ?x19 (- 0 15))) +(flet ($P54 (< x9 6)) +(flet ($P55 (< ?x35 22)) +(flet ($P56 (< x5 (- 0 26))) +(flet ($P57 (< ?x34 5)) +(flet ($P58 (= ?x37 x1)) +(flet ($P59 (< ?x47 (- 0 28))) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or P6 (not $P15)) $P33) (or (or $P42 P6) (not $P12))) (or (or $P19 (not $P50)) P3)) (or (or (not $P11) $P44) $P39)) (or (or P5 $P17) (not $P18))) (or (or P5 (not P2)) P4)) (or (or $P30 $P53) $P33)) (or (or $P27 (not $P22)) $P42)) (or (or (not $P16) $P24) (not $P29))) (or (or (not $P56) $P48) (not $P13))) (or (or $P54 $P53) (not $P41))) (or (or (not $P26) $P40) (not $P36))) (or (or (not $P33) $P21) $P54)) (or (or $P22 P8) (not P7))) (or (or (not $P56) (not $P51)) $P43)) (or (or P6 $P19) (not $P22))) (or (or (not $P31) P4) (not P1))) (or (or (not $P17) (not $P10)) $P48)) (or (or $P40 $P22) (not $P29))) (or (or (not $P21) $P49) $P55)) (or (or $P14 (not $P20)) P5)) (or (or $P41 (not $P44)) (not $P33))) (or (or $P26 $P42) $P46)) (or (or $P53 (not $P23)) (not $P57))) (or (or (not P3) $P35) $P17)) (or (or (not $P13) (not P9)) $P37)) (or (or (not $P14) (not $P14)) $P54)) (or (or $P32 $P29) (not $P28))) (or (or (not $P18) (not $P38)) $P21)) (or (or (not $P59) (not P8)) $P48)) (or (or P5 $P37) (not P3))) (or (or $P10 $P13) (not P4))) (or (or P4 (not $P43)) $P36)) (or (or P5 (not P1)) $P20)) (or (or P6 $P21) (not $P30))) (or (or (not $P24) $P45) (not P5))) (or (or $P38 $P50) (not P1))) (or (or (not P0) $P13) $P19)) (or (or (not $P10) $P22) $P32)) (or (or (not $P25) $P35) (not $P46))) (or (or (not P2) $P21) $P51)) (or (or $P40 (not $P39)) $P10)) (or (or $P13 (not $P20)) $P59)) (or (or $P19 (not $P14)) (not $P46))) (or (or (not $P38) (not $P51)) $P52)) (or (or (not $P48) $P25) P7)) (or (or (not $P36) (not $P59)) $P40)) (or (or (not $P46) $P27) $P10)) (or (or $P10 (not P1)) (not $P17))) (or (or $P54 $P18) (not $P23))) (or (or (not $P28) P3) (not $P42))) (or (or (not $P53) $P47) (not $P56))) (or (or $P23 (not P5)) (not $P31))) (or (or $P47 (not $P49)) $P36)) (or (or $P30 (not $P59)) $P20)) (or (or (not $P33) P1) (not P0))) (or (or (not $P49) $P34) (not $P11))) (or (or (not P3) $P30) (not $P25))) (or (or (not $P59) (not $P47)) (not $P12))) (or (or (not $P39) $P37) (not $P56))) (or (or (not $P58) (not $P48)) (not $P41))) (or (or $P32 $P30) (not $P11))) (or (or $P34 $P12) (not $P41))) (or (or P1 (not $P17)) (not $P59))) (or (or (not $P40) $P15) $P27)) (or (or (not P0) $P58) $P18)) (or (or $P58 $P41) $P30)) (or (or (not $P27) P2) P0)) (or (or (not $P19) $P22) (not $P58))) (or (or $P18 (not $P38)) (not $P31))) (or (or (not $P32) (not $P11)) $P39)) (or (or (not P6) P1) $P15)) (or (or (not $P32) P9) (not $P28))) (or (or (not $P22) $P39) $P30)) (or (or $P54 $P35) $P11)) (or (or $P47 P9) $P54)) (or (or (not $P39) (not $P30)) (not $P58))) (or (or (not $P23) (not $P39)) $P37)) (or (or (not P2) (not $P48)) $P49)) (or (or (not $P19) (not $P45)) (not P5))) (or (or $P20 $P34) (not $P37))) (or (or $P16 $P11) (not $P43))) (or (or $P44 (not $P21)) $P24)) (or (or $P57 P7) $P49)) (or (or $P54 $P11) (not P2))) (or (or (not $P29) $P23) P3)) (or (or (not $P50) $P56) $P33)) (or (or (not $P10) $P56) (not $P19))) (or (or $P21 (not $P39)) (not $P33))) (or (or (not $P33) $P23) P8)) (or (or (not $P58) (not $P29)) $P54)) (or (or (not $P42) (not $P20)) P1)) (or (or P3 $P44) (not P2))) (or (or (not P1) $P19) (not $P18))) (or (or $P53 (not $P23)) (not $P40))) (or (or (not $P55) (not P8)) (not $P38))) (or (or (not P2) $P49) $P58)) (or (or P2 $P20) (not $P27))) (or (or $P51 (not P5)) $P24)) (or (or P2 (not $P59)) (not $P26)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0100_10_15.smt b/test/regress/regress0/uflra/pb_real_10_0100_10_15.smt new file mode 100644 index 000000000..c893c569e --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0100_10_15.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status sat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (f1_1 x4)) +(let (?x11 (f0_2 x0 x0)) +(let (?x12 (- (- (* (- 0 22) x3) (* 6 x9)) (* 14 x6))) +(let (?x13 (+ (- (* (- 0 19) x2) (* 15 ?x10)) (* 12 x4))) +(let (?x14 (f0_1 x7)) +(let (?x15 (f1_2 x5 x7)) +(let (?x16 (f1_2 x8 x8)) +(let (?x17 (f1_2 x0 x9)) +(let (?x18 (f1_2 ?x10 x3)) +(let (?x19 (f0_2 x7 x9)) +(let (?x20 (f0_2 x7 x9)) +(let (?x21 (- (- (* (- 0 6) x7) (* 5 x6)) (* 9 x2))) +(let (?x22 (f0_2 x5 x5)) +(let (?x23 (f1_2 x9 x0)) +(let (?x24 (f0_1 x7)) +(let (?x25 (f0_1 x5)) +(let (?x26 (f0_1 x7)) +(let (?x27 (+ (- (* 13 x6) (* 27 x1)) (* 4 x7))) +(let (?x28 (f0_1 x8)) +(let (?x29 (f1_2 x3 x0)) +(let (?x30 (+ (+ (* (- 0 10) x7) (* 23 x1)) (* 4 x4))) +(let (?x31 (+ (+ (* (- 0 4) x7) (* 6 x7)) (* 2 x1))) +(let (?x32 (f1_2 x0 x7)) +(let (?x33 (f1_1 x9)) +(let (?x34 (f1_2 ?x23 ?x25)) +(let (?x35 (f1_1 x5)) +(let (?x36 (f1_2 x7 x4)) +(let (?x37 (f0_2 x0 x7)) +(let (?x38 (+ (+ (* 25 ?x36) (* 20 x2)) (* 23 ?x27))) +(let (?x39 (f1_2 x2 x1)) +(let (?x40 (+ (- (* 29 ?x11) (* 29 ?x32)) (* 20 ?x15))) +(let (?x41 (f1_2 ?x33 ?x18)) +(let (?x42 (+ (+ (* (- 0 13) ?x21) (* 22 ?x23)) (* 9 x6))) +(let (?x43 (f1_1 x9)) +(let (?x44 (f0_1 x9)) +(let (?x45 (+ (+ (* 20 ?x15) (* 4 ?x34)) (* 22 ?x22))) +(let (?x46 (- (- (* (- 0 14) x7) (* 21 x6)) (* 21 x2))) +(let (?x47 (f0_2 x1 x7)) +(let (?x48 (f1_1 x3)) +(let (?x49 (f1_1 x2)) +(flet ($P10 (< ?x35 (- 0 29))) +(flet ($P11 (< ?x38 21)) +(flet ($P12 (< ?x28 (- 0 6))) +(flet ($P13 (= ?x27 ?x12)) +(flet ($P14 (= ?x41 ?x32)) +(flet ($P15 (< x0 (- 0 9))) +(flet ($P16 (< x0 (- 0 3))) +(flet ($P17 (< ?x25 26)) +(flet ($P18 (< ?x13 2)) +(flet ($P19 (< ?x30 (- 0 29))) +(flet ($P20 (< ?x33 (- 0 26))) +(flet ($P21 (< ?x17 0)) +(flet ($P22 (< x5 0)) +(flet ($P23 (< ?x42 0)) +(flet ($P24 (< ?x27 (- 0 13))) +(flet ($P25 (< ?x22 28)) +(flet ($P26 (< ?x26 (- 0 6))) +(flet ($P27 (< ?x24 11)) +(flet ($P28 (< ?x41 6)) +(flet ($P29 (< ?x18 (- 0 23))) +(flet ($P30 (= ?x31 ?x26)) +(flet ($P31 (< ?x19 (- 0 10))) +(flet ($P32 (< ?x47 19)) +(flet ($P33 (= ?x22 ?x26)) +(flet ($P34 (< ?x31 (- 0 1))) +(flet ($P35 (< ?x16 6)) +(flet ($P36 (< x0 18)) +(flet ($P37 (< x8 28)) +(flet ($P38 (< ?x27 21)) +(flet ($P39 (< ?x32 12)) +(flet ($P40 (= ?x32 ?x27)) +(flet ($P41 (< ?x31 16)) +(flet ($P42 (< ?x47 15)) +(flet ($P43 (< ?x36 8)) +(flet ($P44 (< ?x16 13)) +(flet ($P45 (< ?x23 19)) +(flet ($P46 (< ?x10 13)) +(flet ($P47 (= ?x48 ?x38)) +(flet ($P48 (< ?x20 (- 0 7))) +(flet ($P49 (< ?x21 (- 0 10))) +(flet ($P50 (< ?x33 (- 0 7))) +(flet ($P51 (= ?x32 ?x41)) +(flet ($P52 (< ?x45 18)) +(flet ($P53 (< ?x38 (- 0 13))) +(flet ($P54 (< x1 21)) +(flet ($P55 (= ?x31 ?x30)) +(flet ($P56 (< ?x11 28)) +(flet ($P57 (< ?x48 (- 0 12))) +(flet ($P58 (= x3 ?x28)) +(flet ($P59 (< x6 (- 0 19))) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not P8) (not $P18)) $P23) (or (or $P24 $P37) $P41)) (or (or (not $P29) (not $P37)) (not P2))) (or (or $P41 (not P3)) P0)) (or (or $P15 (not $P36)) (not $P41))) (or (or (not $P21) $P58) P1)) (or (or (not $P58) $P31) $P19)) (or (or $P39 (not $P18)) (not $P53))) (or (or (not $P47) P4) (not P2))) (or (or (not P7) (not $P26)) $P37)) (or (or $P19 (not $P51)) (not $P33))) (or (or (not $P15) (not P3)) $P52)) (or (or $P41 $P12) (not P9))) (or (or $P53 (not $P32)) (not $P34))) (or (or (not $P13) (not $P31)) (not $P16))) (or (or $P25 $P34) $P28)) (or (or $P28 (not $P25)) (not $P14))) (or (or $P38 $P56) (not $P36))) (or (or (not $P23) $P42) (not $P50))) (or (or (not $P43) $P53) $P34)) (or (or (not $P46) $P28) (not $P30))) (or (or (not $P50) $P39) $P17)) (or (or $P51 (not P1)) $P15)) (or (or P8 (not $P47)) (not $P45))) (or (or P1 (not P7)) $P29)) (or (or (not $P37) (not $P28)) (not $P11))) (or (or (not $P22) $P39) $P21)) (or (or $P28 $P20) (not $P16))) (or (or (not $P49) $P29) $P41)) (or (or $P42 (not $P13)) (not $P41))) (or (or (not $P25) $P29) (not $P56))) (or (or $P37 $P38) $P15)) (or (or (not P3) (not $P47)) $P57)) (or (or $P50 $P27) (not $P48))) (or (or (not P3) (not P2)) $P52)) (or (or $P18 (not P9)) (not $P41))) (or (or (not P3) $P44) (not $P56))) (or (or $P50 $P11) P4)) (or (or (not $P50) $P53) P1)) (or (or $P55 (not $P39)) (not $P58))) (or (or $P13 (not $P51)) $P50)) (or (or (not P5) $P31) $P24)) (or (or $P40 $P15) $P42)) (or (or $P35 $P23) (not $P30))) (or (or $P58 $P32) (not $P35))) (or (or $P40 (not $P33)) $P45)) (or (or (not $P28) P6) $P16)) (or (or P1 $P48) P6)) (or (or P4 P2) (not $P38))) (or (or (not $P31) P1) $P29)) (or (or (not $P49) $P56) $P31)) (or (or (not $P24) $P22) $P49)) (or (or $P38 (not $P45)) (not $P30))) (or (or P2 (not $P52)) (not $P55))) (or (or (not P6) (not P3)) P2)) (or (or $P37 $P28) $P47)) (or (or $P21 (not $P27)) (not $P24))) (or (or $P40 P6) (not $P56))) (or (or $P12 (not $P21)) $P51)) (or (or (not $P14) (not P4)) $P58)) (or (or $P20 $P23) (not $P14))) (or (or (not P7) $P21) $P35)) (or (or (not $P46) (not $P48)) $P16)) (or (or (not $P25) P7) $P54)) (or (or (not $P44) (not $P35)) (not $P51))) (or (or (not $P15) (not $P44)) $P46)) (or (or (not $P49) $P13) P5)) (or (or (not $P40) P2) (not $P21))) (or (or $P44 (not $P10)) (not $P18))) (or (or (not $P48) P6) $P21)) (or (or (not $P22) (not $P30)) (not $P57))) (or (or (not $P16) P1) $P28)) (or (or (not $P33) (not $P58)) (not $P55))) (or (or $P17 (not $P23)) $P34)) (or (or P8 (not $P57)) $P44)) (or (or $P26 $P31) (not $P48))) (or (or $P34 (not P4)) (not $P24))) (or (or (not $P39) $P48) (not $P37))) (or (or $P40 P4) $P38)) (or (or $P44 $P49) (not $P32))) (or (or $P26 (not $P25)) $P43)) (or (or (not P0) (not $P53)) (not $P42))) (or (or (not $P17) (not $P57)) (not $P26))) (or (or $P59 (not $P58)) (not $P50))) (or (or (not $P30) $P41) $P40)) (or (or (not $P13) (not $P43)) (not $P45))) (or (or (not $P27) (not $P17)) $P25)) (or (or P8 $P25) (not $P48))) (or (or $P10 (not $P23)) $P34)) (or (or $P36 (not $P55)) (not $P40))) (or (or $P52 (not P2)) $P18)) (or (or $P49 $P12) $P45)) (or (or P6 (not $P43)) (not P0))) (or (or $P56 (not $P38)) (not $P55))) (or (or (not $P41) (not P8)) (not $P21))) (or (or (not $P42) $P38) (not $P41))) (or (or (not $P46) (not $P12)) $P17)) (or (or $P58 (not $P13)) P2)) (or (or (not $P12) (not $P48)) (not P8))) (or (or $P31 $P32) $P57))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0100_10_16.smt b/test/regress/regress0/uflra/pb_real_10_0100_10_16.smt new file mode 100644 index 000000000..27d44cf58 --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0100_10_16.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status sat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (f0_2 x3 x2)) +(let (?x11 (f1_2 x9 x8)) +(let (?x12 (f1_1 x8)) +(let (?x13 (f0_1 x7)) +(let (?x14 (f0_1 x2)) +(let (?x15 (f0_1 x1)) +(let (?x16 (f0_2 x4 x7)) +(let (?x17 (f1_2 x9 x0)) +(let (?x18 (+ (- (* 13 x7) (* 13 x4)) (* 6 x2))) +(let (?x19 (f0_1 x6)) +(let (?x20 (- (+ (* (- 0 22) x0) (* 19 x7)) (* 20 x1))) +(let (?x21 (f0_2 ?x15 x7)) +(let (?x22 (- (- (* (- 0 18) x4) (* 27 x1)) (* 24 x7))) +(let (?x23 (f0_2 x8 x3)) +(let (?x24 (f1_2 x5 x8)) +(let (?x25 (f0_2 x6 x0)) +(let (?x26 (- (+ (* (- 0 1) x1) (* 9 ?x11)) (* 2 ?x21))) +(let (?x27 (f1_2 x7 x7)) +(let (?x28 (+ (+ (* (- 0 10) x2) (* 5 ?x15)) (* 2 ?x11))) +(let (?x29 (- (- (* (- 0 24) x3) (* 24 x8)) (* 4 x1))) +(let (?x30 (f1_2 ?x22 x4)) +(let (?x31 (f1_1 x2)) +(let (?x32 (- (+ (* 19 ?x10) (* 5 ?x24)) (* 17 x1))) +(let (?x33 (- (- (* 22 x3) (* 6 x9)) (* 13 x2))) +(let (?x34 (f1_2 x8 x5)) +(let (?x35 (- (+ (* (- 0 23) ?x18) (* 17 x8)) (* 19 ?x20))) +(let (?x36 (f0_2 x7 x0)) +(let (?x37 (f1_1 x2)) +(let (?x38 (+ (+ (* (- 0 9) x5) (* 8 x6)) (* 14 x1))) +(let (?x39 (f1_2 ?x35 ?x12)) +(let (?x40 (- (- (* 10 x3) (* 22 x1)) (* 29 x8))) +(let (?x41 (f1_2 ?x30 ?x28)) +(let (?x42 (f0_1 x4)) +(let (?x43 (+ (+ (* 29 x2) (* 1 x3)) (* 3 ?x37))) +(let (?x44 (f1_2 x2 x3)) +(let (?x45 (+ (- (* 10 x4) (* 6 x3)) (* 24 x1))) +(let (?x46 (+ (+ (* (- 0 12) x8) (* 22 x3)) (* 7 x4))) +(let (?x47 (- (+ (* (- 0 28) ?x44) (* 29 ?x16)) (* 5 x7))) +(let (?x48 (f1_1 x6)) +(let (?x49 (f1_1 x8)) +(flet ($P10 (< ?x41 24)) +(flet ($P11 (< ?x22 (- 0 20))) +(flet ($P12 (< ?x10 (- 0 8))) +(flet ($P13 (< ?x46 2)) +(flet ($P14 (< ?x30 9)) +(flet ($P15 (< x9 11)) +(flet ($P16 (< ?x33 1)) +(flet ($P17 (< ?x47 (- 0 19))) +(flet ($P18 (< ?x36 22)) +(flet ($P19 (< ?x20 4)) +(flet ($P20 (< ?x29 29)) +(flet ($P21 (< ?x47 15)) +(flet ($P22 (< ?x11 8)) +(flet ($P23 (< ?x28 24)) +(flet ($P24 (< ?x31 0)) +(flet ($P25 (< ?x11 11)) +(flet ($P26 (< x7 0)) +(flet ($P27 (< ?x30 (- 0 8))) +(flet ($P28 (< ?x36 (- 0 22))) +(flet ($P29 (= ?x33 ?x45)) +(flet ($P30 (= x3 ?x46)) +(flet ($P31 (= ?x29 ?x18)) +(flet ($P32 (= ?x22 ?x17)) +(flet ($P33 (< ?x46 9)) +(flet ($P34 (< ?x32 4)) +(flet ($P35 (= ?x11 ?x41)) +(flet ($P36 (< ?x27 (- 0 15))) +(flet ($P37 (< ?x48 (- 0 11))) +(flet ($P38 (< ?x37 (- 0 29))) +(flet ($P39 (< ?x11 (- 0 9))) +(flet ($P40 (< ?x43 20)) +(flet ($P41 (< ?x30 7)) +(flet ($P42 (< ?x31 (- 0 22))) +(flet ($P43 (< ?x36 (- 0 4))) +(flet ($P44 (< ?x43 13)) +(flet ($P45 (< ?x11 (- 0 16))) +(flet ($P46 (< ?x40 22)) +(flet ($P47 (< x9 (- 0 19))) +(flet ($P48 (< ?x25 12)) +(flet ($P49 (< ?x23 19)) +(flet ($P50 (< x1 (- 0 16))) +(flet ($P51 (= ?x19 x6)) +(flet ($P52 (= x8 ?x43)) +(flet ($P53 (< x4 (- 0 2))) +(flet ($P54 (= ?x14 ?x48)) +(flet ($P55 (< ?x42 (- 0 23))) +(flet ($P56 (< ?x19 3)) +(flet ($P57 (< ?x36 1)) +(flet ($P58 (< ?x26 0)) +(flet ($P59 (< ?x18 (- 0 21))) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not $P53) (not $P57)) (not $P45)) (or (or (not $P48) $P21) (not P2))) (or (or (not $P54) (not $P48)) (not $P37))) (or (or P6 P9) (not $P24))) (or (or $P14 (not $P25)) $P19)) (or (or (not $P52) (not $P25)) (not $P20))) (or (or (not P8) (not $P43)) $P10)) (or (or (not $P37) $P26) (not $P18))) (or (or $P22 (not $P51)) P3)) (or (or (not P0) (not $P58)) $P49)) (or (or $P21 (not $P26)) (not $P20))) (or (or (not $P48) (not $P56)) (not P0))) (or (or (not $P40) $P11) (not $P17))) (or (or (not P5) (not P7)) $P36)) (or (or (not P0) (not $P28)) $P47)) (or (or (not $P13) $P21) (not $P58))) (or (or $P28 (not $P33)) $P47)) (or (or $P48 P4) (not $P44))) (or (or $P11 $P14) $P55)) (or (or $P58 (not $P50)) (not $P41))) (or (or (not $P36) $P46) P1)) (or (or $P29 $P28) $P41)) (or (or (not $P43) P8) (not P3))) (or (or (not $P41) (not P6)) $P49)) (or (or $P13 (not $P14)) (not $P46))) (or (or $P28 $P47) $P35)) (or (or (not $P19) (not $P37)) (not $P28))) (or (or (not $P17) (not $P28)) (not $P55))) (or (or P8 (not $P30)) $P38)) (or (or (not $P51) $P34) $P53)) (or (or P5 $P34) (not $P54))) (or (or (not $P38) $P45) (not $P23))) (or (or (not $P51) $P28) (not $P44))) (or (or $P28 $P31) (not $P41))) (or (or $P25 $P20) $P47)) (or (or $P51 $P37) P5)) (or (or (not $P28) $P22) (not $P26))) (or (or (not $P32) (not $P20)) $P35)) (or (or P7 $P49) (not $P13))) (or (or (not $P32) $P30) (not P8))) (or (or P8 (not $P30)) P9)) (or (or (not $P22) (not $P20)) $P48)) (or (or $P31 $P53) (not P6))) (or (or $P57 $P18) P4)) (or (or $P50 P2) (not $P13))) (or (or P0 $P16) (not $P23))) (or (or $P43 (not $P21)) $P31)) (or (or $P20 $P18) $P30)) (or (or (not $P52) (not P3)) $P48)) (or (or (not $P29) $P36) P8)) (or (or (not P8) (not $P24)) (not $P56))) (or (or $P40 (not $P29)) (not $P27))) (or (or (not $P35) $P56) (not $P11))) (or (or (not $P11) (not $P59)) (not $P28))) (or (or (not P7) $P28) $P11)) (or (or (not $P16) $P29) (not P0))) (or (or $P58 (not $P32)) $P18)) (or (or (not $P23) (not $P10)) (not P9))) (or (or $P38 (not $P15)) $P29)) (or (or (not P8) (not $P13)) (not P1))) (or (or (not $P39) (not $P38)) (not $P17))) (or (or $P53 $P46) (not P9))) (or (or $P40 (not $P49)) (not P8))) (or (or $P32 (not $P22)) $P44)) (or (or (not P7) (not $P47)) (not $P24))) (or (or $P10 $P20) (not $P26))) (or (or (not $P38) (not $P39)) (not $P58))) (or (or (not $P33) $P15) $P47)) (or (or (not $P48) $P38) P9)) (or (or $P39 (not $P15)) (not $P21))) (or (or (not $P56) $P11) (not $P37))) (or (or (not $P18) $P23) $P26)) (or (or $P59 P2) P6)) (or (or $P27 $P26) (not $P18))) (or (or (not $P45) (not P7)) (not $P16))) (or (or $P31 $P26) (not $P41))) (or (or $P29 $P55) (not $P32))) (or (or $P42 $P12) (not $P15))) (or (or (not $P55) $P57) (not $P25))) (or (or $P18 (not $P19)) P0)) (or (or $P55 (not $P44)) $P37)) (or (or $P38 (not $P37)) $P25)) (or (or P9 $P22) $P15)) (or (or (not $P14) (not $P52)) (not P1))) (or (or $P39 $P41) (not $P52))) (or (or $P39 $P48) (not P1))) (or (or (not $P55) (not $P11)) $P42)) (or (or (not $P57) (not $P15)) (not P6))) (or (or $P24 $P15) $P16)) (or (or $P45 $P41) (not $P14))) (or (or (not $P52) $P45) P2)) (or (or (not P9) $P36) (not $P34))) (or (or (not $P46) (not $P29)) P4)) (or (or $P10 (not $P15)) $P32)) (or (or (not $P30) P1) $P47)) (or (or (not $P14) (not P3)) $P28)) (or (or $P22 (not $P48)) P3)) (or (or (not $P16) $P37) (not $P35))) (or (or $P20 (not $P46)) (not $P38))) (or (or $P38 (not $P53)) $P25))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0100_10_19.smt b/test/regress/regress0/uflra/pb_real_10_0100_10_19.smt new file mode 100644 index 000000000..a9b0fad39 --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0100_10_19.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status sat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (f1_1 x3)) +(let (?x11 (f1_1 x5)) +(let (?x12 (f1_1 x9)) +(let (?x13 (- (- (* (- 0 13) x7) (* 1 x6)) (* 15 x8))) +(let (?x14 (f0_2 x7 x6)) +(let (?x15 (- (+ (* 26 x9) (* 23 x7)) (* 22 x8))) +(let (?x16 (- (- (* 23 x4) (* 22 x3)) (* 15 x9))) +(let (?x17 (f0_1 x9)) +(let (?x18 (+ (- (* (- 0 12) x3) (* 15 x6)) (* 17 x9))) +(let (?x19 (f1_1 x1)) +(let (?x20 (f1_1 ?x13)) +(let (?x21 (- (- (* 10 x9) (* 11 x5)) (* 3 x3))) +(let (?x22 (- (- (* (- 0 12) x1) (* 14 ?x17)) (* 24 x3))) +(let (?x23 (f0_2 ?x12 ?x13)) +(let (?x24 (f0_2 x3 x1)) +(let (?x25 (+ (+ (* 16 ?x17) (* 10 ?x16)) (* 26 ?x15))) +(let (?x26 (- (- (* (- 0 4) x6) (* 9 x7)) (* 23 x5))) +(let (?x27 (f1_1 x9)) +(let (?x28 (f0_1 x8)) +(let (?x29 (f1_2 x5 x5)) +(let (?x30 (- (+ (* (- 0 9) x8) (* 19 x9)) (* 25 x2))) +(let (?x31 (f1_2 x8 ?x12)) +(let (?x32 (+ (+ (* 10 x4) (* 18 x2)) (* 23 x5))) +(let (?x33 (+ (+ (* 4 ?x31) (* 26 x7)) (* 13 ?x32))) +(let (?x34 (f0_2 x7 x0)) +(let (?x35 (- (+ (* (- 0 14) x6) (* 1 ?x11)) (* 15 ?x20))) +(let (?x36 (f0_1 x6)) +(let (?x37 (+ (+ (* 3 x3) (* 4 x5)) (* 29 x0))) +(let (?x38 (f1_1 x5)) +(let (?x39 (f1_1 x0)) +(let (?x40 (f1_1 x2)) +(let (?x41 (f0_1 x5)) +(let (?x42 (- (- (* 29 ?x22) (* 2 ?x29)) (* 3 ?x10))) +(let (?x43 (+ (+ (* 2 x3) (* 25 x2)) (* 27 x0))) +(let (?x44 (- (+ (* (- 0 11) x8) (* 26 ?x36)) (* 1 ?x28))) +(let (?x45 (f0_2 x8 x5)) +(let (?x46 (+ (- (* 29 x9) (* 26 x3)) (* 27 x7))) +(let (?x47 (f1_1 x2)) +(let (?x48 (f1_2 ?x11 ?x13)) +(let (?x49 (f0_1 x2)) +(flet ($P10 (= x9 x5)) +(flet ($P11 (< x4 24)) +(flet ($P12 (< x5 (- 0 25))) +(flet ($P13 (< x1 (- 0 16))) +(flet ($P14 (< ?x13 (- 0 15))) +(flet ($P15 (< ?x13 3)) +(flet ($P16 (< ?x41 21)) +(flet ($P17 (= ?x28 ?x32)) +(flet ($P18 (< x9 (- 0 1))) +(flet ($P19 (< ?x10 8)) +(flet ($P20 (< x4 (- 0 22))) +(flet ($P21 (< ?x47 6)) +(flet ($P22 (< x2 (- 0 26))) +(flet ($P23 (< ?x41 22)) +(flet ($P24 (< ?x25 22)) +(flet ($P25 (< x7 (- 0 3))) +(flet ($P26 (< ?x25 23)) +(flet ($P27 (< x8 (- 0 1))) +(flet ($P28 (< x6 (- 0 13))) +(flet ($P29 (< x4 (- 0 24))) +(flet ($P30 (< x6 (- 0 15))) +(flet ($P31 (< ?x44 (- 0 14))) +(flet ($P32 (< ?x10 (- 0 16))) +(flet ($P33 (< ?x21 28)) +(flet ($P34 (< ?x17 27)) +(flet ($P35 (< ?x31 26)) +(flet ($P36 (= ?x47 ?x24)) +(flet ($P37 (< ?x49 27)) +(flet ($P38 (< ?x36 (- 0 7))) +(flet ($P39 (= ?x32 ?x23)) +(flet ($P40 (< ?x23 24)) +(flet ($P41 (< ?x35 12)) +(flet ($P42 (< ?x35 17)) +(flet ($P43 (< ?x34 (- 0 2))) +(flet ($P44 (= x5 ?x37)) +(flet ($P45 (< ?x14 22)) +(flet ($P46 (< ?x24 6)) +(flet ($P47 (< ?x14 (- 0 14))) +(flet ($P48 (< ?x22 (- 0 11))) +(flet ($P49 (< ?x32 7)) +(flet ($P50 (< ?x38 (- 0 18))) +(flet ($P51 (< ?x20 (- 0 3))) +(flet ($P52 (< ?x46 (- 0 1))) +(flet ($P53 (< ?x35 11)) +(flet ($P54 (= ?x37 ?x30)) +(flet ($P55 (< ?x36 29)) +(flet ($P56 (= ?x23 ?x21)) +(flet ($P57 (< ?x16 (- 0 29))) +(flet ($P58 (< ?x39 (- 0 9))) +(flet ($P59 (< ?x43 29)) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not $P28) (not $P43)) $P54) (or (or $P33 (not $P28)) $P32)) (or (or (not $P41) (not $P41)) P9)) (or (or (not $P54) (not $P49)) (not $P21))) (or (or $P43 (not $P17)) $P16)) (or (or (not P7) (not $P46)) (not $P58))) (or (or (not $P25) $P56) P4)) (or (or $P54 (not $P20)) $P38)) (or (or $P42 (not P1)) (not $P53))) (or (or $P23 $P40) (not $P32))) (or (or P2 $P52) $P57)) (or (or (not P5) $P15) (not P7))) (or (or (not $P16) (not P5)) $P44)) (or (or $P35 $P34) (not P8))) (or (or $P37 $P23) P8)) (or (or $P42 (not $P18)) $P48)) (or (or (not $P54) (not $P59)) $P48)) (or (or (not $P10) (not $P12)) $P47)) (or (or (not $P16) (not $P53)) (not P7))) (or (or (not $P17) $P21) P2)) (or (or (not $P55) (not $P54)) $P29)) (or (or $P48 $P42) $P32)) (or (or $P29 $P29) (not $P58))) (or (or (not $P25) $P13) (not $P37))) (or (or (not $P58) (not $P46)) $P34)) (or (or $P42 $P53) $P44)) (or (or (not $P22) (not $P48)) $P52)) (or (or P7 $P50) $P14)) (or (or $P27 (not $P20)) (not $P24))) (or (or P0 $P57) (not $P18))) (or (or $P13 $P37) (not $P24))) (or (or $P51 (not P2)) $P41)) (or (or (not $P22) (not $P48)) $P34)) (or (or (not $P26) $P33) (not $P23))) (or (or (not $P33) (not $P51)) P4)) (or (or $P52 (not $P38)) (not $P31))) (or (or (not $P48) (not $P29)) (not $P56))) (or (or P7 (not $P58)) P2)) (or (or (not $P35) P1) P0)) (or (or $P35 $P14) $P33)) (or (or (not $P33) $P10) $P25)) (or (or (not $P39) (not $P57)) (not $P33))) (or (or $P17 (not $P17)) (not $P56))) (or (or (not $P17) (not $P17)) $P56)) (or (or $P52 (not $P55)) $P47)) (or (or $P47 $P57) (not $P32))) (or (or $P15 $P37) $P21)) (or (or (not $P39) (not $P43)) (not $P54))) (or (or $P40 P2) (not $P55))) (or (or $P11 $P52) (not $P31))) (or (or (not $P36) $P46) $P57)) (or (or P7 (not P2)) (not $P24))) (or (or (not $P41) $P28) P8)) (or (or (not $P36) (not P4)) P0)) (or (or (not $P18) $P28) $P39)) (or (or $P59 $P29) $P23)) (or (or (not P8) $P49) (not $P31))) (or (or (not $P49) $P20) (not P8))) (or (or $P39 (not $P54)) $P14)) (or (or (not $P31) $P48) (not $P25))) (or (or (not $P30) (not $P58)) $P56)) (or (or P8 (not $P50)) $P44)) (or (or (not $P25) (not $P31)) (not P6))) (or (or (not $P49) $P49) (not $P56))) (or (or (not $P20) (not $P48)) (not $P29))) (or (or $P29 (not $P16)) (not $P24))) (or (or $P28 $P10) $P27)) (or (or (not P6) $P40) $P10)) (or (or $P34 $P46) $P39)) (or (or (not $P41) $P30) $P15)) (or (or $P33 (not $P58)) (not $P12))) (or (or (not $P32) (not P1)) $P26)) (or (or (not $P30) $P38) $P20)) (or (or (not $P44) (not $P30)) (not $P39))) (or (or (not $P39) $P24) $P18)) (or (or $P43 (not P4)) $P46)) (or (or $P59 $P21) (not $P57))) (or (or P8 $P32) $P46)) (or (or (not $P33) (not $P20)) (not P7))) (or (or $P39 P8) $P42)) (or (or (not $P53) (not $P16)) (not P9))) (or (or (not $P12) $P54) (not $P10))) (or (or (not $P11) $P56) $P33)) (or (or (not $P53) $P17) (not P6))) (or (or $P48 (not $P11)) (not $P10))) (or (or $P37 $P57) (not $P53))) (or (or (not P8) (not $P36)) P6)) (or (or $P11 $P26) (not $P17))) (or (or $P23 $P52) (not $P42))) (or (or (not $P36) (not P1)) (not $P34))) (or (or (not $P46) (not $P18)) $P17)) (or (or P5 (not $P33)) (not $P27))) (or (or (not $P15) (not $P11)) $P58)) (or (or $P20 $P28) $P48)) (or (or $P53 $P46) $P15)) (or (or $P51 (not $P34)) P4)) (or (or (not $P24) $P46) (not $P23))) (or (or $P37 $P45) (not $P42))) (or (or P0 $P23) $P29)) (or (or (not P0) (not $P12)) $P41))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt new file mode 100644 index 000000000..4508d1f85 --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status unsat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (f0_1 x3)) +(let (?x11 (f0_1 x4)) +(let (?x12 (f1_2 x7 x0)) +(let (?x13 (- (- (* (- 0 11) x9) (* 21 x4)) (* 11 x7))) +(let (?x14 (- (+ (* 26 x3) (* 17 x5)) (* 1 x6))) +(let (?x15 (- (+ (* 18 x2) (* 9 x9)) (* 7 x6))) +(let (?x16 (- (- (* 24 x6) (* 9 x9)) (* 13 x5))) +(let (?x17 (+ (- (* 13 x0) (* 15 x3)) (* 6 x2))) +(let (?x18 (f0_1 x6)) +(let (?x19 (f0_2 x1 x6)) +(let (?x20 (- (+ (* 29 x6) (* 21 x7)) (* 25 x9))) +(let (?x21 (+ (+ (* (- 0 18) x6) (* 13 x5)) (* 2 x7))) +(let (?x22 (+ (+ (* 16 x0) (* 10 x1)) (* 15 x3))) +(let (?x23 (f1_2 x5 x0)) +(let (?x24 (- (+ (* 2 x8) (* 27 x5)) (* 9 x0))) +(let (?x25 (- (+ (* (- 0 27) x1) (* 23 x9)) (* 22 x5))) +(let (?x26 (f0_2 ?x21 x6)) +(let (?x27 (f1_1 x7)) +(let (?x28 (f0_2 ?x14 ?x17)) +(let (?x29 (- (+ (* 26 ?x10) (* 24 ?x26)) (* 6 x7))) +(let (?x30 (f0_2 x1 x0)) +(let (?x31 (f1_2 x8 x5)) +(let (?x32 (f1_1 ?x21)) +(let (?x33 (f1_1 ?x14)) +(let (?x34 (f0_2 x8 x7)) +(let (?x35 (f0_2 ?x33 ?x31)) +(let (?x36 (+ (- (* (- 0 13) x3) (* 8 x9)) (* 6 x4))) +(let (?x37 (- (- (* (- 0 9) x1) (* 22 x3)) (* 19 x8))) +(let (?x38 (f0_2 x2 x9)) +(let (?x39 (f0_2 ?x13 ?x11)) +(let (?x40 (f1_2 x0 x7)) +(let (?x41 (f1_1 x2)) +(let (?x42 (f0_1 x1)) +(let (?x43 (f1_2 x7 x4)) +(let (?x44 (+ (+ (* 7 x5) (* 15 x5)) (* 24 x0))) +(let (?x45 (+ (+ (* 27 x7) (* 22 x9)) (* 24 x6))) +(let (?x46 (f1_2 x8 x6)) +(let (?x47 (+ (+ (* (- 0 24) x6) (* 13 x2)) (* 15 x7))) +(let (?x48 (f0_2 ?x26 ?x43)) +(let (?x49 (+ (+ (* 15 x2) (* 6 x5)) (* 10 x9))) +(flet ($P10 (< ?x36 (- 0 5))) +(flet ($P11 (< ?x48 (- 0 26))) +(flet ($P12 (< ?x34 6)) +(flet ($P13 (< ?x29 13)) +(flet ($P14 (< ?x17 20)) +(flet ($P15 (< x4 (- 0 27))) +(flet ($P16 (< ?x39 (- 0 11))) +(flet ($P17 (< ?x49 (- 0 25))) +(flet ($P18 (< ?x11 10)) +(flet ($P19 (< ?x35 (- 0 28))) +(flet ($P20 (< x6 6)) +(flet ($P21 (< ?x37 10)) +(flet ($P22 (< ?x25 9)) +(flet ($P23 (< ?x29 (- 0 5))) +(flet ($P24 (< ?x44 (- 0 25))) +(flet ($P25 (< ?x25 28)) +(flet ($P26 (< x5 (- 0 12))) +(flet ($P27 (< ?x45 16)) +(flet ($P28 (= ?x22 ?x10)) +(flet ($P29 (< x5 14)) +(flet ($P30 (= ?x14 ?x14)) +(flet ($P31 (< ?x31 15)) +(flet ($P32 (= ?x12 ?x17)) +(flet ($P33 (< ?x45 (- 0 6))) +(flet ($P34 (< ?x27 (- 0 25))) +(flet ($P35 (= ?x46 ?x13)) +(flet ($P36 (= ?x33 ?x48)) +(flet ($P37 (< ?x49 (- 0 23))) +(flet ($P38 (= ?x29 ?x45)) +(flet ($P39 (< ?x14 (- 0 20))) +(flet ($P40 (< ?x37 12)) +(flet ($P41 (< x1 (- 0 4))) +(flet ($P42 (< x1 29)) +(flet ($P43 (< ?x29 8)) +(flet ($P44 (< ?x20 (- 0 26))) +(flet ($P45 (< ?x23 0)) +(flet ($P46 (= x4 ?x15)) +(flet ($P47 (< ?x19 9)) +(flet ($P48 (< ?x43 4)) +(flet ($P49 (< ?x45 16)) +(flet ($P50 (< ?x16 (- 0 8))) +(flet ($P51 (< ?x37 (- 0 18))) +(flet ($P52 (< ?x27 10)) +(flet ($P53 (= ?x40 ?x30)) +(flet ($P54 (< ?x20 26)) +(flet ($P55 (< ?x34 11)) +(flet ($P56 (= ?x39 ?x49)) +(flet ($P57 (< ?x43 (- 0 22))) +(flet ($P58 (< ?x46 (- 0 3))) +(flet ($P59 (< x7 (- 0 22))) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not P8) $P49) $P33) (or (or (not P2) $P55) (not $P51))) (or (or (not P8) $P17) (not $P28))) (or (or (not $P50) (not $P17)) (not $P39))) (or (or (not $P26) $P48) (not $P13))) (or (or $P55 (not $P31)) $P38)) (or (or $P30 $P17) (not $P11))) (or (or (not $P40) (not $P17)) $P24)) (or (or $P41 $P20) P4)) (or (or $P33 (not P7)) $P31)) (or (or P4 $P43) $P11)) (or (or $P25 P7) (not $P54))) (or (or (not $P11) (not $P59)) (not $P35))) (or (or (not $P54) (not $P54)) $P34)) (or (or $P46 $P48) (not $P43))) (or (or (not $P50) $P49) (not $P36))) (or (or (not $P50) $P25) (not $P54))) (or (or (not $P43) (not $P37)) (not $P38))) (or (or (not $P21) (not $P38)) $P29)) (or (or (not $P13) (not $P36)) $P11)) (or (or (not $P50) (not $P15)) $P23)) (or (or $P57 $P23) $P52)) (or (or $P27 $P44) (not $P30))) (or (or (not P8) (not $P46)) (not $P32))) (or (or (not $P51) (not $P49)) (not $P16))) (or (or (not $P35) (not $P12)) (not $P38))) (or (or (not $P28) $P37) (not $P20))) (or (or $P59 $P36) (not $P28))) (or (or (not $P58) (not $P43)) (not $P45))) (or (or (not $P32) (not $P58)) P3)) (or (or (not P5) (not $P58)) $P55)) (or (or $P51 $P53) (not $P18))) (or (or $P21 $P43) (not $P19))) (or (or (not $P26) (not $P55)) (not $P30))) (or (or $P46 $P40) $P55)) (or (or $P14 $P30) (not $P35))) (or (or P3 $P44) (not $P50))) (or (or $P46 (not $P33)) (not $P54))) (or (or (not $P44) $P53) (not $P20))) (or (or (not $P29) $P44) $P50)) (or (or (not $P48) (not $P19)) $P40)) (or (or (not $P49) P8) $P29)) (or (or $P58 (not P2)) $P37)) (or (or $P11 (not $P52)) P2)) (or (or $P43 $P50) (not $P37))) (or (or $P19 $P43) P0)) (or (or (not $P17) $P51) (not $P29))) (or (or P0 (not $P57)) (not $P11))) (or (or (not $P39) $P10) $P42)) (or (or (not $P14) (not $P42)) (not $P21))) (or (or $P43 P8) $P19)) (or (or (not $P21) P3) $P38)) (or (or P5 (not $P33)) (not $P10))) (or (or (not $P35) (not $P28)) $P44)) (or (or $P47 (not $P53)) $P20)) (or (or $P54 (not $P21)) (not $P23))) (or (or (not P0) (not $P35)) $P24)) (or (or $P35 $P45) (not P7))) (or (or (not $P54) (not $P46)) (not $P49))) (or (or (not $P55) $P21) $P43)) (or (or (not $P16) $P36) (not $P19))) (or (or (not P1) $P48) (not $P44))) (or (or (not $P10) $P54) $P43)) (or (or (not $P14) (not $P43)) $P18)) (or (or P0 $P43) $P38)) (or (or (not $P38) (not $P43)) (not $P46))) (or (or P0 (not $P19)) (not $P12))) (or (or $P14 $P56) $P58)) (or (or $P51 $P56) (not $P12))) (or (or $P59 $P34) (not $P26))) (or (or (not P4) $P50) $P42)) (or (or $P38 (not $P44)) $P58)) (or (or $P53 (not P1)) (not $P37))) (or (or (not P2) $P20) $P23)) (or (or P3 $P47) $P18)) (or (or $P49 (not $P11)) $P34)) (or (or (not $P38) $P34) $P21)) (or (or (not $P32) $P17) (not $P22))) (or (or (not $P13) $P29) $P58)) (or (or (not $P24) $P52) (not $P44))) (or (or (not $P16) $P30) (not $P38))) (or (or (not $P22) (not $P23)) (not $P31))) (or (or (not $P57) (not $P31)) $P18)) (or (or $P38 $P46) $P19)) (or (or $P38 $P23) (not $P24))) (or (or $P30 $P34) (not $P51))) (or (or (not $P50) $P42) (not $P41))) (or (or (not P7) (not $P37)) (not $P31))) (or (or (not $P42) $P38) (not $P27))) (or (or (not $P29) $P54) (not $P58))) (or (or $P44 $P18) $P21)) (or (or $P35 (not P4)) $P15)) (or (or $P14 $P38) $P17)) (or (or (not $P51) (not P4)) (not $P46))) (or (or (not $P50) $P16) (not $P27))) (or (or (not $P13) $P52) $P17)) (or (or (not $P57) (not $P24)) (not $P32))) (or (or (not $P12) $P14) (not P7))) (or (or $P39 $P28) (not $P25))) (or (or $P30 (not P4)) P8)) (or (or $P22 P9) (not $P59))) (or (or (not $P18) $P56) (not $P13))) (or (or $P20 (not $P32)) $P33)) (or (or (not $P23) $P52) P1)) (or (or $P11 (not $P20)) (not P9))) (or (or (not $P14) (not $P14)) $P59)) (or (or $P40 (not P9)) (not $P12))) (or (or (not $P14) (not $P33)) (not $P45))) (or (or (not $P17) (not P7)) (not $P54))) (or (or (not $P55) $P55) P5)) (or (or $P21 $P28) (not $P31))) (or (or $P50 $P26) $P20)) (or (or $P27 $P30) (not $P49))) (or (or P0 (not $P48)) $P58)) (or (or $P39 $P57) (not $P49))) (or (or (not $P20) $P28) (not $P10))) (or (or $P57 $P23) (not P1))) (or (or P5 $P25) $P11)) (or (or (not P8) (not $P47)) (not $P56))) (or (or $P26 (not P3)) (not $P27))) (or (or (not $P58) P5) (not P0))) (or (or $P12 P2) $P27)) (or (or $P22 $P58) (not $P57))) (or (or $P47 (not $P11)) $P33)) (or (or $P22 (not $P14)) $P13)) (or (or (not P0) (not $P23)) $P47)) (or (or (not $P50) $P15) (not $P32))) (or (or (not $P32) $P52) (not $P33))) (or (or (not $P58) $P46) $P26)) (or (or $P45 (not $P18)) (not $P26))) (or (or $P47 P6) (not $P37))) (or (or (not $P43) P1) (not $P36))) (or (or (not P0) (not $P49)) $P30)) (or (or (not $P59) (not P3)) (not $P52))) (or (or (not $P48) $P18) $P46)) (or (or (not P5) (not $P10)) $P43)) (or (or $P42 $P12) $P45)) (or (or $P57 (not $P18)) $P29)) (or (or $P41 P1) $P56)) (or (or (not $P43) (not $P16)) (not P2))) (or (or (not $P17) $P51) $P15)) (or (or $P31 (not $P23)) P7)) (or (or (not $P27) (not $P49)) (not P5))) (or (or (not $P13) $P57) (not $P56))) (or (or P7 P9) $P15)) (or (or (not $P54) $P52) (not $P17))) (or (or P8 (not $P35)) (not $P52))) (or (or $P25 (not $P16)) P5)) (or (or $P15 $P13) (not $P34))) (or (or (not P7) (not $P14)) $P22)) (or (or $P25 $P43) P3)) (or (or (not $P38) $P18) $P48)) (or (or P7 $P46) (not $P31))) (or (or (not $P47) (not $P16)) (not $P43))) (or (or P8 (not $P41)) P7)) (or (or (not $P35) (not P1)) (not P4))) (or (or $P56 $P48) $P26)) (or (or (not $P41) P3) (not $P53))) (or (or (not $P36) P1) (not $P56))) (or (or $P25 P1) $P23)) (or (or (not $P35) $P39) P9)) (or (or (not $P40) $P41) (not $P52))) (or (or (not $P34) (not $P13)) $P37)) (or (or P0 (not $P25)) (not P8))) (or (or (not $P31) (not $P41)) (not P8))) (or (or P7 P4) $P39)) (or (or (not $P33) (not $P39)) (not $P57))) (or (or $P24 (not $P13)) (not $P38))) (or (or $P58 $P29) P2)) (or (or (not $P50) (not $P38)) $P43)) (or (or (not $P44) $P37) $P11)) (or (or $P14 (not $P53)) (not $P47))) (or (or $P29 P2) (not $P24))) (or (or (not $P45) (not $P10)) $P50)) (or (or $P38 (not $P54)) (not $P18))) (or (or (not $P19) $P41) (not P4))) (or (or $P37 $P10) (not $P50))) (or (or (not $P48) $P41) $P47)) (or (or (not $P17) $P28) $P27)) (or (or (not $P17) (not $P35)) $P43)) (or (or (not $P24) $P12) $P11)) (or (or P5 (not $P24)) (not P1))) (or (or $P28 (not $P29)) (not P5))) (or (or (not $P30) (not $P22)) $P40)) (or (or (not $P47) P2) $P58)) (or (or $P22 (not $P26)) $P12)) (or (or (not $P38) (not $P59)) (not $P23))) (or (or (not P8) $P58) (not $P39))) (or (or $P51 $P41) $P21)) (or (or (not $P20) $P57) (not $P42))) (or (or $P38 $P17) (not $P52))) (or (or (not P1) $P25) (not $P58))) (or (or (not $P20) P2) $P47)) (or (or (not $P11) (not $P37)) (not $P33))) (or (or $P49 $P28) P7)) (or (or $P28 (not $P39)) $P45)) (or (or (not $P14) $P21) P8)) (or (or $P12 $P57) P5)) (or (or (not $P43) (not $P48)) $P46)) (or (or $P45 (not $P18)) $P28))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_25.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_25.smt new file mode 100644 index 000000000..2ad1e5d03 --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0200_10_25.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status unsat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (f1_2 x2 x1)) +(let (?x11 (- (- (* (- 0 8) x8) (* 22 x9)) (* 6 x3))) +(let (?x12 (- (- (* 18 x5) (* 20 x9)) (* 27 x4))) +(let (?x13 (f0_1 x3)) +(let (?x14 (f0_1 x2)) +(let (?x15 (- (+ (* 16 x4) (* 3 x9)) (* 3 x8))) +(let (?x16 (- (- (* (- 0 3) x3) (* 12 x6)) (* 12 x2))) +(let (?x17 (+ (- (* (- 0 15) x6) (* 12 x7)) (* 6 x4))) +(let (?x18 (+ (+ (* 6 x0) (* 15 x3)) (* 10 x4))) +(let (?x19 (- (- (* (- 0 17) x6) (* 23 x3)) (* 14 x0))) +(let (?x20 (f0_1 x0)) +(let (?x21 (+ (+ (* 20 x4) (* 9 x2)) (* 27 x7))) +(let (?x22 (+ (- (* 22 x9) (* 20 x7)) (* 18 x6))) +(let (?x23 (f1_2 ?x19 ?x16)) +(let (?x24 (f1_2 x5 ?x19)) +(let (?x25 (f1_1 ?x22)) +(let (?x26 (f0_2 ?x19 ?x19)) +(let (?x27 (+ (- (* 13 ?x12) (* 20 x4)) (* 29 ?x10))) +(let (?x28 (f0_2 x3 ?x13)) +(let (?x29 (- (+ (* (- 0 17) x5) (* 4 x9)) (* 4 x3))) +(let (?x30 (+ (+ (* 4 x8) (* 23 x7)) (* 4 x5))) +(let (?x31 (f0_2 x7 x4)) +(let (?x32 (+ (- (* 16 ?x15) (* 14 ?x29)) (* 20 x1))) +(let (?x33 (f1_2 x2 x3)) +(let (?x34 (f1_1 ?x28)) +(let (?x35 (+ (+ (* (- 0 26) x9) (* 15 x7)) (* 22 x1))) +(let (?x36 (f0_1 ?x11)) +(let (?x37 (+ (- (* 2 x5) (* 24 x4)) (* 3 x1))) +(let (?x38 (f1_1 ?x21)) +(let (?x39 (+ (- (* (- 0 24) x9) (* 13 x2)) (* 18 x5))) +(let (?x40 (- (- (* 17 x4) (* 18 x9)) (* 4 x1))) +(let (?x41 (f0_2 x1 x5)) +(let (?x42 (f0_1 x1)) +(let (?x43 (f0_1 x0)) +(let (?x44 (+ (- (* (- 0 20) x8) (* 13 x4)) (* 2 x1))) +(let (?x45 (f1_1 ?x31)) +(let (?x46 (f0_1 ?x18)) +(let (?x47 (f0_1 x9)) +(let (?x48 (- (+ (* 18 x1) (* 12 x5)) (* 2 x2))) +(let (?x49 (+ (+ (* 24 x2) (* 10 x1)) (* 19 x4))) +(flet ($P10 (= ?x28 ?x27)) +(flet ($P11 (< ?x22 2)) +(flet ($P12 (< ?x12 7)) +(flet ($P13 (= ?x48 ?x33)) +(flet ($P14 (< ?x12 12)) +(flet ($P15 (< ?x45 19)) +(flet ($P16 (< ?x20 26)) +(flet ($P17 (< x4 28)) +(flet ($P18 (< ?x43 (- 0 26))) +(flet ($P19 (< ?x16 28)) +(flet ($P20 (= x6 ?x46)) +(flet ($P21 (< ?x48 (- 0 27))) +(flet ($P22 (< x0 (- 0 23))) +(flet ($P23 (< ?x27 (- 0 4))) +(flet ($P24 (< x3 (- 0 22))) +(flet ($P25 (< x6 (- 0 21))) +(flet ($P26 (< x4 3)) +(flet ($P27 (< ?x18 7)) +(flet ($P28 (= ?x31 x3)) +(flet ($P29 (< ?x13 21)) +(flet ($P30 (< ?x19 (- 0 27))) +(flet ($P31 (< ?x23 1)) +(flet ($P32 (< ?x16 0)) +(flet ($P33 (< ?x41 (- 0 16))) +(flet ($P34 (< ?x21 4)) +(flet ($P35 (< ?x33 7)) +(flet ($P36 (= ?x27 ?x30)) +(flet ($P37 (< x7 (- 0 7))) +(flet ($P38 (< ?x39 17)) +(flet ($P39 (< ?x44 (- 0 14))) +(flet ($P40 (< ?x45 0)) +(flet ($P41 (< ?x34 (- 0 9))) +(flet ($P42 (= ?x19 ?x43)) +(flet ($P43 (< ?x12 0)) +(flet ($P44 (< ?x10 (- 0 15))) +(flet ($P45 (< ?x15 21)) +(flet ($P46 (< x4 (- 0 24))) +(flet ($P47 (= ?x42 ?x27)) +(flet ($P48 (< ?x21 (- 0 10))) +(flet ($P49 (< x7 1)) +(flet ($P50 (< x4 26)) +(flet ($P51 (< ?x18 16)) +(flet ($P52 (= ?x13 ?x43)) +(flet ($P53 (< ?x20 26)) +(flet ($P54 (< ?x34 6)) +(flet ($P55 (< ?x36 20)) +(flet ($P56 (< ?x16 (- 0 17))) +(flet ($P57 (< ?x32 24)) +(flet ($P58 (< ?x13 8)) +(flet ($P59 (= ?x12 x6)) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not $P25) (not $P24)) (not $P19)) (or (or (not $P52) $P36) (not $P35))) (or (or (not $P18) $P41) P4)) (or (or $P24 (not $P44)) P5)) (or (or $P30 (not $P23)) P0)) (or (or P1 (not $P32)) (not $P21))) (or (or $P40 (not $P50)) $P25)) (or (or (not $P27) $P54) $P15)) (or (or (not P3) $P23) (not $P35))) (or (or (not P8) $P46) $P16)) (or (or $P32 (not $P12)) (not $P15))) (or (or (not $P31) $P41) P8)) (or (or P2 (not $P30)) $P23)) (or (or (not P1) $P20) $P42)) (or (or (not $P54) (not $P32)) $P14)) (or (or (not $P25) P2) (not $P48))) (or (or (not $P14) (not $P29)) (not P4))) (or (or (not $P15) P1) (not $P47))) (or (or (not $P59) $P30) (not $P12))) (or (or (not $P45) (not $P48)) (not $P25))) (or (or $P12 $P19) P2)) (or (or (not $P33) (not P7)) (not $P55))) (or (or $P35 $P32) $P18)) (or (or (not $P59) (not $P29)) P8)) (or (or $P46 (not P8)) (not P9))) (or (or (not $P24) $P57) $P37)) (or (or P7 (not $P28)) (not P6))) (or (or (not $P32) (not $P49)) (not $P31))) (or (or P2 (not $P40)) P6)) (or (or (not $P37) $P53) $P52)) (or (or $P44 $P20) $P27)) (or (or $P24 (not $P42)) (not $P16))) (or (or (not $P52) (not $P50)) $P30)) (or (or (not $P44) $P37) (not $P32))) (or (or (not $P26) $P33) P3)) (or (or (not P5) $P27) $P46)) (or (or (not $P31) $P45) (not $P56))) (or (or (not $P43) $P25) (not $P13))) (or (or $P54 $P41) (not $P43))) (or (or (not $P34) $P39) (not P9))) (or (or $P51 (not P6)) (not $P48))) (or (or (not $P56) (not $P31)) (not $P54))) (or (or (not $P37) $P40) $P55)) (or (or (not $P20) (not $P57)) (not $P21))) (or (or (not $P23) (not P1)) $P11)) (or (or P9 $P38) $P18)) (or (or (not $P33) $P18) (not $P31))) (or (or (not $P29) (not $P51)) (not $P40))) (or (or (not $P35) (not P4)) $P51)) (or (or (not $P29) (not $P38)) (not $P11))) (or (or (not $P34) (not $P52)) (not $P28))) (or (or $P17 $P19) P2)) (or (or $P48 $P13) (not $P23))) (or (or (not $P52) (not $P21)) (not $P17))) (or (or $P21 $P10) P7)) (or (or (not $P10) $P37) $P25)) (or (or (not $P19) $P54) (not $P38))) (or (or (not $P55) $P54) P9)) (or (or $P53 $P39) $P21)) (or (or P2 P4) (not $P27))) (or (or (not $P58) (not $P47)) (not $P36))) (or (or (not $P15) (not $P41)) $P29)) (or (or (not $P10) (not $P56)) $P16)) (or (or $P36 (not P9)) $P14)) (or (or (not $P32) (not $P47)) (not $P16))) (or (or $P49 $P19) (not P5))) (or (or $P52 $P17) $P39)) (or (or (not $P57) (not $P35)) (not $P42))) (or (or $P27 (not $P44)) $P29)) (or (or $P16 $P24) $P55)) (or (or (not $P20) $P10) $P17)) (or (or (not $P37) (not $P54)) $P12)) (or (or (not P8) $P39) (not P5))) (or (or (not $P28) (not P8)) (not $P21))) (or (or $P39 (not $P25)) $P12)) (or (or (not $P27) $P25) (not $P35))) (or (or $P48 P6) $P20)) (or (or $P44 (not P8)) P1)) (or (or (not $P37) (not $P35)) (not P8))) (or (or (not $P35) (not $P50)) $P39)) (or (or (not $P33) (not $P38)) (not $P23))) (or (or $P44 (not $P59)) $P42)) (or (or (not $P48) P6) (not $P32))) (or (or $P55 $P13) P2)) (or (or (not $P19) $P52) $P35)) (or (or (not $P55) $P30) (not $P17))) (or (or $P34 $P19) (not $P30))) (or (or (not $P25) (not $P57)) $P45)) (or (or (not $P20) $P25) (not $P57))) (or (or P3 (not $P19)) (not $P54))) (or (or (not $P52) P3) P9)) (or (or $P52 (not $P16)) $P46)) (or (or (not P0) $P45) (not $P13))) (or (or $P48 $P27) (not $P18))) (or (or (not $P39) $P50) (not $P48))) (or (or (not P3) (not $P32)) (not $P13))) (or (or $P19 (not $P24)) $P41)) (or (or $P49 (not $P19)) (not P5))) (or (or $P56 (not $P37)) P1)) (or (or (not $P31) (not $P58)) (not P7))) (or (or $P27 (not $P39)) (not $P17))) (or (or (not $P36) $P19) $P27)) (or (or (not P7) P8) $P50)) (or (or (not $P16) (not P5)) $P24)) (or (or (not $P48) $P37) (not P3))) (or (or $P22 $P16) P6)) (or (or $P24 (not $P44)) $P54)) (or (or (not $P28) (not $P51)) $P59)) (or (or (not $P50) $P34) (not $P57))) (or (or P5 (not P7)) $P55)) (or (or P2 (not $P10)) $P43)) (or (or $P31 $P36) (not $P20))) (or (or (not $P45) (not $P48)) (not $P53))) (or (or (not $P55) $P16) (not $P28))) (or (or (not P3) (not $P12)) P0)) (or (or $P14 $P52) (not P6))) (or (or P6 $P19) $P12)) (or (or (not $P18) $P51) (not $P40))) (or (or (not $P44) (not $P27)) (not $P53))) (or (or (not $P55) $P16) (not P7))) (or (or $P27 P6) (not $P35))) (or (or (not $P52) (not $P26)) $P55)) (or (or $P44 (not $P33)) $P25)) (or (or P9 P2) (not $P15))) (or (or $P20 $P59) (not $P56))) (or (or $P50 (not $P15)) $P48)) (or (or P0 (not $P25)) (not $P16))) (or (or (not $P54) (not $P24)) (not $P20))) (or (or $P50 (not $P34)) (not $P54))) (or (or $P50 $P24) (not $P14))) (or (or (not $P18) (not P8)) (not $P58))) (or (or (not $P13) P2) P4)) (or (or (not $P32) $P24) (not $P18))) (or (or $P51 (not $P48)) $P43)) (or (or (not $P10) $P47) $P35)) (or (or P3 (not $P16)) $P26)) (or (or $P41 $P58) (not $P55))) (or (or (not $P49) (not $P36)) (not P0))) (or (or $P18 $P49) P4)) (or (or P4 (not $P32)) (not P6))) (or (or $P22 (not P4)) $P11)) (or (or $P39 (not $P13)) (not $P19))) (or (or $P38 (not $P25)) (not $P33))) (or (or (not $P56) $P57) (not P0))) (or (or $P42 P5) $P10)) (or (or (not $P24) $P52) (not $P35))) (or (or (not $P52) $P36) P8)) (or (or $P28 (not $P50)) $P25)) (or (or (not $P28) (not $P11)) $P44)) (or (or $P48 $P21) $P16)) (or (or $P55 $P42) $P12)) (or (or $P52 (not $P47)) (not $P14))) (or (or (not $P49) $P12) P8)) (or (or $P28 (not $P57)) P3)) (or (or (not P4) $P29) (not $P59))) (or (or (not $P57) P6) (not $P28))) (or (or (not P9) (not $P47)) $P24)) (or (or (not $P11) (not $P40)) $P44)) (or (or (not $P46) (not P3)) $P33)) (or (or $P30 (not $P18)) $P46)) (or (or $P13 P4) (not $P37))) (or (or $P51 (not P7)) (not $P14))) (or (or $P37 $P56) (not $P45))) (or (or $P55 $P20) (not $P32))) (or (or (not $P25) P4) P8)) (or (or $P36 $P35) (not $P19))) (or (or (not $P43) $P28) $P55)) (or (or (not $P51) (not $P40)) $P22)) (or (or (not P7) $P56) $P31)) (or (or (not $P31) (not $P57)) (not $P29))) (or (or $P44 (not $P25)) P8)) (or (or (not $P40) $P58) $P35)) (or (or $P50 (not $P11)) (not $P24))) (or (or (not $P48) $P37) (not $P19))) (or (or (not $P28) $P39) $P36)) (or (or (not $P27) (not $P29)) $P10)) (or (or P0 P5) (not $P56))) (or (or (not $P35) $P10) (not $P17))) (or (or (not P2) (not P1)) $P52)) (or (or (not $P35) (not $P57)) (not $P44))) (or (or (not $P34) $P50) $P27)) (or (or $P40 $P23) $P47)) (or (or $P28 $P46) (not $P59))) (or (or (not $P35) $P51) $P10)) (or (or (not $P28) $P41) $P46)) (or (or $P10 (not $P41)) $P33)) (or (or $P51 P5) (not P8))) (or (or $P49 $P26) $P32)) (or (or (not P5) (not $P59)) (not $P30))) (or (or $P29 (not $P10)) (not $P52))) (or (or (not $P40) (not $P47)) (not $P39))) (or (or P7 $P22) (not $P19))) (or (or $P14 (not $P31)) P4)) (or (or $P10 P9) (not $P19))) (or (or (not $P53) (not $P29)) (not P3))) (or (or P2 (not $P51)) $P15)) (or (or P5 (not $P41)) $P59)) (or (or (not $P40) (not $P12)) (not P5))) (or (or P3 $P30) P7)) (or (or $P54 $P28) $P22))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt new file mode 100644 index 000000000..d0e9bfed6 --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status unsat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (f1_1 x2)) +(let (?x11 (f1_2 x8 x9)) +(let (?x12 (f1_1 x6)) +(let (?x13 (f1_1 ?x10)) +(let (?x14 (f0_1 x8)) +(let (?x15 (f1_1 x9)) +(let (?x16 (f1_1 x7)) +(let (?x17 (- (+ (* 28 x2) (* 12 x1)) (* 1 x5))) +(let (?x18 (+ (- (* 19 x0) (* 26 x5)) (* 13 x4))) +(let (?x19 (+ (- (* (- 0 2) x8) (* 20 x4)) (* 15 x3))) +(let (?x20 (f1_2 x9 x4)) +(let (?x21 (f1_1 x9)) +(let (?x22 (f1_2 x7 x1)) +(let (?x23 (+ (+ (* 15 x2) (* 20 ?x11)) (* 3 ?x19))) +(let (?x24 (f1_2 x1 x4)) +(let (?x25 (f1_1 x2)) +(let (?x26 (f0_1 ?x20)) +(let (?x27 (f0_2 x9 x1)) +(let (?x28 (f1_1 ?x16)) +(let (?x29 (f0_1 ?x17)) +(let (?x30 (f0_1 x3)) +(let (?x31 (f0_2 x1 x0)) +(let (?x32 (f1_2 ?x29 x2)) +(let (?x33 (f0_1 x5)) +(let (?x34 (f0_1 ?x25)) +(let (?x35 (f0_2 x0 x2)) +(let (?x36 (+ (+ (* 18 ?x30) (* 25 x4)) (* 13 ?x19))) +(let (?x37 (f1_1 x8)) +(let (?x38 (f1_2 x0 x3)) +(let (?x39 (f1_1 ?x38)) +(let (?x40 (f1_1 x2)) +(let (?x41 (f1_2 ?x28 ?x38)) +(let (?x42 (f0_1 x9)) +(let (?x43 (f0_1 x8)) +(let (?x44 (f1_1 x2)) +(let (?x45 (- (- (* (- 0 8) x1) (* 17 x2)) (* 21 x5))) +(let (?x46 (- (- (* 9 ?x39) (* 15 ?x18)) (* 10 ?x38))) +(let (?x47 (f1_1 x6)) +(let (?x48 (f0_2 x1 x9)) +(let (?x49 (+ (+ (* 2 x2) (* 25 x4)) (* 5 x0))) +(flet ($P10 (< x1 24)) +(flet ($P11 (< x5 (- 0 12))) +(flet ($P12 (= ?x15 ?x45)) +(flet ($P13 (< ?x43 28)) +(flet ($P14 (< ?x26 (- 0 3))) +(flet ($P15 (< ?x34 9)) +(flet ($P16 (< ?x26 (- 0 16))) +(flet ($P17 (= ?x33 ?x48)) +(flet ($P18 (< x4 (- 0 28))) +(flet ($P19 (< ?x47 (- 0 11))) +(flet ($P20 (< ?x26 22)) +(flet ($P21 (< ?x44 (- 0 4))) +(flet ($P22 (= ?x17 ?x17)) +(flet ($P23 (< ?x19 (- 0 2))) +(flet ($P24 (= ?x46 ?x27)) +(flet ($P25 (< ?x16 (- 0 6))) +(flet ($P26 (< ?x31 22)) +(flet ($P27 (= ?x35 ?x41)) +(flet ($P28 (< ?x43 (- 0 13))) +(flet ($P29 (< x0 21)) +(flet ($P30 (< ?x31 (- 0 14))) +(flet ($P31 (< ?x13 (- 0 1))) +(flet ($P32 (< ?x49 22)) +(flet ($P33 (< ?x19 1)) +(flet ($P34 (< ?x39 (- 0 23))) +(flet ($P35 (= ?x31 ?x11)) +(flet ($P36 (= ?x35 ?x44)) +(flet ($P37 (< ?x36 20)) +(flet ($P38 (< ?x34 (- 0 20))) +(flet ($P39 (= x0 x4)) +(flet ($P40 (< ?x39 (- 0 8))) +(flet ($P41 (< ?x35 (- 0 8))) +(flet ($P42 (< ?x40 26)) +(flet ($P43 (< ?x14 8)) +(flet ($P44 (= ?x11 ?x44)) +(flet ($P45 (< ?x22 (- 0 13))) +(flet ($P46 (< ?x14 28)) +(flet ($P47 (= ?x36 ?x44)) +(flet ($P48 (< ?x17 24)) +(flet ($P49 (< ?x20 9)) +(flet ($P50 (< ?x29 13)) +(flet ($P51 (< ?x22 16)) +(flet ($P52 (< ?x16 9)) +(flet ($P53 (= ?x23 ?x27)) +(flet ($P54 (< ?x37 16)) +(flet ($P55 (< ?x37 0)) +(flet ($P56 (< ?x38 7)) +(flet ($P57 (< x6 9)) +(flet ($P58 (< ?x44 18)) +(flet ($P59 (= ?x22 ?x32)) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not $P16) (not $P33)) (not P1)) (or (or (not $P20) (not $P43)) $P57)) (or (or $P41 (not P3)) $P27)) (or (or (not $P14) $P14) (not $P23))) (or (or (not $P42) $P52) (not $P13))) (or (or $P28 (not $P27)) (not $P44))) (or (or (not $P35) P2) $P11)) (or (or (not $P22) (not $P44)) (not $P10))) (or (or $P59 $P20) (not $P32))) (or (or (not $P54) P9) (not $P58))) (or (or (not $P27) (not $P19)) (not $P37))) (or (or $P44 $P26) $P49)) (or (or P5 $P13) $P34)) (or (or (not $P29) $P32) (not $P49))) (or (or (not $P31) $P36) (not $P33))) (or (or (not $P14) $P51) (not P4))) (or (or (not $P34) (not $P36)) (not $P18))) (or (or $P30 P7) (not $P15))) (or (or $P56 $P33) (not $P42))) (or (or (not $P35) (not $P52)) (not $P40))) (or (or (not $P44) $P27) $P25)) (or (or (not P7) $P47) (not $P49))) (or (or (not P0) (not $P27)) (not $P25))) (or (or $P17 P9) $P22)) (or (or (not $P21) (not $P49)) $P53)) (or (or (not $P49) $P18) $P41)) (or (or (not $P34) (not $P38)) (not $P35))) (or (or $P10 $P13) $P11)) (or (or $P17 (not P2)) (not $P33))) (or (or $P59 (not $P22)) $P31)) (or (or (not $P33) $P53) (not $P31))) (or (or P2 (not $P21)) (not $P47))) (or (or $P21 $P20) $P22)) (or (or P3 $P30) (not $P38))) (or (or (not $P22) $P35) $P23)) (or (or (not $P24) (not $P46)) $P31)) (or (or (not $P53) $P37) $P26)) (or (or (not $P43) $P22) (not $P39))) (or (or (not $P33) $P28) $P43)) (or (or $P55 (not $P50)) $P33)) (or (or (not $P12) P5) $P42)) (or (or (not $P30) (not $P52)) $P36)) (or (or $P58 $P47) (not $P19))) (or (or (not $P45) $P32) (not $P36))) (or (or $P36 (not $P37)) (not P5))) (or (or P6 (not $P12)) (not P2))) (or (or (not $P10) (not $P10)) $P20)) (or (or (not $P51) (not P4)) (not $P23))) (or (or $P14 (not $P46)) (not $P57))) (or (or (not $P50) (not P8)) (not $P56))) (or (or $P11 (not P6)) P1)) (or (or (not $P36) (not $P43)) (not P8))) (or (or (not $P20) (not P8)) $P22)) (or (or $P32 (not P1)) $P21)) (or (or (not P7) (not $P11)) (not $P46))) (or (or (not P8) $P17) $P22)) (or (or $P26 (not $P29)) $P42)) (or (or (not $P34) (not $P15)) (not $P37))) (or (or $P46 $P11) (not $P51))) (or (or $P49 P3) (not $P33))) (or (or $P47 $P20) $P46)) (or (or $P35 $P41) (not $P51))) (or (or (not $P12) $P44) (not $P33))) (or (or (not $P23) (not $P43)) (not P8))) (or (or $P55 (not P6)) P2)) (or (or $P24 $P29) (not $P44))) (or (or (not $P35) $P49) (not $P51))) (or (or $P27 $P43) (not $P42))) (or (or $P57 (not $P56)) $P10)) (or (or $P55 $P43) (not $P25))) (or (or $P19 $P29) $P58)) (or (or $P53 $P22) (not $P27))) (or (or $P12 $P50) (not $P36))) (or (or $P57 $P44) (not P8))) (or (or $P14 (not P5)) (not $P11))) (or (or (not $P41) (not P6)) (not $P22))) (or (or (not $P46) (not $P55)) $P34)) (or (or (not P4) (not $P43)) (not $P33))) (or (or P7 P9) (not $P16))) (or (or $P43 $P20) P0)) (or (or P5 (not P3)) (not $P29))) (or (or $P42 $P14) P5)) (or (or (not $P20) (not $P29)) P2)) (or (or (not $P14) $P14) $P32)) (or (or $P10 $P15) (not $P28))) (or (or (not $P55) (not $P38)) P4)) (or (or P1 $P43) (not $P12))) (or (or $P29 (not $P38)) (not $P45))) (or (or $P28 $P20) $P49)) (or (or (not $P12) $P19) P7)) (or (or P9 (not P9)) (not $P36))) (or (or (not P0) (not $P22)) (not $P26))) (or (or $P26 (not $P15)) (not P0))) (or (or $P44 $P14) $P35)) (or (or $P31 (not $P37)) $P38)) (or (or $P10 P8) (not $P59))) (or (or (not P4) (not $P57)) $P46)) (or (or (not $P58) (not $P27)) (not $P48))) (or (or $P12 P1) (not $P39))) (or (or (not $P26) $P55) $P46)) (or (or (not $P29) P9) (not P1))) (or (or P8 P1) $P20)) (or (or (not $P20) $P41) (not P1))) (or (or $P28 (not $P27)) (not $P30))) (or (or $P32 $P15) (not $P44))) (or (or (not $P15) (not $P56)) P2)) (or (or (not $P45) (not $P37)) (not $P59))) (or (or (not P4) $P55) $P27)) (or (or P5 (not $P21)) $P41)) (or (or (not $P17) $P24) (not $P43))) (or (or $P33 $P57) (not $P45))) (or (or $P18 (not $P39)) (not $P13))) (or (or (not $P19) (not $P30)) P4)) (or (or (not P2) (not $P41)) $P28)) (or (or $P32 (not $P46)) $P25)) (or (or (not P7) (not $P43)) (not $P10))) (or (or (not $P48) P4) $P18)) (or (or $P29 $P14) (not $P26))) (or (or (not P3) (not $P46)) $P26)) (or (or $P56 P9) (not $P44))) (or (or (not $P18) $P59) $P12)) (or (or $P58 (not $P20)) (not $P54))) (or (or (not $P20) $P17) (not P3))) (or (or (not $P17) $P58) (not $P30))) (or (or (not $P49) (not $P10)) $P33)) (or (or (not $P14) P8) (not $P25))) (or (or (not $P53) $P37) (not $P22))) (or (or $P28 $P56) (not $P43))) (or (or (not $P34) (not $P40)) (not $P47))) (or (or (not P7) (not $P17)) (not $P21))) (or (or (not P2) (not $P48)) (not $P42))) (or (or $P53 (not $P50)) (not P4))) (or (or $P37 $P34) $P25)) (or (or $P28 (not $P25)) $P50)) (or (or P4 (not P5)) (not $P26))) (or (or (not P3) $P19) $P49)) (or (or $P21 $P37) $P22)) (or (or (not $P35) (not $P13)) P0)) (or (or $P57 $P40) P8)) (or (or $P32 P7) $P31)) (or (or (not P4) $P53) (not $P36))) (or (or (not $P35) (not $P16)) (not $P52))) (or (or $P16 (not $P23)) (not $P34))) (or (or P7 $P22) (not $P30))) (or (or (not $P41) $P39) (not $P51))) (or (or $P29 (not $P23)) $P16)) (or (or $P53 $P31) $P23)) (or (or (not $P24) (not $P44)) (not $P39))) (or (or $P25 $P28) P4)) (or (or (not $P54) $P47) $P33)) (or (or $P40 $P26) (not $P56))) (or (or $P10 (not $P24)) (not $P59))) (or (or $P25 (not $P41)) $P39)) (or (or $P28 (not $P27)) (not $P54))) (or (or (not $P52) (not $P34)) $P59)) (or (or (not $P57) (not $P50)) (not $P38))) (or (or $P51 P5) $P28)) (or (or $P24 $P16) $P26)) (or (or $P39 $P39) $P49)) (or (or $P48 (not $P25)) $P46)) (or (or $P43 (not $P59)) (not $P57))) (or (or $P48 (not $P54)) $P35)) (or (or (not P2) $P10) $P32)) (or (or (not $P33) $P47) $P32)) (or (or $P50 $P44) $P21)) (or (or (not $P10) (not $P22)) (not $P50))) (or (or (not $P47) $P19) (not P5))) (or (or $P29 $P32) (not $P12))) (or (or (not $P25) (not P2)) (not $P47))) (or (or $P15 $P55) (not $P26))) (or (or (not P0) (not $P58)) (not $P21))) (or (or (not $P42) (not $P18)) (not P4))) (or (or P3 (not $P33)) (not $P59))) (or (or (not $P15) (not P7)) (not $P57))) (or (or (not $P35) (not $P25)) P8)) (or (or (not $P11) (not $P15)) (not $P59))) (or (or (not $P13) (not P9)) $P57)) (or (or (not $P23) $P36) $P24)) (or (or (not $P49) $P36) $P33)) (or (or (not $P31) (not $P47)) (not $P55))) (or (or $P20 $P42) (not $P14))) (or (or $P17 (not $P31)) (not $P11))) (or (or (not $P46) P3) (not $P17))) (or (or $P30 (not $P12)) (not $P17))) (or (or $P56 $P50) (not $P43))) (or (or $P38 (not $P44)) $P30)) (or (or (not $P28) (not $P14)) $P18)) (or (or P9 $P22) (not $P57))) (or (or (not $P53) $P47) (not P4))) (or (or $P51 $P38) P3)) (or (or P6 (not $P25)) (not $P10))) (or (or $P53 $P40) $P41)) (or (or (not $P29) (not $P55)) (not $P43))) (or (or $P21 (not $P59)) (not $P34))) (or (or (not $P20) (not $P52)) (not $P55))) (or (or $P41 P5) (not $P28))) (or (or P3 (not $P50)) $P39)) (or (or (not $P15) (not $P14)) P5)) (or (or $P33 $P22) $P58)) (or (or $P52 (not P3)) (not $P58)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_27.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_27.smt new file mode 100644 index 000000000..b7adaeeb0 --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0200_10_27.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status unsat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (+ (- (* (- 0 13) x0) (* 2 x6)) (* 15 x5))) +(let (?x11 (f0_2 ?x10 x8)) +(let (?x12 (f1_2 x8 x0)) +(let (?x13 (f0_1 ?x10)) +(let (?x14 (f1_2 x4 x0)) +(let (?x15 (f0_1 x0)) +(let (?x16 (+ (- (* 9 x7) (* 28 x6)) (* 9 x9))) +(let (?x17 (f1_2 x1 x3)) +(let (?x18 (f1_1 x5)) +(let (?x19 (+ (- (* 22 ?x14) (* 8 x2)) (* 7 x5))) +(let (?x20 (f0_2 ?x10 ?x11)) +(let (?x21 (f1_1 ?x16)) +(let (?x22 (f1_1 x9)) +(let (?x23 (f1_2 x2 x7)) +(let (?x24 (f0_1 x0)) +(let (?x25 (f0_2 x9 x5)) +(let (?x26 (f0_2 x8 x6)) +(let (?x27 (+ (- (* 8 x4) (* 15 x5)) (* 4 x2))) +(let (?x28 (+ (+ (* 29 x3) (* 3 x1)) (* 4 x0))) +(let (?x29 (f1_1 x0)) +(let (?x30 (+ (- (* (- 0 4) ?x18) (* 26 ?x23)) (* 12 ?x22))) +(let (?x31 (f0_1 x4)) +(let (?x32 (f1_2 ?x27 ?x30)) +(let (?x33 (f0_1 x4)) +(let (?x34 (f0_1 x7)) +(let (?x35 (- (+ (* 26 x6) (* 28 x4)) (* 13 x3))) +(let (?x36 (- (- (* 10 ?x12) (* 14 ?x21)) (* 10 x3))) +(let (?x37 (f1_2 ?x22 ?x22)) +(let (?x38 (+ (- (* (- 0 6) x9) (* 29 x7)) (* 9 x0))) +(let (?x39 (f1_2 x7 x2)) +(let (?x40 (- (- (* (- 0 13) ?x26) (* 3 ?x32)) (* 17 ?x14))) +(let (?x41 (- (+ (* (- 0 6) x7) (* 8 x1)) (* 22 x4))) +(let (?x42 (f0_1 x5)) +(let (?x43 (- (+ (* 11 x9) (* 28 x3)) (* 25 x2))) +(let (?x44 (+ (+ (* 11 x6) (* 7 x5)) (* 15 x8))) +(let (?x45 (f1_2 x8 x4)) +(let (?x46 (f1_1 x4)) +(let (?x47 (f0_2 x0 x0)) +(let (?x48 (f1_1 x9)) +(let (?x49 (f1_2 x1 x2)) +(flet ($P10 (< ?x38 16)) +(flet ($P11 (= ?x27 ?x15)) +(flet ($P12 (< ?x12 (- 0 21))) +(flet ($P13 (< ?x16 (- 0 6))) +(flet ($P14 (= x0 ?x24)) +(flet ($P15 (= ?x46 x2)) +(flet ($P16 (= ?x12 ?x16)) +(flet ($P17 (= ?x23 ?x22)) +(flet ($P18 (< ?x16 (- 0 27))) +(flet ($P19 (< ?x38 (- 0 11))) +(flet ($P20 (< ?x38 (- 0 21))) +(flet ($P21 (< ?x22 1)) +(flet ($P22 (< ?x41 (- 0 1))) +(flet ($P23 (< x5 22)) +(flet ($P24 (= ?x42 x9)) +(flet ($P25 (< ?x27 (- 0 2))) +(flet ($P26 (= x3 ?x46)) +(flet ($P27 (< ?x20 (- 0 10))) +(flet ($P28 (< ?x20 15)) +(flet ($P29 (< ?x23 20)) +(flet ($P30 (= ?x10 ?x37)) +(flet ($P31 (< ?x22 (- 0 13))) +(flet ($P32 (< ?x31 18)) +(flet ($P33 (< x1 0)) +(flet ($P34 (< ?x20 11)) +(flet ($P35 (< x2 13)) +(flet ($P36 (< x5 (- 0 14))) +(flet ($P37 (= ?x33 ?x37)) +(flet ($P38 (< ?x23 9)) +(flet ($P39 (< ?x33 26)) +(flet ($P40 (< ?x28 4)) +(flet ($P41 (= ?x30 x6)) +(flet ($P42 (= ?x10 ?x29)) +(flet ($P43 (< x5 21)) +(flet ($P44 (< ?x26 (- 0 28))) +(flet ($P45 (< ?x34 (- 0 10))) +(flet ($P46 (< ?x16 (- 0 7))) +(flet ($P47 (< ?x48 (- 0 19))) +(flet ($P48 (< x4 25)) +(flet ($P49 (= ?x25 ?x20)) +(flet ($P50 (< ?x23 (- 0 1))) +(flet ($P51 (= x6 ?x47)) +(flet ($P52 (= ?x20 ?x32)) +(flet ($P53 (< ?x30 28)) +(flet ($P54 (< ?x25 7)) +(flet ($P55 (= ?x36 ?x38)) +(flet ($P56 (= ?x47 x8)) +(flet ($P57 (< ?x23 (- 0 9))) +(flet ($P58 (= ?x23 ?x23)) +(flet ($P59 (< x7 11)) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not $P19) $P19) (not $P54)) (or (or P3 (not $P12)) $P14)) (or (or $P28 $P54) (not $P53))) (or (or $P57 $P14) $P44)) (or (or (not $P58) $P34) $P28)) (or (or $P39 (not $P50)) (not $P36))) (or (or (not P3) (not $P34)) (not $P28))) (or (or $P12 P5) $P32)) (or (or $P51 $P45) (not $P29))) (or (or $P42 $P26) $P53)) (or (or $P25 $P55) (not $P20))) (or (or (not $P38) $P58) $P57)) (or (or (not P3) (not P3)) (not $P57))) (or (or P5 (not $P40)) $P10)) (or (or (not $P27) $P27) (not $P24))) (or (or P0 $P16) (not P3))) (or (or P7 (not $P17)) $P22)) (or (or (not $P55) P8) P6)) (or (or P2 $P37) (not $P14))) (or (or (not $P51) (not $P53)) P8)) (or (or (not $P14) $P34) (not P5))) (or (or $P17 $P43) $P16)) (or (or (not $P18) (not $P46)) (not $P57))) (or (or $P44 P2) $P51)) (or (or (not $P56) (not $P26)) (not $P48))) (or (or $P36 (not $P34)) (not P4))) (or (or $P20 (not $P43)) $P49)) (or (or $P34 (not $P17)) (not $P32))) (or (or $P10 $P18) $P43)) (or (or (not $P38) $P53) $P12)) (or (or P6 $P39) P4)) (or (or $P32 $P25) P7)) (or (or (not P2) (not $P43)) (not $P54))) (or (or $P15 (not $P20)) (not $P19))) (or (or (not $P38) $P41) $P34)) (or (or (not $P16) (not $P49)) P2)) (or (or $P18 (not $P23)) (not $P19))) (or (or $P37 $P59) (not P0))) (or (or (not $P34) P4) (not $P29))) (or (or $P32 (not $P50)) (not $P59))) (or (or (not $P58) P4) (not $P19))) (or (or P0 (not $P27)) $P13)) (or (or $P35 (not $P22)) (not $P55))) (or (or $P12 $P55) $P17)) (or (or (not $P35) (not $P22)) (not $P41))) (or (or $P19 $P36) (not $P44))) (or (or (not $P37) $P47) (not $P15))) (or (or $P16 $P31) $P25)) (or (or (not $P10) $P34) (not $P36))) (or (or P0 (not $P22)) P3)) (or (or (not $P55) (not $P40)) (not $P48))) (or (or (not $P40) $P51) P9)) (or (or (not $P40) P8) (not $P15))) (or (or (not P1) $P40) (not P9))) (or (or (not $P26) (not $P31)) (not $P40))) (or (or (not $P55) $P29) (not $P19))) (or (or (not $P19) $P16) (not $P23))) (or (or $P13 (not $P16)) P5)) (or (or (not $P18) $P20) P9)) (or (or (not $P49) (not $P40)) $P13)) (or (or (not $P24) $P25) (not $P54))) (or (or $P52 $P28) (not $P17))) (or (or $P47 $P40) (not $P41))) (or (or (not $P40) $P55) (not $P23))) (or (or $P50 (not $P28)) (not $P36))) (or (or (not $P22) (not $P25)) (not $P12))) (or (or (not P2) P2) P1)) (or (or (not $P57) (not $P53)) $P32)) (or (or (not P7) $P52) $P39)) (or (or $P42 $P59) (not $P12))) (or (or $P56 $P21) (not $P35))) (or (or (not $P35) $P35) (not $P22))) (or (or (not P9) (not P2)) $P17)) (or (or (not $P12) (not $P47)) (not $P14))) (or (or (not P1) (not $P24)) $P28)) (or (or (not $P17) (not $P53)) (not $P34))) (or (or (not $P56) (not $P31)) (not $P48))) (or (or (not $P19) (not $P46)) $P24)) (or (or (not $P23) $P12) (not $P10))) (or (or $P19 (not P9)) P6)) (or (or (not $P18) (not $P45)) (not $P54))) (or (or (not $P11) $P41) P6)) (or (or (not $P31) $P45) $P46)) (or (or (not $P42) $P20) (not $P39))) (or (or (not $P35) P4) (not P7))) (or (or (not $P13) $P16) (not $P35))) (or (or (not P2) (not $P52)) $P24)) (or (or $P43 (not $P13)) $P12)) (or (or $P54 $P50) P5)) (or (or (not $P17) (not P3)) (not $P32))) (or (or $P57 (not $P15)) $P44)) (or (or P4 (not $P55)) $P51)) (or (or (not $P47) P5) (not $P18))) (or (or P7 $P53) (not $P45))) (or (or $P20 $P33) (not $P47))) (or (or P1 $P34) $P51)) (or (or $P52 (not P4)) $P36)) (or (or (not $P20) (not $P29)) (not P8))) (or (or $P54 $P45) $P48)) (or (or $P48 $P44) $P31)) (or (or (not $P40) (not $P49)) (not $P41))) (or (or (not $P57) (not $P27)) (not $P21))) (or (or (not $P12) $P30) (not $P59))) (or (or $P57 (not $P30)) (not $P17))) (or (or (not $P54) P9) P0)) (or (or P2 $P59) (not P9))) (or (or $P34 $P27) (not P7))) (or (or $P30 $P38) $P45)) (or (or (not $P47) $P35) $P53)) (or (or $P38 (not $P30)) (not P1))) (or (or (not $P24) (not $P24)) $P22)) (or (or (not $P12) (not $P53)) $P33)) (or (or $P55 (not $P16)) (not $P56))) (or (or $P51 (not $P27)) (not $P55))) (or (or (not P9) $P24) $P47)) (or (or (not $P45) (not $P58)) (not P2))) (or (or $P23 $P42) (not $P44))) (or (or $P32 (not $P39)) P9)) (or (or $P25 (not $P13)) (not $P10))) (or (or (not P2) $P28) (not $P32))) (or (or $P27 $P15) P8)) (or (or (not $P30) P8) $P12)) (or (or (not P0) (not $P48)) (not $P16))) (or (or $P28 (not $P17)) (not $P37))) (or (or $P31 $P56) $P54)) (or (or (not P6) (not $P50)) $P46)) (or (or $P42 (not $P53)) (not $P12))) (or (or $P34 (not $P36)) $P39)) (or (or $P52 (not $P49)) P2)) (or (or (not $P58) (not $P11)) (not $P15))) (or (or $P14 $P54) (not $P39))) (or (or (not $P29) $P29) (not $P47))) (or (or (not P4) (not $P21)) (not $P35))) (or (or $P27 (not $P51)) (not $P23))) (or (or $P36 (not $P41)) (not $P16))) (or (or $P23 (not $P52)) (not $P26))) (or (or $P59 (not $P51)) P6)) (or (or (not $P23) $P54) $P13)) (or (or (not $P36) P3) (not $P14))) (or (or (not $P16) $P39) (not $P30))) (or (or (not $P22) (not $P15)) $P46)) (or (or (not $P14) P3) $P40)) (or (or (not $P42) $P42) $P17)) (or (or (not $P41) (not $P42)) (not $P22))) (or (or (not $P37) $P10) $P19)) (or (or (not $P16) (not $P16)) $P24)) (or (or (not $P31) (not P8)) (not $P56))) (or (or $P19 $P46) $P12)) (or (or (not $P32) $P44) $P24)) (or (or $P30 (not $P44)) $P38)) (or (or P1 (not $P52)) $P56)) (or (or (not $P13) $P59) (not $P49))) (or (or $P51 (not $P47)) (not $P58))) (or (or $P55 (not $P47)) (not $P46))) (or (or $P57 $P57) $P40)) (or (or (not $P30) (not P3)) (not $P42))) (or (or (not $P20) (not $P37)) $P42)) (or (or $P43 (not $P54)) $P15)) (or (or $P10 $P30) (not $P54))) (or (or (not $P49) $P57) $P20)) (or (or (not $P55) $P29) $P15)) (or (or (not $P10) (not $P14)) (not $P17))) (or (or (not P0) (not $P55)) (not $P34))) (or (or P7 (not $P28)) (not $P49))) (or (or $P42 P4) (not $P56))) (or (or (not $P45) P3) P7)) (or (or (not $P50) P5) (not P8))) (or (or $P37 (not $P40)) $P50)) (or (or P1 (not $P49)) $P18)) (or (or (not $P58) P8) (not $P12))) (or (or $P53 P2) (not P7))) (or (or $P23 $P34) (not $P56))) (or (or (not $P47) (not $P43)) $P41)) (or (or (not P3) (not $P38)) $P47)) (or (or $P19 P7) (not $P55))) (or (or (not $P49) $P44) P7)) (or (or (not $P27) (not P6)) $P52)) (or (or P1 $P10) (not P5))) (or (or (not $P15) $P27) (not $P31))) (or (or (not $P43) (not $P50)) (not $P36))) (or (or $P17 $P37) (not $P13))) (or (or $P52 (not $P17)) P6)) (or (or P5 $P19) (not $P16))) (or (or P5 (not $P57)) $P38)) (or (or $P10 $P10) $P57)) (or (or $P51 (not $P33)) (not $P56))) (or (or (not $P46) $P28) (not P0))) (or (or (not P1) P7) $P16)) (or (or (not $P52) (not $P32)) P1)) (or (or $P17 $P58) $P19)) (or (or (not $P36) (not $P12)) (not $P10))) (or (or $P15 (not $P30)) P1)) (or (or $P50 (not $P47)) $P23)) (or (or $P57 (not P4)) (not $P23))) (or (or $P53 P2) $P48)) (or (or (not P6) (not $P56)) $P33)) (or (or (not $P44) $P58) $P16)) (or (or (not $P35) $P41) (not $P18))) (or (or (not $P13) (not P5)) (not $P12))) (or (or (not $P39) (not $P51)) $P54))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_29.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_29.smt new file mode 100644 index 000000000..bd3bc16cf --- /dev/null +++ b/test/regress/regress0/uflra/pb_real_10_0200_10_29.smt @@ -0,0 +1,126 @@ +(benchmark mathsat +:source { MathSat group } +:logic QF_UFLRA +:status unsat +:category { random } +:difficulty { 3 } +:extrafuns ((f0_1 Real Real)) +:extrafuns ((f0_2 Real Real Real)) +:extrafuns ((f0_3 Real Real Real Real)) +:extrafuns ((f0_4 Real Real Real Real Real)) +:extrafuns ((f1_1 Real Real)) +:extrafuns ((f1_2 Real Real Real)) +:extrafuns ((f1_3 Real Real Real Real)) +:extrafuns ((f1_4 Real Real Real Real Real)) +:extrafuns ((x0 Real)) +:extrafuns ((x1 Real)) +:extrafuns ((x2 Real)) +:extrafuns ((x3 Real)) +:extrafuns ((x4 Real)) +:extrafuns ((x5 Real)) +:extrafuns ((x6 Real)) +:extrafuns ((x7 Real)) +:extrafuns ((x8 Real)) +:extrafuns ((x9 Real)) +:extrapreds ((P0)) +:extrapreds ((P1)) +:extrapreds ((P2)) +:extrapreds ((P3)) +:extrapreds ((P4)) +:extrapreds ((P5)) +:extrapreds ((P6)) +:extrapreds ((P7)) +:extrapreds ((P8)) +:extrapreds ((P9)) +:formula +(let (?x10 (f0_2 x2 x0)) +(let (?x11 (f1_1 x7)) +(let (?x12 (f1_2 x7 x2)) +(let (?x13 (f0_2 x0 ?x12)) +(let (?x14 (f1_1 x6)) +(let (?x15 (+ (- (* 13 x2) (* 27 x7)) (* 14 x6))) +(let (?x16 (f0_2 x2 x3)) +(let (?x17 (f1_2 x3 x3)) +(let (?x18 (f1_1 x1)) +(let (?x19 (- (+ (* 24 x0) (* 26 x6)) (* 1 x7))) +(let (?x20 (f1_1 x8)) +(let (?x21 (f1_2 ?x16 ?x14)) +(let (?x22 (f1_1 x0)) +(let (?x23 (f1_2 x4 ?x15)) +(let (?x24 (- (+ (* (- 0 4) x1) (* 4 x6)) (* 12 ?x23))) +(let (?x25 (f1_1 x5)) +(let (?x26 (f1_2 x3 x2)) +(let (?x27 (- (- (* (- 0 8) ?x13) (* 2 x6)) (* 16 ?x15))) +(let (?x28 (f1_1 x3)) +(let (?x29 (f1_2 x0 x9)) +(let (?x30 (f0_1 x6)) +(let (?x31 (+ (- (* (- 0 14) x6) (* 18 x9)) (* 23 x0))) +(let (?x32 (- (+ (* (- 0 29) x0) (* 2 x7)) (* 9 x6))) +(let (?x33 (- (- (* 29 x6) (* 23 x6)) (* 9 x3))) +(let (?x34 (- (- (* 10 ?x24) (* 15 ?x26)) (* 2 ?x33))) +(let (?x35 (f0_1 x3)) +(let (?x36 (+ (- (* (- 0 23) x9) (* 27 x6)) (* 1 x8))) +(let (?x37 (- (- (* (- 0 9) x9) (* 28 x8)) (* 17 x6))) +(let (?x38 (f0_1 x3)) +(let (?x39 (f0_2 ?x10 ?x32)) +(let (?x40 (+ (+ (* 26 x9) (* 15 x5)) (* 2 x4))) +(let (?x41 (- (+ (* (- 0 13) x9) (* 19 x6)) (* 23 x1))) +(let (?x42 (f1_2 ?x12 ?x14)) +(let (?x43 (f1_1 x2)) +(let (?x44 (f0_1 ?x37)) +(let (?x45 (f1_2 x1 x4)) +(let (?x46 (- (+ (* (- 0 27) ?x22) (* 20 ?x38)) (* 16 ?x15))) +(let (?x47 (f0_1 ?x36)) +(let (?x48 (- (- (* (- 0 12) ?x40) (* 17 ?x32)) (* 15 ?x34))) +(let (?x49 (f1_2 x3 x2)) +(flet ($P10 (= ?x12 x6)) +(flet ($P11 (< ?x43 18)) +(flet ($P12 (< ?x10 24)) +(flet ($P13 (< ?x35 7)) +(flet ($P14 (< x7 (- 0 3))) +(flet ($P15 (< ?x34 29)) +(flet ($P16 (< ?x44 (- 0 28))) +(flet ($P17 (= ?x26 ?x20)) +(flet ($P18 (= ?x25 ?x45)) +(flet ($P19 (< ?x23 9)) +(flet ($P20 (< x5 19)) +(flet ($P21 (= ?x20 ?x49)) +(flet ($P22 (< ?x39 (- 0 13))) +(flet ($P23 (< ?x22 (- 0 29))) +(flet ($P24 (< ?x16 (- 0 17))) +(flet ($P25 (< ?x35 27)) +(flet ($P26 (< ?x30 25)) +(flet ($P27 (= x9 x2)) +(flet ($P28 (= ?x46 ?x39)) +(flet ($P29 (< ?x22 (- 0 10))) +(flet ($P30 (< ?x31 2)) +(flet ($P31 (< ?x48 17)) +(flet ($P32 (< x0 (- 0 23))) +(flet ($P33 (< ?x10 27)) +(flet ($P34 (< ?x47 25)) +(flet ($P35 (< ?x40 27)) +(flet ($P36 (= ?x45 ?x29)) +(flet ($P37 (< ?x35 12)) +(flet ($P38 (< ?x23 26)) +(flet ($P39 (< ?x44 11)) +(flet ($P40 (< ?x20 (- 0 15))) +(flet ($P41 (< x5 16)) +(flet ($P42 (< ?x17 11)) +(flet ($P43 (< ?x37 (- 0 24))) +(flet ($P44 (< ?x35 14)) +(flet ($P45 (< x9 (- 0 8))) +(flet ($P46 (< x5 (- 0 10))) +(flet ($P47 (< ?x26 17)) +(flet ($P48 (< x3 (- 0 19))) +(flet ($P49 (= ?x17 ?x43)) +(flet ($P50 (< ?x19 (- 0 15))) +(flet ($P51 (< ?x49 17)) +(flet ($P52 (< ?x23 13)) +(flet ($P53 (< ?x45 10)) +(flet ($P54 (= x0 ?x39)) +(flet ($P55 (< ?x25 28)) +(flet ($P56 (< ?x17 26)) +(flet ($P57 (< ?x31 9)) +(flet ($P58 (< ?x46 (- 0 18))) +(flet ($P59 (= ?x16 ?x41)) +(and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (not $P17) $P37) (not $P18)) (or (or (not $P21) $P32) (not $P29))) (or (or $P34 (not P8)) (not $P43))) (or (or (not $P13) $P44) P0)) (or (or (not P3) $P28) $P19)) (or (or (not $P43) P2) (not P9))) (or (or (not $P47) $P58) $P28)) (or (or (not $P48) $P28) (not P3))) (or (or (not P4) $P36) (not $P46))) (or (or $P57 (not $P51)) (not $P47))) (or (or $P22 (not $P46)) (not P9))) (or (or $P26 (not $P55)) $P23)) (or (or $P49 $P55) (not $P11))) (or (or P8 (not $P31)) $P30)) (or (or (not $P14) (not P8)) P7)) (or (or $P26 $P23) $P15)) (or (or $P57 (not $P22)) P4)) (or (or $P44 $P18) (not P1))) (or (or (not $P42) (not $P26)) (not $P49))) (or (or $P57 $P30) $P10)) (or (or $P27 $P55) (not $P53))) (or (or $P33 (not P5)) (not $P11))) (or (or $P16 $P53) (not $P54))) (or (or $P46 (not $P23)) $P41)) (or (or (not $P51) P1) (not $P55))) (or (or (not $P22) $P49) P0)) (or (or $P34 P7) $P26)) (or (or P0 $P44) $P11)) (or (or (not $P15) (not $P15)) (not $P29))) (or (or (not $P42) (not $P41)) (not $P49))) (or (or (not P2) (not P9)) $P40)) (or (or (not P9) $P27) (not $P38))) (or (or (not $P12) $P32) P4)) (or (or (not $P28) $P16) (not $P25))) (or (or (not $P46) $P42) $P53)) (or (or (not $P37) (not $P44)) (not $P57))) (or (or (not $P51) (not $P50)) (not $P12))) (or (or (not $P35) $P44) $P23)) (or (or $P38 $P29) (not $P43))) (or (or (not $P42) $P16) (not $P41))) (or (or $P16 $P24) (not P3))) (or (or (not P5) $P16) (not P9))) (or (or $P27 (not $P31)) (not P5))) (or (or $P56 (not P5)) (not $P34))) (or (or $P10 $P10) (not $P41))) (or (or (not $P54) $P17) P8)) (or (or $P19 (not $P42)) $P25)) (or (or $P54 $P39) $P45)) (or (or (not $P49) $P31) $P30)) (or (or $P11 (not $P20)) (not P9))) (or (or $P22 P9) (not $P52))) (or (or $P16 $P29) $P33)) (or (or (not P2) $P18) (not $P40))) (or (or $P40 (not $P39)) (not P9))) (or (or (not $P53) (not $P44)) (not $P48))) (or (or (not P2) (not $P26)) (not $P14))) (or (or $P52 (not $P44)) (not P7))) (or (or $P55 $P33) $P37)) (or (or (not P1) (not $P22)) (not $P24))) (or (or $P41 (not P3)) $P28)) (or (or $P23 $P44) $P27)) (or (or (not $P11) P6) $P32)) (or (or $P11 $P57) $P52)) (or (or (not $P28) (not $P58)) $P55)) (or (or (not $P22) (not $P46)) (not $P29))) (or (or (not $P32) $P56) (not $P46))) (or (or (not $P47) (not $P58)) (not $P42))) (or (or $P14 $P59) $P38)) (or (or P9 $P53) (not $P54))) (or (or $P47 P2) $P43)) (or (or $P30 (not $P39)) (not $P55))) (or (or $P29 (not P6)) $P26)) (or (or (not $P52) (not $P13)) (not $P34))) (or (or P1 $P50) P9)) (or (or (not $P45) (not $P11)) P1)) (or (or (not $P57) $P42) (not P7))) (or (or $P36 (not $P29)) (not $P24))) (or (or $P16 (not P3)) $P22)) (or (or $P46 (not $P47)) (not $P13))) (or (or (not $P33) (not $P45)) $P16)) (or (or $P28 (not $P11)) (not $P47))) (or (or $P41 (not $P31)) (not $P27))) (or (or (not $P28) $P18) $P19)) (or (or (not P6) $P29) (not $P20))) (or (or P3 $P49) (not $P17))) (or (or $P30 $P11) (not $P45))) (or (or (not $P58) (not $P53)) P7)) (or (or $P14 (not $P11)) (not $P39))) (or (or (not $P59) (not $P47)) P8)) (or (or (not $P35) P2) $P51)) (or (or (not $P11) (not $P51)) (not P7))) (or (or (not $P53) (not $P19)) (not $P15))) (or (or (not $P41) P7) $P48)) (or (or (not $P12) (not $P55)) P5)) (or (or (not $P59) (not $P21)) $P18)) (or (or (not $P50) (not $P17)) (not $P21))) (or (or (not P7) (not $P57)) (not $P44))) (or (or $P12 P1) $P21)) (or (or (not $P54) (not $P31)) $P43)) (or (or $P10 (not $P59)) $P40)) (or (or $P34 $P51) (not $P46))) (or (or $P58 $P28) (not P1))) (or (or (not $P27) $P39) P6)) (or (or $P14 (not $P22)) $P26)) (or (or (not P0) (not $P56)) $P21)) (or (or $P12 $P26) (not $P31))) (or (or (not $P53) (not $P13)) $P22)) (or (or $P20 $P30) (not $P38))) (or (or $P44 $P57) $P40)) (or (or (not P1) $P44) (not $P19))) (or (or $P57 (not $P32)) $P42)) (or (or (not $P38) $P48) $P28)) (or (or $P26 P3) $P23)) (or (or $P16 $P11) P8)) (or (or (not $P53) (not $P37)) (not P2))) (or (or $P56 (not $P45)) (not $P10))) (or (or $P23 P2) $P26)) (or (or (not $P20) $P51) (not $P21))) (or (or $P25 $P43) $P19)) (or (or P3 (not $P51)) $P13)) (or (or (not $P19) $P24) P0)) (or (or $P13 $P48) $P23)) (or (or (not $P47) (not $P36)) P8)) (or (or (not $P58) $P56) P9)) (or (or (not P0) (not $P21)) $P46)) (or (or $P52 P3) $P15)) (or (or (not $P53) (not $P44)) (not $P36))) (or (or (not $P10) $P57) $P18)) (or (or (not P1) (not P6)) $P21)) (or (or (not P3) $P49) (not $P59))) (or (or (not $P43) (not $P15)) $P53)) (or (or (not $P11) (not $P45)) $P38)) (or (or (not P6) (not $P55)) (not $P26))) (or (or (not $P48) (not P7)) (not $P51))) (or (or (not $P21) (not $P25)) $P29)) (or (or (not $P25) (not $P48)) $P42)) (or (or $P21 (not $P34)) $P52)) (or (or (not P3) (not P8)) (not P6))) (or (or $P30 (not $P14)) (not $P46))) (or (or $P20 $P12) (not P4))) (or (or $P40 (not $P23)) (not $P36))) (or (or (not $P36) (not $P49)) $P10)) (or (or (not P6) (not $P58)) P7)) (or (or (not $P16) (not $P25)) (not $P39))) (or (or (not $P56) $P56) (not $P49))) (or (or $P44 (not $P26)) (not $P49))) (or (or (not $P33) $P18) $P46)) (or (or (not $P24) $P37) (not $P57))) (or (or (not $P16) $P57) (not $P10))) (or (or (not $P19) (not $P19)) $P27)) (or (or P1 $P38) (not $P26))) (or (or (not $P30) $P45) (not $P26))) (or (or $P42 $P57) (not $P58))) (or (or $P18 (not $P11)) $P47)) (or (or $P16 $P59) (not $P33))) (or (or $P49 (not $P31)) (not $P20))) (or (or (not P4) $P59) (not $P14))) (or (or (not $P26) $P19) $P37)) (or (or $P47 (not P8)) (not $P27))) (or (or P1 $P46) $P23)) (or (or $P52 $P31) (not $P32))) (or (or (not $P56) (not $P20)) (not P9))) (or (or (not $P18) $P50) $P11)) (or (or (not $P15) $P21) (not $P29))) (or (or $P19 $P25) (not $P30))) (or (or (not $P53) (not P7)) (not $P43))) (or (or (not $P43) (not P2)) (not $P55))) (or (or $P50 $P34) $P59)) (or (or P5 P9) (not $P52))) (or (or P9 $P29) $P47)) (or (or (not $P49) (not $P19)) (not $P25))) (or (or (not $P22) (not $P13)) P6)) (or (or (not $P41) $P15) P8)) (or (or (not $P46) $P56) P1)) (or (or $P48 $P51) $P50)) (or (or (not $P15) (not $P13)) $P41)) (or (or $P22 $P41) $P48)) (or (or (not $P34) (not $P45)) P4)) (or (or $P29 P5) (not $P55))) (or (or (not $P23) (not $P51)) (not $P40))) (or (or (not P7) $P14) (not $P49))) (or (or $P31 (not P1)) (not $P28))) (or (or (not $P40) (not $P44)) (not $P10))) (or (or (not $P15) $P25) $P10)) (or (or (not $P32) (not $P50)) $P29)) (or (or (not $P31) P3) $P36)) (or (or P6 $P30) $P23)) (or (or (not $P53) $P36) $P54)) (or (or (not $P10) (not P8)) P5)) (or (or $P26 $P24) $P35)) (or (or (not $P38) (not $P49)) $P46)) (or (or P0 (not $P52)) P4)) (or (or (not $P28) (not $P12)) $P31)) (or (or $P59 $P28) (not $P30))) (or (or (not $P26) $P34) (not $P47))) (or (or (not $P57) (not P2)) $P38)) (or (or (not $P13) $P45) (not $P19))) (or (or (not $P45) (not P1)) (not $P32))) (or (or (not $P28) (not $P15)) (not $P34))) (or (or $P50 $P56) $P35))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |