path: root/test/regress/regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smtv1.smt2

(set-option :incremental false)
(set-info :source "Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com)")
(set-info :status unsat)
(set-info :category "industrial")
(set-info :difficulty "0")
(set-logic QF_LRA)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Real)
(declare-fun x_13 () Real)
(declare-fun x_14 () Real)
(declare-fun x_15 () Real)
(declare-fun x_16 () Real)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Real)
(declare-fun x_23 () Real)
(declare-fun x_24 () Real)
(declare-fun x_25 () Real)
(declare-fun x_26 () Real)
(declare-fun x_27 () Real)
(declare-fun x_28 () Real)
(declare-fun x_29 () Real)
(declare-fun x_30 () Real)
(declare-fun x_31 () Real)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(declare-fun x_38 () Real)
(declare-fun x_39 () Real)
(declare-fun x_40 () Real)
(declare-fun x_41 () Real)
(declare-fun x_42 () Real)
(declare-fun x_43 () Real)
(declare-fun x_44 () Real)
(declare-fun x_45 () Real)
(declare-fun x_46 () Real)
(declare-fun x_47 () Real)
(declare-fun x_48 () Real)
(declare-fun x_49 () Real)
(declare-fun x_50 () Real)
(declare-fun x_51 () Real)
(declare-fun x_52 () Real)
(declare-fun x_53 () Real)
(declare-fun x_54 () Real)
(declare-fun x_55 () Real)
(declare-fun x_56 () Real)
(declare-fun x_57 () Real)
(declare-fun x_58 () Real)
(declare-fun x_59 () Real)
(declare-fun x_60 () Real)
(declare-fun x_61 () Real)
(declare-fun x_62 () Real)
(declare-fun x_63 () Real)
(declare-fun x_64 () Real)
(declare-fun x_65 () Real)
(declare-fun x_66 () Real)
(declare-fun x_67 () Real)
(declare-fun x_68 () Real)
(declare-fun x_69 () Real)
(declare-fun x_70 () Real)
(declare-fun x_71 () Real)
(declare-fun x_72 () Real)
(declare-fun x_73 () Real)
(declare-fun x_74 () Real)
(declare-fun x_75 () Real)
(declare-fun x_76 () Real)
(declare-fun x_77 () Real)
(declare-fun x_78 () Real)
(declare-fun x_79 () Real)
(declare-fun x_80 () Real)
(declare-fun x_81 () Real)
(declare-fun x_82 () Real)
(declare-fun x_83 () Real)
(declare-fun x_84 () Real)
(assert (= x_76 1.0))
(assert (= x_76 1.0))
(assert (= x_0 0.0))
(assert (= x_0 0.0))
(assert (not (<= x_6 0.0)))
(assert (not (<= x_7 0.0)))
(assert (= x_70 1.0))
(assert (= x_70 1.0))
(assert (= x_75 1.0))
(assert (= x_75 1.0))
(assert (= x_69 1.0))
(assert (= x_69 1.0))
(assert (= x_74 1.0))
(assert (= x_74 1.0))
(assert (= x_68 1.0))
(assert (= x_68 1.0))
(assert (= x_38 1.0))
(assert (= x_38 1.0))
(assert (not (<= x_44 0.0)))
(assert (= x_73 1.0))
(assert (= x_73 1.0))
(assert (= x_67 1.0))
(assert (= x_67 1.0))
(assert (= x_72 1.0))
(assert (= x_72 1.0))
(assert (= x_66 1.0))
(assert (= x_66 1.0))
(assert (= x_65 1.0))
(assert (= x_65 1.0))
(assert (= x_60 1.0))
(assert (= x_60 1.0))
(assert (= x_64 1.0))
(assert (= x_64 1.0))
(assert (= x_55 1.0))
(assert (= x_55 1.0))
(assert (= x_63 1.0))
(assert (= x_63 1.0))
(assert (= x_36 1.0))
(assert (= x_36 1.0))
(assert (= x_50 1.0))
(assert (= x_50 1.0))
(assert (= x_62 1.0))
(assert (= x_62 1.0))
(assert (= x_35 1.0))
(assert (= x_35 1.0))
(assert (= x_61 1.0))
(assert (= x_61 1.0))
(assert (= x_34 1.0))
(assert (= x_34 1.0))
(assert (= x_59 1.0))
(assert (= x_59 1.0))
(assert (= x_40 1.0))
(assert (= x_40 1.0))
(assert (= x_54 1.0))
(assert (= x_54 1.0))
(assert (not (<= x_84 0.0)))
(assert (= x_58 1.0))
(assert (= x_58 1.0))
(assert (= x_49 1.0))
(assert (= x_49 1.0))
(assert (= x_57 1.0))
(assert (= x_57 1.0))
(assert (= x_56 1.0))
(assert (= x_56 1.0))
(assert (>= x_82 0.0))
(assert (= x_53 1.0))
(assert (= x_53 1.0))
(assert (= x_48 1.0))
(assert (= x_48 1.0))
(assert (= x_52 1.0))
(assert (= x_52 1.0))
(assert (= x_51 1.0))
(assert (= x_51 1.0))
(assert (= x_47 1.0))
(assert (= x_47 1.0))
(assert (= x_46 1.0))
(assert (= x_46 1.0))
(assert (= x_14 0.0))
(assert (= x_14 0.0))
(assert (= x_28 0.0))
(assert (= x_28 0.0))
(assert (= x_25 0.0))
(assert (= x_25 0.0))
(assert (= x_22 0.0))
(assert (= x_22 0.0))
(assert (= x_19 0.0))
(assert (= x_19 0.0))
(assert (= x_15 0.0))
(assert (= x_15 0.0))
(assert (= x_27 0.0))
(assert (= x_27 0.0))
(assert (= x_24 0.0))
(assert (= x_24 0.0))
(assert (= x_21 0.0))
(assert (= x_21 0.0))
(assert (= x_18 0.0))
(assert (= x_18 0.0))
(assert (= x_16 0.0))
(assert (= x_16 0.0))
(assert (= x_26 0.0))
(assert (= x_26 0.0))
(assert (= x_23 0.0))
(assert (= x_23 0.0))
(assert (= x_20 0.0))
(assert (= x_20 0.0))
(assert (= x_17 0.0))
(assert (= x_17 0.0))
(assert (= x_33 0.0))
(assert (= x_33 0.0))
(assert (= x_32 0.0))
(assert (= x_32 0.0))
(assert (= x_31 0.0))
(assert (= x_31 0.0))
(assert (= x_30 0.0))
(assert (= x_30 0.0))
(assert (= x_29 0.0))
(assert (= x_29 0.0))
(assert (<= (+ x_13 (* (/ (- 1) 1) x_73) (* (/ (- 1) 1) x_83)) 0.0))
(assert (<= (+ x_13 (* (/ (- 1) 1) x_72) (* (/ (- 1) 1) x_83)) 0.0))
(assert (<= (+ x_13 (* (/ (- 1) 1) x_74) (* (/ (- 1) 1) x_83)) 0.0))
(assert (<= (+ x_13 (* (/ (- 1) 1) x_75) (* (/ (- 1) 1) x_83)) 0.0))
(assert (<= (+ x_13 (* (/ (- 1) 1) x_76) (* (/ (- 1) 1) x_83)) 0.0))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_72) (* (/ (- 1) 1) x_84)) 0.0))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_73) (* (/ (- 1) 1) x_84)) 0.0))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_74) (* (/ (- 1) 1) x_84)) 0.0))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_75) (* (/ (- 1) 1) x_84)) 0.0))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_76) (* (/ (- 1) 1) x_84)) 0.0))
(assert (>= (+ x_72 (* (/ (- 1) 1) x_73) x_82) 0.0))
(assert (>= (+ x_72 (* (/ (- 1) 1) x_74) x_82) 0.0))
(assert (>= (+ x_72 (* (/ (- 1) 1) x_75) x_82) 0.0))
(assert (>= (+ x_72 (* (/ (- 1) 1) x_76) x_82) 0.0))
(assert (<= (+ x_72 (* (/ (- 1) 1) x_73) (* (/ (- 1) 1) x_82)) 0.0))
(assert (>= (+ x_73 (* (/ (- 1) 1) x_74) x_82) 0.0))
(assert (>= (+ x_73 (* (/ (- 1) 1) x_75) x_82) 0.0))
(assert (>= (+ x_73 (* (/ (- 1) 1) x_76) x_82) 0.0))
(assert (<= (+ x_72 (* (/ (- 1) 1) x_74) (* (/ (- 1) 1) x_82)) 0.0))
(assert (<= (+ x_73 (* (/ (- 1) 1) x_74) (* (/ (- 1) 1) x_82)) 0.0))
(assert (>= (+ x_74 (* (/ (- 1) 1) x_75) x_82) 0.0))
(assert (>= (+ x_74 (* (/ (- 1) 1) x_76) x_82) 0.0))
(assert (<= (+ x_72 (* (/ (- 1) 1) x_75) (* (/ (- 1) 1) x_82)) 0.0))
(assert (<= (+ x_73 (* (/ (- 1) 1) x_75) (* (/ (- 1) 1) x_82)) 0.0))
(assert (<= (+ x_74 (* (/ (- 1) 1) x_75) (* (/ (- 1) 1) x_82)) 0.0))
(assert (>= (+ x_75 (* (/ (- 1) 1) x_76) x_82) 0.0))
(assert (<= (+ x_72 (* (/ (- 1) 1) x_76) (* (/ (- 1) 1) x_82)) 0.0))
(assert (<= (+ x_73 (* (/ (- 1) 1) x_76) (* (/ (- 1) 1) x_82)) 0.0))
(assert (<= (+ x_74 (* (/ (- 1) 1) x_76) (* (/ (- 1) 1) x_82)) 0.0))
(assert (>= (+ x_7 x_13 (* (/ (- 1) 1) x_40)) 0.0))
(assert (<= (+ x_75 (* (/ (- 1) 1) x_76) (* (/ (- 1) 1) x_82)) 0.0))
(assert (>= (+ x_7 x_13 (* (/ (- 1) 1) x_34)) 0.0))
(assert (>= (+ x_9 (* (/ (- 1) 1) x_13)) 0.0))
(assert (<= (+ x_9 (* (/ (- 1) 1) x_13)) 0.0))
(assert (>= (+ x_7 x_13 (* (/ (- 1) 1) x_35)) 0.0))
(assert (>= (+ x_7 x_13 (* (/ (- 1) 1) x_36)) 0.0))
(assert (>= (+ x_11 (* (/ (- 1) 1) x_13)) 0.0))
(assert (<= (+ x_11 (* (/ (- 1) 1) x_13)) 0.0))
(assert (>= (+ x_7 x_13 (* (/ (- 1) 1) x_38)) 0.0))
(assert (let ((_let_0 (/ 1001 1000))) (<= (+ x_39 (* (- _let_0) x_40) (* _let_0 x_72) (* (/ (- 1) 1) x_77)) 0.0)))
(assert (let ((_let_0 (/ 999 1000))) (>= (+ x_39 (* (- _let_0) x_40) (* _let_0 x_72) (* (/ (- 1) 1) x_77)) 0.0)))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_34 (* (- _let_0) x_41) (* (/ (- 1) 1) x_73) (* _let_0 x_78)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (<= (+ x_34 (* (- _let_0) x_41) (* (/ (- 1) 1) x_73) (* _let_0 x_78)) 0.0)))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_35 (* (- _let_0) x_42) (* (/ (- 1) 1) x_74) (* _let_0 x_79)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (<= (+ x_35 (* (- _let_0) x_42) (* (/ (- 1) 1) x_74) (* _let_0 x_79)) 0.0)))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_36 (* (- _let_0) x_43) (* (/ (- 1) 1) x_75) (* _let_0 x_80)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (<= (+ x_36 (* (- _let_0) x_43) (* (/ (- 1) 1) x_75) (* _let_0 x_80)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (>= (+ x_13 (* (- _let_0) x_19) (* _let_0 x_39) (* (/ (- 1) 1) x_40)) 0.0)))
(assert (<= (+ x_19 (* (/ (- 1) 1) x_45)) 0.0))
(assert (let ((_let_0 (/ 1001 1000))) (<= (+ x_37 (* (- _let_0) x_38) (* _let_0 x_76) (* (/ (- 1) 1) x_81)) 0.0)))
(assert (let ((_let_0 (/ 999 1000))) (>= (+ x_37 (* (- _let_0) x_38) (* _let_0 x_76) (* (/ (- 1) 1) x_81)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (>= (+ x_13 (* (- _let_0) x_22) (* (/ (- 1) 1) x_34) (* _let_0 x_41)) 0.0)))
(assert (<= (+ x_22 (* (/ (- 1) 1) x_45)) 0.0))
(assert (let ((_let_0 (/ 1000 1001))) (not (<= (+ x_13 (* (- _let_0) x_19) (* _let_0 x_39) (* (/ (- 1) 1) x_40)) 0.0))))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_40)) 0.0))
(assert (let ((_let_0 (/ 1000 999))) (>= (+ x_13 (* (- _let_0) x_25) (* (/ (- 1) 1) x_35) (* _let_0 x_42)) 0.0)))
(assert (<= (+ x_25 (* (/ (- 1) 1) x_45)) 0.0))
(assert (let ((_let_0 (/ 1000 1001))) (not (<= (+ x_13 (* (- _let_0) x_22) (* (/ (- 1) 1) x_34) (* _let_0 x_41)) 0.0))))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_34)) 0.0))
(assert (let ((_let_0 (/ 1000 999))) (>= (+ x_13 (* (- _let_0) x_28) (* (/ (- 1) 1) x_36) (* _let_0 x_43)) 0.0)))
(assert (<= (+ x_28 (* (/ (- 1) 1) x_45)) 0.0))
(assert (let ((_let_0 (/ 1000 1001))) (not (<= (+ x_13 (* (- _let_0) x_25) (* (/ (- 1) 1) x_35) (* _let_0 x_42)) 0.0))))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_35)) 0.0))
(assert (let ((_let_0 (/ 1000 999))) (>= (+ x_13 (* (- _let_0) x_14) (* _let_0 x_37) (* (/ (- 1) 1) x_38)) 0.0)))
(assert (<= (+ x_14 (* (/ (- 1) 1) x_45)) 0.0))
(assert (let ((_let_0 (/ 1000 1001))) (not (<= (+ x_13 (* (- _let_0) x_28) (* (/ (- 1) 1) x_36) (* _let_0 x_43)) 0.0))))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_36)) 0.0))
(assert (let ((_let_0 (/ 1000 1001))) (not (<= (+ x_13 (* (- _let_0) x_14) (* _let_0 x_37) (* (/ (- 1) 1) x_38)) 0.0))))
(assert (>= (+ x_13 (* (/ (- 1) 1) x_38)) 0.0))
(assert (let ((_let_0 (- (/ 1001 1000)))) (let ((_let_1 (/ 1001 2000))) (let ((_let_2 (- (/ 1 2)))) (<= (+ x_19 (* _let_0 x_29) (* _let_0 x_44) (* _let_1 x_72) (* _let_1 x_76) (* _let_2 x_77) (* _let_2 x_81)) _let_1)))))
(assert (let ((_let_0 (/ 999 1000))) (let ((_let_1 (- (/ 1 2)))) (let ((_let_2 (/ 999 2000))) (>= (+ x_19 (* (- _let_0) x_29) (* _let_0 x_44) (* _let_2 x_72) (* _let_2 x_76) (* _let_1 x_77) (* _let_1 x_81)) (- (/ 3001 2000)))))))
(assert (let ((_let_0 (- (/ 1001 1000)))) (let ((_let_1 (/ 1001 2000))) (let ((_let_2 (- (/ 1 2)))) (<= (+ x_22 (* _let_0 x_30) (* _let_0 x_44) (* _let_1 x_72) (* _let_1 x_76) (* _let_2 x_77) (* _let_2 x_81)) _let_1)))))
(assert (let ((_let_0 (/ 999 1000))) (let ((_let_1 (- (/ 1 2)))) (let ((_let_2 (/ 999 2000))) (>= (+ x_22 (* (- _let_0) x_30) (* _let_0 x_44) (* _let_2 x_72) (* _let_2 x_76) (* _let_1 x_77) (* _let_1 x_81)) (- (/ 3001 2000)))))))
(assert (let ((_let_0 (- (/ 1001 1000)))) (let ((_let_1 (/ 1001 2000))) (let ((_let_2 (- (/ 1 2)))) (<= (+ x_25 (* _let_0 x_31) (* _let_0 x_44) (* _let_1 x_72) (* _let_1 x_76) (* _let_2 x_77) (* _let_2 x_81)) _let_1)))))
(assert (let ((_let_0 (/ 999 1000))) (let ((_let_1 (- (/ 1 2)))) (let ((_let_2 (/ 999 2000))) (>= (+ x_25 (* (- _let_0) x_31) (* _let_0 x_44) (* _let_2 x_72) (* _let_2 x_76) (* _let_1 x_77) (* _let_1 x_81)) (- (/ 3001 2000)))))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_21)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_21)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_22)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_22)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_18)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_18)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_19)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_19)) 0.0))
(assert (let ((_let_0 (- (/ 1001 1000)))) (let ((_let_1 (/ 1001 2000))) (let ((_let_2 (- (/ 1 2)))) (<= (+ x_28 (* _let_0 x_32) (* _let_0 x_44) (* _let_1 x_72) (* _let_1 x_76) (* _let_2 x_77) (* _let_2 x_81)) _let_1)))))
(assert (let ((_let_0 (/ 999 1000))) (let ((_let_1 (- (/ 1 2)))) (let ((_let_2 (/ 999 2000))) (>= (+ x_28 (* (- _let_0) x_32) (* _let_0 x_44) (* _let_2 x_72) (* _let_2 x_76) (* _let_1 x_77) (* _let_1 x_81)) (- (/ 3001 2000)))))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_24)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_24)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_25)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_25)) 0.0))
(assert (>= (+ x_20 (* (/ (- 1) 1) x_34)) (/ (- 1) 1)))
(assert (<= (+ x_20 (* (/ (- 1) 1) x_34)) (/ (- 1) 1)))
(assert (= (+ x_6 (* (/ (- 1) 1) x_9)) 0.0))
(assert (= (+ x_6 (* (/ (- 1) 1) x_9)) 0.0))
(assert (>= (+ x_17 (* (/ (- 1) 1) x_40)) (/ (- 1) 1)))
(assert (<= (+ x_17 (* (/ (- 1) 1) x_40)) (/ (- 1) 1)))
(assert (= (+ x_6 (* (/ (- 1) 1) x_8)) 0.0))
(assert (= (+ x_6 (* (/ (- 1) 1) x_8)) 0.0))
(assert (let ((_let_0 (- (/ 1001 1000)))) (let ((_let_1 (/ 1001 2000))) (let ((_let_2 (- (/ 1 2)))) (<= (+ x_14 (* _let_0 x_33) (* _let_0 x_44) (* _let_1 x_72) (* _let_1 x_76) (* _let_2 x_77) (* _let_2 x_81)) _let_1)))))
(assert (let ((_let_0 (/ 999 1000))) (let ((_let_1 (- (/ 1 2)))) (let ((_let_2 (/ 999 2000))) (>= (+ x_14 (* (- _let_0) x_33) (* _let_0 x_44) (* _let_2 x_72) (* _let_2 x_76) (* _let_1 x_77) (* _let_1 x_81)) (- (/ 3001 2000)))))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_27)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_27)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_28)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_28)) 0.0))
(assert (>= (+ x_23 (* (/ (- 1) 1) x_35)) (/ (- 1) 1)))
(assert (<= (+ x_23 (* (/ (- 1) 1) x_35)) (/ (- 1) 1)))
(assert (= (+ x_6 (* (/ (- 1) 1) x_10)) 0.0))
(assert (= (+ x_6 (* (/ (- 1) 1) x_10)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_41)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_41)) (- (/ 999 1000))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_2)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_2)) (- (/ 999 1000))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_39)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_39)) (- (/ 999 1000))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_1)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_1)) (- (/ 999 1000))))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_13 (* (- _let_0) x_19) (* (/ (- 1) 1) x_72) (* _let_0 x_77)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_13 (* (- _let_0) x_19) (* (/ (- 1) 1) x_72) (* _let_0 x_77)) 0.0))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_15)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_15)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_14)) 0.0))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_14)) 0.0))
(assert (>= (+ x_26 (* (/ (- 1) 1) x_36)) (/ (- 1) 1)))
(assert (<= (+ x_26 (* (/ (- 1) 1) x_36)) (/ (- 1) 1)))
(assert (= (+ x_6 (* (/ (- 1) 1) x_11)) 0.0))
(assert (= (+ x_6 (* (/ (- 1) 1) x_11)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_42)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_42)) (- (/ 999 1000))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_3)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_3)) (- (/ 999 1000))))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_13 (* (- _let_0) x_22) (* (/ (- 1) 1) x_73) (* _let_0 x_78)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_13 (* (- _let_0) x_22) (* (/ (- 1) 1) x_73) (* _let_0 x_78)) 0.0))))
(assert (>= (+ x_16 (* (/ (- 1) 1) x_38)) (/ (- 1) 1)))
(assert (<= (+ x_16 (* (/ (- 1) 1) x_38)) (/ (- 1) 1)))
(assert (= (+ x_6 (* (/ (- 1) 1) x_12)) 0.0))
(assert (= (+ x_6 (* (/ (- 1) 1) x_12)) 0.0))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_43)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_43)) (- (/ 999 1000))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_4)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_4)) (- (/ 999 1000))))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_13 (* (- _let_0) x_25) (* (/ (- 1) 1) x_74) (* _let_0 x_79)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_13 (* (- _let_0) x_25) (* (/ (- 1) 1) x_74) (* _let_0 x_79)) 0.0))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_37)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_37)) (- (/ 999 1000))))
(assert (>= (+ x_0 (* (/ (- 1) 1) x_5)) (- (/ 1001 1000))))
(assert (<= (+ x_0 (* (/ (- 1) 1) x_5)) (- (/ 999 1000))))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_13 (* (- _let_0) x_28) (* (/ (- 1) 1) x_75) (* _let_0 x_80)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_13 (* (- _let_0) x_28) (* (/ (- 1) 1) x_75) (* _let_0 x_80)) 0.0))))
(assert (= (+ x_1 (* (/ (- 1) 1) x_39)) 0.0))
(assert (= (+ x_1 (* (/ (- 1) 1) x_39)) 0.0))
(assert (= (+ x_2 (* (/ (- 1) 1) x_41)) 0.0))
(assert (= (+ x_2 (* (/ (- 1) 1) x_41)) 0.0))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_13 (* (- _let_0) x_14) (* (/ (- 1) 1) x_76) (* _let_0 x_81)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_13 (* (- _let_0) x_14) (* (/ (- 1) 1) x_76) (* _let_0 x_81)) 0.0))))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_7 (* (- _let_0) x_18) (* _let_0 x_19)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_7 (* (- _let_0) x_18) (* _let_0 x_19)) 0.0))))
(assert (= (+ x_3 (* (/ (- 1) 1) x_42)) 0.0))
(assert (= (+ x_3 (* (/ (- 1) 1) x_42)) 0.0))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_7 (* (- _let_0) x_21) (* _let_0 x_22)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_7 (* (- _let_0) x_21) (* _let_0 x_22)) 0.0))))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_7 (* (- _let_0) x_24) (* _let_0 x_25)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_7 (* (- _let_0) x_24) (* _let_0 x_25)) 0.0))))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_7 (* (- _let_0) x_27) (* _let_0 x_28)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_7 (* (- _let_0) x_27) (* _let_0 x_28)) 0.0))))
(assert (let ((_let_0 (/ 1000 1001))) (>= (+ x_7 (* _let_0 x_14) (* (- _let_0) x_15)) 0.0)))
(assert (let ((_let_0 (/ 1000 999))) (not (<= (+ x_7 (* _let_0 x_14) (* (- _let_0) x_15)) 0.0))))
(assert (<= (+ x_0 x_6 (* (/ (- 1) 1) x_83)) 1.0))
(assert (= (+ x_4 (* (/ (- 1) 1) x_43)) 0.0))
(assert (= (+ x_4 (* (/ (- 1) 1) x_43)) 0.0))
(assert (not (>= (+ x_0 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (not (<= (+ x_1 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (not (<= (+ x_2 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (>= (+ x_0 x_6 (* (/ (- 1) 1) x_84)) 1.0))
(assert (not (<= (+ x_3 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (= (+ x_4 (* (/ (- 1) 1) x_45)) 0.0))
(assert (= (+ x_4 (* (/ (- 1) 1) x_45)) 0.0))
(assert (= (+ x_5 (* (/ (- 1) 1) x_37)) 0.0))
(assert (= (+ x_5 (* (/ (- 1) 1) x_37)) 0.0))
(assert (>= (+ x_5 (* (/ (- 1) 1) x_45)) 0.0))
(assert (<= (+ x_40 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_46)) 0.0))
(assert (<= (+ x_40 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_51)) 0.0))
(assert (<= (+ x_40 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_56)) 0.0))
(assert (<= (+ x_40 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_61)) 0.0))
(assert (<= (+ x_40 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_66)) 0.0))
(assert (<= (+ x_34 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_47)) 0.0))
(assert (<= (+ x_34 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_52)) 0.0))
(assert (<= (+ x_34 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_57)) 0.0))
(assert (<= (+ x_34 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_62)) 0.0))
(assert (<= (+ x_34 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_67)) 0.0))
(assert (<= (+ x_35 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_48)) 0.0))
(assert (<= (+ x_35 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_53)) 0.0))
(assert (<= (+ x_35 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_58)) 0.0))
(assert (<= (+ x_35 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_63)) 0.0))
(assert (<= (+ x_35 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_68)) 0.0))
(assert (>= (+ x_0 x_6 x_7) 1.0))
(assert (<= (+ x_36 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_49)) 0.0))
(assert (<= (+ x_36 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_54)) 0.0))
(assert (<= (+ x_36 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_59)) 0.0))
(assert (<= (+ x_36 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_64)) 0.0))
(assert (<= (+ x_36 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_69)) 0.0))
(assert (<= (+ x_38 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_50)) 0.0))
(assert (<= (+ x_38 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_55)) 0.0))
(assert (<= (+ x_38 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_60)) 0.0))
(assert (<= (+ x_38 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_65)) 0.0))
(assert (<= (+ x_38 (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_70)) 0.0))
(assert (not (<= (+ x_0 (* (/ 1000 999) x_1) x_6) 1.0)))
(assert (>= (+ x_40 x_44 (* (/ (- 1) 1) x_46)) 0.0))
(assert (not (<= (+ x_0 (* (/ 1000 999) x_2) x_6) 1.0)))
(assert (not (<= (+ x_0 (* (/ 1000 1001) x_1) x_6) 1.0)))
(assert (>= (+ x_0 x_6) 1.0))
(assert (>= (+ x_40 x_44 (* (/ (- 1) 1) x_51)) 0.0))
(assert (not (<= (+ x_0 (* (/ 1000 999) x_3) x_6) 1.0)))
(assert (not (<= (+ x_0 (* (/ 1000 1001) x_2) x_6) 1.0)))
(assert (>= (+ x_40 x_44 (* (/ (- 1) 1) x_56)) 0.0))
(assert (not (<= (+ x_0 (* (/ 1000 999) x_4) x_6) 1.0)))
(assert (not (<= (+ x_0 (* (/ 1000 1001) x_3) x_6) 1.0)))
(assert (>= (+ x_40 x_44 (* (/ (- 1) 1) x_61)) 0.0))
(assert (not (<= (+ x_0 (* (/ 1000 999) x_5) x_6) 1.0)))
(assert (not (<= (+ x_0 (* (/ 1000 1001) x_4) x_6) 1.0)))
(assert (>= (+ x_40 x_44 (* (/ (- 1) 1) x_66)) 0.0))
(assert (not (<= (+ x_0 (* (/ 1000 1001) x_5) x_6) 1.0)))
(assert (>= (+ x_34 x_44 (* (/ (- 1) 1) x_47)) 0.0))
(assert (>= (+ x_1 x_5 (* (/ 1001 500) x_44)) (/ 1001 1000)))
(assert (<= (+ x_1 x_5 (* (- (/ 999 500)) x_44)) (/ 4999 1000)))
(assert (>= (+ x_34 x_44 (* (/ (- 1) 1) x_52)) 0.0))
(assert (>= (+ x_34 x_44 (* (/ (- 1) 1) x_57)) 0.0))
(assert (>= (+ x_34 x_44 (* (/ (- 1) 1) x_62)) 0.0))
(assert (>= (+ x_34 x_44 (* (/ (- 1) 1) x_67)) 0.0))
(assert (let ((_let_0 (/ 1998 1001))) (<= (+ x_7 (* _let_0 x_44) (* (- _let_0) x_82)) (/ (- 2) 1))))
(assert (>= (+ x_0 x_6 (* (/ (- 1) 1) x_9)) 0.0))
(assert (>= (+ x_0 x_6 (* (/ (- 1) 1) x_8)) 0.0))
(assert (>= (+ x_35 x_44 (* (/ (- 1) 1) x_48)) 0.0))
(assert (>= (+ x_0 x_6 (* (/ (- 1) 1) x_10)) 0.0))
(assert (>= (+ x_35 x_44 (* (/ (- 1) 1) x_53)) 0.0))
(assert (<= (+ x_6 x_44 x_82 (* (- (/ 999 1001)) x_83)) (- (/ 1501 1000))))
(assert (not (<= (+ x_7 (* (/ (- 1) 1) x_82) (* (- (/ 2 999)) x_83)) (/ 1001 999))))
(assert (>= (+ x_0 x_6 (* (/ (- 1) 1) x_11)) 0.0))
(assert (>= (+ x_35 x_44 (* (/ (- 1) 1) x_58)) 0.0))
(assert (>= (+ x_0 x_6 (* (/ (- 1) 1) x_12)) 0.0))
(assert (>= (+ x_35 x_44 (* (/ (- 1) 1) x_63)) 0.0))
(assert (>= (+ x_35 x_44 (* (/ (- 1) 1) x_68)) 0.0))
(assert (= (+ x_0 x_6 (* (/ (- 1) 1) x_13)) 0.0))
(assert (= (+ x_0 x_6 (* (/ (- 1) 1) x_13)) 0.0))
(assert (>= (+ x_36 x_44 (* (/ (- 1) 1) x_49)) 0.0))
(assert (>= (+ x_6 (* (- (/ 1001 999)) x_7) (* (/ (- 1) 1) x_44) (* (/ (- 1) 1) x_84)) (/ 5003 1998)))
(assert (= (+ x_0 (* (/ (- 1) 1) x_71)) 0.0))
(assert (= (+ x_0 (* (/ (- 1) 1) x_71)) 0.0))
(assert (= (+ x_40 (* (/ (- 1) 1) x_72)) 0.0))
(assert (= (+ x_40 (* (/ (- 1) 1) x_72)) 0.0))
(assert (>= (+ x_36 x_44 (* (/ (- 1) 1) x_54)) 0.0))
(assert (= (+ x_1 (* (/ (- 1) 1) x_77)) 0.0))
(assert (= (+ x_1 (* (/ (- 1) 1) x_77)) 0.0))
(assert (= (+ x_34 (* (/ (- 1) 1) x_73)) 0.0))
(assert (= (+ x_34 (* (/ (- 1) 1) x_73)) 0.0))
(assert (>= (+ x_36 x_44 (* (/ (- 1) 1) x_59)) 0.0))
(assert (= (+ x_2 (* (/ (- 1) 1) x_78)) 0.0))
(assert (= (+ x_2 (* (/ (- 1) 1) x_78)) 0.0))
(assert (= (+ x_35 (* (/ (- 1) 1) x_74)) 0.0))
(assert (= (+ x_35 (* (/ (- 1) 1) x_74)) 0.0))
(assert (>= (+ x_36 x_44 (* (/ (- 1) 1) x_64)) 0.0))
(assert (= (+ x_3 (* (/ (- 1) 1) x_79)) 0.0))
(assert (= (+ x_3 (* (/ (- 1) 1) x_79)) 0.0))
(assert (= (+ x_36 (* (/ (- 1) 1) x_75)) 0.0))
(assert (= (+ x_36 (* (/ (- 1) 1) x_75)) 0.0))
(assert (>= (+ x_36 x_44 (* (/ (- 1) 1) x_69)) 0.0))
(assert (= (+ x_4 (* (/ (- 1) 1) x_80)) 0.0))
(assert (= (+ x_4 (* (/ (- 1) 1) x_80)) 0.0))
(assert (= (+ x_38 (* (/ (- 1) 1) x_76)) 0.0))
(assert (= (+ x_38 (* (/ (- 1) 1) x_76)) 0.0))
(assert (>= (+ x_38 x_44 (* (/ (- 1) 1) x_50)) 0.0))
(assert (= (+ x_5 (* (/ (- 1) 1) x_81)) 0.0))
(assert (= (+ x_5 (* (/ (- 1) 1) x_81)) 0.0))
(assert (= (+ x_39 (* (/ (- 1) 1) x_77)) 0.0))
(assert (= (+ x_39 (* (/ (- 1) 1) x_77)) 0.0))
(assert (>= (+ x_38 x_44 (* (/ (- 1) 1) x_55)) 0.0))
(assert (= (+ x_41 (* (/ (- 1) 1) x_78)) 0.0))
(assert (= (+ x_41 (* (/ (- 1) 1) x_78)) 0.0))
(assert (>= (+ x_38 x_44 (* (/ (- 1) 1) x_60)) 0.0))
(assert (= (+ x_42 (* (/ (- 1) 1) x_79)) 0.0))
(assert (= (+ x_42 (* (/ (- 1) 1) x_79)) 0.0))
(assert (>= (+ x_38 x_44 (* (/ (- 1) 1) x_65)) 0.0))
(assert (= (+ x_43 (* (/ (- 1) 1) x_80)) 0.0))
(assert (= (+ x_43 (* (/ (- 1) 1) x_80)) 0.0))
(assert (>= (+ x_38 x_44 (* (/ (- 1) 1) x_70)) 0.0))
(assert (= (+ x_37 (* (/ (- 1) 1) x_81)) 0.0))
(assert (= (+ x_37 (* (/ (- 1) 1) x_81)) 0.0))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_26) x_32) 0.0)))
(assert (not (= (+ x_0 (* 2.0 x_6) x_7 (* (/ (- 1) 1) x_13)) 0.0)))
(assert (not (= (+ x_45 (* (/ (- 1) 1) x_71)) 0.0)))
(assert (not (= x_6 1.0)))
(assert (not (= (+ x_6 x_7) 1.0)))
(assert (not (= (+ x_0 x_6 x_7) 0.0)))
(assert (not (= (+ x_6 x_7 (* (/ (- 1) 1) x_11) x_13) 0.0)))
(assert (not (= x_7 0.0)))
(assert (not (= (+ x_6 x_7 (* (/ (- 1) 1) x_10) x_13) 0.0)))
(assert (let ((_let_0 (/ 1 2))) (not (= (+ x_6 (* _let_0 x_7) (* (- _let_0) x_9)) 0.0))))
(assert (not (= (+ x_10 (* (/ (- 1) 1) x_13)) 0.0)))
(assert (not (= (+ x_6 x_7 (* (/ (- 1) 1) x_12) x_13) 0.0)))
(assert (not (= (+ x_6 x_7 (* (/ (- 1) 1) x_9) x_13) 0.0)))
(assert (not (= (+ x_0 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (not (= (+ x_8 (* (/ (- 1) 1) x_13)) 0.0)))
(assert (not (= (+ x_6 x_7 (* (/ (- 1) 1) x_8) x_13) 0.0)))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_36)) (/ (- 1) 1))))
(assert (let ((_let_0 (/ 1 2))) (not (= (+ x_6 (* _let_0 x_7) (* (- _let_0) x_8)) 0.0))))
(assert (not (= (+ x_5 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_23) x_31) 0.0)))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_38)) (/ (- 1) 1))))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_17) x_29) 0.0)))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_20) x_30) 0.0)))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_16) x_33) 0.0)))
(assert (not (= (+ x_2 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (let ((_let_0 (/ 1 2))) (not (= (+ x_6 (* _let_0 x_7) (* (- _let_0) x_10)) 0.0))))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_40)) (/ (- 1) 1))))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_35)) (/ (- 1) 1))))
(assert (not (= (+ x_3 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (not (= (+ x_7 (* (/ (- 1) 1) x_34)) (/ (- 1) 1))))
(assert (let ((_let_0 (/ 1 2))) (not (= (+ x_6 (* _let_0 x_7) (* (- _let_0) x_11)) 0.0))))
(assert (not (= (+ x_1 (* (/ (- 1) 1) x_45)) 0.0)))
(assert (not (= (+ x_12 (* (/ (- 1) 1) x_13)) 0.0)))
(assert (let ((_let_0 (/ 1 2))) (not (= (+ x_6 (* _let_0 x_7) (* (- _let_0) x_12)) 0.0))))
(check-sat-assuming ( true ))