path: root/test/regress/regress2/ho/fta0409.smt2

; EXPECT: unsat
(set-logic HO_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)