(set-option :produce-unsat-cores true)
(set-logic QF_UFNIA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const i2 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i7 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const i12 Int)
(declare-const v10 Bool)
(declare-sort S0 0)
(declare-const v11 Bool)
(declare-const S0-0 S0)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const i13 Int)
(declare-const i14 Int)
(declare-const v14 Bool)
(declare-const S0-1 S0)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-sort S1 0)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const i15 Int)
(declare-const S1-0 S1)
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_1))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_2))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_3))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_4))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_5))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_6))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_7))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_8))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_9))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_10))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_11))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_12))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_13))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_14))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_15))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_16))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_17))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_18))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_19))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_20))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_21))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_22))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_23))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_24))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_25))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_26))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_27))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_28))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_29))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_30))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_31))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_32))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_33))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) false) :named IP_34))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_35))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) false) :named IP_36))
(assert (! (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) :named IP_37))
(assert (! (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_38))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_39))
(assert (! (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) :named IP_40))
(assert (! (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_41))
(assert (! (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) :named IP_42))
(assert (! (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) :named IP_43))
(assert (! (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) :named IP_44))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) :named IP_45))
(assert (! (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) :named IP_46))
(assert (! (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) :named IP_47))
(assert (! (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) :named IP_48))
(assert (! (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_49))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) :named IP_50))
(assert (! (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) :named IP_51))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))))) :named IP_52))
(assert (! (and (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_53))
(assert (! (or (and (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (and (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))))) :named IP_54))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_55))
(assert (! (and (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) :named IP_56))
(assert (! (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) :named IP_57))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) :named IP_58))
(assert (! (=> (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_59))
(assert (! (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) :named IP_60))
(assert (! (and (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) :named IP_61))
(assert (! (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) :named IP_62))
(assert (! (=> (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)))) :named IP_63))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_64))
(assert (! (and (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (and (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (and (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))))) (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (and (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (and (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (=> (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)))) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (and (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (and (=> (=> (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (and (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (and (and (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))))) :named IP_65))
(assert (! (=> (=> (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)) (and (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1)))) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12)))) (or (distinct (div (abs (- 0)) 80) i12) (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_66))
(assert (! (or (or (distinct (div (abs (- 0)) 80) i12) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (distinct (div (abs (- 0)) 80) i12)) (or (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))) (= v10 (not (or v2 v6 v5 v0 v6 v4 v1 v2 v1 v1))))) :named IP_67))
(check-sat)
(check-sat-assuming (IP_28 IP_39))
(get-unsat-core)
(check-sat-assuming (IP_13 IP_63))
(get-unsat-core)
(check-sat-assuming (IP_45 IP_63))
(get-unsat-core)
(check-sat-assuming (IP_13 IP_52))
(get-unsat-core)
(check-sat-assuming (IP_19 IP_30))
(get-unsat-core)
(check-sat-assuming (IP_15 IP_37))
(get-unsat-core)
(check-sat-assuming (IP_17 IP_48))
(get-unsat-core)
(check-sat-assuming (IP_32 IP_51))
(get-unsat-core)
(check-sat-assuming (IP_40 IP_56))
(get-unsat-core)
(check-sat-assuming (IP_10 IP_12))
(get-unsat-core)
(exit)