From: Gereon Kremer Date: Sat, 5 Mar 2022 01:46:57 +0000 (+0100) Subject: Add regressions for fixed issue (#8237) X-Git-Tag: cvc5-1.0.0~317 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bd992288696666553dd0ec1d1f67620a46a06cc9;p=cvc5.git Add regressions for fixed issue (#8237) Adds regressions for an issue that has been fixed in the meantime. Fixes #4334 --- diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 50969c740..8d50b53f7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -772,6 +772,7 @@ set(regress_0_tests regress0/nl/issue3971.smt2 regress0/nl/issue3991.smt2 regress0/nl/issue4007-rint-uf.smt2 + regress0/nl/issue4334-sat-proof-min.smt2 regress0/nl/issue4463-ack-model.smt2 regress0/nl/issue5534-no-assertions.smt2 regress0/nl/issue5726-downpolys.smt2 @@ -1933,6 +1934,7 @@ set(regress_1_tests regress1/nl/issue3803-nl-check-model.smt2 regress1/nl/issue3955-ee-double-notify.smt2 regress1/nl/issue3966-conf-coeff.smt2 + regress1/nl/issue4334-sat-proof.smt2 regress1/nl/issue4791-llr.smt2 regress1/nl/issue5372-2-no-m-presolve.smt2 regress1/nl/issue5461-iand-init-refine.smt2 diff --git a/test/regress/regress0/nl/issue4334-sat-proof-min.smt2 b/test/regress/regress0/nl/issue4334-sat-proof-min.smt2 new file mode 100644 index 000000000..3b5817829 --- /dev/null +++ b/test/regress/regress0/nl/issue4334-sat-proof-min.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: -i -q +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-option :produce-unsat-cores true) +(assert (distinct 0 (mod 0 0))) +(check-sat) +(check-sat) +(check-sat) +(check-sat) \ No newline at end of file diff --git a/test/regress/regress1/nl/issue4334-sat-proof.smt2 b/test/regress/regress1/nl/issue4334-sat-proof.smt2 new file mode 100644 index 000000000..b8ea48b9b --- /dev/null +++ b/test/regress/regress1/nl/issue4334-sat-proof.smt2 @@ -0,0 +1,241 @@ +; COMMAND-LINE: -i --produce-unsat-cores --nl-ext-purify +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +; EXPECT: sat +(set-logic QF_NIA) +(set-option :produce-unsat-cores true) +(set-option :nl-ext-purify true) +(declare-const v0 Bool) +(declare-const v1 Bool) +(declare-const v2 Bool) +(declare-const v3 Bool) +(declare-const v4 Bool) +(declare-const v5 Bool) +(declare-const v6 Bool) +(declare-const v7 Bool) +(declare-const v8 Bool) +(declare-const v9 Bool) +(declare-const v10 Bool) +(declare-const v11 Bool) +(declare-const v12 Bool) +(declare-const v13 Bool) +(declare-const v14 Bool) +(declare-const i0 Int) +(push 1) +(pop 1) +(declare-const v15 Bool) +(declare-const i1 Int) +(declare-const i2 Int) +(declare-const v16 Bool) +(push 1) +(declare-const v17 Bool) +(push 1) +(declare-const v18 Bool) +(declare-const v19 Bool) +(declare-const v20 Bool) +(push 1) +(declare-const v21 Bool) +(declare-const i3 Int) +(declare-const v22 Bool) +(declare-const v23 Bool) +(declare-const v24 Bool) +(declare-const v25 Bool) +(declare-const i4 Int) +(pop 1) +(declare-const i5 Int) +(declare-const v26 Bool) +(declare-const i6 Int) +(declare-const v27 Bool) +(declare-const v28 Bool) +(pop 1) +(declare-const v29 Bool) +(declare-const i7 Int) +(declare-const v30 Bool) +(declare-const v31 Bool) +(declare-const v32 Bool) +(declare-const v33 Bool) +(pop 1) +(declare-const v34 Bool) +(declare-const v35 Bool) +(declare-const v36 Bool) +(declare-const v37 Bool) +(declare-const i8 Int) +(declare-const v38 Bool) +(push 1) +(declare-const v39 Bool) +(pop 1) +(declare-const v40 Bool) +(push 1) +(pop 1) +(declare-const v41 Bool) +(declare-const v42 Bool) +(declare-const i9 Int) +(declare-const v43 Bool) +(declare-const v44 Bool) +(push 1) +(push 1) +(declare-const v45 Bool) +(push 1) +(push 1) +(declare-const v46 Bool) +(declare-const v47 Bool) +(declare-const i10 Int) +(declare-const v48 Bool) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) v16 v11) :named IP_1)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4)) :named IP_2)) +(assert (! (or v16) :named IP_3)) +(assert (! (or v45 (and v9 v4) v16 (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) v11 v16 v45 (and v9 v4) v45 v11 (and v9 v4) (<= (abs 814) 855)) :named IP_4)) +(assert (! (or v45 (and v9 v4) (and v9 v4)) :named IP_5)) +(assert (! (or v45) :named IP_6)) +(assert (! (or (and v9 v4)) :named IP_7)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4)) :named IP_8)) +(assert (! (or (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_9)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_10)) +(assert (! (or (and v9 v4) v11) :named IP_11)) +(assert (! (or (and v9 v4) v11 v16 v45) :named IP_12)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_13)) +(assert (! (or v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_14)) +(assert (! (or (<= (abs 814) 855)) :named IP_15)) +(assert (! (or v11 (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_16)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_17)) +(assert (! (or v11 v11) :named IP_18)) +(assert (! (or v45 v16 (and v9 v4) (and v9 v4) (and v9 v4) v16) :named IP_19)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_20)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v11) :named IP_21)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_22)) +(assert (! (or v16 (and v9 v4) v11 (and v9 v4) v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) v16 v45) :named IP_23)) +(assert (! (or (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16 v45) :named IP_24)) +(assert (! (or v11 v45 v11 v45) :named IP_25)) +(assert (! (or v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855)) :named IP_26)) +(assert (! (or (and v9 v4) (<= (abs 814) 855) (and v9 v4) (<= (abs 814) 855) (<= (abs 814) 855) v45) :named IP_27)) +(assert (! (or v16 v11) :named IP_28)) +(assert (! (or v11 v16) :named IP_29)) +(assert (! (or v11 v11) :named IP_30)) +(assert (! (or v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_31)) +(assert (! (or (and v9 v4)) :named IP_32)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_33)) +(assert (! (or (and v9 v4)) :named IP_34)) +(assert (! (or v11 v11 v16) :named IP_35)) +(assert (! (or v45 (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855)) :named IP_36)) +(assert (! (or v11 v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) v16 (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_37)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_38)) +(assert (! (or v16 v45) :named IP_39)) +(assert (! (or v16 (and v9 v4)) :named IP_40)) +(assert (! (or v45 v45) :named IP_41)) +(assert (! (or v16 v45 v45 v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16) :named IP_42)) +(assert (! (or (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_43)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16 v11) :named IP_44)) +(assert (! (or (<= (abs 814) 855)) :named IP_45)) +(assert (! (or v45 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_46)) +(assert (! (or (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v45 v45) :named IP_47)) +(assert (! (or (and v9 v4) v11) :named IP_48)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16) :named IP_49)) +(assert (! (or (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4)) :named IP_50)) +(assert (! (or (and v9 v4) (and v9 v4)) :named IP_51)) +(assert (! (or v45 (<= (abs 814) 855) v11) :named IP_52)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_53)) +(assert (! (or (and v9 v4) v16 v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45 (<= (abs 814) 855) v45) :named IP_54)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16 v45) :named IP_55)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4)) :named IP_56)) +(assert (! (or (and v9 v4) (<= (abs 814) 855)) :named IP_57)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_58)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45 (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_59)) +(assert (! (or v16 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_60)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) v16 (and v9 v4) v45 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16 (<= (abs 814) 855) v16 (<= (abs 814) 855) v45) :named IP_61)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_62)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_63)) +(assert (! (or v45) :named IP_64)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v11 v16) :named IP_65)) +(assert (! (or (and v9 v4) (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_66)) +(assert (! (or v45 v45) :named IP_67)) +(assert (! (or (and v9 v4) v16 v11 (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4)) :named IP_68)) +(assert (! (or (and v9 v4)) :named IP_69)) +(assert (! (or v16 (<= (abs 814) 855) v45 v16) :named IP_70)) +(assert (! (or v11 v45 v16 (and v9 v4)) :named IP_71)) +(assert (! (or (and v9 v4) (and v9 v4)) :named IP_72)) +(assert (! (or (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_73)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v11) :named IP_74)) +(assert (! (or (<= (abs 814) 855) v16 v11) :named IP_75)) +(assert (! (or (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_76)) +(assert (! (or v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855)) :named IP_77)) +(assert (! (or v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v45) :named IP_78)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4)) :named IP_79)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_80)) +(assert (! (or (<= (abs 814) 855)) :named IP_81)) +(assert (! (or v45 v11 (and v9 v4)) :named IP_82)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16 v45 v16) :named IP_83)) +(assert (! (or (and v9 v4)) :named IP_84)) +(assert (! (or (<= (abs 814) 855) v11 v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_85)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_86)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v16) :named IP_87)) +(assert (! (or v45 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_88)) +(assert (! (or (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16 v16) :named IP_89)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v11 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_90)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_91)) +(assert (! (or v45 v45 v16) :named IP_92)) +(assert (! (or v16) :named IP_93)) +(assert (! (or (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45 (<= (abs 814) 855) v45 (<= (abs 814) 855)) :named IP_94)) +(assert (! (or v45 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_95)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_96)) +(assert (! (or (and v9 v4)) :named IP_97)) +(assert (! (or v11) :named IP_98)) +(assert (! (or v45 (<= (abs 814) 855) (and v9 v4) (<= (abs 814) 855) v16 v45) :named IP_99)) +(assert (! (or (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855)) :named IP_100)) +(assert (! (or (<= (abs 814) 855) (<= (abs 814) 855) (<= (abs 814) 855) v16 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_101)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_102)) +(assert (! (or v11 (and v9 v4)) :named IP_103)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_104)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_105)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v45 v16 (<= (abs 814) 855)) :named IP_106)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (and v9 v4) (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_107)) +(assert (! (or v45 v11 (and v9 v4) v45) :named IP_108)) +(assert (! (or v16) :named IP_109)) +(assert (! (or (and v9 v4) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_110)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45 v16 v11 v45 (and v9 v4)) :named IP_111)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_112)) +(assert (! (or v11 (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_113)) +(assert (! (or v11) :named IP_114)) +(assert (! (or (<= (abs 814) 855)) :named IP_115)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_116)) +(assert (! (or v45) :named IP_117)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) v11 (and v9 v4)) :named IP_118)) +(assert (! (or v16) :named IP_119)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_120)) +(assert (! (or v11 (and v9 v4) v11 (<= (abs 814) 855) v16 v45 (<= (abs 814) 855) v16 (and v9 v4) v16 v45 (<= (abs 814) 855) v16) :named IP_121)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_122)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_123)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_124)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_125)) +(assert (! (or v11 v11 v16) :named IP_126)) +(assert (! (or (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) (<= (abs 814) 855)) :named IP_127)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v45) :named IP_128)) +(assert (! (or v45 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16) :named IP_129)) +(assert (! (or v16 v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_130)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_131)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_132)) +(assert (! (or (<= (abs 814) 855)) :named IP_133)) +(assert (! (or v11) :named IP_134)) +(assert (! (or (<= (abs 814) 855) v45) :named IP_135)) +(assert (! (or v16 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_136)) +(assert (! (or (<= (abs 814) 855) v16 v11) :named IP_137)) +(assert (! (or v45 (<= (abs 814) 855) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4)) :named IP_138)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_139)) +(assert (! (or v45) :named IP_140)) +(assert (! (or (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0)) :named IP_141)) +(assert (! (or v16 v45 (<= (abs 814) 855)) :named IP_142)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (<= (abs 814) 855) (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) v45 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) v16) :named IP_143)) +(assert (! (or v11 (=> (and (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct 815 (mod 814 (- 855 i1 (* i0 i0)))) (distinct v34 v35 v9 v36 v38 v35) v38 v5 v4 v35) v0) (<= (abs 814) 855) v11) :named IP_144)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815))) :named IP_145)) +(assert (! (or v11) :named IP_146)) +(assert (! (or (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4) (and v9 v4)) :named IP_147)) +(assert (! (or v11 v45 (distinct (abs (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (* (mod 855 824) (+ i1 814 (* i0 i0) 855) (mod 281 814) (- 855 i1 (* i0 i0)) 815)) (and v9 v4)) :named IP_148)) +(assert (! (or v11) :named IP_149)) +(assert (! (or (and v9 v4) (<= (abs 814) 855)) :named IP_150)) +(assert (! (or v16 v16) :named IP_151)) +(assert (! (or v45 v16) :named IP_152)) +(check-sat) +(check-sat-assuming (IP_144 IP_147)) +(check-sat-assuming (IP_35 IP_87)) +(check-sat-assuming (IP_55 IP_106)) +(exit)