(set-logic QF_UFNRA)
(set-option :snorm-infer-eq true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(push 1)
(declare-const v16 Bool)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const v17 Bool)
(pop 1)
(declare-const r4 Real)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const v20 Bool)
(declare-sort S0 0)
(declare-const v21 Bool)
(declare-const v22 Bool)
(declare-const v23 Bool)
(declare-sort S1 0)
(push 1)
(declare-sort S2 0)
(declare-const r5 Real)
(declare-const v24 Bool)
(declare-sort S3 0)
(pop 1)
(declare-const v25 Bool)
(push 1)
(declare-sort S2 0)
(push 1)
(declare-sort S3 0)
(declare-const v26 Bool)
(declare-const v27 Bool)
(pop 1)
(declare-const S0-0 S0)
(assert (or v14 v19 v6))
(assert (or v20 v6 (<= r4 r1 (- (/ r0 r0)))))
(assert (or v0 v5 v13))
(assert (or v10 v13 (<= 622 r4 622 r0)))
(assert (or (=> v12 v11) v6 v23))
(assert (or v13 (<= r4 r1 (- (/ r0 r0))) v1))
(assert (or v11 v20 v14))
(assert (or (<= r4 r1 (- (/ r0 r0))) (<= r4 r1 (- (/ r0 r0))) v23))
(assert (or v19 v14 v20))
(assert (or v0 (=> v12 v11) v10))
(assert (or v4 v4 (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0))))))
(assert (or (=> v12 v11) v13 v23))
(assert (or v19 v10 v14))
(assert (or v1 v2 v20))
(assert (or v13 (<= 622 r4 622 r0) v6))
(assert (or (<= r4 r1 (- (/ r0 r0))) v14 (<= r4 r1 (- (/ r0 r0)))))
(assert (or v10 (=> v12 v11) (=> v12 v11)))
(assert (or v11 v10 (<= r4 r1 (- (/ r0 r0)))))
(assert (or v13 (=> v12 v11) v14))
(assert (or (=> v12 v11) v1 v11))
(assert (or v11 v10 v14))
(assert (or v10 v4 (<= 622 r4 622 r0)))
(assert (or v19 (<= 622 r4 622 r0) v6))
(assert (or v0 v19 v19))
(assert (or (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0)))) v14 v1))
(assert (or v4 v4 v13))
(assert (or v2 (<= r4 r1 (- (/ r0 r0))) (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0))))))
(assert (or (<= 622 r4 622 r0) v10 v19))
(assert (or v19 (<= r4 r1 (- (/ r0 r0))) (<= r4 r1 (- (/ r0 r0)))))
(assert (or v14 v2 (<= 622 r4 622 r0)))
(assert (or (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0)))) v10 (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0))))))
(assert (or v13 (<= 622 r4 622 r0) v14))
(assert (or (<= 622 r4 622 r0) v0 v20))
(assert (or v19 v14 v0))
(assert (or v14 (<= 622 r4 622 r0) v11))
(assert (or (<= r4 r1 (- (/ r0 r0))) v4 v13))
(assert (or v6 v10 v4))
(assert (or v13 v14 v20))
(assert (or v11 v20 v13))
(assert (or (<= r4 r1 (- (/ r0 r0))) v6 v13))
(assert (or v10 (<= r4 r1 (- (/ r0 r0))) v19))
(assert (or v5 v14 v10))
(assert (or v6 (<= r4 r1 (- (/ r0 r0))) v4))
(assert (or v23 v19 (=> v12 v11)))
(assert (or (<= r4 r1 (- (/ r0 r0))) v14 v1))
(assert (or v0 v5 (<= r4 r1 (- (/ r0 r0)))))
(assert (or v6 v5 (=> v12 v11)))
(assert (or v6 v0 v13))
(assert (or v10 v0 (<= r4 r1 (- (/ r0 r0)))))
(assert (or v20 v10 v4))
(assert (or v6 v6 v5))
(assert (or v5 v11 (=> v12 v11)))
(assert (or v10 (=> v12 v11) v11))
(assert (or v5 v10 (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0))))))
(assert (or v6 v2 v5))
(assert (or v0 v6 v13))
(assert (or v19 (<= r4 r1 (- (/ r0 r0))) (<= r4 r1 (- (/ r0 r0)))))
(assert (or v11 (<= 622 r4 622 r0) v2))
(assert (or v1 (<= r4 r1 (- (/ r0 r0))) v14))
(assert (or v20 v6 v20))
(assert (or v6 (<= 622 r4 622 r0) v19))
(assert (or v20 (<= r4 r1 (- (/ r0 r0))) (<= 622 r4 622 r0)))
(assert (or (<= r4 r1 (- (/ r0 r0))) v2 (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0))))))
(assert (or v6 v1 v6))
(assert (or v5 v11 v10))
(assert (or v23 (<= 622 r4 622 r0) v20))
(assert (or v4 v23 v4))
(assert (or (=> v12 v11) v0 v1))
(assert (or v2 (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0)))) v0))
(assert (or (<= 622 r4 622 r0) v19 v10))
(assert (or (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0)))) v14 v13))
(assert (or v14 v19 v1))
(assert (or v14 v13 (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0))))))
(assert (or v5 v0 v0))
(assert (or (<= r4 r1 (- (/ r0 r0))) v19 v10))
(assert (or v14 v1 v14))
(assert (or (=> v12 v11) v0 v0))
(assert (or v5 (<= 622 r4 622 r0) (<= 622 r4 622 r0)))
(assert (or v2 v19 v10))
(assert (or v0 v10 v6))
(assert (or v0 (<= 622 r4 622 r0) v11))
(assert (or v6 (<= r4 r1 (- (/ r0 r0))) (=> v12 v11)))
(assert (or v4 v14 v6))
(assert (or v11 (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0)))) (or v7 v8 (>= (- (/ r0 r0)) r1) v9 v5 v1 v14 (=> v12 v11) (<= r4 r1 (- (/ r0 r0))))))
(assert (or v1 v19 (<= 622 r4 622 r0)))
(check-sat)