(set-logic QF_NRA_ODE)
(declare-fun w_0_1_t () Real)
(declare-fun w_0_1_0 () Real)
(declare-fun w_1_2_t () Real)
(declare-fun w_1_2_0 () Real)
(declare-fun w_2_3_t () Real)
(declare-fun w_2_3_0 () Real)
(declare-fun w_3_4_t () Real)
(declare-fun w_3_4_0 () Real)
(declare-fun w_4_5_t () Real)
(declare-fun w_4_5_0 () Real)
(declare-fun w_5_6_t () Real)
(declare-fun w_5_6_0 () Real)
(declare-fun w_6_7_t () Real)
(declare-fun w_6_7_0 () Real)
(declare-fun w_7_8_t () Real)
(declare-fun w_7_8_0 () Real)
(declare-fun w_8_1_t () Real)
(declare-fun w_8_1_0 () Real)
(declare-fun w_9_2_t () Real)
(declare-fun w_9_2_0 () Real)
(declare-fun w_10_3_t () Real)
(declare-fun w_10_3_0 () Real)
(declare-fun w_11_4_t () Real)
(declare-fun w_11_4_0 () Real)
(declare-fun w_12_5_t () Real)
(declare-fun w_12_5_0 () Real)
(declare-fun w_13_6_t () Real)
(declare-fun w_13_6_0 () Real)
(declare-fun w_14_7_t () Real)
(declare-fun w_14_7_0 () Real)
(declare-fun w_15_8_t () Real)
(declare-fun w_15_8_0 () Real)
(declare-fun w_16_1_t () Real)
(declare-fun w_16_1_0 () Real)
(declare-fun w_17_2_t () Real)
(declare-fun w_17_2_0 () Real)
(declare-fun w_18_3_t () Real)
(declare-fun w_18_3_0 () Real)
(declare-fun w_19_4_t () Real)
(declare-fun w_19_4_0 () Real)
(declare-fun w_20_5_t () Real)
(declare-fun w_20_5_0 () Real)
(declare-fun w_21_6_t () Real)
(declare-fun w_21_6_0 () Real)
(declare-fun w_22_7_t () Real)
(declare-fun w_22_7_0 () Real)
(declare-fun w_23_8_t () Real)
(declare-fun w_23_8_0 () Real)
(declare-fun v_0_1_t () Real)
(declare-fun v_0_1_0 () Real)
(declare-fun v_1_2_t () Real)
(declare-fun v_1_2_0 () Real)
(declare-fun v_2_3_t () Real)
(declare-fun v_2_3_0 () Real)
(declare-fun v_3_4_t () Real)
(declare-fun v_3_4_0 () Real)
(declare-fun v_4_5_t () Real)
(declare-fun v_4_5_0 () Real)
(declare-fun v_5_6_t () Real)
(declare-fun v_5_6_0 () Real)
(declare-fun v_6_7_t () Real)
(declare-fun v_6_7_0 () Real)
(declare-fun v_7_8_t () Real)
(declare-fun v_7_8_0 () Real)
(declare-fun v_8_1_t () Real)
(declare-fun v_8_1_0 () Real)
(declare-fun v_9_2_t () Real)
(declare-fun v_9_2_0 () Real)
(declare-fun v_10_3_t () Real)
(declare-fun v_10_3_0 () Real)
(declare-fun v_11_4_t () Real)
(declare-fun v_11_4_0 () Real)
(declare-fun v_12_5_t () Real)
(declare-fun v_12_5_0 () Real)
(declare-fun v_13_6_t () Real)
(declare-fun v_13_6_0 () Real)
(declare-fun v_14_7_t () Real)
(declare-fun v_14_7_0 () Real)
(declare-fun v_15_8_t () Real)
(declare-fun v_15_8_0 () Real)
(declare-fun v_16_1_t () Real)
(declare-fun v_16_1_0 () Real)
(declare-fun v_17_2_t () Real)
(declare-fun v_17_2_0 () Real)
(declare-fun v_18_3_t () Real)
(declare-fun v_18_3_0 () Real)
(declare-fun v_19_4_t () Real)
(declare-fun v_19_4_0 () Real)
(declare-fun v_20_5_t () Real)
(declare-fun v_20_5_0 () Real)
(declare-fun v_21_6_t () Real)
(declare-fun v_21_6_0 () Real)
(declare-fun v_22_7_t () Real)
(declare-fun v_22_7_0 () Real)
(declare-fun v_23_8_t () Real)
(declare-fun v_23_8_0 () Real)
(declare-fun u_0_1_t () Real)
(declare-fun u_0_1_0 () Real)
(declare-fun u_1_2_t () Real)
(declare-fun u_1_2_0 () Real)
(declare-fun u_2_3_t () Real)
(declare-fun u_2_3_0 () Real)
(declare-fun u_3_4_t () Real)
(declare-fun u_3_4_0 () Real)
(declare-fun u_4_5_t () Real)
(declare-fun u_4_5_0 () Real)
(declare-fun u_5_6_t () Real)
(declare-fun u_5_6_0 () Real)
(declare-fun u_6_7_t () Real)
(declare-fun u_6_7_0 () Real)
(declare-fun u_7_8_t () Real)
(declare-fun u_7_8_0 () Real)
(declare-fun u_8_1_t () Real)
(declare-fun u_8_1_0 () Real)
(declare-fun u_9_2_t () Real)
(declare-fun u_9_2_0 () Real)
(declare-fun u_10_3_t () Real)
(declare-fun u_10_3_0 () Real)
(declare-fun u_11_4_t () Real)
(declare-fun u_11_4_0 () Real)
(declare-fun u_12_5_t () Real)
(declare-fun u_12_5_0 () Real)
(declare-fun u_13_6_t () Real)
(declare-fun u_13_6_0 () Real)
(declare-fun u_14_7_t () Real)
(declare-fun u_14_7_0 () Real)
(declare-fun u_15_8_t () Real)
(declare-fun u_15_8_0 () Real)
(declare-fun u_16_1_t () Real)
(declare-fun u_16_1_0 () Real)
(declare-fun u_17_2_t () Real)
(declare-fun u_17_2_0 () Real)
(declare-fun u_18_3_t () Real)
(declare-fun u_18_3_0 () Real)
(declare-fun u_19_4_t () Real)
(declare-fun u_19_4_0 () Real)
(declare-fun u_20_5_t () Real)
(declare-fun u_20_5_0 () Real)
(declare-fun u_21_6_t () Real)
(declare-fun u_21_6_0 () Real)
(declare-fun u_22_7_t () Real)
(declare-fun u_22_7_0 () Real)
(declare-fun u_23_8_t () Real)
(declare-fun u_23_8_0 () Real)
(declare-fun tau_0_1_t () Real)
(declare-fun tau_0_1_0 () Real)
(declare-fun tau_1_2_t () Real)
(declare-fun tau_1_2_0 () Real)
(declare-fun tau_2_3_t () Real)
(declare-fun tau_2_3_0 () Real)
(declare-fun tau_3_4_t () Real)
(declare-fun tau_3_4_0 () Real)
(declare-fun tau_4_5_t () Real)
(declare-fun tau_4_5_0 () Real)
(declare-fun tau_5_6_t () Real)
(declare-fun tau_5_6_0 () Real)
(declare-fun tau_6_7_t () Real)
(declare-fun tau_6_7_0 () Real)
(declare-fun tau_7_8_t () Real)
(declare-fun tau_7_8_0 () Real)
(declare-fun tau_8_1_t () Real)
(declare-fun tau_8_1_0 () Real)
(declare-fun tau_9_2_t () Real)
(declare-fun tau_9_2_0 () Real)
(declare-fun tau_10_3_t () Real)
(declare-fun tau_10_3_0 () Real)
(declare-fun tau_11_4_t () Real)
(declare-fun tau_11_4_0 () Real)
(declare-fun tau_12_5_t () Real)
(declare-fun tau_12_5_0 () Real)
(declare-fun tau_13_6_t () Real)
(declare-fun tau_13_6_0 () Real)
(declare-fun tau_14_7_t () Real)
(declare-fun tau_14_7_0 () Real)
(declare-fun tau_15_8_t () Real)
(declare-fun tau_15_8_0 () Real)
(declare-fun tau_16_1_t () Real)
(declare-fun tau_16_1_0 () Real)
(declare-fun tau_17_2_t () Real)
(declare-fun tau_17_2_0 () Real)
(declare-fun tau_18_3_t () Real)
(declare-fun tau_18_3_0 () Real)
(declare-fun tau_19_4_t () Real)
(declare-fun tau_19_4_0 () Real)
(declare-fun tau_20_5_t () Real)
(declare-fun tau_20_5_0 () Real)
(declare-fun tau_21_6_t () Real)
(declare-fun tau_21_6_0 () Real)
(declare-fun tau_22_7_t () Real)
(declare-fun tau_22_7_0 () Real)
(declare-fun tau_23_8_t () Real)
(declare-fun tau_23_8_0 () Real)
(declare-fun s_0_1_t () Real)
(declare-fun s_0_1_0 () Real)
(declare-fun s_1_2_t () Real)
(declare-fun s_1_2_0 () Real)
(declare-fun s_2_3_t () Real)
(declare-fun s_2_3_0 () Real)
(declare-fun s_3_4_t () Real)
(declare-fun s_3_4_0 () Real)
(declare-fun s_4_5_t () Real)
(declare-fun s_4_5_0 () Real)
(declare-fun s_5_6_t () Real)
(declare-fun s_5_6_0 () Real)
(declare-fun s_6_7_t () Real)
(declare-fun s_6_7_0 () Real)
(declare-fun s_7_8_t () Real)
(declare-fun s_7_8_0 () Real)
(declare-fun s_8_1_t () Real)
(declare-fun s_8_1_0 () Real)
(declare-fun s_9_2_t () Real)
(declare-fun s_9_2_0 () Real)
(declare-fun s_10_3_t () Real)
(declare-fun s_10_3_0 () Real)
(declare-fun s_11_4_t () Real)
(declare-fun s_11_4_0 () Real)
(declare-fun s_12_5_t () Real)
(declare-fun s_12_5_0 () Real)
(declare-fun s_13_6_t () Real)
(declare-fun s_13_6_0 () Real)
(declare-fun s_14_7_t () Real)
(declare-fun s_14_7_0 () Real)
(declare-fun s_15_8_t () Real)
(declare-fun s_15_8_0 () Real)
(declare-fun s_16_1_t () Real)
(declare-fun s_16_1_0 () Real)
(declare-fun s_17_2_t () Real)
(declare-fun s_17_2_0 () Real)
(declare-fun s_18_3_t () Real)
(declare-fun s_18_3_0 () Real)
(declare-fun s_19_4_t () Real)
(declare-fun s_19_4_0 () Real)
(declare-fun s_20_5_t () Real)
(declare-fun s_20_5_0 () Real)
(declare-fun s_21_6_t () Real)
(declare-fun s_21_6_0 () Real)
(declare-fun s_22_7_t () Real)
(declare-fun s_22_7_0 () Real)
(declare-fun s_23_8_t () Real)
(declare-fun s_23_8_0 () Real)
(declare-fun time_1 () Real)
(declare-fun time_10 () Real)
(declare-fun time_19 () Real)
(declare-fun time_28 () Real)
(declare-fun time_37 () Real)
(declare-fun time_46 () Real)
(declare-fun time_55 () Real)
(declare-fun time_64 () Real)
(declare-fun time_65 () Real)
(declare-fun time_74 () Real)
(declare-fun time_83 () Real)
(declare-fun time_92 () Real)
(declare-fun time_101 () Real)
(declare-fun time_110 () Real)
(declare-fun time_119 () Real)
(declare-fun time_128 () Real)
(declare-fun time_129 () Real)
(declare-fun time_138 () Real)
(declare-fun time_147 () Real)
(declare-fun time_156 () Real)
(declare-fun time_165 () Real)
(declare-fun time_174 () Real)
(declare-fun time_183 () Real)
(declare-fun time_192 () Real)
(define-ode 1 (= d/dt[tau_0_1] 1.000000))
(define-ode 1 (= d/dt[u_0_1] ((1.000000 - 0.000000) - ((u_0_1 / 400.000000) + 0.000000))))
(define-ode 1 (= d/dt[w_0_1] (((1.000000 - (u_0_1 / 0.070000)) - w_0_1) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_0_1 - 0.030000)))))))))))
(define-ode 1 (= d/dt[v_0_1] ((1.000000 - v_0_1) / 60.000000)))
(define-ode 1 (= d/dt[s_0_1] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_0_1 - 0.908700)))))) - s_0_1) / 2.734200)))
(define-ode 10 (= d/dt[tau_1_2] 1.000000))
(define-ode 10 (= d/dt[u_1_2] ((1.000000 - 0.000000) - ((u_1_2 / 6.000000) + 0.000000))))
(define-ode 10 (= d/dt[w_1_2] ((0.940000 - w_1_2) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_1_2 - 0.030000)))))))))))
(define-ode 10 (= d/dt[v_1_2] (0.000000 - (v_1_2 / 1150.000000))))
(define-ode 10 (= d/dt[s_1_2] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_1_2 - 0.908700)))))) - s_1_2) / 2.734200)))
(define-ode 19 (= d/dt[tau_2_3] 1.000000))
(define-ode 19 (= d/dt[u_2_3] ((1.000000 - 0.000000) - (1.000000 / ((30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_2_3 - 0.650000)))))))) + (0.000000 - ((w_2_3 * s_2_3) / 1.887500)))))))
(define-ode 19 (= d/dt[w_2_3] (0.000000 - (w_2_3 / 200.000000))))
(define-ode 19 (= d/dt[v_2_3] (0.000000 - (v_2_3 / 1150.000000))))
(define-ode 19 (= d/dt[s_2_3] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_2_3 - 0.908700)))))) - s_2_3) / 16.000000)))
(define-ode 28 (= d/dt[tau_3_4] 1.000000))
(define-ode 28 (= d/dt[u_3_4] ((1.000000 - (0.000000 - (v_3_4 * ((u_3_4 - 0.300000) * ((1.550000 - u_3_4) / 0.110000))))) - ((1.000000 / (30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_3_4 - 0.650000))))))))) + (0.000000 - ((w_3_4 * s_3_4) / 1.887500))))))
(define-ode 28 (= d/dt[w_3_4] (0.000000 - (w_3_4 / 200.000000))))
(define-ode 28 (= d/dt[v_3_4] (0.000000 - (v_3_4 / 1.450600))))
(define-ode 28 (= d/dt[s_3_4] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_3_4 - 0.908700)))))) - s_3_4) / 16.000000)))
(define-ode 37 (= d/dt[tau_4_5] 1.000000))
(define-ode 37 (= d/dt[u_4_5] ((0.000000 - (0.000000 - (v_4_5 * ((u_4_5 - 0.300000) * ((1.550000 - u_4_5) / 0.110000))))) - ((1.000000 / (30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_4_5 - 0.650000))))))))) + (0.000000 - ((w_4_5 * s_4_5) / 1.887500))))))
(define-ode 37 (= d/dt[w_4_5] (0.000000 - (w_4_5 / 200.000000))))
(define-ode 37 (= d/dt[v_4_5] (0.000000 - (v_4_5 / 1.450600))))
(define-ode 37 (= d/dt[s_4_5] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_4_5 - 0.908700)))))) - s_4_5) / 16.000000)))
(define-ode 46 (= d/dt[tau_5_6] 1.000000))
(define-ode 46 (= d/dt[u_5_6] ((0.000000 - 0.000000) - (1.000000 / ((30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_5_6 - 0.650000)))))))) + (0.000000 - ((w_5_6 * s_5_6) / 1.887500)))))))
(define-ode 46 (= d/dt[w_5_6] (0.000000 - (w_5_6 / 200.000000))))
(define-ode 46 (= d/dt[v_5_6] (0.000000 - (v_5_6 / 1150.000000))))
(define-ode 46 (= d/dt[s_5_6] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_5_6 - 0.908700)))))) - s_5_6) / 16.000000)))
(define-ode 55 (= d/dt[tau_6_7] 1.000000))
(define-ode 55 (= d/dt[u_6_7] ((0.000000 - 0.000000) - ((u_6_7 / 6.000000) + 0.000000))))
(define-ode 55 (= d/dt[w_6_7] ((0.940000 - w_6_7) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_6_7 - 0.030000)))))))))))
(define-ode 55 (= d/dt[v_6_7] (0.000000 - (v_6_7 / 1150.000000))))
(define-ode 55 (= d/dt[s_6_7] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_6_7 - 0.908700)))))) - s_6_7) / 2.734200)))
(define-ode 64 (= d/dt[tau_7_8] 1.000000))
(define-ode 64 (= d/dt[u_7_8] ((0.000000 - 0.000000) - ((u_7_8 / 400.000000) + 0.000000))))
(define-ode 64 (= d/dt[w_7_8] (((1.000000 - (u_7_8 / 0.070000)) - w_7_8) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_7_8 - 0.030000)))))))))))
(define-ode 64 (= d/dt[v_7_8] ((1.000000 - v_7_8) / 60.000000)))
(define-ode 64 (= d/dt[s_7_8] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_7_8 - 0.908700)))))) - s_7_8) / 2.734200)))
(define-ode 65 (= d/dt[tau_8_1] 1.000000))
(define-ode 65 (= d/dt[u_8_1] ((1.000000 - 0.000000) - ((u_8_1 / 400.000000) + 0.000000))))
(define-ode 65 (= d/dt[w_8_1] (((1.000000 - (u_8_1 / 0.070000)) - w_8_1) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_8_1 - 0.030000)))))))))))
(define-ode 65 (= d/dt[v_8_1] ((1.000000 - v_8_1) / 60.000000)))
(define-ode 65 (= d/dt[s_8_1] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_8_1 - 0.908700)))))) - s_8_1) / 2.734200)))
(define-ode 74 (= d/dt[tau_9_2] 1.000000))
(define-ode 74 (= d/dt[u_9_2] ((1.000000 - 0.000000) - ((u_9_2 / 6.000000) + 0.000000))))
(define-ode 74 (= d/dt[w_9_2] ((0.940000 - w_9_2) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_9_2 - 0.030000)))))))))))
(define-ode 74 (= d/dt[v_9_2] (0.000000 - (v_9_2 / 1150.000000))))
(define-ode 74 (= d/dt[s_9_2] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_9_2 - 0.908700)))))) - s_9_2) / 2.734200)))
(define-ode 83 (= d/dt[tau_10_3] 1.000000))
(define-ode 83 (= d/dt[u_10_3] ((1.000000 - 0.000000) - (1.000000 / ((30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_10_3 - 0.650000)))))))) + (0.000000 - ((w_10_3 * s_10_3) / 1.887500)))))))
(define-ode 83 (= d/dt[w_10_3] (0.000000 - (w_10_3 / 200.000000))))
(define-ode 83 (= d/dt[v_10_3] (0.000000 - (v_10_3 / 1150.000000))))
(define-ode 83 (= d/dt[s_10_3] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_10_3 - 0.908700)))))) - s_10_3) / 16.000000)))
(define-ode 92 (= d/dt[tau_11_4] 1.000000))
(define-ode 92 (= d/dt[u_11_4] ((1.000000 - (0.000000 - (v_11_4 * ((u_11_4 - 0.300000) * ((1.550000 - u_11_4) / 0.110000))))) - ((1.000000 / (30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_11_4 - 0.650000))))))))) + (0.000000 - ((w_11_4 * s_11_4) / 1.887500))))))
(define-ode 92 (= d/dt[w_11_4] (0.000000 - (w_11_4 / 200.000000))))
(define-ode 92 (= d/dt[v_11_4] (0.000000 - (v_11_4 / 1.450600))))
(define-ode 92 (= d/dt[s_11_4] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_11_4 - 0.908700)))))) - s_11_4) / 16.000000)))
(define-ode 101 (= d/dt[tau_12_5] 1.000000))
(define-ode 101 (= d/dt[u_12_5] ((0.000000 - (0.000000 - (v_12_5 * ((u_12_5 - 0.300000) * ((1.550000 - u_12_5) / 0.110000))))) - ((1.000000 / (30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_12_5 - 0.650000))))))))) + (0.000000 - ((w_12_5 * s_12_5) / 1.887500))))))
(define-ode 101 (= d/dt[w_12_5] (0.000000 - (w_12_5 / 200.000000))))
(define-ode 101 (= d/dt[v_12_5] (0.000000 - (v_12_5 / 1.450600))))
(define-ode 101 (= d/dt[s_12_5] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_12_5 - 0.908700)))))) - s_12_5) / 16.000000)))
(define-ode 110 (= d/dt[tau_13_6] 1.000000))
(define-ode 110 (= d/dt[u_13_6] ((0.000000 - 0.000000) - (1.000000 / ((30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_13_6 - 0.650000)))))))) + (0.000000 - ((w_13_6 * s_13_6) / 1.887500)))))))
(define-ode 110 (= d/dt[w_13_6] (0.000000 - (w_13_6 / 200.000000))))
(define-ode 110 (= d/dt[v_13_6] (0.000000 - (v_13_6 / 1150.000000))))
(define-ode 110 (= d/dt[s_13_6] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_13_6 - 0.908700)))))) - s_13_6) / 16.000000)))
(define-ode 119 (= d/dt[tau_14_7] 1.000000))
(define-ode 119 (= d/dt[u_14_7] ((0.000000 - 0.000000) - ((u_14_7 / 6.000000) + 0.000000))))
(define-ode 119 (= d/dt[w_14_7] ((0.940000 - w_14_7) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_14_7 - 0.030000)))))))))))
(define-ode 119 (= d/dt[v_14_7] (0.000000 - (v_14_7 / 1150.000000))))
(define-ode 119 (= d/dt[s_14_7] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_14_7 - 0.908700)))))) - s_14_7) / 2.734200)))
(define-ode 128 (= d/dt[tau_15_8] 1.000000))
(define-ode 128 (= d/dt[u_15_8] ((0.000000 - 0.000000) - ((u_15_8 / 400.000000) + 0.000000))))
(define-ode 128 (= d/dt[w_15_8] (((1.000000 - (u_15_8 / 0.070000)) - w_15_8) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_15_8 - 0.030000)))))))))))
(define-ode 128 (= d/dt[v_15_8] ((1.000000 - v_15_8) / 60.000000)))
(define-ode 128 (= d/dt[s_15_8] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_15_8 - 0.908700)))))) - s_15_8) / 2.734200)))
(define-ode 129 (= d/dt[tau_16_1] 1.000000))
(define-ode 129 (= d/dt[u_16_1] ((1.000000 - 0.000000) - ((u_16_1 / 400.000000) + 0.000000))))
(define-ode 129 (= d/dt[w_16_1] (((1.000000 - (u_16_1 / 0.070000)) - w_16_1) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_16_1 - 0.030000)))))))))))
(define-ode 129 (= d/dt[v_16_1] ((1.000000 - v_16_1) / 60.000000)))
(define-ode 129 (= d/dt[s_16_1] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_16_1 - 0.908700)))))) - s_16_1) / 2.734200)))
(define-ode 138 (= d/dt[tau_17_2] 1.000000))
(define-ode 138 (= d/dt[u_17_2] ((1.000000 - 0.000000) - ((u_17_2 / 6.000000) + 0.000000))))
(define-ode 138 (= d/dt[w_17_2] ((0.940000 - w_17_2) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_17_2 - 0.030000)))))))))))
(define-ode 138 (= d/dt[v_17_2] (0.000000 - (v_17_2 / 1150.000000))))
(define-ode 138 (= d/dt[s_17_2] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_17_2 - 0.908700)))))) - s_17_2) / 2.734200)))
(define-ode 147 (= d/dt[tau_18_3] 1.000000))
(define-ode 147 (= d/dt[u_18_3] ((1.000000 - 0.000000) - (1.000000 / ((30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_18_3 - 0.650000)))))))) + (0.000000 - ((w_18_3 * s_18_3) / 1.887500)))))))
(define-ode 147 (= d/dt[w_18_3] (0.000000 - (w_18_3 / 200.000000))))
(define-ode 147 (= d/dt[v_18_3] (0.000000 - (v_18_3 / 1150.000000))))
(define-ode 147 (= d/dt[s_18_3] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_18_3 - 0.908700)))))) - s_18_3) / 16.000000)))
(define-ode 156 (= d/dt[tau_19_4] 1.000000))
(define-ode 156 (= d/dt[u_19_4] ((1.000000 - (0.000000 - (v_19_4 * ((u_19_4 - 0.300000) * ((1.550000 - u_19_4) / 0.110000))))) - ((1.000000 / (30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_19_4 - 0.650000))))))))) + (0.000000 - ((w_19_4 * s_19_4) / 1.887500))))))
(define-ode 156 (= d/dt[w_19_4] (0.000000 - (w_19_4 / 200.000000))))
(define-ode 156 (= d/dt[v_19_4] (0.000000 - (v_19_4 / 1.450600))))
(define-ode 156 (= d/dt[s_19_4] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_19_4 - 0.908700)))))) - s_19_4) / 16.000000)))
(define-ode 165 (= d/dt[tau_20_5] 1.000000))
(define-ode 165 (= d/dt[u_20_5] ((0.000000 - (0.000000 - (v_20_5 * ((u_20_5 - 0.300000) * ((1.550000 - u_20_5) / 0.110000))))) - ((1.000000 / (30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_20_5 - 0.650000))))))))) + (0.000000 - ((w_20_5 * s_20_5) / 1.887500))))))
(define-ode 165 (= d/dt[w_20_5] (0.000000 - (w_20_5 / 200.000000))))
(define-ode 165 (= d/dt[v_20_5] (0.000000 - (v_20_5 / 1.450600))))
(define-ode 165 (= d/dt[s_20_5] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_20_5 - 0.908700)))))) - s_20_5) / 16.000000)))
(define-ode 174 (= d/dt[tau_21_6] 1.000000))
(define-ode 174 (= d/dt[u_21_6] ((0.000000 - 0.000000) - (1.000000 / ((30.018100 + ((0.995700 - 30.018100) * (1.000000 / (1.000000 + exp((-2.000000 * (2.045800 * (u_21_6 - 0.650000)))))))) + (0.000000 - ((w_21_6 * s_21_6) / 1.887500)))))))
(define-ode 174 (= d/dt[w_21_6] (0.000000 - (w_21_6 / 200.000000))))
(define-ode 174 (= d/dt[v_21_6] (0.000000 - (v_21_6 / 1150.000000))))
(define-ode 174 (= d/dt[s_21_6] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_21_6 - 0.908700)))))) - s_21_6) / 16.000000)))
(define-ode 183 (= d/dt[tau_22_7] 1.000000))
(define-ode 183 (= d/dt[u_22_7] ((0.000000 - 0.000000) - ((u_22_7 / 6.000000) + 0.000000))))
(define-ode 183 (= d/dt[w_22_7] ((0.940000 - w_22_7) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_22_7 - 0.030000)))))))))))
(define-ode 183 (= d/dt[v_22_7] (0.000000 - (v_22_7 / 1150.000000))))
(define-ode 183 (= d/dt[s_22_7] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_22_7 - 0.908700)))))) - s_22_7) / 2.734200)))
(define-ode 192 (= d/dt[tau_23_8] 1.000000))
(define-ode 192 (= d/dt[u_23_8] ((0.000000 - 0.000000) - ((u_23_8 / 400.000000) + 0.000000))))
(define-ode 192 (= d/dt[w_23_8] (((1.000000 - (u_23_8 / 0.070000)) - w_23_8) / (60.000000 + ((15.000000 - 60.000000) * (1.000000 / (1.000000 + exp((-2.000000 * (65.000000 * (u_23_8 - 0.030000)))))))))))
(define-ode 192 (= d/dt[v_23_8] ((1.000000 - v_23_8) / 60.000000)))
(define-ode 192 (= d/dt[s_23_8] (((1.000000 / (1.000000 + exp((-2.000000 * (2.099400 * (u_23_8 - 0.908700)))))) - s_23_8) / 2.734200)))
(assert (<= 0.000000 w_0_1_t))
(assert (<= w_0_1_t 1.500000))
(assert (<= 0.000000 w_0_1_0))
(assert (<= w_0_1_0 1.500000))
(assert (<= 0.000000 w_1_2_t))
(assert (<= w_1_2_t 1.500000))
(assert (<= 0.000000 w_1_2_0))
(assert (<= w_1_2_0 1.500000))
(assert (<= 0.000000 w_2_3_t))
(assert (<= w_2_3_t 1.500000))
(assert (<= 0.000000 w_2_3_0))
(assert (<= w_2_3_0 1.500000))
(assert (<= 0.000000 w_3_4_t))
(assert (<= w_3_4_t 1.500000))
(assert (<= 0.000000 w_3_4_0))
(assert (<= w_3_4_0 1.500000))
(assert (<= 0.000000 w_4_5_t))
(assert (<= w_4_5_t 1.500000))
(assert (<= 0.000000 w_4_5_0))
(assert (<= w_4_5_0 1.500000))
(assert (<= 0.000000 w_5_6_t))
(assert (<= w_5_6_t 1.500000))
(assert (<= 0.000000 w_5_6_0))
(assert (<= w_5_6_0 1.500000))
(assert (<= 0.000000 w_6_7_t))
(assert (<= w_6_7_t 1.500000))
(assert (<= 0.000000 w_6_7_0))
(assert (<= w_6_7_0 1.500000))
(assert (<= 0.000000 w_7_8_t))
(assert (<= w_7_8_t 1.500000))
(assert (<= 0.000000 w_7_8_0))
(assert (<= w_7_8_0 1.500000))
(assert (<= 0.000000 w_8_1_t))
(assert (<= w_8_1_t 1.500000))
(assert (<= 0.000000 w_8_1_0))
(assert (<= w_8_1_0 1.500000))
(assert (<= 0.000000 w_9_2_t))
(assert (<= w_9_2_t 1.500000))
(assert (<= 0.000000 w_9_2_0))
(assert (<= w_9_2_0 1.500000))
(assert (<= 0.000000 w_10_3_t))
(assert (<= w_10_3_t 1.500000))
(assert (<= 0.000000 w_10_3_0))
(assert (<= w_10_3_0 1.500000))
(assert (<= 0.000000 w_11_4_t))
(assert (<= w_11_4_t 1.500000))
(assert (<= 0.000000 w_11_4_0))
(assert (<= w_11_4_0 1.500000))
(assert (<= 0.000000 w_12_5_t))
(assert (<= w_12_5_t 1.500000))
(assert (<= 0.000000 w_12_5_0))
(assert (<= w_12_5_0 1.500000))
(assert (<= 0.000000 w_13_6_t))
(assert (<= w_13_6_t 1.500000))
(assert (<= 0.000000 w_13_6_0))
(assert (<= w_13_6_0 1.500000))
(assert (<= 0.000000 w_14_7_t))
(assert (<= w_14_7_t 1.500000))
(assert (<= 0.000000 w_14_7_0))
(assert (<= w_14_7_0 1.500000))
(assert (<= 0.000000 w_15_8_t))
(assert (<= w_15_8_t 1.500000))
(assert (<= 0.000000 w_15_8_0))
(assert (<= w_15_8_0 1.500000))
(assert (<= 0.000000 w_16_1_t))
(assert (<= w_16_1_t 1.500000))
(assert (<= 0.000000 w_16_1_0))
(assert (<= w_16_1_0 1.500000))
(assert (<= 0.000000 w_17_2_t))
(assert (<= w_17_2_t 1.500000))
(assert (<= 0.000000 w_17_2_0))
(assert (<= w_17_2_0 1.500000))
(assert (<= 0.000000 w_18_3_t))
(assert (<= w_18_3_t 1.500000))
(assert (<= 0.000000 w_18_3_0))
(assert (<= w_18_3_0 1.500000))
(assert (<= 0.000000 w_19_4_t))
(assert (<= w_19_4_t 1.500000))
(assert (<= 0.000000 w_19_4_0))
(assert (<= w_19_4_0 1.500000))
(assert (<= 0.000000 w_20_5_t))
(assert (<= w_20_5_t 1.500000))
(assert (<= 0.000000 w_20_5_0))
(assert (<= w_20_5_0 1.500000))
(assert (<= 0.000000 w_21_6_t))
(assert (<= w_21_6_t 1.500000))
(assert (<= 0.000000 w_21_6_0))
(assert (<= w_21_6_0 1.500000))
(assert (<= 0.000000 w_22_7_t))
(assert (<= w_22_7_t 1.500000))
(assert (<= 0.000000 w_22_7_0))
(assert (<= w_22_7_0 1.500000))
(assert (<= 0.000000 w_23_8_t))
(assert (<= w_23_8_t 1.500000))
(assert (<= 0.000000 w_23_8_0))
(assert (<= w_23_8_0 1.500000))
(assert (<= 0.000000 v_0_1_t))
(assert (<= v_0_1_t 1.200000))
(assert (<= 0.000000 v_0_1_0))
(assert (<= v_0_1_0 1.200000))
(assert (<= 0.000000 v_1_2_t))
(assert (<= v_1_2_t 1.200000))
(assert (<= 0.000000 v_1_2_0))
(assert (<= v_1_2_0 1.200000))
(assert (<= 0.000000 v_2_3_t))
(assert (<= v_2_3_t 1.200000))
(assert (<= 0.000000 v_2_3_0))
(assert (<= v_2_3_0 1.200000))
(assert (<= 0.000000 v_3_4_t))
(assert (<= v_3_4_t 1.200000))
(assert (<= 0.000000 v_3_4_0))
(assert (<= v_3_4_0 1.200000))
(assert (<= 0.000000 v_4_5_t))
(assert (<= v_4_5_t 1.200000))
(assert (<= 0.000000 v_4_5_0))
(assert (<= v_4_5_0 1.200000))
(assert (<= 0.000000 v_5_6_t))
(assert (<= v_5_6_t 1.200000))
(assert (<= 0.000000 v_5_6_0))
(assert (<= v_5_6_0 1.200000))
(assert (<= 0.000000 v_6_7_t))
(assert (<= v_6_7_t 1.200000))
(assert (<= 0.000000 v_6_7_0))
(assert (<= v_6_7_0 1.200000))
(assert (<= 0.000000 v_7_8_t))
(assert (<= v_7_8_t 1.200000))
(assert (<= 0.000000 v_7_8_0))
(assert (<= v_7_8_0 1.200000))
(assert (<= 0.000000 v_8_1_t))
(assert (<= v_8_1_t 1.200000))
(assert (<= 0.000000 v_8_1_0))
(assert (<= v_8_1_0 1.200000))
(assert (<= 0.000000 v_9_2_t))
(assert (<= v_9_2_t 1.200000))
(assert (<= 0.000000 v_9_2_0))
(assert (<= v_9_2_0 1.200000))
(assert (<= 0.000000 v_10_3_t))
(assert (<= v_10_3_t 1.200000))
(assert (<= 0.000000 v_10_3_0))
(assert (<= v_10_3_0 1.200000))
(assert (<= 0.000000 v_11_4_t))
(assert (<= v_11_4_t 1.200000))
(assert (<= 0.000000 v_11_4_0))
(assert (<= v_11_4_0 1.200000))
(assert (<= 0.000000 v_12_5_t))
(assert (<= v_12_5_t 1.200000))
(assert (<= 0.000000 v_12_5_0))
(assert (<= v_12_5_0 1.200000))
(assert (<= 0.000000 v_13_6_t))
(assert (<= v_13_6_t 1.200000))
(assert (<= 0.000000 v_13_6_0))
(assert (<= v_13_6_0 1.200000))
(assert (<= 0.000000 v_14_7_t))
(assert (<= v_14_7_t 1.200000))
(assert (<= 0.000000 v_14_7_0))
(assert (<= v_14_7_0 1.200000))
(assert (<= 0.000000 v_15_8_t))
(assert (<= v_15_8_t 1.200000))
(assert (<= 0.000000 v_15_8_0))
(assert (<= v_15_8_0 1.200000))
(assert (<= 0.000000 v_16_1_t))
(assert (<= v_16_1_t 1.200000))
(assert (<= 0.000000 v_16_1_0))
(assert (<= v_16_1_0 1.200000))
(assert (<= 0.000000 v_17_2_t))
(assert (<= v_17_2_t 1.200000))
(assert (<= 0.000000 v_17_2_0))
(assert (<= v_17_2_0 1.200000))
(assert (<= 0.000000 v_18_3_t))
(assert (<= v_18_3_t 1.200000))
(assert (<= 0.000000 v_18_3_0))
(assert (<= v_18_3_0 1.200000))
(assert (<= 0.000000 v_19_4_t))
(assert (<= v_19_4_t 1.200000))
(assert (<= 0.000000 v_19_4_0))
(assert (<= v_19_4_0 1.200000))
(assert (<= 0.000000 v_20_5_t))
(assert (<= v_20_5_t 1.200000))
(assert (<= 0.000000 v_20_5_0))
(assert (<= v_20_5_0 1.200000))
(assert (<= 0.000000 v_21_6_t))
(assert (<= v_21_6_t 1.200000))
(assert (<= 0.000000 v_21_6_0))
(assert (<= v_21_6_0 1.200000))
(assert (<= 0.000000 v_22_7_t))
(assert (<= v_22_7_t 1.200000))
(assert (<= 0.000000 v_22_7_0))
(assert (<= v_22_7_0 1.200000))
(assert (<= 0.000000 v_23_8_t))
(assert (<= v_23_8_t 1.200000))
(assert (<= 0.000000 v_23_8_0))
(assert (<= v_23_8_0 1.200000))
(assert (<= 0.000000 u_0_1_t))
(assert (<= u_0_1_t 1.800000))
(assert (<= 0.000000 u_0_1_0))
(assert (<= u_0_1_0 1.800000))
(assert (<= 0.000000 u_1_2_t))
(assert (<= u_1_2_t 1.800000))
(assert (<= 0.000000 u_1_2_0))
(assert (<= u_1_2_0 1.800000))
(assert (<= 0.000000 u_2_3_t))
(assert (<= u_2_3_t 1.800000))
(assert (<= 0.000000 u_2_3_0))
(assert (<= u_2_3_0 1.800000))
(assert (<= 0.000000 u_3_4_t))
(assert (<= u_3_4_t 1.800000))
(assert (<= 0.000000 u_3_4_0))
(assert (<= u_3_4_0 1.800000))
(assert (<= 0.000000 u_4_5_t))
(assert (<= u_4_5_t 1.800000))
(assert (<= 0.000000 u_4_5_0))
(assert (<= u_4_5_0 1.800000))
(assert (<= 0.000000 u_5_6_t))
(assert (<= u_5_6_t 1.800000))
(assert (<= 0.000000 u_5_6_0))
(assert (<= u_5_6_0 1.800000))
(assert (<= 0.000000 u_6_7_t))
(assert (<= u_6_7_t 1.800000))
(assert (<= 0.000000 u_6_7_0))
(assert (<= u_6_7_0 1.800000))
(assert (<= 0.000000 u_7_8_t))
(assert (<= u_7_8_t 1.800000))
(assert (<= 0.000000 u_7_8_0))
(assert (<= u_7_8_0 1.800000))
(assert (<= 0.000000 u_8_1_t))
(assert (<= u_8_1_t 1.800000))
(assert (<= 0.000000 u_8_1_0))
(assert (<= u_8_1_0 1.800000))
(assert (<= 0.000000 u_9_2_t))
(assert (<= u_9_2_t 1.800000))
(assert (<= 0.000000 u_9_2_0))
(assert (<= u_9_2_0 1.800000))
(assert (<= 0.000000 u_10_3_t))
(assert (<= u_10_3_t 1.800000))
(assert (<= 0.000000 u_10_3_0))
(assert (<= u_10_3_0 1.800000))
(assert (<= 0.000000 u_11_4_t))
(assert (<= u_11_4_t 1.800000))
(assert (<= 0.000000 u_11_4_0))
(assert (<= u_11_4_0 1.800000))
(assert (<= 0.000000 u_12_5_t))
(assert (<= u_12_5_t 1.800000))
(assert (<= 0.000000 u_12_5_0))
(assert (<= u_12_5_0 1.800000))
(assert (<= 0.000000 u_13_6_t))
(assert (<= u_13_6_t 1.800000))
(assert (<= 0.000000 u_13_6_0))
(assert (<= u_13_6_0 1.800000))
(assert (<= 0.000000 u_14_7_t))
(assert (<= u_14_7_t 1.800000))
(assert (<= 0.000000 u_14_7_0))
(assert (<= u_14_7_0 1.800000))
(assert (<= 0.000000 u_15_8_t))
(assert (<= u_15_8_t 1.800000))
(assert (<= 0.000000 u_15_8_0))
(assert (<= u_15_8_0 1.800000))
(assert (<= 0.000000 u_16_1_t))
(assert (<= u_16_1_t 1.800000))
(assert (<= 0.000000 u_16_1_0))
(assert (<= u_16_1_0 1.800000))
(assert (<= 0.000000 u_17_2_t))
(assert (<= u_17_2_t 1.800000))
(assert (<= 0.000000 u_17_2_0))
(assert (<= u_17_2_0 1.800000))
(assert (<= 0.000000 u_18_3_t))
(assert (<= u_18_3_t 1.800000))
(assert (<= 0.000000 u_18_3_0))
(assert (<= u_18_3_0 1.800000))
(assert (<= 0.000000 u_19_4_t))
(assert (<= u_19_4_t 1.800000))
(assert (<= 0.000000 u_19_4_0))
(assert (<= u_19_4_0 1.800000))
(assert (<= 0.000000 u_20_5_t))
(assert (<= u_20_5_t 1.800000))
(assert (<= 0.000000 u_20_5_0))
(assert (<= u_20_5_0 1.800000))
(assert (<= 0.000000 u_21_6_t))
(assert (<= u_21_6_t 1.800000))
(assert (<= 0.000000 u_21_6_0))
(assert (<= u_21_6_0 1.800000))
(assert (<= 0.000000 u_22_7_t))
(assert (<= u_22_7_t 1.800000))
(assert (<= 0.000000 u_22_7_0))
(assert (<= u_22_7_0 1.800000))
(assert (<= 0.000000 u_23_8_t))
(assert (<= u_23_8_t 1.800000))
(assert (<= 0.000000 u_23_8_0))
(assert (<= u_23_8_0 1.800000))
(assert (<= 0.000000 tau_0_1_t))
(assert (<= tau_0_1_t 500.000000))
(assert (<= 0.000000 tau_0_1_0))
(assert (<= tau_0_1_0 500.000000))
(assert (<= 0.000000 tau_1_2_t))
(assert (<= tau_1_2_t 500.000000))
(assert (<= 0.000000 tau_1_2_0))
(assert (<= tau_1_2_0 500.000000))
(assert (<= 0.000000 tau_2_3_t))
(assert (<= tau_2_3_t 500.000000))
(assert (<= 0.000000 tau_2_3_0))
(assert (<= tau_2_3_0 500.000000))
(assert (<= 0.000000 tau_3_4_t))
(assert (<= tau_3_4_t 500.000000))
(assert (<= 0.000000 tau_3_4_0))
(assert (<= tau_3_4_0 500.000000))
(assert (<= 0.000000 tau_4_5_t))
(assert (<= tau_4_5_t 500.000000))
(assert (<= 0.000000 tau_4_5_0))
(assert (<= tau_4_5_0 500.000000))
(assert (<= 0.000000 tau_5_6_t))
(assert (<= tau_5_6_t 500.000000))
(assert (<= 0.000000 tau_5_6_0))
(assert (<= tau_5_6_0 500.000000))
(assert (<= 0.000000 tau_6_7_t))
(assert (<= tau_6_7_t 500.000000))
(assert (<= 0.000000 tau_6_7_0))
(assert (<= tau_6_7_0 500.000000))
(assert (<= 0.000000 tau_7_8_t))
(assert (<= tau_7_8_t 500.000000))
(assert (<= 0.000000 tau_7_8_0))
(assert (<= tau_7_8_0 500.000000))
(assert (<= 0.000000 tau_8_1_t))
(assert (<= tau_8_1_t 500.000000))
(assert (<= 0.000000 tau_8_1_0))
(assert (<= tau_8_1_0 500.000000))
(assert (<= 0.000000 tau_9_2_t))
(assert (<= tau_9_2_t 500.000000))
(assert (<= 0.000000 tau_9_2_0))
(assert (<= tau_9_2_0 500.000000))
(assert (<= 0.000000 tau_10_3_t))
(assert (<= tau_10_3_t 500.000000))
(assert (<= 0.000000 tau_10_3_0))
(assert (<= tau_10_3_0 500.000000))
(assert (<= 0.000000 tau_11_4_t))
(assert (<= tau_11_4_t 500.000000))
(assert (<= 0.000000 tau_11_4_0))
(assert (<= tau_11_4_0 500.000000))
(assert (<= 0.000000 tau_12_5_t))
(assert (<= tau_12_5_t 500.000000))
(assert (<= 0.000000 tau_12_5_0))
(assert (<= tau_12_5_0 500.000000))
(assert (<= 0.000000 tau_13_6_t))
(assert (<= tau_13_6_t 500.000000))
(assert (<= 0.000000 tau_13_6_0))
(assert (<= tau_13_6_0 500.000000))
(assert (<= 0.000000 tau_14_7_t))
(assert (<= tau_14_7_t 500.000000))
(assert (<= 0.000000 tau_14_7_0))
(assert (<= tau_14_7_0 500.000000))
(assert (<= 0.000000 tau_15_8_t))
(assert (<= tau_15_8_t 500.000000))
(assert (<= 0.000000 tau_15_8_0))
(assert (<= tau_15_8_0 500.000000))
(assert (<= 0.000000 tau_16_1_t))
(assert (<= tau_16_1_t 500.000000))
(assert (<= 0.000000 tau_16_1_0))
(assert (<= tau_16_1_0 500.000000))
(assert (<= 0.000000 tau_17_2_t))
(assert (<= tau_17_2_t 500.000000))
(assert (<= 0.000000 tau_17_2_0))
(assert (<= tau_17_2_0 500.000000))
(assert (<= 0.000000 tau_18_3_t))
(assert (<= tau_18_3_t 500.000000))
(assert (<= 0.000000 tau_18_3_0))
(assert (<= tau_18_3_0 500.000000))
(assert (<= 0.000000 tau_19_4_t))
(assert (<= tau_19_4_t 500.000000))
(assert (<= 0.000000 tau_19_4_0))
(assert (<= tau_19_4_0 500.000000))
(assert (<= 0.000000 tau_20_5_t))
(assert (<= tau_20_5_t 500.000000))
(assert (<= 0.000000 tau_20_5_0))
(assert (<= tau_20_5_0 500.000000))
(assert (<= 0.000000 tau_21_6_t))
(assert (<= tau_21_6_t 500.000000))
(assert (<= 0.000000 tau_21_6_0))
(assert (<= tau_21_6_0 500.000000))
(assert (<= 0.000000 tau_22_7_t))
(assert (<= tau_22_7_t 500.000000))
(assert (<= 0.000000 tau_22_7_0))
(assert (<= tau_22_7_0 500.000000))
(assert (<= 0.000000 tau_23_8_t))
(assert (<= tau_23_8_t 500.000000))
(assert (<= 0.000000 tau_23_8_0))
(assert (<= tau_23_8_0 500.000000))
(assert (<= 0.000000 s_0_1_t))
(assert (<= s_0_1_t 1.000000))
(assert (<= 0.000000 s_0_1_0))
(assert (<= s_0_1_0 1.000000))
(assert (<= 0.000000 s_1_2_t))
(assert (<= s_1_2_t 1.000000))
(assert (<= 0.000000 s_1_2_0))
(assert (<= s_1_2_0 1.000000))
(assert (<= 0.000000 s_2_3_t))
(assert (<= s_2_3_t 1.000000))
(assert (<= 0.000000 s_2_3_0))
(assert (<= s_2_3_0 1.000000))
(assert (<= 0.000000 s_3_4_t))
(assert (<= s_3_4_t 1.000000))
(assert (<= 0.000000 s_3_4_0))
(assert (<= s_3_4_0 1.000000))
(assert (<= 0.000000 s_4_5_t))
(assert (<= s_4_5_t 1.000000))
(assert (<= 0.000000 s_4_5_0))
(assert (<= s_4_5_0 1.000000))
(assert (<= 0.000000 s_5_6_t))
(assert (<= s_5_6_t 1.000000))
(assert (<= 0.000000 s_5_6_0))
(assert (<= s_5_6_0 1.000000))
(assert (<= 0.000000 s_6_7_t))
(assert (<= s_6_7_t 1.000000))
(assert (<= 0.000000 s_6_7_0))
(assert (<= s_6_7_0 1.000000))
(assert (<= 0.000000 s_7_8_t))
(assert (<= s_7_8_t 1.000000))
(assert (<= 0.000000 s_7_8_0))
(assert (<= s_7_8_0 1.000000))
(assert (<= 0.000000 s_8_1_t))
(assert (<= s_8_1_t 1.000000))
(assert (<= 0.000000 s_8_1_0))
(assert (<= s_8_1_0 1.000000))
(assert (<= 0.000000 s_9_2_t))
(assert (<= s_9_2_t 1.000000))
(assert (<= 0.000000 s_9_2_0))
(assert (<= s_9_2_0 1.000000))
(assert (<= 0.000000 s_10_3_t))
(assert (<= s_10_3_t 1.000000))
(assert (<= 0.000000 s_10_3_0))
(assert (<= s_10_3_0 1.000000))
(assert (<= 0.000000 s_11_4_t))
(assert (<= s_11_4_t 1.000000))
(assert (<= 0.000000 s_11_4_0))
(assert (<= s_11_4_0 1.000000))
(assert (<= 0.000000 s_12_5_t))
(assert (<= s_12_5_t 1.000000))
(assert (<= 0.000000 s_12_5_0))
(assert (<= s_12_5_0 1.000000))
(assert (<= 0.000000 s_13_6_t))
(assert (<= s_13_6_t 1.000000))
(assert (<= 0.000000 s_13_6_0))
(assert (<= s_13_6_0 1.000000))
(assert (<= 0.000000 s_14_7_t))
(assert (<= s_14_7_t 1.000000))
(assert (<= 0.000000 s_14_7_0))
(assert (<= s_14_7_0 1.000000))
(assert (<= 0.000000 s_15_8_t))
(assert (<= s_15_8_t 1.000000))
(assert (<= 0.000000 s_15_8_0))
(assert (<= s_15_8_0 1.000000))
(assert (<= 0.000000 s_16_1_t))
(assert (<= s_16_1_t 1.000000))
(assert (<= 0.000000 s_16_1_0))
(assert (<= s_16_1_0 1.000000))
(assert (<= 0.000000 s_17_2_t))
(assert (<= s_17_2_t 1.000000))
(assert (<= 0.000000 s_17_2_0))
(assert (<= s_17_2_0 1.000000))
(assert (<= 0.000000 s_18_3_t))
(assert (<= s_18_3_t 1.000000))
(assert (<= 0.000000 s_18_3_0))
(assert (<= s_18_3_0 1.000000))
(assert (<= 0.000000 s_19_4_t))
(assert (<= s_19_4_t 1.000000))
(assert (<= 0.000000 s_19_4_0))
(assert (<= s_19_4_0 1.000000))
(assert (<= 0.000000 s_20_5_t))
(assert (<= s_20_5_t 1.000000))
(assert (<= 0.000000 s_20_5_0))
(assert (<= s_20_5_0 1.000000))
(assert (<= 0.000000 s_21_6_t))
(assert (<= s_21_6_t 1.000000))
(assert (<= 0.000000 s_21_6_0))
(assert (<= s_21_6_0 1.000000))
(assert (<= 0.000000 s_22_7_t))
(assert (<= s_22_7_t 1.000000))
(assert (<= 0.000000 s_22_7_0))
(assert (<= s_22_7_0 1.000000))
(assert (<= 0.000000 s_23_8_t))
(assert (<= s_23_8_t 1.000000))
(assert (<= 0.000000 s_23_8_0))
(assert (<= s_23_8_0 1.000000))
(assert (<= 0.000000 time_1))
(assert (<= time_1 500.000000))
(assert (<= 0.000000 time_10))
(assert (<= time_10 500.000000))
(assert (<= 0.000000 time_19))
(assert (<= time_19 500.000000))
(assert (<= 0.000000 time_28))
(assert (<= time_28 500.000000))
(assert (<= 0.000000 time_37))
(assert (<= time_37 500.000000))
(assert (<= 0.000000 time_46))
(assert (<= time_46 500.000000))
(assert (<= 0.000000 time_55))
(assert (<= time_55 500.000000))
(assert (<= 0.000000 time_64))
(assert (<= time_64 500.000000))
(assert (<= 0.000000 time_65))
(assert (<= time_65 500.000000))
(assert (<= 0.000000 time_74))
(assert (<= time_74 500.000000))
(assert (<= 0.000000 time_83))
(assert (<= time_83 500.000000))
(assert (<= 0.000000 time_92))
(assert (<= time_92 500.000000))
(assert (<= 0.000000 time_101))
(assert (<= time_101 500.000000))
(assert (<= 0.000000 time_110))
(assert (<= time_110 500.000000))
(assert (<= 0.000000 time_119))
(assert (<= time_119 500.000000))
(assert (<= 0.000000 time_128))
(assert (<= time_128 500.000000))
(assert (<= 0.000000 time_129))
(assert (<= time_129 500.000000))
(assert (<= 0.000000 time_138))
(assert (<= time_138 500.000000))
(assert (<= 0.000000 time_147))
(assert (<= time_147 500.000000))
(assert (<= 0.000000 time_156))
(assert (<= time_156 500.000000))
(assert (<= 0.000000 time_165))
(assert (<= time_165 500.000000))
(assert (<= 0.000000 time_174))
(assert (<= time_174 500.000000))
(assert (<= 0.000000 time_183))
(assert (<= time_183 500.000000))
(assert (<= 0.000000 time_192))
(assert (<= time_192 500.000000))
(assert (and (= s_0_1_0 0.000000) (= w_0_1_0 1.000000) (= v_0_1_0 1.000000) (= u_0_1_0 0.000000) (= tau_0_1_0 0.000000) (forall_t (>= u_0_1_t 0.000000)) (>= u_0_1_t 0.000000) (>= u_0_1_0 0.000000) (forall_t (<= u_0_1_t 0.006000)) (<= u_0_1_t 0.006000) (<= u_0_1_0 0.006000) (forall_t (>= v_0_1_t 0.000000)) (>= v_0_1_t 0.000000) (>= v_0_1_0 0.000000) (forall_t (>= w_0_1_t 0.000000)) (>= w_0_1_t 0.000000) (>= w_0_1_0 0.000000) (forall_t (>= s_0_1_t 0.000000)) (>= s_0_1_t 0.000000) (>= s_0_1_0 0.000000) (forall_t (<= tau_0_1_t 1.000000)) (<= tau_0_1_t 1.000000) (<= tau_0_1_0 1.000000) (>= u_0_1_t 0.006000) (= s_1_2_0 s_0_1_t) (= w_1_2_0 w_0_1_t) (= v_1_2_0 v_0_1_t) (= u_1_2_0 u_0_1_t) (= tau_1_2_0 tau_0_1_t) (forall_t (>= u_1_2_t 0.006000)) (>= u_1_2_t 0.006000) (>= u_1_2_0 0.006000) (forall_t (<= u_1_2_t 0.013000)) (<= u_1_2_t 0.013000) (<= u_1_2_0 0.013000) (forall_t (>= v_1_2_t 0.000000)) (>= v_1_2_t 0.000000) (>= v_1_2_0 0.000000) (forall_t (>= w_1_2_t 0.000000)) (>= w_1_2_t 0.000000) (>= w_1_2_0 0.000000) (forall_t (>= s_1_2_t 0.000000)) (>= s_1_2_t 0.000000) (>= s_1_2_0 0.000000) (forall_t (<= tau_1_2_t 1.000000)) (<= tau_1_2_t 1.000000) (<= tau_1_2_0 1.000000) (>= u_1_2_t 0.013000) (= s_2_3_0 s_1_2_t) (= w_2_3_0 w_1_2_t) (= v_2_3_0 v_1_2_t) (= u_2_3_0 u_1_2_t) (= tau_2_3_0 tau_1_2_t) (forall_t (>= u_2_3_t 0.013000)) (>= u_2_3_t 0.013000) (>= u_2_3_0 0.013000) (forall_t (<= u_2_3_t 0.300000)) (<= u_2_3_t 0.300000) (<= u_2_3_0 0.300000) (forall_t (>= v_2_3_t 0.000000)) (>= v_2_3_t 0.000000) (>= v_2_3_0 0.000000) (forall_t (>= w_2_3_t 0.000000)) (>= w_2_3_t 0.000000) (>= w_2_3_0 0.000000) (forall_t (>= s_2_3_t 0.000000)) (>= s_2_3_t 0.000000) (>= s_2_3_0 0.000000) (forall_t (<= tau_2_3_t 1.000000)) (<= tau_2_3_t 1.000000) (<= tau_2_3_0 1.000000) (>= u_2_3_t 0.300000) (= s_3_4_0 s_2_3_t) (= w_3_4_0 w_2_3_t) (= v_3_4_0 v_2_3_t) (= u_3_4_0 u_2_3_t) (= tau_3_4_0 tau_2_3_t) (forall_t (>= u_3_4_t 0.300000)) (>= u_3_4_t 0.300000) (>= u_3_4_0 0.300000) (forall_t (>= v_3_4_t 0.000000)) (>= v_3_4_t 0.000000) (>= v_3_4_0 0.000000) (forall_t (>= w_3_4_t 0.000000)) (>= w_3_4_t 0.000000) (>= w_3_4_0 0.000000) (forall_t (>= s_3_4_t 0.000000)) (>= s_3_4_t 0.000000) (>= s_3_4_0 0.000000) (forall_t (<= tau_3_4_t 1.000000)) (<= tau_3_4_t 1.000000) (<= tau_3_4_0 1.000000) (>= tau_3_4_t 1.000000) (= s_4_5_0 s_3_4_t) (= w_4_5_0 w_3_4_t) (= v_4_5_0 v_3_4_t) (= u_4_5_0 u_3_4_t) (= tau_4_5_0 tau_3_4_t) (forall_t (>= u_4_5_t 0.300000)) (>= u_4_5_t 0.300000) (>= u_4_5_0 0.300000) (forall_t (>= v_4_5_t 0.000000)) (>= v_4_5_t 0.000000) (>= v_4_5_0 0.000000) (forall_t (>= w_4_5_t 0.000000)) (>= w_4_5_t 0.000000) (>= w_4_5_0 0.000000) (forall_t (>= s_4_5_t 0.000000)) (>= s_4_5_t 0.000000) (>= s_4_5_0 0.000000) (forall_t (>= tau_4_5_t 1.000000)) (>= tau_4_5_t 1.000000) (>= tau_4_5_0 1.000000) (<= u_4_5_t 0.300000) (= s_5_6_0 s_4_5_t) (= w_5_6_0 w_4_5_t) (= v_5_6_0 v_4_5_t) (= u_5_6_0 u_4_5_t) (= tau_5_6_0 tau_4_5_t) (forall_t (>= u_5_6_t 0.013000)) (>= u_5_6_t 0.013000) (>= u_5_6_0 0.013000) (forall_t (>= v_5_6_t 0.000000)) (>= v_5_6_t 0.000000) (>= v_5_6_0 0.000000) (forall_t (>= w_5_6_t 0.000000)) (>= w_5_6_t 0.000000) (>= w_5_6_0 0.000000) (forall_t (>= s_5_6_t 0.000000)) (>= s_5_6_t 0.000000) (>= s_5_6_0 0.000000) (forall_t (>= tau_5_6_t 1.000000)) (>= tau_5_6_t 1.000000) (>= tau_5_6_0 1.000000) (<= u_5_6_t 0.013000) (= s_6_7_0 s_5_6_t) (= w_6_7_0 w_5_6_t) (= v_6_7_0 v_5_6_t) (= u_6_7_0 u_5_6_t) (= tau_6_7_0 tau_5_6_t) (forall_t (>= u_6_7_t 0.006000)) (>= u_6_7_t 0.006000) (>= u_6_7_0 0.006000) (forall_t (>= v_6_7_t 0.000000)) (>= v_6_7_t 0.000000) (>= v_6_7_0 0.000000) (forall_t (>= w_6_7_t 0.000000)) (>= w_6_7_t 0.000000) (>= w_6_7_0 0.000000) (forall_t (>= s_6_7_t 0.000000)) (>= s_6_7_t 0.000000) (>= s_6_7_0 0.000000) (forall_t (>= tau_6_7_t 1.000000)) (>= tau_6_7_t 1.000000) (>= tau_6_7_0 1.000000) (<= u_6_7_t 0.006000) (= s_7_8_0 s_6_7_t) (= w_7_8_0 w_6_7_t) (= v_7_8_0 v_6_7_t) (= u_7_8_0 u_6_7_t) (= tau_7_8_0 tau_6_7_t) (forall_t (>= u_7_8_t 0.000000)) (>= u_7_8_t 0.000000) (>= u_7_8_0 0.000000) (forall_t (>= v_7_8_t 0.000000)) (>= v_7_8_t 0.000000) (>= v_7_8_0 0.000000) (forall_t (>= w_7_8_t 0.000000)) (>= w_7_8_t 0.000000) (>= w_7_8_0 0.000000) (forall_t (>= s_7_8_t 0.000000)) (>= s_7_8_t 0.000000) (>= s_7_8_0 0.000000) (forall_t (>= tau_7_8_t 1.000000)) (>= tau_7_8_t 1.000000) (>= tau_7_8_0 1.000000) (>= tau_7_8_t 500.000000) (= tau_7_8_t tau_7_8_t) (= s_8_1_0 s_7_8_t) (= w_8_1_0 w_7_8_t) (= v_8_1_0 v_7_8_t) (= u_8_1_0 u_7_8_t) (= tau_8_1_0 0.000000) (forall_t (>= u_8_1_t 0.000000)) (>= u_8_1_t 0.000000) (>= u_8_1_0 0.000000) (forall_t (<= u_8_1_t 0.006000)) (<= u_8_1_t 0.006000) (<= u_8_1_0 0.006000) (forall_t (>= v_8_1_t 0.000000)) (>= v_8_1_t 0.000000) (>= v_8_1_0 0.000000) (forall_t (>= w_8_1_t 0.000000)) (>= w_8_1_t 0.000000) (>= w_8_1_0 0.000000) (forall_t (>= s_8_1_t 0.000000)) (>= s_8_1_t 0.000000) (>= s_8_1_0 0.000000) (forall_t (<= tau_8_1_t 1.000000)) (<= tau_8_1_t 1.000000) (<= tau_8_1_0 1.000000) (>= u_8_1_t 0.006000) (= s_9_2_0 s_8_1_t) (= w_9_2_0 w_8_1_t) (= v_9_2_0 v_8_1_t) (= u_9_2_0 u_8_1_t) (= tau_9_2_0 tau_8_1_t) (forall_t (>= u_9_2_t 0.006000)) (>= u_9_2_t 0.006000) (>= u_9_2_0 0.006000) (forall_t (<= u_9_2_t 0.013000)) (<= u_9_2_t 0.013000) (<= u_9_2_0 0.013000) (forall_t (>= v_9_2_t 0.000000)) (>= v_9_2_t 0.000000) (>= v_9_2_0 0.000000) (forall_t (>= w_9_2_t 0.000000)) (>= w_9_2_t 0.000000) (>= w_9_2_0 0.000000) (forall_t (>= s_9_2_t 0.000000)) (>= s_9_2_t 0.000000) (>= s_9_2_0 0.000000) (forall_t (<= tau_9_2_t 1.000000)) (<= tau_9_2_t 1.000000) (<= tau_9_2_0 1.000000) (>= u_9_2_t 0.013000) (= s_10_3_0 s_9_2_t) (= w_10_3_0 w_9_2_t) (= v_10_3_0 v_9_2_t) (= u_10_3_0 u_9_2_t) (= tau_10_3_0 tau_9_2_t) (forall_t (>= u_10_3_t 0.013000)) (>= u_10_3_t 0.013000) (>= u_10_3_0 0.013000) (forall_t (<= u_10_3_t 0.300000)) (<= u_10_3_t 0.300000) (<= u_10_3_0 0.300000) (forall_t (>= v_10_3_t 0.000000)) (>= v_10_3_t 0.000000) (>= v_10_3_0 0.000000) (forall_t (>= w_10_3_t 0.000000)) (>= w_10_3_t 0.000000) (>= w_10_3_0 0.000000) (forall_t (>= s_10_3_t 0.000000)) (>= s_10_3_t 0.000000) (>= s_10_3_0 0.000000) (forall_t (<= tau_10_3_t 1.000000)) (<= tau_10_3_t 1.000000) (<= tau_10_3_0 1.000000) (>= u_10_3_t 0.300000) (= s_11_4_0 s_10_3_t) (= w_11_4_0 w_10_3_t) (= v_11_4_0 v_10_3_t) (= u_11_4_0 u_10_3_t) (= tau_11_4_0 tau_10_3_t) (forall_t (>= u_11_4_t 0.300000)) (>= u_11_4_t 0.300000) (>= u_11_4_0 0.300000) (forall_t (>= v_11_4_t 0.000000)) (>= v_11_4_t 0.000000) (>= v_11_4_0 0.000000) (forall_t (>= w_11_4_t 0.000000)) (>= w_11_4_t 0.000000) (>= w_11_4_0 0.000000) (forall_t (>= s_11_4_t 0.000000)) (>= s_11_4_t 0.000000) (>= s_11_4_0 0.000000) (forall_t (<= tau_11_4_t 1.000000)) (<= tau_11_4_t 1.000000) (<= tau_11_4_0 1.000000) (>= tau_11_4_t 1.000000) (= s_12_5_0 s_11_4_t) (= w_12_5_0 w_11_4_t) (= v_12_5_0 v_11_4_t) (= u_12_5_0 u_11_4_t) (= tau_12_5_0 tau_11_4_t) (forall_t (>= u_12_5_t 0.300000)) (>= u_12_5_t 0.300000) (>= u_12_5_0 0.300000) (forall_t (>= v_12_5_t 0.000000)) (>= v_12_5_t 0.000000) (>= v_12_5_0 0.000000) (forall_t (>= w_12_5_t 0.000000)) (>= w_12_5_t 0.000000) (>= w_12_5_0 0.000000) (forall_t (>= s_12_5_t 0.000000)) (>= s_12_5_t 0.000000) (>= s_12_5_0 0.000000) (forall_t (>= tau_12_5_t 1.000000)) (>= tau_12_5_t 1.000000) (>= tau_12_5_0 1.000000) (<= u_12_5_t 0.300000) (= s_13_6_0 s_12_5_t) (= w_13_6_0 w_12_5_t) (= v_13_6_0 v_12_5_t) (= u_13_6_0 u_12_5_t) (= tau_13_6_0 tau_12_5_t) (forall_t (>= u_13_6_t 0.013000)) (>= u_13_6_t 0.013000) (>= u_13_6_0 0.013000) (forall_t (>= v_13_6_t 0.000000)) (>= v_13_6_t 0.000000) (>= v_13_6_0 0.000000) (forall_t (>= w_13_6_t 0.000000)) (>= w_13_6_t 0.000000) (>= w_13_6_0 0.000000) (forall_t (>= s_13_6_t 0.000000)) (>= s_13_6_t 0.000000) (>= s_13_6_0 0.000000) (forall_t (>= tau_13_6_t 1.000000)) (>= tau_13_6_t 1.000000) (>= tau_13_6_0 1.000000) (<= u_13_6_t 0.013000) (= s_14_7_0 s_13_6_t) (= w_14_7_0 w_13_6_t) (= v_14_7_0 v_13_6_t) (= u_14_7_0 u_13_6_t) (= tau_14_7_0 tau_13_6_t) (forall_t (>= u_14_7_t 0.006000)) (>= u_14_7_t 0.006000) (>= u_14_7_0 0.006000) (forall_t (>= v_14_7_t 0.000000)) (>= v_14_7_t 0.000000) (>= v_14_7_0 0.000000) (forall_t (>= w_14_7_t 0.000000)) (>= w_14_7_t 0.000000) (>= w_14_7_0 0.000000) (forall_t (>= s_14_7_t 0.000000)) (>= s_14_7_t 0.000000) (>= s_14_7_0 0.000000) (forall_t (>= tau_14_7_t 1.000000)) (>= tau_14_7_t 1.000000) (>= tau_14_7_0 1.000000) (<= u_14_7_t 0.006000) (= s_15_8_0 s_14_7_t) (= w_15_8_0 w_14_7_t) (= v_15_8_0 v_14_7_t) (= u_15_8_0 u_14_7_t) (= tau_15_8_0 tau_14_7_t) (forall_t (>= u_15_8_t 0.000000)) (>= u_15_8_t 0.000000) (>= u_15_8_0 0.000000) (forall_t (>= v_15_8_t 0.000000)) (>= v_15_8_t 0.000000) (>= v_15_8_0 0.000000) (forall_t (>= w_15_8_t 0.000000)) (>= w_15_8_t 0.000000) (>= w_15_8_0 0.000000) (forall_t (>= s_15_8_t 0.000000)) (>= s_15_8_t 0.000000) (>= s_15_8_0 0.000000) (forall_t (>= tau_15_8_t 1.000000)) (>= tau_15_8_t 1.000000) (>= tau_15_8_0 1.000000) (>= tau_15_8_t 500.000000) (= tau_15_8_t tau_15_8_t) (= s_16_1_0 s_15_8_t) (= w_16_1_0 w_15_8_t) (= v_16_1_0 v_15_8_t) (= u_16_1_0 u_15_8_t) (= tau_16_1_0 0.000000) (forall_t (>= u_16_1_t 0.000000)) (>= u_16_1_t 0.000000) (>= u_16_1_0 0.000000) (forall_t (<= u_16_1_t 0.006000)) (<= u_16_1_t 0.006000) (<= u_16_1_0 0.006000) (forall_t (>= v_16_1_t 0.000000)) (>= v_16_1_t 0.000000) (>= v_16_1_0 0.000000) (forall_t (>= w_16_1_t 0.000000)) (>= w_16_1_t 0.000000) (>= w_16_1_0 0.000000) (forall_t (>= s_16_1_t 0.000000)) (>= s_16_1_t 0.000000) (>= s_16_1_0 0.000000) (forall_t (<= tau_16_1_t 1.000000)) (<= tau_16_1_t 1.000000) (<= tau_16_1_0 1.000000) (>= u_16_1_t 0.006000) (= s_17_2_0 s_16_1_t) (= w_17_2_0 w_16_1_t) (= v_17_2_0 v_16_1_t) (= u_17_2_0 u_16_1_t) (= tau_17_2_0 tau_16_1_t) (forall_t (>= u_17_2_t 0.006000)) (>= u_17_2_t 0.006000) (>= u_17_2_0 0.006000) (forall_t (<= u_17_2_t 0.013000)) (<= u_17_2_t 0.013000) (<= u_17_2_0 0.013000) (forall_t (>= v_17_2_t 0.000000)) (>= v_17_2_t 0.000000) (>= v_17_2_0 0.000000) (forall_t (>= w_17_2_t 0.000000)) (>= w_17_2_t 0.000000) (>= w_17_2_0 0.000000) (forall_t (>= s_17_2_t 0.000000)) (>= s_17_2_t 0.000000) (>= s_17_2_0 0.000000) (forall_t (<= tau_17_2_t 1.000000)) (<= tau_17_2_t 1.000000) (<= tau_17_2_0 1.000000) (>= u_17_2_t 0.013000) (= s_18_3_0 s_17_2_t) (= w_18_3_0 w_17_2_t) (= v_18_3_0 v_17_2_t) (= u_18_3_0 u_17_2_t) (= tau_18_3_0 tau_17_2_t) (forall_t (>= u_18_3_t 0.013000)) (>= u_18_3_t 0.013000) (>= u_18_3_0 0.013000) (forall_t (<= u_18_3_t 0.300000)) (<= u_18_3_t 0.300000) (<= u_18_3_0 0.300000) (forall_t (>= v_18_3_t 0.000000)) (>= v_18_3_t 0.000000) (>= v_18_3_0 0.000000) (forall_t (>= w_18_3_t 0.000000)) (>= w_18_3_t 0.000000) (>= w_18_3_0 0.000000) (forall_t (>= s_18_3_t 0.000000)) (>= s_18_3_t 0.000000) (>= s_18_3_0 0.000000) (forall_t (<= tau_18_3_t 1.000000)) (<= tau_18_3_t 1.000000) (<= tau_18_3_0 1.000000) (>= u_18_3_t 0.300000) (= s_19_4_0 s_18_3_t) (= w_19_4_0 w_18_3_t) (= v_19_4_0 v_18_3_t) (= u_19_4_0 u_18_3_t) (= tau_19_4_0 tau_18_3_t) (forall_t (>= u_19_4_t 0.300000)) (>= u_19_4_t 0.300000) (>= u_19_4_0 0.300000) (forall_t (>= v_19_4_t 0.000000)) (>= v_19_4_t 0.000000) (>= v_19_4_0 0.000000) (forall_t (>= w_19_4_t 0.000000)) (>= w_19_4_t 0.000000) (>= w_19_4_0 0.000000) (forall_t (>= s_19_4_t 0.000000)) (>= s_19_4_t 0.000000) (>= s_19_4_0 0.000000) (forall_t (<= tau_19_4_t 1.000000)) (<= tau_19_4_t 1.000000) (<= tau_19_4_0 1.000000) (>= tau_19_4_t 1.000000) (= s_20_5_0 s_19_4_t) (= w_20_5_0 w_19_4_t) (= v_20_5_0 v_19_4_t) (= u_20_5_0 u_19_4_t) (= tau_20_5_0 tau_19_4_t) (forall_t (>= u_20_5_t 0.300000)) (>= u_20_5_t 0.300000) (>= u_20_5_0 0.300000) (forall_t (>= v_20_5_t 0.000000)) (>= v_20_5_t 0.000000) (>= v_20_5_0 0.000000) (forall_t (>= w_20_5_t 0.000000)) (>= w_20_5_t 0.000000) (>= w_20_5_0 0.000000) (forall_t (>= s_20_5_t 0.000000)) (>= s_20_5_t 0.000000) (>= s_20_5_0 0.000000) (forall_t (>= tau_20_5_t 1.000000)) (>= tau_20_5_t 1.000000) (>= tau_20_5_0 1.000000) (<= u_20_5_t 0.300000) (= s_21_6_0 s_20_5_t) (= w_21_6_0 w_20_5_t) (= v_21_6_0 v_20_5_t) (= u_21_6_0 u_20_5_t) (= tau_21_6_0 tau_20_5_t) (forall_t (>= u_21_6_t 0.013000)) (>= u_21_6_t 0.013000) (>= u_21_6_0 0.013000) (forall_t (>= v_21_6_t 0.000000)) (>= v_21_6_t 0.000000) (>= v_21_6_0 0.000000) (forall_t (>= w_21_6_t 0.000000)) (>= w_21_6_t 0.000000) (>= w_21_6_0 0.000000) (forall_t (>= s_21_6_t 0.000000)) (>= s_21_6_t 0.000000) (>= s_21_6_0 0.000000) (forall_t (>= tau_21_6_t 1.000000)) (>= tau_21_6_t 1.000000) (>= tau_21_6_0 1.000000) (<= u_21_6_t 0.013000) (= s_22_7_0 s_21_6_t) (= w_22_7_0 w_21_6_t) (= v_22_7_0 v_21_6_t) (= u_22_7_0 u_21_6_t) (= tau_22_7_0 tau_21_6_t) (forall_t (>= u_22_7_t 0.006000)) (>= u_22_7_t 0.006000) (>= u_22_7_0 0.006000) (forall_t (>= v_22_7_t 0.000000)) (>= v_22_7_t 0.000000) (>= v_22_7_0 0.000000) (forall_t (>= w_22_7_t 0.000000)) (>= w_22_7_t 0.000000) (>= w_22_7_0 0.000000) (forall_t (>= s_22_7_t 0.000000)) (>= s_22_7_t 0.000000) (>= s_22_7_0 0.000000) (forall_t (>= tau_22_7_t 1.000000)) (>= tau_22_7_t 1.000000) (>= tau_22_7_0 1.000000) (<= u_22_7_t 0.006000) (= s_23_8_0 s_22_7_t) (= w_23_8_0 w_22_7_t) (= v_23_8_0 v_22_7_t) (= u_23_8_0 u_22_7_t) (= tau_23_8_0 tau_22_7_t) (forall_t (>= u_23_8_t 0.000000)) (>= u_23_8_t 0.000000) (>= u_23_8_0 0.000000) (forall_t (>= v_23_8_t 0.000000)) (>= v_23_8_t 0.000000) (>= v_23_8_0 0.000000) (forall_t (>= w_23_8_t 0.000000)) (>= w_23_8_t 0.000000) (>= w_23_8_0 0.000000) (forall_t (>= s_23_8_t 0.000000)) (>= s_23_8_t 0.000000) (>= s_23_8_0 0.000000) (forall_t (>= tau_23_8_t 1.000000)) (>= tau_23_8_t 1.000000) (>= tau_23_8_0 1.000000) (>= s_23_8_t 0.000000) (>= w_23_8_t 0.000000) (>= v_23_8_t 0.000000) (>= u_23_8_t 0.000000) (= tau_23_8_t 499.000000)))
(check-sat)
(exit)