diff options
Diffstat (limited to 'test/regress/regress1/ho/fta0409.smt2')
| -rw-r--r-- | test/regress/regress1/ho/fta0409.smt2 | 427 |
1 files changed, 427 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/fta0409.smt2 b/test/regress/regress1/ho/fta0409.smt2 new file mode 100644 index 000000000..51ac5f2da --- /dev/null +++ b/test/regress/regress1/ho/fta0409.smt2 @@ -0,0 +1,427 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-sort Nat$ 0) +(declare-sort Complex$ 0) +(declare-sort Nat_poly$ 0) +(declare-sort Complex_poly$ 0) +(declare-sort Complex_poly_poly$ 0) +(declare-fun n$ () Nat$) +(declare-fun q$ () Complex_poly$) +(declare-fun r$ () Complex_poly$) +(declare-fun dvd$ (Complex_poly$ Complex_poly$) Bool) +(declare-fun one$ () Nat$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun dvd$a (Complex$ Complex$) Bool) +(declare-fun dvd$b (Nat$ Nat$) Bool) +(declare-fun dvd$c (Complex_poly_poly$ Complex_poly_poly$) Bool) +(declare-fun dvd$d (Nat_poly$ Nat_poly$) Bool) +(declare-fun one$a () Complex_poly$) +(declare-fun one$b () Complex$) +(declare-fun one$c () Nat_poly$) +(declare-fun plus$ (Complex$ Complex$) Complex$) +(declare-fun poly$ (Complex_poly$) (-> Complex$ Complex$)) +(declare-fun zero$ () Complex$) +(declare-fun coeff$ (Complex_poly_poly$ Nat$) Complex_poly$) +(declare-fun monom$ (Complex$ Nat$) Complex_poly$) +(declare-fun order$ (Complex$ Complex_poly$) Nat$) +(declare-fun pCons$ (Complex$ Complex_poly$) Complex_poly$) +(declare-fun plus$a (Nat$ Nat$) Nat$) +(declare-fun plus$b (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun plus$c (Complex_poly$ Complex_poly$) Complex_poly$) +(declare-fun poly$a (Complex_poly_poly$ Complex_poly$) Complex_poly$) +(declare-fun poly$b (Nat_poly$ Nat$) Nat$) +(declare-fun power$ (Complex_poly$ Nat$) Complex_poly$) +(declare-fun psize$ (Complex_poly$) Nat$) +(declare-fun times$ (Nat$ Nat$) Nat$) +(declare-fun zero$a () Nat$) +(declare-fun zero$b () Complex_poly_poly$) +(declare-fun zero$c () Complex_poly$) +(declare-fun zero$d () Nat_poly$) +(declare-fun coeff$a (Nat_poly$ Nat$) Nat$) +(declare-fun coeff$b (Complex_poly$ Nat$) Complex$) +(declare-fun degree$ (Complex_poly_poly$) Nat$) +(declare-fun monom$a (Complex_poly$ Nat$) Complex_poly_poly$) +(declare-fun monom$b (Nat$ Nat$) Nat_poly$) +(declare-fun order$a (Complex_poly$ Complex_poly_poly$) Nat$) +(declare-fun pCons$a (Complex_poly$ Complex_poly_poly$) Complex_poly_poly$) +(declare-fun pCons$b (Nat$ Nat_poly$) Nat_poly$) +(declare-fun power$a (Complex_poly_poly$ Nat$) Complex_poly_poly$) +(declare-fun power$b (Nat_poly$ Nat$) Nat_poly$) +(declare-fun power$c (Nat$ Nat$) Nat$) +(declare-fun power$d (Complex$ Nat$) Complex$) +(declare-fun degree$a (Nat_poly$) Nat$) +(declare-fun degree$b (Complex_poly$) Nat$) +(declare-fun is_zero$ (Complex_poly$) Bool) +(declare-fun less_eq$ (Nat$ Nat$) Bool) +(declare-fun of_bool$ (Bool) Complex$) +(declare-fun constant$ ((-> Complex$ Complex$)) Bool) +(declare-fun of_bool$a (Bool) Complex_poly$) +(declare-fun of_bool$b (Bool) Nat$) +(declare-fun pcompose$ (Complex_poly$ Complex_poly$) Complex_poly$) +(declare-fun pcompose$a (Complex_poly_poly$ Complex_poly_poly$) Complex_poly_poly$) +(declare-fun pcompose$b (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun poly_shift$ (Nat$ Complex_poly$) Complex_poly$) +(declare-fun offset_poly$ (Complex_poly$ Complex$) Complex_poly$) +(declare-fun poly_cutoff$ (Nat$ Complex_poly$) Complex_poly$) +(declare-fun rsquarefree$ (Complex_poly$) Bool) +(declare-fun offset_poly$a (Nat_poly$ Nat$) Nat_poly$) +(declare-fun reflect_poly$ (Complex_poly$) Complex_poly$) +(declare-fun reflect_poly$a (Complex_poly_poly$) Complex_poly_poly$) +(declare-fun reflect_poly$b (Nat_poly$) Nat_poly$) +(declare-fun synthetic_div$ (Complex_poly$ Complex$) Complex_poly$) +(assert (! (not (= (poly$ (power$ q$ n$)) (poly$ r$))) :named a0)) +(assert (! (forall ((?v0 Complex$)) (= (poly$ (power$ q$ n$) ?v0) (poly$ r$ ?v0))) :named a1)) +(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Nat$) (?v2 Complex_poly$)) (= (poly$a (power$a ?v0 ?v1) ?v2) (power$ (poly$a ?v0 ?v2) ?v1))) :named a2)) +(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$) (?v2 Nat$)) (= (poly$b (power$b ?v0 ?v1) ?v2) (power$c (poly$b ?v0 ?v2) ?v1))) :named a3)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Complex$)) (= (poly$ (power$ ?v0 ?v1) ?v2) (power$d (poly$ ?v0 ?v2) ?v1))) :named a4)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= (poly$ ?v0) (poly$ ?v1)) (= ?v0 ?v1))) :named a5)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (not (constant$ (poly$ ?v0))) (exists ((?v1 Complex$)) (= (poly$ ?v0 ?v1) zero$)))) :named a6)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (reflect_poly$ (power$ ?v0 ?v1)) (power$ (reflect_poly$ ?v0) ?v1))) :named a7)) +(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Nat$)) (= (coeff$ (power$a ?v0 ?v1) zero$a) (power$ (coeff$ ?v0 zero$a) ?v1))) :named a8)) +(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$)) (= (coeff$a (power$b ?v0 ?v1) zero$a) (power$c (coeff$a ?v0 zero$a) ?v1))) :named a9)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (coeff$b (power$ ?v0 ?v1) zero$a) (power$d (coeff$b ?v0 zero$a) ?v1))) :named a10)) +(assert (! (forall ((?v0 (-> Complex$ Complex$))) (= (constant$ ?v0) (forall ((?v1 Complex$) (?v2 Complex$)) (= (?v0 ?v1) (?v0 ?v2))))) :named a11)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (exists ((?v2 Complex_poly$)) (and (= (psize$ ?v2) (psize$ ?v0)) (forall ((?v3 Complex$)) (= (poly$ ?v2 ?v3) (poly$ ?v0 (plus$ ?v1 ?v3))))))) :named a12)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$) (?v2 Complex$)) (= (poly$ (offset_poly$ ?v0 ?v1) ?v2) (poly$ ?v0 (plus$ ?v1 ?v2)))) :named a13)) +(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$) (?v2 Nat$)) (= (poly$b (offset_poly$a ?v0 ?v1) ?v2) (poly$b ?v0 (plus$a ?v1 ?v2)))) :named a14)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex$)) (= (poly$ (pcompose$ ?v0 ?v1) ?v2) (poly$ ?v0 (poly$ ?v1 ?v2)))) :named a15)) +(assert (! (forall ((?v0 Complex_poly$)) (= (power$ ?v0 one$) ?v0)) :named a16)) +(assert (! (forall ((?v0 Nat$)) (= (power$c ?v0 one$) ?v0)) :named a17)) +(assert (! (forall ((?v0 Nat$)) (= (power$ one$a ?v0) one$a)) :named a18)) +(assert (! (forall ((?v0 Nat$)) (= (power$c one$ ?v0) one$)) :named a19)) +(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Nat$)) (= (coeff$ (power$a ?v0 ?v1) (degree$ (power$a ?v0 ?v1))) (power$ (coeff$ ?v0 (degree$ ?v0)) ?v1))) :named a20)) +(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$)) (= (coeff$a (power$b ?v0 ?v1) (degree$a (power$b ?v0 ?v1))) (power$c (coeff$a ?v0 (degree$a ?v0)) ?v1))) :named a21)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (coeff$b (power$ ?v0 ?v1) (degree$b (power$ ?v0 ?v1))) (power$d (coeff$b ?v0 (degree$b ?v0)) ?v1))) :named a22)) +(assert (! (forall ((?v0 Nat$)) (= (coeff$ zero$b ?v0) zero$c)) :named a23)) +(assert (! (forall ((?v0 Nat$)) (= (coeff$a zero$d ?v0) zero$a)) :named a24)) +(assert (! (forall ((?v0 Nat$)) (= (coeff$b zero$c ?v0) zero$)) :named a25)) +(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat_poly$) (?v2 Nat$)) (= (coeff$a (plus$b ?v0 ?v1) ?v2) (plus$a (coeff$a ?v0 ?v2) (coeff$a ?v1 ?v2)))) :named a26)) +(assert (! (forall ((?v0 Complex_poly$)) (= (poly$a zero$b ?v0) zero$c)) :named a27)) +(assert (! (forall ((?v0 Nat$)) (= (poly$b zero$d ?v0) zero$a)) :named a28)) +(assert (! (forall ((?v0 Complex$)) (= (poly$ zero$c ?v0) zero$)) :named a29)) +(assert (! (= (degree$b one$a) zero$a) :named a30)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex$)) (= (poly$ (plus$c ?v0 ?v1) ?v2) (plus$ (poly$ ?v0 ?v2) (poly$ ?v1 ?v2)))) :named a31)) +(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat_poly$) (?v2 Nat$)) (= (poly$b (plus$b ?v0 ?v1) ?v2) (plus$a (poly$b ?v0 ?v2) (poly$b ?v1 ?v2)))) :named a32)) +(assert (! (forall ((?v0 Complex$)) (= (poly$ one$a ?v0) one$b)) :named a33)) +(assert (! (forall ((?v0 Nat$)) (= (poly$b one$c ?v0) one$)) :named a34)) +(assert (! (forall ((?v0 Complex_poly$)) (= (= (coeff$b ?v0 (degree$b ?v0)) zero$) (= ?v0 zero$c))) :named a35)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (= (= (coeff$ ?v0 (degree$ ?v0)) zero$c) (= ?v0 zero$b))) :named a36)) +(assert (! (forall ((?v0 Nat_poly$)) (= (= (coeff$a ?v0 (degree$a ?v0)) zero$a) (= ?v0 zero$d))) :named a37)) +(assert (! (= (coeff$b one$a (degree$b one$a)) one$b) :named a38)) +(assert (! (= (coeff$a one$c (degree$a one$c)) one$) :named a39)) +(assert (! (forall ((?v0 Complex_poly$)) (= (= (poly$ (reflect_poly$ ?v0) zero$) zero$) (= ?v0 zero$c))) :named a40)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (= (= (poly$a (reflect_poly$a ?v0) zero$c) zero$c) (= ?v0 zero$b))) :named a41)) +(assert (! (forall ((?v0 Nat_poly$)) (= (= (poly$b (reflect_poly$b ?v0) zero$a) zero$a) (= ?v0 zero$d))) :named a42)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (not (= (coeff$b ?v0 zero$a) zero$)) (= (reflect_poly$ (reflect_poly$ ?v0)) ?v0))) :named a43)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (=> (not (= (coeff$ ?v0 zero$a) zero$c)) (= (reflect_poly$a (reflect_poly$a ?v0)) ?v0))) :named a44)) +(assert (! (forall ((?v0 Nat_poly$)) (=> (not (= (coeff$a ?v0 zero$a) zero$a)) (= (reflect_poly$b (reflect_poly$b ?v0)) ?v0))) :named a45)) +(assert (! (forall ((?v0 Complex_poly$)) (= (= (coeff$b (reflect_poly$ ?v0) zero$a) zero$) (= ?v0 zero$c))) :named a46)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (= (= (coeff$ (reflect_poly$a ?v0) zero$a) zero$c) (= ?v0 zero$b))) :named a47)) +(assert (! (forall ((?v0 Nat_poly$)) (= (= (coeff$a (reflect_poly$b ?v0) zero$a) zero$a) (= ?v0 zero$d))) :named a48)) +(assert (! (forall ((?v0 Complex_poly$)) (= (coeff$b (reflect_poly$ ?v0) zero$a) (coeff$b ?v0 (degree$b ?v0)))) :named a49)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (not (= (coeff$b ?v0 zero$a) zero$)) (= (degree$b (reflect_poly$ ?v0)) (degree$b ?v0)))) :named a50)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (=> (not (= (coeff$ ?v0 zero$a) zero$c)) (= (degree$ (reflect_poly$a ?v0)) (degree$ ?v0)))) :named a51)) +(assert (! (forall ((?v0 Nat_poly$)) (=> (not (= (coeff$a ?v0 zero$a) zero$a)) (= (degree$a (reflect_poly$b ?v0)) (degree$a ?v0)))) :named a52)) +(assert (! (forall ((?v0 Complex_poly$)) (= (poly$ (reflect_poly$ ?v0) zero$) (coeff$b ?v0 (degree$b ?v0)))) :named a53)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (= (poly$a (reflect_poly$a ?v0) zero$c) (coeff$ ?v0 (degree$ ?v0)))) :named a54)) +(assert (! (forall ((?v0 Nat_poly$)) (= (poly$b (reflect_poly$b ?v0) zero$a) (coeff$a ?v0 (degree$a ?v0)))) :named a55)) +(assert (! (forall ((?v0 Complex_poly$)) (= (poly$ ?v0 zero$) (coeff$b ?v0 zero$a))) :named a56)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (= (poly$a ?v0 zero$c) (coeff$ ?v0 zero$a))) :named a57)) +(assert (! (forall ((?v0 Nat_poly$)) (= (poly$b ?v0 zero$a) (coeff$a ?v0 zero$a))) :named a58)) +(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat_poly$) (?v2 Nat$)) (= (coeff$a (plus$b ?v0 ?v1) ?v2) (plus$a (coeff$a ?v0 ?v2) (coeff$a ?v1 ?v2)))) :named a59)) +(assert (! (forall ((?v0 Complex_poly$)) (= (forall ((?v1 Complex$)) (= (poly$ ?v0 ?v1) zero$)) (= ?v0 zero$c))) :named a60)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (= (forall ((?v1 Complex_poly$)) (= (poly$a ?v0 ?v1) zero$c)) (= ?v0 zero$b))) :named a61)) +(assert (! (forall ((?v0 Nat$)) (= (coeff$ zero$b ?v0) zero$c)) :named a62)) +(assert (! (forall ((?v0 Nat$)) (= (coeff$a zero$d ?v0) zero$a)) :named a63)) +(assert (! (forall ((?v0 Nat$)) (= (coeff$b zero$c ?v0) zero$)) :named a64)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (=> (not (= ?v0 zero$b)) (not (= (coeff$ ?v0 (degree$ ?v0)) zero$c)))) :named a65)) +(assert (! (forall ((?v0 Nat_poly$)) (=> (not (= ?v0 zero$d)) (not (= (coeff$a ?v0 (degree$a ?v0)) zero$a)))) :named a66)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (not (= ?v0 zero$c)) (not (= (coeff$b ?v0 (degree$b ?v0)) zero$)))) :named a67)) +(assert (! (forall ((?v0 Complex_poly$)) (! (= (power$ ?v0 zero$a) one$a) :pattern ((power$ ?v0)))) :named a68)) +(assert (! (forall ((?v0 Nat$)) (! (= (power$c ?v0 zero$a) one$) :pattern ((power$c ?v0)))) :named a69)) +(assert (! (forall ((?v0 Nat$)) (= (power$d zero$ ?v0) (ite (= ?v0 zero$a) one$b zero$))) :named a70)) +(assert (! (forall ((?v0 Nat$)) (= (power$ zero$c ?v0) (ite (= ?v0 zero$a) one$a zero$c))) :named a71)) +(assert (! (forall ((?v0 Nat$)) (= (power$c zero$a ?v0) (ite (= ?v0 zero$a) one$ zero$a))) :named a72)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (= (degree$b (offset_poly$ ?v0 ?v1)) (degree$b ?v0))) :named a73)) +(assert (! (forall ((?v0 Complex_poly$)) (= (constant$ (poly$ ?v0)) (= (degree$b ?v0) zero$a))) :named a74)) +(assert (! (forall ((?v0 Complex$)) (= zero$ (poly$ zero$c ?v0))) :named a75)) +(assert (! (forall ((?v0 Complex_poly$)) (= zero$c (poly$a zero$b ?v0))) :named a76)) +(assert (! (forall ((?v0 Complex_poly$)) (= (exists ((?v1 Complex$)) (and (= (poly$ ?v0 ?v1) zero$) (not (= (poly$ zero$c ?v1) zero$)))) false)) :named a77)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (= (exists ((?v1 Complex_poly$)) (and (= (poly$a ?v0 ?v1) zero$c) (not (= (poly$a zero$b ?v1) zero$c)))) false)) :named a78)) +(assert (! (forall ((?v0 Nat_poly$)) (= (exists ((?v1 Nat$)) (and (= (poly$b ?v0 ?v1) zero$a) (not (= (poly$b zero$d ?v1) zero$a)))) false)) :named a79)) +(assert (! (= (exists ((?v0 Complex_poly$)) (not (= (poly$a zero$b ?v0) zero$c))) false) :named a80)) +(assert (! (= (exists ((?v0 Nat$)) (not (= (poly$b zero$d ?v0) zero$a))) false) :named a81)) +(assert (! (= (exists ((?v0 Complex$)) (not (= (poly$ zero$c ?v0) zero$))) false) :named a82)) +(assert (! (= (exists ((?v0 Complex_poly$)) (= (poly$a zero$b ?v0) zero$c)) true) :named a83)) +(assert (! (= (exists ((?v0 Nat$)) (= (poly$b zero$d ?v0) zero$a)) true) :named a84)) +(assert (! (= (exists ((?v0 Complex$)) (= (poly$ zero$c ?v0) zero$)) true) :named a85)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (=> (not (= ?v0 zero$)) (not (= (power$d ?v0 ?v1) zero$)))) :named a86)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (=> (not (= ?v0 zero$c)) (not (= (power$ ?v0 ?v1) zero$c)))) :named a87)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (not (= ?v0 zero$a)) (not (= (power$c ?v0 ?v1) zero$a)))) :named a88)) +(assert (! (forall ((?v0 Complex$)) (= (plus$ zero$ ?v0) ?v0)) :named a89)) +(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c zero$c ?v0) ?v0)) :named a90)) +(assert (! (forall ((?v0 Nat$)) (= (plus$a zero$a ?v0) ?v0)) :named a91)) +(assert (! (forall ((?v0 Complex$)) (= (plus$ ?v0 zero$) ?v0)) :named a92)) +(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c ?v0 zero$c) ?v0)) :named a93)) +(assert (! (forall ((?v0 Nat$)) (= (plus$a ?v0 zero$a) ?v0)) :named a94)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= (plus$ ?v0 ?v1) ?v1) (= ?v0 zero$))) :named a95)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= (plus$c ?v0 ?v1) ?v1) (= ?v0 zero$c))) :named a96)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (plus$a ?v0 ?v1) ?v1) (= ?v0 zero$a))) :named a97)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= (plus$ ?v0 ?v1) ?v0) (= ?v1 zero$))) :named a98)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= (plus$c ?v0 ?v1) ?v0) (= ?v1 zero$c))) :named a99)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (plus$a ?v0 ?v1) ?v0) (= ?v1 zero$a))) :named a100)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= ?v0 (plus$ ?v1 ?v0)) (= ?v1 zero$))) :named a101)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= ?v0 (plus$c ?v1 ?v0)) (= ?v1 zero$c))) :named a102)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= ?v0 (plus$a ?v1 ?v0)) (= ?v1 zero$a))) :named a103)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= ?v0 (plus$ ?v0 ?v1)) (= ?v1 zero$))) :named a104)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= ?v0 (plus$c ?v0 ?v1)) (= ?v1 zero$c))) :named a105)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= ?v0 (plus$a ?v0 ?v1)) (= ?v1 zero$a))) :named a106)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (plus$a ?v0 ?v1) zero$a) (and (= ?v0 zero$a) (= ?v1 zero$a)))) :named a107)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= zero$a (plus$a ?v0 ?v1)) (and (= ?v0 zero$a) (= ?v1 zero$a)))) :named a108)) +(assert (! (forall ((?v0 Complex_poly$)) (! (= (power$ ?v0 zero$a) one$a) :pattern ((power$ ?v0)))) :named a109)) +(assert (! (forall ((?v0 Nat$)) (! (= (power$c ?v0 zero$a) one$) :pattern ((power$c ?v0)))) :named a110)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (plus$a ?v0 ?v1) (plus$a ?v2 ?v1)) (= ?v0 ?v2))) :named a111)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (plus$a ?v0 ?v1) (plus$a ?v0 ?v2)) (= ?v1 ?v2))) :named a112)) +(assert (! (forall ((?v0 Complex_poly$)) (= (pcompose$ zero$c ?v0) zero$c)) :named a113)) +(assert (! (= (reflect_poly$ zero$c) zero$c) :named a114)) +(assert (! (= (degree$b zero$c) zero$a) :named a115)) +(assert (! (forall ((?v0 Complex_poly$)) (= (= (psize$ ?v0) zero$a) (= ?v0 zero$c))) :named a116)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (= (= (offset_poly$ ?v0 ?v1) zero$c) (= ?v0 zero$c))) :named a117)) +(assert (! (forall ((?v0 Complex$)) (= (offset_poly$ zero$c ?v0) zero$c)) :named a118)) +(assert (! (forall ((?v0 Complex_poly$)) (= (exists ((?v1 Complex$)) (not (= (poly$ ?v0 ?v1) zero$))) (not (= ?v0 zero$c)))) :named a119)) +(assert (! (forall ((?v0 Complex$)) (= (= zero$ ?v0) (= ?v0 zero$))) :named a120)) +(assert (! (forall ((?v0 Complex_poly$)) (= (= zero$c ?v0) (= ?v0 zero$c))) :named a121)) +(assert (! (forall ((?v0 Nat$)) (= (= zero$a ?v0) (= ?v0 zero$a))) :named a122)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (= (plus$a ?v0 ?v1) (plus$a ?v2 ?v1)) (= ?v0 ?v2))) :named a123)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (= (plus$a ?v0 ?v1) (plus$a ?v0 ?v2)) (= ?v1 ?v2))) :named a124)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a ?v0 (plus$a ?v1 ?v2)) (plus$a ?v1 (plus$a ?v0 ?v2)))) :named a125)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (plus$a ?v0 ?v1) (plus$a ?v1 ?v0))) :named a126)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a (plus$a ?v0 ?v1) ?v2) (plus$a ?v0 (plus$a ?v1 ?v2)))) :named a127)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$) (?v3 Nat$)) (= (plus$a (plus$a ?v0 ?v1) (plus$a ?v2 ?v3)) (plus$a (plus$a ?v0 ?v2) (plus$a ?v1 ?v3)))) :named a128)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a (plus$a ?v0 ?v1) ?v2) (plus$a ?v0 (plus$a ?v1 ?v2)))) :named a129)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a ?v0 (plus$a ?v1 ?v2)) (plus$a ?v1 (plus$a ?v0 ?v2)))) :named a130)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a (plus$a ?v0 ?v1) ?v2) (plus$a (plus$a ?v0 ?v2) ?v1))) :named a131)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (plus$a ?v0 ?v1) (plus$a ?v1 ?v0))) :named a132)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a ?v0 (plus$a ?v1 ?v2)) (plus$a (plus$a ?v0 ?v1) ?v2))) :named a133)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$) (?v3 Nat$)) (=> (and (= ?v0 ?v1) (= ?v2 ?v3)) (= (plus$a ?v0 ?v2) (plus$a ?v1 ?v3)))) :named a134)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$a (plus$a ?v0 ?v1) ?v2) (plus$a ?v0 (plus$a ?v1 ?v2)))) :named a135)) +(assert (! (forall ((?v0 Nat$)) (= (= one$ ?v0) (= ?v0 one$))) :named a136)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (= ?v0 (plus$ ?v0 ?v1)) (= ?v1 zero$))) :named a137)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (= ?v0 (plus$c ?v0 ?v1)) (= ?v1 zero$c))) :named a138)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= ?v0 (plus$a ?v0 ?v1)) (= ?v1 zero$a))) :named a139)) +(assert (! (forall ((?v0 Complex$)) (= (plus$ zero$ ?v0) ?v0)) :named a140)) +(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c zero$c ?v0) ?v0)) :named a141)) +(assert (! (forall ((?v0 Complex$)) (= (plus$ ?v0 zero$) ?v0)) :named a142)) +(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c ?v0 zero$c) ?v0)) :named a143)) +(assert (! (forall ((?v0 Nat$)) (= (plus$a ?v0 zero$a) ?v0)) :named a144)) +(assert (! (forall ((?v0 Complex$)) (= (plus$ zero$ ?v0) ?v0)) :named a145)) +(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c zero$c ?v0) ?v0)) :named a146)) +(assert (! (forall ((?v0 Nat$)) (= (plus$a zero$a ?v0) ?v0)) :named a147)) +(assert (! (forall ((?v0 Complex$)) (= (plus$ zero$ ?v0) ?v0)) :named a148)) +(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c zero$c ?v0) ?v0)) :named a149)) +(assert (! (forall ((?v0 Nat$)) (= (plus$a zero$a ?v0) ?v0)) :named a150)) +(assert (! (forall ((?v0 Complex$)) (= (plus$ ?v0 zero$) ?v0)) :named a151)) +(assert (! (forall ((?v0 Complex_poly$)) (= (plus$c ?v0 zero$c) ?v0)) :named a152)) +(assert (! (forall ((?v0 Nat$)) (= (plus$a ?v0 zero$a) ?v0)) :named a153)) +(assert (! (forall ((?v0 Complex_poly$)) (= (power$ ?v0 one$) ?v0)) :named a154)) +(assert (! (forall ((?v0 Nat$)) (= (power$c ?v0 one$) ?v0)) :named a155)) +(assert (! (forall ((?v0 Nat$)) (= (poly_cutoff$ ?v0 one$a) (ite (= ?v0 zero$a) zero$c one$a))) :named a156)) +(assert (! (forall ((?v0 Nat$)) (= (plus$a ?v0 zero$a) ?v0)) :named a157)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (plus$a ?v0 ?v1) zero$a) (and (= ?v0 zero$a) (= ?v1 zero$a)))) :named a158)) +(assert (! (forall ((?v0 Nat$)) (= (poly_shift$ ?v0 one$a) (ite (= ?v0 zero$a) one$a zero$c))) :named a159)) +(assert (! (not (= zero$ one$b)) :named a160)) +(assert (! (not (= zero$c one$a)) :named a161)) +(assert (! (not (= zero$a one$)) :named a162)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (= (= (synthetic_div$ ?v0 ?v1) zero$c) (= (degree$b ?v0) zero$a))) :named a163)) +(assert (! (= (of_bool$ false) zero$) :named a164)) +(assert (! (= (of_bool$a false) zero$c) :named a165)) +(assert (! (= (of_bool$b false) zero$a) :named a166)) +(assert (! (= (of_bool$b true) one$) :named a167)) +(assert (! (forall ((?v0 Complex$)) (= (synthetic_div$ zero$c ?v0) zero$c)) :named a168)) +(assert (! (forall ((?v0 Nat$)) (= (poly_shift$ ?v0 zero$c) zero$c)) :named a169)) +(assert (! (forall ((?v0 Nat$)) (= (poly_cutoff$ ?v0 zero$c) zero$c)) :named a170)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (plus$a ?v0 ?v1) (plus$a ?v0 ?v2)) (= ?v1 ?v2))) :named a171)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (plus$a ?v0 ?v1) (plus$a ?v2 ?v1)) (= ?v0 ?v2))) :named a172)) +(assert (! (forall ((?v0 Bool)) (! (= (of_bool$ ?v0) (ite ?v0 one$b zero$)) :pattern ((of_bool$ ?v0)))) :named a173)) +(assert (! (forall ((?v0 Bool)) (! (= (of_bool$a ?v0) (ite ?v0 one$a zero$c)) :pattern ((of_bool$a ?v0)))) :named a174)) +(assert (! (forall ((?v0 Bool)) (! (= (of_bool$b ?v0) (ite ?v0 one$ zero$a)) :pattern ((of_bool$b ?v0)))) :named a175)) +(assert (! (forall ((?v0 (-> Complex$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$ ?v1)) (and (=> ?v1 (?v0 one$b)) (=> (not ?v1) (?v0 zero$))))) :named a176)) +(assert (! (forall ((?v0 (-> Complex_poly$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$a ?v1)) (and (=> ?v1 (?v0 one$a)) (=> (not ?v1) (?v0 zero$c))))) :named a177)) +(assert (! (forall ((?v0 (-> Nat$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$b ?v1)) (and (=> ?v1 (?v0 one$)) (=> (not ?v1) (?v0 zero$a))))) :named a178)) +(assert (! (forall ((?v0 (-> Complex$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$ ?v1)) (not (or (and ?v1 (not (?v0 one$b))) (and (not ?v1) (not (?v0 zero$))))))) :named a179)) +(assert (! (forall ((?v0 (-> Complex_poly$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$a ?v1)) (not (or (and ?v1 (not (?v0 one$a))) (and (not ?v1) (not (?v0 zero$c))))))) :named a180)) +(assert (! (forall ((?v0 (-> Nat$ Bool)) (?v1 Bool)) (= (?v0 (of_bool$b ?v1)) (not (or (and ?v1 (not (?v0 one$))) (and (not ?v1) (not (?v0 zero$a))))))) :named a181)) +(assert (! (forall ((?v0 Nat$)) (= (plus$a zero$a ?v0) ?v0)) :named a182)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (= (plus$a ?v0 ?v1) ?v0) (= ?v1 zero$a))) :named a183)) +(assert (! (forall ((?v0 Nat$)) (=> (and (=> (= ?v0 zero$a) false) (=> (not (= ?v0 zero$a)) false)) false)) :named a184)) +(assert (! (forall ((?v0 (-> Nat$ (-> Nat$ Bool))) (?v1 Nat$) (?v2 Nat$)) (=> (and (forall ((?v3 Nat$) (?v4 Nat$)) (= (?v0 ?v3 ?v4) (?v0 ?v4 ?v3))) (and (forall ((?v3 Nat$)) (?v0 ?v3 zero$a)) (forall ((?v3 Nat$) (?v4 Nat$)) (=> (?v0 ?v3 ?v4) (?v0 ?v3 (plus$a ?v3 ?v4)))))) (?v0 ?v1 ?v2))) :named a185)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (forall ((?v2 Complex$)) (=> (= (poly$ ?v0 ?v2) zero$) (= (poly$ ?v1 ?v2) zero$))) (or (dvd$ ?v0 (power$ ?v1 (degree$b ?v0))) (and (= ?v0 zero$c) (= ?v1 zero$c))))) :named a186)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Nat$)) (=> (and (forall ((?v3 Complex$)) (=> (= (poly$ ?v0 ?v3) zero$) (= (poly$ ?v1 ?v3) zero$))) (and (= (degree$b ?v0) ?v2) (not (= ?v2 zero$a)))) (dvd$ ?v0 (power$ ?v1 ?v2)))) :named a187)) +(assert (! (forall ((?v0 Complex_poly$)) (! (= (is_zero$ ?v0) (= ?v0 zero$c)) :pattern ((is_zero$ ?v0)))) :named a188)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (= (= (poly$ ?v0 ?v1) zero$) (or (= ?v0 zero$c) (not (= (order$ ?v1 ?v0) zero$a))))) :named a189)) +(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Complex_poly$)) (= (= (poly$a ?v0 ?v1) zero$c) (or (= ?v0 zero$b) (not (= (order$a ?v1 ?v0) zero$a))))) :named a190)) +(assert (! (forall ((?v0 Complex$)) (dvd$a ?v0 zero$)) :named a191)) +(assert (! (forall ((?v0 Complex_poly$)) (dvd$ ?v0 zero$c)) :named a192)) +(assert (! (forall ((?v0 Nat$)) (dvd$b ?v0 zero$a)) :named a193)) +(assert (! (forall ((?v0 Complex$)) (= (dvd$a zero$ ?v0) (= ?v0 zero$))) :named a194)) +(assert (! (forall ((?v0 Complex_poly$)) (= (dvd$ zero$c ?v0) (= ?v0 zero$c))) :named a195)) +(assert (! (forall ((?v0 Nat$)) (= (dvd$b zero$a ?v0) (= ?v0 zero$a))) :named a196)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (dvd$ ?v0 (plus$c ?v0 ?v1)) (dvd$ ?v0 ?v1))) :named a197)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (dvd$b ?v0 (plus$a ?v0 ?v1)) (dvd$b ?v0 ?v1))) :named a198)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (dvd$ ?v0 (plus$c ?v1 ?v0)) (dvd$ ?v0 ?v1))) :named a199)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (dvd$b ?v0 (plus$a ?v1 ?v0)) (dvd$b ?v0 ?v1))) :named a200)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (not (= ?v0 zero$a)) (= (dvd$b (power$c ?v1 ?v0) (power$c ?v2 ?v0)) (dvd$b ?v1 ?v2)))) :named a201)) +(assert (! (forall ((?v0 Complex$)) (=> (dvd$a zero$ ?v0) (= ?v0 zero$))) :named a202)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (dvd$ zero$c ?v0) (= ?v0 zero$c))) :named a203)) +(assert (! (forall ((?v0 Nat$)) (=> (dvd$b zero$a ?v0) (= ?v0 zero$a))) :named a204)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (dvd$ ?v0 ?v1) (= (dvd$ ?v0 (plus$c ?v1 ?v2)) (dvd$ ?v0 ?v2)))) :named a205)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (dvd$b ?v0 ?v1) (= (dvd$b ?v0 (plus$a ?v1 ?v2)) (dvd$b ?v0 ?v2)))) :named a206)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (dvd$ ?v0 ?v1) (= (dvd$ ?v0 (plus$c ?v2 ?v1)) (dvd$ ?v0 ?v2)))) :named a207)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (dvd$b ?v0 ?v1) (= (dvd$b ?v0 (plus$a ?v2 ?v1)) (dvd$b ?v0 ?v2)))) :named a208)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (and (dvd$ ?v0 ?v1) (dvd$ ?v0 ?v2)) (dvd$ ?v0 (plus$c ?v1 ?v2)))) :named a209)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (and (dvd$b ?v0 ?v1) (dvd$b ?v0 ?v2)) (dvd$b ?v0 (plus$a ?v1 ?v2)))) :named a210)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (=> (and (dvd$ ?v0 ?v1) (dvd$ ?v1 one$a)) (dvd$ ?v0 one$a))) :named a211)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (and (dvd$b ?v0 ?v1) (dvd$b ?v1 one$)) (dvd$b ?v0 one$))) :named a212)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (=> (dvd$ ?v0 one$a) (dvd$ ?v0 ?v1))) :named a213)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (dvd$b ?v0 one$) (dvd$b ?v0 ?v1))) :named a214)) +(assert (! (forall ((?v0 Complex_poly$)) (dvd$ one$a ?v0)) :named a215)) +(assert (! (forall ((?v0 Nat$)) (dvd$b one$ ?v0)) :named a216)) +(assert (! (forall ((?v0 Complex_poly$)) (dvd$ ?v0 ?v0)) :named a217)) +(assert (! (forall ((?v0 Nat$)) (dvd$b ?v0 ?v0)) :named a218)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (and (dvd$ ?v0 ?v1) (dvd$ ?v1 ?v2)) (dvd$ ?v0 ?v2))) :named a219)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (and (dvd$b ?v0 ?v1) (dvd$b ?v1 ?v2)) (dvd$b ?v0 ?v2))) :named a220)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$) (?v2 Nat$)) (=> (dvd$ ?v0 ?v1) (dvd$ (power$ ?v0 ?v2) (power$ ?v1 ?v2)))) :named a221)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (dvd$b ?v0 ?v1) (dvd$b (power$c ?v0 ?v2) (power$c ?v1 ?v2)))) :named a222)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (=> (and (dvd$b (power$c ?v0 ?v1) (power$c ?v2 ?v1)) (not (= ?v1 zero$a))) (dvd$b ?v0 ?v2))) :named a223)) +(assert (! (not (dvd$ zero$c one$a)) :named a224)) +(assert (! (not (dvd$b zero$a one$)) :named a225)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (dvd$ (power$ ?v0 ?v1) one$a) (or (dvd$ ?v0 one$a) (= ?v1 zero$a)))) :named a226)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (dvd$b (power$c ?v0 ?v1) one$) (or (dvd$b ?v0 one$) (= ?v1 zero$a)))) :named a227)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (! (=> (not (= (poly$ ?v0 ?v1) zero$)) (= (order$ ?v1 ?v0) zero$a)) :pattern ((order$ ?v1 ?v0)))) :named a228)) +(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Complex_poly$)) (! (=> (not (= (poly$a ?v0 ?v1) zero$c)) (= (order$a ?v1 ?v0) zero$a)) :pattern ((order$a ?v1 ?v0)))) :named a229)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (not (= ?v0 zero$c)) (= (dvd$ ?v0 one$a) (= (degree$b ?v0) zero$a)))) :named a230)) +(assert (! (forall ((?v0 Complex_poly$)) (= (rsquarefree$ ?v0) (and (not (= ?v0 zero$c)) (forall ((?v1 Complex$)) (or (= (order$ ?v1 ?v0) zero$a) (= (order$ ?v1 ?v0) one$)))))) :named a231)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$) (?v2 Complex_poly$)) (=> (not (= ?v0 zero$c)) (= (exists ((?v3 Complex$)) (and (= (poly$ (pCons$ ?v1 ?v0) ?v3) zero$) (not (= (poly$ ?v2 ?v3) zero$)))) (not (dvd$ (pCons$ ?v1 ?v0) (power$ ?v2 (psize$ ?v0))))))) :named a232)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (! (= (dvd$a ?v0 ?v1) (=> (= ?v0 zero$) (= ?v1 zero$))) :pattern ((dvd$a ?v0 ?v1)))) :named a233)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (dvd$ ?v0 one$a) (= (monom$ (coeff$b ?v0 (degree$b ?v0)) zero$a) ?v0))) :named a234)) +(assert (! (forall ((?v0 Nat$)) (= (dvd$b ?v0 one$) (= ?v0 one$))) :named a235)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$) (?v2 Complex$) (?v3 Complex_poly$)) (= (= (pCons$ ?v0 ?v1) (pCons$ ?v2 ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))) :named a236)) +(assert (! (= (pCons$ zero$ zero$c) zero$c) :named a237)) +(assert (! (= (pCons$a zero$c zero$b) zero$b) :named a238)) +(assert (! (= (pCons$b zero$a zero$d) zero$d) :named a239)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly_poly$)) (= (= (pCons$a ?v0 ?v1) zero$b) (and (= ?v0 zero$c) (= ?v1 zero$b)))) :named a240)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat_poly$)) (= (= (pCons$b ?v0 ?v1) zero$d) (and (= ?v0 zero$a) (= ?v1 zero$d)))) :named a241)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (= (pCons$ ?v0 ?v1) zero$c) (and (= ?v0 zero$) (= ?v1 zero$c)))) :named a242)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (coeff$b (pCons$ ?v0 ?v1) zero$a) ?v0)) :named a243)) +(assert (! (forall ((?v0 Nat$)) (= (monom$ zero$ ?v0) zero$c)) :named a244)) +(assert (! (forall ((?v0 Nat$)) (= (monom$a zero$c ?v0) zero$b)) :named a245)) +(assert (! (forall ((?v0 Nat$)) (= (monom$b zero$a ?v0) zero$d)) :named a246)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (= (= (monom$a ?v0 ?v1) zero$b) (= ?v0 zero$c))) :named a247)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (monom$b ?v0 ?v1) zero$d) (= ?v0 zero$a))) :named a248)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (= (= (monom$ ?v0 ?v1) zero$c) (= ?v0 zero$))) :named a249)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$b (monom$ ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$))) :named a250)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$ (monom$a ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$c))) :named a251)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$a (monom$b ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$a))) :named a252)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$) (?v2 Complex$) (?v3 Complex_poly$)) (= (plus$c (pCons$ ?v0 ?v1) (pCons$ ?v2 ?v3)) (pCons$ (plus$ ?v0 ?v2) (plus$c ?v1 ?v3)))) :named a253)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat_poly$) (?v2 Nat$) (?v3 Nat_poly$)) (= (plus$b (pCons$b ?v0 ?v1) (pCons$b ?v2 ?v3)) (pCons$b (plus$a ?v0 ?v2) (plus$b ?v1 ?v3)))) :named a254)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (= (coeff$b (monom$ ?v0 ?v1) (degree$b (monom$ ?v0 ?v1))) ?v0)) :named a255)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (=> (not (= ?v0 zero$)) (= (order$ zero$ (monom$ ?v0 ?v1)) ?v1))) :named a256)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (=> (not (= ?v0 zero$c)) (= (order$a zero$c (monom$a ?v0 ?v1)) ?v1))) :named a257)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (pcompose$ (pCons$ ?v0 zero$c) ?v1) (pCons$ ?v0 zero$c))) :named a258)) +(assert (! (forall ((?v0 Complex$)) (= (reflect_poly$ (pCons$ ?v0 zero$c)) (pCons$ ?v0 zero$c))) :named a259)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$) (?v2 Complex$)) (= (synthetic_div$ (pCons$ ?v0 ?v1) ?v2) (pCons$ (poly$ ?v1 ?v2) (synthetic_div$ ?v1 ?v2)))) :named a260)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (=> (= ?v0 zero$c) (= (coeff$b (pCons$ ?v1 ?v0) (degree$b (pCons$ ?v1 ?v0))) ?v1))) :named a261)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (=> (not (= ?v0 zero$c)) (= (coeff$b (pCons$ ?v1 ?v0) (degree$b (pCons$ ?v1 ?v0))) (coeff$b ?v0 (degree$b ?v0))))) :named a262)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (= (dvd$c (pCons$a ?v0 zero$b) (pCons$a ?v1 zero$b)) (dvd$ ?v0 ?v1))) :named a263)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (dvd$d (pCons$b ?v0 zero$d) (pCons$b ?v1 zero$d)) (dvd$b ?v0 ?v1))) :named a264)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (dvd$ (pCons$ ?v0 zero$c) (pCons$ ?v1 zero$c)) (dvd$a ?v0 ?v1))) :named a265)) +(assert (! (= (= (pCons$b one$ zero$d) one$c) true) :named a266)) +(assert (! (= (= (pCons$ one$b zero$c) one$a) true) :named a267)) +(assert (! (= (= one$c (pCons$b one$ zero$d)) true) :named a268)) +(assert (! (= (= one$a (pCons$ one$b zero$c)) true) :named a269)) +(assert (! (= (monom$b one$ zero$a) one$c) :named a270)) +(assert (! (forall ((?v0 Complex_poly$)) (= (pcompose$ ?v0 (pCons$ zero$ (pCons$ one$b zero$c))) ?v0)) :named a271)) +(assert (! (forall ((?v0 Complex_poly_poly$)) (= (pcompose$a ?v0 (pCons$a zero$c (pCons$a one$a zero$b))) ?v0)) :named a272)) +(assert (! (forall ((?v0 Nat_poly$)) (= (pcompose$b ?v0 (pCons$b zero$a (pCons$b one$ zero$d))) ?v0)) :named a273)) +(assert (! (forall ((?v0 Nat$)) (=> (dvd$b zero$a ?v0) (= ?v0 zero$a))) :named a274)) +(assert (! (forall ((?v0 Nat$)) (= (not (= ?v0 zero$a)) (and (dvd$b ?v0 zero$a) (not (= ?v0 zero$a))))) :named a275)) +(assert (! (forall ((?v0 Nat$)) (! (= (dvd$b zero$a ?v0) (= ?v0 zero$a)) :pattern ((dvd$b zero$a ?v0)))) :named a276)) +(assert (! (forall ((?v0 Nat$)) (not (and (dvd$b zero$a ?v0) (not (= zero$a ?v0))))) :named a277)) +(assert (! (forall ((?v0 Nat$)) (dvd$b ?v0 zero$a)) :named a278)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Complex_poly$)) (= (= (monom$a ?v0 ?v1) (pCons$a ?v2 zero$b)) (and (= ?v0 ?v2) (or (= ?v0 zero$c) (= ?v1 zero$a))))) :named a279)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (monom$b ?v0 ?v1) (pCons$b ?v2 zero$d)) (and (= ?v0 ?v2) (or (= ?v0 zero$a) (= ?v1 zero$a))))) :named a280)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$) (?v2 Complex$)) (= (= (monom$ ?v0 ?v1) (pCons$ ?v2 zero$c)) (and (= ?v0 ?v2) (or (= ?v0 zero$) (= ?v1 zero$a))))) :named a281)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (forall ((?v1 Complex$) (?v2 Complex_poly$)) (=> (= ?v0 (pCons$ ?v1 ?v2)) false)) false)) :named a282)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (forall ((?v1 Complex$) (?v2 Complex_poly$)) (=> (= ?v0 (pCons$ ?v1 ?v2)) false)) false)) :named a283)) +(assert (! (forall ((?v0 (-> Complex_poly$ (-> Complex_poly$ Bool))) (?v1 Complex_poly$) (?v2 Complex_poly$)) (=> (and (?v0 zero$c zero$c) (forall ((?v3 Complex$) (?v4 Complex_poly$) (?v5 Complex$) (?v6 Complex_poly$)) (=> (?v0 ?v4 ?v6) (?v0 (pCons$ ?v3 ?v4) (pCons$ ?v5 ?v6))))) (?v0 ?v1 ?v2))) :named a284)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$) (?v2 Complex$) (?v3 Nat$)) (= (= (monom$ ?v0 ?v1) (monom$ ?v2 ?v3)) (and (= ?v0 ?v2) (or (= ?v0 zero$) (= ?v1 ?v3))))) :named a285)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Complex_poly$) (?v3 Nat$)) (= (= (monom$a ?v0 ?v1) (monom$a ?v2 ?v3)) (and (= ?v0 ?v2) (or (= ?v0 zero$c) (= ?v1 ?v3))))) :named a286)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$) (?v3 Nat$)) (= (= (monom$b ?v0 ?v1) (monom$b ?v2 ?v3)) (and (= ?v0 ?v2) (or (= ?v0 zero$a) (= ?v1 ?v3))))) :named a287)) +(assert (! (forall ((?v0 Complex$)) (! (= (monom$ ?v0 zero$a) (pCons$ ?v0 zero$c)) :pattern ((monom$ ?v0)))) :named a288)) +(assert (! (forall ((?v0 (-> Complex_poly_poly$ Bool)) (?v1 Complex_poly_poly$)) (=> (and (?v0 zero$b) (forall ((?v2 Complex_poly$) (?v3 Complex_poly_poly$)) (=> (and (or (not (= ?v2 zero$c)) (not (= ?v3 zero$b))) (?v0 ?v3)) (?v0 (pCons$a ?v2 ?v3))))) (?v0 ?v1))) :named a289)) +(assert (! (forall ((?v0 (-> Nat_poly$ Bool)) (?v1 Nat_poly$)) (=> (and (?v0 zero$d) (forall ((?v2 Nat$) (?v3 Nat_poly$)) (=> (and (or (not (= ?v2 zero$a)) (not (= ?v3 zero$d))) (?v0 ?v3)) (?v0 (pCons$b ?v2 ?v3))))) (?v0 ?v1))) :named a290)) +(assert (! (forall ((?v0 (-> Complex_poly$ Bool)) (?v1 Complex_poly$)) (=> (and (?v0 zero$c) (forall ((?v2 Complex$) (?v3 Complex_poly$)) (=> (and (or (not (= ?v2 zero$)) (not (= ?v3 zero$c))) (?v0 ?v3)) (?v0 (pCons$ ?v2 ?v3))))) (?v0 ?v1))) :named a291)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$)) (=> (= (poly$ ?v0 ?v1) zero$) (= (poly$ (pCons$ zero$ ?v0) ?v1) zero$))) :named a292)) +(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Complex_poly$)) (=> (= (poly$a ?v0 ?v1) zero$c) (= (poly$a (pCons$a zero$c ?v0) ?v1) zero$c))) :named a293)) +(assert (! (forall ((?v0 Nat_poly$) (?v1 Nat$)) (=> (= (poly$b ?v0 ?v1) zero$a) (= (poly$b (pCons$b zero$a ?v0) ?v1) zero$a))) :named a294)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (=> (not (= ?v0 zero$)) (= (degree$b (monom$ ?v0 ?v1)) ?v1))) :named a295)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$)) (=> (not (= ?v0 zero$c)) (= (degree$ (monom$a ?v0 ?v1)) ?v1))) :named a296)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (=> (not (= ?v0 zero$a)) (= (degree$a (monom$b ?v0 ?v1)) ?v1))) :named a297)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$b (monom$ ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$))) :named a298)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$ (monom$a ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$c))) :named a299)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (coeff$a (monom$b ?v0 ?v1) ?v2) (ite (= ?v1 ?v2) ?v0 zero$a))) :named a300)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly$)) (=> (dvd$ ?v0 ?v1) (dvd$ ?v0 (pCons$ zero$ ?v1)))) :named a301)) +(assert (! (forall ((?v0 Complex_poly_poly$) (?v1 Complex_poly_poly$)) (=> (dvd$c ?v0 ?v1) (dvd$c ?v0 (pCons$a zero$c ?v1)))) :named a302)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (poly$ (pCons$ (poly$ zero$c ?v0) zero$c) ?v1) (poly$ zero$c ?v1))) :named a303)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= ?v0 (poly$ (pCons$ ?v0 zero$c) ?v1))) :named a304)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (plus$b (monom$b ?v0 ?v1) (monom$b ?v2 ?v1)) (monom$b (plus$a ?v0 ?v2) ?v1))) :named a305)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex$)) (= (offset_poly$ (pCons$ ?v0 zero$c) ?v1) (pCons$ ?v0 zero$c))) :named a306)) +(assert (! (forall ((?v0 Complex_poly$)) (= (exists ((?v1 Complex_poly$)) (= (poly$a (pCons$a ?v0 zero$b) ?v1) zero$c)) (= ?v0 zero$c))) :named a307)) +(assert (! (forall ((?v0 Nat$)) (= (exists ((?v1 Nat$)) (= (poly$b (pCons$b ?v0 zero$d) ?v1) zero$a)) (= ?v0 zero$a))) :named a308)) +(assert (! (forall ((?v0 Complex$)) (= (exists ((?v1 Complex$)) (= (poly$ (pCons$ ?v0 zero$c) ?v1) zero$)) (= ?v0 zero$))) :named a309)) +(assert (! (forall ((?v0 Complex_poly$)) (= (exists ((?v1 Complex_poly$)) (not (= (poly$a (pCons$a ?v0 zero$b) ?v1) zero$c))) (not (= ?v0 zero$c)))) :named a310)) +(assert (! (forall ((?v0 Nat$)) (= (exists ((?v1 Nat$)) (not (= (poly$b (pCons$b ?v0 zero$d) ?v1) zero$a))) (not (= ?v0 zero$a)))) :named a311)) +(assert (! (forall ((?v0 Complex$)) (= (exists ((?v1 Complex$)) (not (= (poly$ (pCons$ ?v0 zero$c) ?v1) zero$))) (not (= ?v0 zero$)))) :named a312)) +(assert (! (forall ((?v0 Complex$)) (= (poly$ (pCons$ zero$ zero$c) ?v0) (poly$ zero$c ?v0))) :named a313)) +(assert (! (forall ((?v0 Complex_poly$)) (= (poly$a (pCons$a zero$c zero$b) ?v0) (poly$a zero$b ?v0))) :named a314)) +(assert (! (forall ((?v0 Complex$)) (= (degree$b (pCons$ ?v0 zero$c)) zero$a)) :named a315)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (and (= (degree$b ?v0) zero$a) (forall ((?v1 Complex$)) (=> (= ?v0 (pCons$ ?v1 zero$c)) false))) false)) :named a316)) +(assert (! (= (pCons$b one$ zero$d) one$c) :named a317)) +(assert (! (= (pCons$ one$b zero$c) one$a) :named a318)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (monom$b ?v0 ?v1) one$c) (and (= ?v0 one$) (= ?v1 zero$a)))) :named a319)) +(assert (! (forall ((?v0 Complex$)) (= ?v0 (poly$ (pCons$ zero$ (pCons$ one$b zero$c)) ?v0))) :named a320)) +(assert (! (forall ((?v0 Complex_poly$)) (= ?v0 (poly$a (pCons$a zero$c (pCons$a one$a zero$b)) ?v0))) :named a321)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (not (exists ((?v1 Complex$) (?v2 Complex_poly$)) (and (not (= ?v1 zero$)) (and (= ?v2 zero$c) (= ?v0 (pCons$ ?v1 ?v2)))))) (exists ((?v1 Complex$)) (= (poly$ ?v0 ?v1) zero$)))) :named a322)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex$) (?v2 Complex$)) (=> (not (= ?v0 zero$c)) (exists ((?v3 Complex$)) (= (poly$ (pCons$ ?v1 (pCons$ ?v2 ?v0)) ?v3) zero$)))) :named a323)) +(assert (! (forall ((?v0 Complex_poly$) (?v1 Complex_poly_poly$)) (= (dvd$c (pCons$a ?v0 zero$b) ?v1) (forall ((?v2 Nat$)) (dvd$ ?v0 (coeff$ ?v1 ?v2))))) :named a324)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat_poly$)) (= (dvd$d (pCons$b ?v0 zero$d) ?v1) (forall ((?v2 Nat$)) (dvd$b ?v0 (coeff$a ?v1 ?v2))))) :named a325)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (dvd$ (pCons$ ?v0 zero$c) ?v1) (forall ((?v2 Nat$)) (dvd$a ?v0 (coeff$b ?v1 ?v2))))) :named a326)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (degree$a (power$b (pCons$b ?v0 (pCons$b one$ zero$d)) ?v1)) ?v1)) :named a327)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (= (degree$b (power$ (pCons$ ?v0 (pCons$ one$b zero$c)) ?v1)) ?v1)) :named a328)) +(assert (! (forall ((?v0 Complex_poly$)) (= (pcompose$ ?v0 zero$c) (pCons$ (coeff$b ?v0 zero$a) zero$c))) :named a329)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (coeff$a (power$b (pCons$b ?v0 (pCons$b one$ zero$d)) ?v1) ?v1) one$)) :named a330)) +(assert (! (forall ((?v0 Complex$) (?v1 Nat$)) (= (coeff$b (power$ (pCons$ ?v0 (pCons$ one$b zero$c)) ?v1) ?v1) one$b)) :named a331)) +(assert (! (forall ((?v0 Complex$) (?v1 Complex_poly$)) (= (dvd$ (pCons$ ?v0 ?v1) one$a) (and (= ?v1 zero$c) (not (= ?v0 zero$))))) :named a332)) +(assert (! (forall ((?v0 Complex$)) (=> (not (= ?v0 zero$)) (dvd$ (pCons$ ?v0 zero$c) one$a))) :named a333)) +(assert (! (forall ((?v0 Complex_poly$)) (=> (and (dvd$ ?v0 one$a) (forall ((?v1 Complex$)) (=> (and (= ?v0 (monom$ ?v1 zero$a)) (not (= ?v1 zero$))) false))) false)) :named a334)) +(assert (! (forall ((?v0 Complex$)) (=> (not (= ?v0 zero$)) (dvd$ (monom$ ?v0 zero$a) one$a))) :named a335)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (times$ ?v0 ?v1) (times$ ?v2 ?v1)) (or (= ?v0 ?v2) (= ?v1 zero$a)))) :named a336)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (= (times$ ?v0 ?v1) (times$ ?v0 ?v2)) (or (= ?v1 ?v2) (= ?v0 zero$a)))) :named a337)) +(assert (! (forall ((?v0 Nat$)) (! (= (times$ ?v0 zero$a) zero$a) :pattern ((times$ ?v0)))) :named a338)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (times$ ?v0 ?v1) zero$a) (or (= ?v0 zero$a) (= ?v1 zero$a)))) :named a339)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (suc$ ?v0) (suc$ ?v1)) (= ?v0 ?v1))) :named a340)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (suc$ ?v0) (suc$ ?v1)) (= ?v0 ?v1))) :named a341)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (times$ ?v0 ?v1) one$) (and (= ?v0 one$) (= ?v1 one$)))) :named a342)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= one$ (times$ ?v0 ?v1)) (and (= ?v0 one$) (= ?v1 one$)))) :named a343)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (times$ ?v0 ?v1) (suc$ zero$a)) (and (= ?v0 (suc$ zero$a)) (= ?v1 (suc$ zero$a))))) :named a344)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (suc$ zero$a) (times$ ?v0 ?v1)) (and (= ?v0 (suc$ zero$a)) (= ?v1 (suc$ zero$a))))) :named a345)) +(assert (! (forall ((?v0 Nat$)) (! (= (power$c (suc$ zero$a) ?v0) (suc$ zero$a)) :pattern ((power$c (suc$ zero$a) ?v0)))) :named a346)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (= (power$c ?v0 ?v1) (suc$ zero$a)) (or (= ?v1 zero$a) (= ?v0 (suc$ zero$a))))) :named a347)) +(assert (! (forall ((?v0 Nat$)) (less_eq$ zero$a ?v0)) :named a348)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (less_eq$ (suc$ ?v0) (suc$ ?v1)) (less_eq$ ?v0 ?v1))) :named a349)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (= (plus$a ?v0 (suc$ ?v1)) (suc$ (plus$a ?v0 ?v1)))) :named a350)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$)) (! (= (times$ ?v0 (suc$ ?v1)) (plus$a ?v0 (times$ ?v0 ?v1))) :pattern ((times$ ?v0 (suc$ ?v1))))) :named a351)) +(assert (! (forall ((?v0 Nat$) (?v1 Nat$) (?v2 Nat$)) (= (less_eq$ (plus$a ?v0 ?v1) (plus$a ?v0 ?v2)) (less_eq$ ?v1 ?v2))) :named a352)) +(check-sat) |