(set-logic QF_FPLRA)
(set-option :smt.threads 2)
(set-option :smt.arith.solver 3)
(declare-const fpv0 Float32)
(declare-const fpv3 Float32)
(declare-const fpv4 Float32)
(declare-const fpv6 Float32)
(declare-const fpv11 Float32)
(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 r0 Real)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r9 Real)
(push 1)
(declare-const r10 Real)
(declare-const v8 Bool)
(declare-const v9 Bool)
(pop 1)
(declare-const fpv12 Float32)
(declare-const fpv13 Float32)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const fpv14 Float32)
(declare-const r11 Real)
(declare-const fpv15 Float32)
(declare-const r12 Real)
(push 1)
(declare-const v12 Bool)
(assert (or (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (not v2)))
(assert (or v0 v0 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (> 4794841.0 r1 r0 6175.2345) v0))
(assert (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v3))
(assert (or v0 v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))))
(assert (or v0 v12 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))))
(assert (or (not v2) (not v2) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))))
(assert (or (> 4794841.0 r1 r0 6175.2345) (> 4794841.0 r1 r0 6175.2345) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or v0 v12 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))))
(assert (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0 v1))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) (> 4794841.0 r1 r0 6175.2345)))
(assert (or (not v2) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v0))
(assert (or v3 v7 v12))
(assert (or v3 v1 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))))
(assert (or (not v2) v0 (> 4794841.0 r1 r0 6175.2345)))
(assert (or (not v2) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v3))
(assert (or (not v2) v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))))
(assert (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v12))
(assert (or v0 (> 4794841.0 r1 r0 6175.2345) v0))
(assert (or (> 4794841.0 r1 r0 6175.2345) v1 (not v2)))
(assert (or v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v7))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v1 v7))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (> 4794841.0 r1 r0 6175.2345)))
(assert (or v12 v7 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or v1 v7 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))))
(assert (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or (not v2) v12 v7))
(assert (or v0 (not v2) v0))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3))
(assert (or v7 v0 v12))
(assert (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) (> 4794841.0 r1 r0 6175.2345)))
(assert (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))))
(assert (or v0 (not v2) (> 4794841.0 r1 r0 6175.2345)))
(assert (or v7 (not v2) (not v2)))
(assert (or (> 4794841.0 r1 r0 6175.2345) v0 v3))
(assert (or (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))))
(assert (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0))
(assert (or (not v2) v12 v12))
(assert (or v12 v0 v7))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (> 4794841.0 r1 r0 6175.2345) v3))
(assert (or v3 v7 v0))
(assert (or v7 v0 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v1 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or v7 v0 v7))
(assert (or (not v2) (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))))
(assert (or (not v2) v1 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))))
(assert (or v3 v0 (not v2)))
(assert (or (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v3 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v1 (> 4794841.0 r1 r0 6175.2345)))
(assert (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v12 v7))
(assert (or v1 (> 4794841.0 r1 r0 6175.2345) v7))
(assert (or (not v2) (not v2) v12))
(assert (or (> 4794841.0 r1 r0 6175.2345) v7 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or v1 (not v2) v12))
(assert (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (not v2)))
(assert (or v7 v1 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))))
(assert (or (not v2) v1 (> 4794841.0 r1 r0 6175.2345)))
(assert (or (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v1))
(assert (or v12 v0 v3))
(assert (or v1 v12 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or v3 v0 (> 4794841.0 r1 r0 6175.2345)))
(assert (or v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))))
(assert (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)))
(assert (or v0 v3 v7))
(assert (or (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v0 v0))
(assert (or v0 (> 4794841.0 r1 r0 6175.2345) (> 4794841.0 r1 r0 6175.2345)))
(assert (or v3 (not v2) v7))
(assert (and (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3) (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (not v2)) (or (not v2) v0 (> 4794841.0 r1 r0 6175.2345)) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0 v1) (or (not v2) (not v2) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v12 v7)))
(assert (or (not v2) (not v2) v12))
(assert (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))))
(assert (or v0 (not v2) (> 4794841.0 r1 r0 6175.2345)))
(assert (or (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v0 v0))
(assert (=> (or (> 4794841.0 r1 r0 6175.2345) v7 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))))
(assert (or (or v7 v1 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or v0 (> 4794841.0 r1 r0 6175.2345) v0)))
(assert (and (or v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v7) (or v3 v7 v12) (or v12 v0 v3) (or (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (not v2)) (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v1 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or v3 v7 v0) (or v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)))))
(assert (and (or (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (not v2)) (or (not v2) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v0) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))) (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v12) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (> 4794841.0 r1 r0 6175.2345) v0) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) (> 4794841.0 r1 r0 6175.2345)) (=> (or (> 4794841.0 r1 r0 6175.2345) v7 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or v0 (not v2) (> 4794841.0 r1 r0 6175.2345)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or v0 v3 v7)))
(check-sat)
(assert (and (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v1 v7) (or v1 (> 4794841.0 r1 r0 6175.2345) v7)))
(assert (=> (or v3 v7 v0) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v3)))
(assert (or (or v0 v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v0 v3 v7)))
(assert (=> (or (> 4794841.0 r1 r0 6175.2345) v7 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))))
(assert (or (and (or v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v7) (or v3 v7 v12) (or v12 v0 v3) (or (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (not v2)) (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v1 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or v3 v7 v0) (or v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)))) (or (not v2) v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v1 v12 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v1 v7) (or v1 v7 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))) (or v3 v0 (not v2)) (or (not v2) v12 v7) (or v0 v0 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (> 4794841.0 r1 r0 6175.2345) v0) (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0) (or v0 v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)))))
(assert (and (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or (not v2) v12 v12) (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3)))
(assert (and (and (or (> 4794841.0 r1 r0 6175.2345) v1 (not v2)) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (and (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or (not v2) v12 v12) (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3)) (or (or v0 v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v0 v3 v7)) (or v1 v12 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v3 v0 (> 4794841.0 r1 r0 6175.2345)) (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or v3 v0 (not v2)) (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0) (or (not v2) (not v2) v12)) (or v3 v1 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))) (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0) (or v0 v0 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v1 v7) (or (or v0 v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v0 v3 v7)) (or (> 4794841.0 r1 r0 6175.2345) v7 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))))
(assert (or (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (not v2)))
(assert (and (or v1 (> 4794841.0 r1 r0 6175.2345) v7) (or (not v2) (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v1 (> 4794841.0 r1 r0 6175.2345) v7) (or (not v2) (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v3 v7 v0)))
(assert (=> (or v7 v0 v7) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3)))
(assert (or (or v12 v0 v3) (or v7 (not v2) (not v2))))
(assert (or (and (or (> 4794841.0 r1 r0 6175.2345) v1 (not v2)) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (and (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or (not v2) v12 v12) (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3)) (or (or v0 v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v0 v3 v7)) (or v1 v12 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v3 v0 (> 4794841.0 r1 r0 6175.2345)) (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or v3 v0 (not v2)) (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0) (or (not v2) (not v2) v12)) (or v7 v1 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or v0 v3 v7) (or (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v1 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (not v2) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v0) (or v7 v0 v7) (or (not v2) v1 (> 4794841.0 r1 r0 6175.2345)) (and (or (> 4794841.0 r1 r0 6175.2345) v1 (not v2)) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (and (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or (not v2) v12 v12) (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3)) (or (or v0 v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v0 v3 v7)) (or v1 v12 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v3 v0 (> 4794841.0 r1 r0 6175.2345)) (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or v3 v0 (not v2)) (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0) (or (not v2) (not v2) v12)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v12 v7) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) (> 4794841.0 r1 r0 6175.2345)) (and (=> (or (> 4794841.0 r1 r0 6175.2345) v7 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (> 4794841.0 r1 r0 6175.2345)) (=> (or v3 v7 v0) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v3)) (or v0 v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))))))
(assert (=> (or (not v2) v12 v12) (or (not v2) v1 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)))))
(assert (or (and (and (or (not v2) v0 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2))) (or (not v2) v12 v12) (or v12 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3) (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) (not v2) v3)) (or v0 (not v2) v0)))
(assert (or v0 (> 4794841.0 r1 r0 6175.2345) (> 4794841.0 r1 r0 6175.2345)))
(check-sat)
(assert (=> (or (not v2) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v1) (or v7 v0 v12)))
(assert (or (or (not v2) v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (and (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v1 v7) (or v1 (> 4794841.0 r1 r0 6175.2345) v7))))
(assert (or (or (not v2) v1 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))) (or (or (not v2) v7 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (and (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v1 v7) (or v1 (> 4794841.0 r1 r0 6175.2345) v7))) (or (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v0 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753))) (or (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) (> 4794841.0 r1 r0 6175.2345) (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0))) (or v3 (fp.leq fpv13 fpv0 fpv13 ((_ to_fp 8 24) RTZ 19.0)) v12) (or (or v7 v1 (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2)) (or v0 (> 4794841.0 r1 r0 6175.2345) v0))) (or (not v2) (not v2) v12) (and (or (distinct v5 v0 (< r9 r1 r9) v3 v4 (fp.isPositive ((_ to_fp 8 24) RNA 51988804.0)) (< r9 r1 r9) (< r9 r1 r9) v3 v6 v2) v1 v7) (or v1 (> 4794841.0 r1 r0 6175.2345) v7)) (or (not v2) v1 (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)))))
(assert (or v3 v7 v0))
(assert (=> (or (not v2) (fp.lt ((_ to_fp 8 24) RTP 31710778011.0) ((_ to_fp 8 24) RNE 0.2141515746) ((_ to_fp 8 24) RTN 52611.0) ((_ to_fp 8 24) RTZ 19.0) ((_ to_fp 8 24) RTP 885.67753)) v3) (or v0 (not v2) v0)))
(assert (or (or v12 v0 v7) (or (not v2) v1 (> 4794841.0 r1 r0 6175.2345))))
(minimize r0)
(minimize r1)
(minimize r2)
(minimize r9)
(maximize r11)
(minimize r12)
(check-sat)
(exit)