path: root/test/regress/regress1/lemmas/clocksynchro_5clocks.main_invar.base.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)
(check-sat-assuming ( (let ((_let_0 (= x_37 x_5))) (let ((_let_1 (= x_39 x_1))) (let ((_let_2 (= x_41 x_2))) (let ((_let_3 (= x_42 x_3))) (let ((_let_4 (= x_43 x_4))) (let ((_let_5 (= x_8 x_13))) (let ((_let_6 (not _let_5))) (let ((_let_7 (+ (+ x_13 x_6) x_7))) (let ((_let_8 (= x_8 _let_7))) (let ((_let_9 (= x_9 x_13))) (let ((_let_10 (not _let_9))) (let ((_let_11 (= x_9 _let_7))) (let ((_let_12 (= x_10 x_13))) (let ((_let_13 (not _let_12))) (let ((_let_14 (= x_10 _let_7))) (let ((_let_15 (= x_11 x_13))) (let ((_let_16 (not _let_15))) (let ((_let_17 (= x_11 _let_7))) (let ((_let_18 (= x_12 x_13))) (let ((_let_19 (not _let_18))) (let ((_let_20 (= x_12 _let_7))) (let ((_let_21 (or (not (<= x_40 x_13)) _let_8))) (let ((_let_22 (or (not (<= x_34 x_13)) _let_11))) (let ((_let_23 (or (not (<= x_35 x_13)) _let_14))) (let ((_let_24 (or (not (<= x_36 x_13)) _let_17))) (let ((_let_25 (or (not (<= x_38 x_13)) _let_20))) (let ((_let_26 (= x_29 0.0))) (let ((_let_27 (= x_30 0.0))) (let ((_let_28 (= x_31 0.0))) (let ((_let_29 (= x_32 0.0))) (let ((_let_30 (= x_33 0.0))) (let ((_let_31 (= x_8 x_6))) (let ((_let_32 (= x_9 x_6))) (let ((_let_33 (= x_10 x_6))) (let ((_let_34 (= x_11 x_6))) (let ((_let_35 (= x_12 x_6))) (let ((_let_36 (= x_40 1.0))) (let ((_let_37 (= x_34 1.0))) (let ((_let_38 (= x_35 1.0))) (let ((_let_39 (= x_36 1.0))) (let ((_let_40 (= x_38 1.0))) (let ((_let_41 (= x_17 0.0))) (let ((_let_42 (= x_20 0.0))) (let ((_let_43 (= x_23 0.0))) (let ((_let_44 (= x_26 0.0))) (let ((_let_45 (= x_16 0.0))) (let ((_let_46 (= x_18 0.0))) (let ((_let_47 (= x_21 0.0))) (let ((_let_48 (= x_24 0.0))) (let ((_let_49 (= x_27 0.0))) (let ((_let_50 (= x_15 0.0))) (let ((_let_51 (= x_19 0.0))) (let ((_let_52 (= x_22 0.0))) (let ((_let_53 (= x_25 0.0))) (let ((_let_54 (= x_28 0.0))) (let ((_let_55 (= x_14 0.0))) (let ((_let_56 (= 1.0 x_6))) (let ((_let_57 (= x_40 (/ (+ 1 1) 1)))) (let ((_let_58 (= (+ x_6 x_7) 1.0))) (let ((_let_59 (and (not _let_56) (not _let_58)))) (let ((_let_60 (= x_34 (/ (+ 1 1) 1)))) (let ((_let_61 (= x_35 (/ (+ 1 1) 1)))) (let ((_let_62 (= x_36 (/ (+ 1 1) 1)))) (let ((_let_63 (= x_38 (/ (+ 1 1) 1)))) (let ((_let_64 (<= x_8 (+ x_0 x_6)))) (let ((_let_65 (<= x_9 (+ x_0 x_6)))) (let ((_let_66 (<= x_10 (+ x_0 x_6)))) (let ((_let_67 (<= x_11 (+ x_0 x_6)))) (let ((_let_68 (<= x_12 (+ x_0 x_6)))) (let ((_let_69 (not (<= (- (+ x_0 x_6) x_83) 1.0)))) (let ((_let_70 (not (>= (- (+ x_0 x_6) x_84) 1.0)))) (let ((_let_71 (- 1 1))) (let ((_let_72 (not (<= (/ _let_71 1) x_82)))) (let ((_let_73 (not (= x_6 (+ x_0 x_6))))) (let ((_let_74 (and (or _let_73 (not (>= (+ (+ x_0 x_6) x_7) 1.0))) (not (= x_6 (+ (+ (+ x_0 x_6) x_6) x_7)))))) (let ((_let_75 (and (= x_6 (+ x_0 x_6)) (not (>= (+ x_0 x_6) 1.0))))) (let ((_let_76 (< x_0 0.0))) (let ((_let_77 (or (not (>= (+ x_0 x_6) 1.0)) (= x_6 (+ (+ (+ x_0 x_6) x_6) x_7))))) (let ((_let_78 (- 0.0 x_1))) (let ((_let_79 (* _let_78 1000.0))) (let ((_let_80 (/ 1 999))) (let ((_let_81 (- 0.0 x_5))) (let ((_let_82 (* _let_81 1000.0))) (let ((_let_83 (/ 1 2))) (let ((_let_84 (/ 1 1001))) (let ((_let_85 (and _let_77 (or (not (>= (+ (+ (* (* (+ (+ (+ 1.0 (* _let_79 _let_80)) 1.0) (* _let_82 _let_80)) 1.0) _let_83) x_44) (/ 3001 1998)) 0.0)) (> (- (- (* (* (+ (+ (+ 1.0 (* _let_79 _let_84)) 1.0) (* _let_82 _let_84)) 1.0) _let_83) x_44) _let_83) 0.0))))) (let ((_let_86 (and (= x_6 (+ (+ (+ x_0 x_6) x_6) x_7)) (not (= (+ 0.0 x_7) 0.0))))) (let ((_let_87 (/ 1 1000))) (let ((_let_88 (- 0 0))) (let ((_let_89 (and (= x_6 (+ (+ (+ x_0 x_6) x_6) x_7)) (or (not (<= (* (* x_7 999.0) _let_87) (/ _let_88 1))) (not (<= (/ _let_88 1) (* (* x_7 1001.0) _let_87))))))) (let ((_let_90 (+ x_0 (/ 999 1000)))) (let ((_let_91 (+ x_0 (/ 1001 1000)))) (let ((_let_92 (- (+ 1 1) 1))) (let ((_let_93 (* x_29 2.0))) (let ((_let_94 (+ (+ 1 1) 1))) (let ((_let_95 (+ (+ 0.0 x_7) 1.0))) (let ((_let_96 (+ (+ x_6 x_6) x_7))) (let ((_let_97 (* x_30 2.0))) (let ((_let_98 (* x_31 2.0))) (let ((_let_99 (* x_32 2.0))) (let ((_let_100 (* x_33 2.0))) (let ((_let_101 (- x_40 x_44))) (let ((_let_102 (- x_34 x_44))) (let ((_let_103 (- x_35 x_44))) (let ((_let_104 (- x_36 x_44))) (let ((_let_105 (- x_38 x_44))) (let ((_let_106 (+ x_40 x_44))) (let ((_let_107 (+ x_34 x_44))) (let ((_let_108 (+ x_35 x_44))) (let ((_let_109 (+ x_36 x_44))) (let ((_let_110 (+ x_38 x_44))) (let ((_let_111 (- x_13 x_83))) (let ((_let_112 (- x_13 x_84))) (let ((_let_113 (+ x_13 x_7))) (let ((_let_114 (- x_40 x_72))) (let ((_let_115 (- x_39 x_77))) (let ((_let_116 (- x_34 x_73))) (let ((_let_117 (- x_41 x_78))) (let ((_let_118 (- x_35 x_74))) (let ((_let_119 (- x_42 x_79))) (let ((_let_120 (- x_36 x_75))) (let ((_let_121 (- x_43 x_80))) (let ((_let_122 (- x_38 x_76))) (let ((_let_123 (- x_37 x_81))) (let ((_let_124 (- x_40 x_13))) (let ((_let_125 (- x_39 x_19))) (let ((_let_126 (- x_34 x_13))) (let ((_let_127 (- x_41 x_22))) (let ((_let_128 (- x_35 x_13))) (let ((_let_129 (- x_42 x_25))) (let ((_let_130 (- x_36 x_13))) (let ((_let_131 (- x_43 x_28))) (let ((_let_132 (- x_38 x_13))) (let ((_let_133 (- x_37 x_14))) (let ((_let_134 (- x_19 x_77))) (let ((_let_135 (* _let_134 1000.0))) (let ((_let_136 (* (- x_19 x_81) 1000.0))) (let ((_let_137 (* (- x_22 x_77) 1000.0))) (let ((_let_138 (* (- x_22 x_81) 1000.0))) (let ((_let_139 (* (- x_25 x_77) 1000.0))) (let ((_let_140 (* (- x_25 x_81) 1000.0))) (let ((_let_141 (* (- x_28 x_77) 1000.0))) (let ((_let_142 (* (- x_28 x_81) 1000.0))) (let ((_let_143 (* (- x_14 x_77) 1000.0))) (let ((_let_144 (- x_14 x_81))) (let ((_let_145 (* _let_144 1000.0))) (let ((_let_146 (- x_13 x_72))) (let ((_let_147 (- x_13 x_73))) (let ((_let_148 (- x_22 x_78))) (let ((_let_149 (- x_13 x_74))) (let ((_let_150 (- x_25 x_79))) (let ((_let_151 (- x_13 x_75))) (let ((_let_152 (- x_28 x_80))) (let ((_let_153 (- x_13 x_76))) (let ((_let_154 (- x_18 x_19))) (let ((_let_155 (- x_21 x_22))) (let ((_let_156 (- x_24 x_25))) (let ((_let_157 (- x_27 x_28))) (let ((_let_158 (- x_15 x_14))) (let ((_let_159 (* (/ (* _let_71 999) 1) _let_87))) (let ((_let_160 (- x_1 x_1))) (let ((_let_161 (* (/ (* _let_71 1001) 1) _let_87))) (let ((_let_162 (- x_2 x_2))) (let ((_let_163 (- x_3 x_3))) (let ((_let_164 (- x_4 x_4))) (let ((_let_165 (- x_5 x_5))) (let ((_let_166 (- 1.0 (+ x_0 x_6)))) (let ((_let_167 (* (* _let_166 999.0) _let_87))) (let ((_let_168 (- x_1 0.0))) (let ((_let_169 (* (* _let_166 1001.0) _let_87))) (let ((_let_170 (- x_2 0.0))) (let ((_let_171 (- x_3 0.0))) (let ((_let_172 (- x_4 0.0))) (let ((_let_173 (- x_5 0.0))) (let ((_let_174 (- (+ x_0 x_6) 1.0))) (let ((_let_175 (* (* _let_174 999.0) _let_87))) (let ((_let_176 (* (* _let_174 1001.0) _let_87))) (let ((_let_177 (- 0.0 x_2))) (let ((_let_178 (- 0.0 x_3))) (let ((_let_179 (- 0.0 x_4))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (<= x_6 0.0)) (not (<= x_7 0.0))) (not (<= x_44 0.0))) (not (< x_82 (+ x_44 (* (* (+ (* (* x_7 1.0) _let_83) 1.0) 1001.0) _let_80))))) (< x_83 (- (* (* (- (- x_7 x_82) 1.0) 999.0) _let_83) 1.0))) (not (< x_83 (* (* (+ (+ (+ x_6 x_44) x_82) (/ 1501 1000)) 1001.0) _let_80)))) (not (<= x_84 0.0))) (<= x_84 (- x_6 (+ (+ x_44 (* (* (+ x_7 2.0) 1001.0) _let_80)) _let_83)))) (= x_0 0.0)) (<= _let_90 x_1)) (<= x_1 _let_91)) (<= _let_90 x_2)) (<= x_2 _let_91)) (<= _let_90 x_3)) (<= x_3 _let_91)) (<= _let_90 x_4)) (<= x_4 _let_91)) (<= _let_90 x_5)) (<= x_5 _let_91)) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (< x_0 x_1) (< x_0 x_2)) (< x_0 x_3)) (< x_0 x_4)) (< x_0 x_5)) (< x_0 x_45)) (<= x_45 x_1)) (<= x_45 x_2)) (<= x_45 x_3)) (<= x_45 x_4)) (<= x_45 x_5)) (or (or (or (or (= x_45 x_1) (= x_45 x_2)) (= x_45 x_3)) (= x_45 x_4)) (= x_45 x_5))) _let_1) _let_2) _let_3) _let_4) _let_0) _let_26) _let_27) _let_28) _let_29) _let_30) _let_31) _let_32) _let_33) _let_34) _let_35) _let_36) _let_37) _let_38) _let_39) _let_40) _let_41) _let_42) _let_43) _let_44) _let_45) _let_46) _let_47) _let_48) _let_49) _let_50) _let_51) _let_52) _let_53) _let_54) _let_55) (= x_46 1.0)) (= x_47 1.0)) (= x_48 1.0)) (= x_49 1.0)) (= x_50 1.0)) (= x_51 1.0)) (= x_52 1.0)) (= x_53 1.0)) (= x_54 1.0)) (= x_55 1.0)) (= x_56 1.0)) (= x_57 1.0)) (= x_58 1.0)) (= x_59 1.0)) (= x_60 1.0)) (= x_61 1.0)) (= x_62 1.0)) (= x_63 1.0)) (= x_64 1.0)) (= x_65 1.0)) (= x_66 1.0)) (= x_67 1.0)) (= x_68 1.0)) (= x_69 1.0)) (= x_70 1.0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_1) (<= _let_90 x_39)) (<= x_39 _let_91)) (or (or (and (and (and (and _let_56 (<= (/ _let_92 1) _let_93)) (<= _let_93 (/ _let_94 1))) _let_57) _let_31) (and (and (and _let_58 (= x_40 _let_95)) (= x_8 _let_96)) _let_26)) (and (and (and _let_59 _let_57) _let_26) _let_31))) (or (or (and (and (and _let_56 (= x_19 x_0)) _let_46) _let_41) (and (and (and _let_58 (= x_18 x_0)) (= x_17 (- x_40 1.0))) _let_51)) (and (and (and _let_59 _let_51) _let_46) _let_41))) _let_2) _let_27) _let_32) _let_37) _let_42) _let_47) _let_52) _let_3) _let_28) _let_33) _let_38) _let_43) _let_48) _let_53) _let_4) _let_29) _let_34) _let_39) _let_44) _let_49) _let_54) _let_0) _let_30) _let_35) _let_40) _let_45) _let_50) _let_55) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_2) (<= _let_90 x_41)) (<= x_41 _let_91)) (or (or (and (and (and (and _let_56 (<= (/ _let_92 1) _let_97)) (<= _let_97 (/ _let_94 1))) _let_60) _let_32) (and (and (and _let_58 (= x_34 _let_95)) (= x_9 _let_96)) _let_27)) (and (and (and _let_59 _let_60) _let_27) _let_32))) (or (or (and (and (and _let_56 (= x_22 x_0)) _let_47) _let_42) (and (and (and _let_58 (= x_21 x_0)) (= x_20 (- x_34 1.0))) _let_52)) (and (and (and _let_59 _let_52) _let_47) _let_42))) _let_1) _let_26) _let_31) _let_36) _let_41) _let_46) _let_51) _let_3) _let_28) _let_33) _let_38) _let_43) _let_48) _let_53) _let_4) _let_29) _let_34) _let_39) _let_44) _let_49) _let_54) _let_0) _let_30) _let_35) _let_40) _let_45) _let_50) _let_55)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_3) (<= _let_90 x_42)) (<= x_42 _let_91)) (or (or (and (and (and (and _let_56 (<= (/ _let_92 1) _let_98)) (<= _let_98 (/ _let_94 1))) _let_61) _let_33) (and (and (and _let_58 (= x_35 _let_95)) (= x_10 _let_96)) _let_28)) (and (and (and _let_59 _let_61) _let_28) _let_33))) (or (or (and (and (and _let_56 (= x_25 x_0)) _let_48) _let_43) (and (and (and _let_58 (= x_24 x_0)) (= x_23 (- x_35 1.0))) _let_53)) (and (and (and _let_59 _let_53) _let_48) _let_43))) _let_1) _let_26) _let_31) _let_36) _let_41) _let_46) _let_51) _let_2) _let_27) _let_32) _let_37) _let_42) _let_47) _let_52) _let_4) _let_29) _let_34) _let_39) _let_44) _let_49) _let_54) _let_0) _let_30) _let_35) _let_40) _let_45) _let_50) _let_55)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_4) (<= _let_90 x_43)) (<= x_43 _let_91)) (or (or (and (and (and (and _let_56 (<= (/ _let_92 1) _let_99)) (<= _let_99 (/ _let_94 1))) _let_62) _let_34) (and (and (and _let_58 (= x_36 _let_95)) (= x_11 _let_96)) _let_29)) (and (and (and _let_59 _let_62) _let_29) _let_34))) (or (or (and (and (and _let_56 (= x_28 x_0)) _let_49) _let_44) (and (and (and _let_58 (= x_27 x_0)) (= x_26 (- x_36 1.0))) _let_54)) (and (and (and _let_59 _let_54) _let_49) _let_44))) _let_1) _let_26) _let_31) _let_36) _let_41) _let_46) _let_51) _let_2) _let_27) _let_32) _let_37) _let_42) _let_47) _let_52) _let_3) _let_28) _let_33) _let_38) _let_43) _let_48) _let_53) _let_0) _let_30) _let_35) _let_40) _let_45) _let_50) _let_55)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= x_0 x_5) (<= _let_90 x_37)) (<= x_37 _let_91)) (or (or (and (and (and (and _let_56 (<= (/ _let_92 1) _let_100)) (<= _let_100 (/ _let_94 1))) _let_63) _let_35) (and (and (and _let_58 (= x_38 _let_95)) (= x_12 _let_96)) _let_30)) (and (and (and _let_59 _let_63) _let_30) _let_35))) (or (or (and (and (and _let_56 (= x_14 x_0)) _let_50) _let_45) (and (and (and _let_58 (= x_15 x_0)) (= x_16 (- x_38 1.0))) _let_55)) (and (and (and _let_59 _let_55) _let_50) _let_45))) _let_1) _let_26) _let_31) _let_36) _let_41) _let_46) _let_51) _let_2) _let_27) _let_32) _let_37) _let_42) _let_47) _let_52) _let_3) _let_28) _let_33) _let_38) _let_43) _let_48) _let_53) _let_4) _let_29) _let_34) _let_39) _let_44) _let_49) _let_54)) (<= _let_101 x_46)) (<= _let_101 x_51)) (<= _let_101 x_56)) (<= _let_101 x_61)) (<= _let_101 x_66)) (<= _let_102 x_47)) (<= _let_102 x_52)) (<= _let_102 x_57)) (<= _let_102 x_62)) (<= _let_102 x_67)) (<= _let_103 x_48)) (<= _let_103 x_53)) (<= _let_103 x_58)) (<= _let_103 x_63)) (<= _let_103 x_68)) (<= _let_104 x_49)) (<= _let_104 x_54)) (<= _let_104 x_59)) (<= _let_104 x_64)) (<= _let_104 x_69)) (<= _let_105 x_50)) (<= _let_105 x_55)) (<= _let_105 x_60)) (<= _let_105 x_65)) (<= _let_105 x_70)) (<= x_46 _let_106)) (<= x_51 _let_106)) (<= x_56 _let_106)) (<= x_61 _let_106)) (<= x_66 _let_106)) (<= x_47 _let_107)) (<= x_52 _let_107)) (<= x_57 _let_107)) (<= x_62 _let_107)) (<= x_67 _let_107)) (<= x_48 _let_108)) (<= x_53 _let_108)) (<= x_58 _let_108)) (<= x_63 _let_108)) (<= x_68 _let_108)) (<= x_49 _let_109)) (<= x_54 _let_109)) (<= x_59 _let_109)) (<= x_64 _let_109)) (<= x_69 _let_109)) (<= x_50 _let_110)) (<= x_55 _let_110)) (<= x_60 _let_110)) (<= x_65 _let_110)) (<= x_70 _let_110)) (= x_45 x_0)))) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not _let_64) (not _let_65)) (not _let_66)) (not _let_67)) (not _let_68)) (= x_71 x_45)) (= x_72 x_40)) (= x_73 x_34)) (= x_74 x_35)) (= x_75 x_36)) (= x_76 x_38)) (= x_77 x_39)) (= x_78 x_41)) (= x_79 x_42)) (= x_80 x_43)) (= x_81 x_37)) (= x_13 (+ (+ (+ x_0 x_6) x_6) x_7))) (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or _let_64 _let_65) _let_66) _let_67) _let_68) (= x_13 (+ x_0 x_6))) (= x_71 x_0)) (= x_77 x_1)) (= x_78 x_2)) (= x_79 x_3)) (= x_80 x_4)) (= x_81 x_5)) (= x_72 1.0)) (= x_73 1.0)) (= x_74 1.0)) (= x_75 1.0)) (= x_76 1.0)))) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (not (<= _let_111 x_72)) (not (<= _let_111 x_73))) (not (<= _let_111 x_74))) (not (<= _let_111 x_75))) (not (<= _let_111 x_76))) (not (<= x_72 _let_112))) (not (<= x_73 _let_112))) (not (<= x_74 _let_112))) (not (<= x_75 _let_112))) (not (<= x_76 _let_112))) (not (<= (- x_72 x_72) x_82))) (not (<= (- x_73 x_72) x_82))) (not (<= (- x_74 x_72) x_82))) (not (<= (- x_75 x_72) x_82))) (not (<= (- x_76 x_72) x_82))) (not (<= (- x_72 x_73) x_82))) (not (<= (- x_73 x_73) x_82))) (not (<= (- x_74 x_73) x_82))) (not (<= (- x_75 x_73) x_82))) (not (<= (- x_76 x_73) x_82))) (not (<= (- x_72 x_74) x_82))) (not (<= (- x_73 x_74) x_82))) (not (<= (- x_74 x_74) x_82))) (not (<= (- x_75 x_74) x_82))) (not (<= (- x_76 x_74) x_82))) (not (<= (- x_72 x_75) x_82))) (not (<= (- x_73 x_75) x_82))) (not (<= (- x_74 x_75) x_82))) (not (<= (- x_75 x_75) x_82))) (not (<= (- x_76 x_75) x_82))) (not (<= (- x_72 x_76) x_82))) (not (<= (- x_73 x_76) x_82))) (not (<= (- x_74 x_76) x_82))) (not (<= (- x_75 x_76) x_82))) (not (<= (- x_76 x_76) x_82))) (and (or _let_6 (not (<= x_40 _let_113))) (not _let_8))) (and (or _let_10 (not (<= x_34 _let_113))) (not _let_11))) (and (or _let_13 (not (<= x_35 _let_113))) (not _let_14))) (and (or _let_16 (not (<= x_36 _let_113))) (not _let_17))) (and (or _let_19 (not (<= x_38 _let_113))) (not _let_20))) (and (and (and (and _let_6 _let_10) _let_13) _let_16) _let_19)) (and _let_5 (or (not (<= (* (* _let_114 999.0) _let_87) _let_115)) (not (<= _let_115 (* (* _let_114 1001.0) _let_87)))))) (and _let_9 (or (not (<= (* (* _let_116 999.0) _let_87) _let_117)) (not (<= _let_117 (* (* _let_116 1001.0) _let_87)))))) (and _let_12 (or (not (<= (* (* _let_118 999.0) _let_87) _let_119)) (not (<= _let_119 (* (* _let_118 1001.0) _let_87)))))) (and _let_15 (or (not (<= (* (* _let_120 999.0) _let_87) _let_121)) (not (<= _let_121 (* (* _let_120 1001.0) _let_87)))))) (and _let_18 (or (not (<= (* (* _let_122 999.0) _let_87) _let_123)) (not (<= _let_123 (* (* _let_122 1001.0) _let_87)))))) (and (and _let_5 (not (<= x_40 x_13))) (or (or (< x_45 x_19) (not (<= (* (* _let_124 999.0) _let_87) _let_125))) (not (<= _let_125 (* (* _let_124 1001.0) _let_87)))))) (and (and _let_9 (not (<= x_34 x_13))) (or (or (< x_45 x_22) (not (<= (* (* _let_126 999.0) _let_87) _let_127))) (not (<= _let_127 (* (* _let_126 1001.0) _let_87)))))) (and (and _let_12 (not (<= x_35 x_13))) (or (or (< x_45 x_25) (not (<= (* (* _let_128 999.0) _let_87) _let_129))) (not (<= _let_129 (* (* _let_128 1001.0) _let_87)))))) (and (and _let_15 (not (<= x_36 x_13))) (or (or (< x_45 x_28) (not (<= (* (* _let_130 999.0) _let_87) _let_131))) (not (<= _let_131 (* (* _let_130 1001.0) _let_87)))))) (and (and _let_18 (not (<= x_38 x_13))) (or (or (< x_45 x_14) (not (<= (* (* _let_132 999.0) _let_87) _let_133))) (not (<= _let_133 (* (* _let_132 1001.0) _let_87)))))) (and _let_21 (or (not (<= x_29 (+ (+ (* (* (+ (+ (+ x_72 (* _let_135 _let_80)) x_76) (* _let_136 _let_80)) 1.0) _let_83) x_44) (/ 3001 1998)))) (< x_29 (- (- (* (* (+ (+ (+ x_72 (* _let_135 _let_84)) x_76) (* _let_136 _let_84)) 1.0) _let_83) x_44) _let_83))))) (and _let_22 (or (not (<= x_30 (+ (+ (* (* (+ (+ (+ x_72 (* _let_137 _let_80)) x_76) (* _let_138 _let_80)) 1.0) _let_83) x_44) (/ 3001 1998)))) (< x_30 (- (- (* (* (+ (+ (+ x_72 (* _let_137 _let_84)) x_76) (* _let_138 _let_84)) 1.0) _let_83) x_44) _let_83))))) (and _let_23 (or (not (<= x_31 (+ (+ (* (* (+ (+ (+ x_72 (* _let_139 _let_80)) x_76) (* _let_140 _let_80)) 1.0) _let_83) x_44) (/ 3001 1998)))) (< x_31 (- (- (* (* (+ (+ (+ x_72 (* _let_139 _let_84)) x_76) (* _let_140 _let_84)) 1.0) _let_83) x_44) _let_83))))) (and _let_24 (or (not (<= x_32 (+ (+ (* (* (+ (+ (+ x_72 (* _let_141 _let_80)) x_76) (* _let_142 _let_80)) 1.0) _let_83) x_44) (/ 3001 1998)))) (< x_32 (- (- (* (* (+ (+ (+ x_72 (* _let_141 _let_84)) x_76) (* _let_142 _let_84)) 1.0) _let_83) x_44) _let_83))))) (and _let_25 (or (not (<= x_33 (+ (+ (* (* (+ (+ (+ x_72 (* _let_143 _let_80)) x_76) (* _let_145 _let_80)) 1.0) _let_83) x_44) (/ 3001 1998)))) (< x_33 (- (- (* (* (+ (+ (+ x_72 (* _let_143 _let_84)) x_76) (* _let_145 _let_84)) 1.0) _let_83) x_44) _let_83))))) (and _let_21 (or (not (<= (* (* _let_146 999.0) _let_87) _let_134)) (not (<= _let_134 (* (* _let_146 1001.0) _let_87)))))) (and _let_22 (or (not (<= (* (* _let_147 999.0) _let_87) _let_148)) (not (<= _let_148 (* (* _let_147 1001.0) _let_87)))))) (and _let_23 (or (not (<= (* (* _let_149 999.0) _let_87) _let_150)) (not (<= _let_150 (* (* _let_149 1001.0) _let_87)))))) (and _let_24 (or (not (<= (* (* _let_151 999.0) _let_87) _let_152)) (not (<= _let_152 (* (* _let_151 1001.0) _let_87)))))) (and _let_25 (or (not (<= (* (* _let_153 999.0) _let_87) _let_144)) (not (<= _let_144 (* (* _let_153 1001.0) _let_87)))))) (and _let_8 (not (= x_17 (+ x_29 x_7))))) (and _let_11 (not (= x_20 (+ x_30 x_7))))) (and _let_14 (not (= x_23 (+ x_31 x_7))))) (and _let_17 (not (= x_26 (+ x_32 x_7))))) (and _let_20 (not (= x_16 (+ x_33 x_7))))) (and _let_8 (or (not (<= (* (* x_7 999.0) _let_87) _let_154)) (not (<= _let_154 (* (* x_7 1001.0) _let_87)))))) (and _let_11 (or (not (<= (* (* x_7 999.0) _let_87) _let_155)) (not (<= _let_155 (* (* x_7 1001.0) _let_87)))))) (and _let_14 (or (not (<= (* (* x_7 999.0) _let_87) _let_156)) (not (<= _let_156 (* (* x_7 1001.0) _let_87)))))) (and _let_17 (or (not (<= (* (* x_7 999.0) _let_87) _let_157)) (not (<= _let_157 (* (* x_7 1001.0) _let_87)))))) (and _let_20 (or (not (<= (* (* x_7 999.0) _let_87) _let_158)) (not (<= _let_158 (* (* x_7 1001.0) _let_87)))))) _let_69) _let_69) _let_69) _let_69) _let_69) _let_70) _let_70) _let_70) _let_70) _let_70) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_72) _let_74) _let_74) _let_74) _let_74) _let_74) (and (and (and (and _let_73 _let_73) _let_73) _let_73) _let_73)) (and (= x_6 (+ x_0 x_6)) (or (not (<= _let_159 _let_160)) (not (<= _let_160 _let_161))))) (and (= x_6 (+ x_0 x_6)) (or (not (<= _let_159 _let_162)) (not (<= _let_162 _let_161))))) (and (= x_6 (+ x_0 x_6)) (or (not (<= _let_159 _let_163)) (not (<= _let_163 _let_161))))) (and (= x_6 (+ x_0 x_6)) (or (not (<= _let_159 _let_164)) (not (<= _let_164 _let_161))))) (and (= x_6 (+ x_0 x_6)) (or (not (<= _let_159 _let_165)) (not (<= _let_165 _let_161))))) (and _let_75 (or (or _let_76 (not (<= _let_167 _let_168))) (not (<= _let_168 _let_169))))) (and _let_75 (or (or _let_76 (not (<= _let_167 _let_170))) (not (<= _let_170 _let_169))))) (and _let_75 (or (or _let_76 (not (<= _let_167 _let_171))) (not (<= _let_171 _let_169))))) (and _let_75 (or (or _let_76 (not (<= _let_167 _let_172))) (not (<= _let_172 _let_169))))) (and _let_75 (or (or _let_76 (not (<= _let_167 _let_173))) (not (<= _let_173 _let_169))))) _let_85) _let_85) _let_85) _let_85) _let_85) (and _let_77 (or (not (<= _let_175 _let_78)) (not (<= _let_78 _let_176))))) (and _let_77 (or (not (<= _let_175 _let_177)) (not (<= _let_177 _let_176))))) (and _let_77 (or (not (<= _let_175 _let_178)) (not (<= _let_178 _let_176))))) (and _let_77 (or (not (<= _let_175 _let_179)) (not (<= _let_179 _let_176))))) (and _let_77 (or (not (<= _let_175 _let_81)) (not (<= _let_81 _let_176))))) _let_86) _let_86) _let_86) _let_86) _let_86) _let_89) _let_89) _let_89) _let_89) _let_89)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ))