(set-info :smt-lib-version 2.6)
(set-logic QF_LRA)
(set-info :source | Clock Synchronization. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :category "industrial")
(set-info :status unsat)
(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)
(declare-fun x_85 () Real)
(declare-fun x_86 () Real)
(declare-fun x_87 () Real)
(declare-fun x_88 () Real)
(declare-fun x_89 () Real)
(declare-fun x_90 () Real)
(declare-fun x_91 () Real)
(declare-fun x_92 () Real)
(declare-fun x_93 () Real)
(declare-fun x_94 () Real)
(declare-fun x_95 () Real)
(declare-fun x_96 () Real)
(declare-fun x_97 () Real)
(declare-fun x_98 () Real)
(declare-fun x_99 () Real)
(declare-fun x_100 () Real)
(declare-fun x_101 () Real)
(declare-fun x_102 () Real)
(declare-fun x_103 () Real)
(declare-fun x_104 () Real)
(declare-fun x_105 () Real)
(assert (let ((?v_41 (= x_44 x_6)) (?v_54 (= x_46 x_1)) (?v_13 (= x_48 x_2)) (?v_20 (= x_49 x_3)) (?v_27 (= x_50 x_4)) (?v_34 (= x_51 x_5)) (?v_93 (= x_9 x_15))) (let ((?v_87 (not ?v_93)) (?v_86 (+ (+ x_15 x_7) x_8))) (let ((?v_124 (= x_9 ?v_86)) (?v_96 (= x_10 x_15))) (let ((?v_88 (not ?v_96)) (?v_128 (= x_10 ?v_86)) (?v_99 (= x_11 x_15))) (let ((?v_89 (not ?v_99)) (?v_132 (= x_11 ?v_86)) (?v_102 (= x_12 x_15))) (let ((?v_90 (not ?v_102)) (?v_136 (= x_12 ?v_86)) (?v_105 (= x_13 x_15))) (let ((?v_91 (not ?v_105)) (?v_140 (= x_13 ?v_86)) (?v_108 (= x_14 x_15))) (let ((?v_92 (not ?v_108)) (?v_144 (= x_14 ?v_86)) (?v_123 (not (<= x_47 x_15))) (?v_127 (not (<= x_40 x_15))) (?v_131 (not (<= x_41 x_15))) (?v_135 (not (<= x_42 x_15))) (?v_139 (not (<= x_43 x_15))) (?v_143 (not (<= x_45 x_15)))) (let ((?v_147 (or ?v_123 ?v_124)) (?v_150 (or ?v_127 ?v_128)) (?v_153 (or ?v_131 ?v_132)) (?v_156 (or ?v_135 ?v_136)) (?v_159 (or ?v_139 ?v_140)) (?v_162 (or ?v_143 ?v_144)) (?v_5 (= x_34 0)) (?v_14 (= x_35 0)) (?v_21 (= x_36 0)) (?v_28 (= x_37 0)) (?v_35 (= x_38 0)) (?v_42 (= x_39 0)) (?v_4 (= x_9 x_7)) (?v_15 (= x_10 x_7)) (?v_22 (= x_11 x_7)) (?v_29 (= x_12 x_7)) (?v_36 (= x_13 x_7)) (?v_43 (= x_14 x_7)) (?v_55 (= x_47 1)) (?v_16 (= x_40 1)) (?v_23 (= x_41 1)) (?v_30 (= x_42 1)) (?v_37 (= x_43 1)) (?v_44 (= x_45 1)) (?v_10 (= x_19 0)) (?v_17 (= x_22 0)) (?v_24 (= x_25 0)) (?v_31 (= x_28 0)) (?v_38 (= x_31 0)) (?v_45 (= x_18 0)) (?v_9 (= x_20 0)) (?v_18 (= x_23 0)) (?v_25 (= x_26 0)) (?v_32 (= x_29 0)) (?v_39 (= x_32 0)) (?v_46 (= x_17 0)) (?v_11 (= x_21 0)) (?v_19 (= x_24 0)) (?v_26 (= x_27 0)) (?v_33 (= x_30 0)) (?v_40 (= x_33 0)) (?v_47 (= x_16 0)) (?v_6 (= 1 x_7)) (?v_3 (+ 1 1))) (let ((?v_8 (= x_47 ?v_3)) (?v_7 (= (+ x_7 x_8) 1))) (let ((?v_12 (and (not ?v_6) (not ?v_7))) (?v_53 (= x_40 ?v_3)) (?v_57 (= x_41 ?v_3)) (?v_59 (= x_42 ?v_3)) (?v_61 (= x_43 ?v_3)) (?v_63 (= x_45 ?v_3)) (?v_76 (+ x_0 x_7))) (let ((?v_77 (<= x_9 ?v_76)) (?v_78 (<= x_10 ?v_76)) (?v_79 (<= x_11 ?v_76)) (?v_80 (<= x_12 ?v_76)) (?v_81 (<= x_13 ?v_76)) (?v_82 (<= x_14 ?v_76)) (?v_173 (not (<= (- ?v_76 x_104) 1))) (?v_174 (not (>= (- ?v_76 x_105) 1))) (?v_180 (- 1 1))) (let ((?v_175 (not (<= ?v_180 x_103))) (?v_179 (= x_7 ?v_76))) (let ((?v_178 (not ?v_179)) (?v_176 (+ (+ ?v_76 x_7) x_8))) (let ((?v_201 (= x_7 ?v_176))) (let ((?v_177 (and (or ?v_178 (not (>= (+ ?v_76 x_8) 1))) (not ?v_201))) (?v_200 (not (>= ?v_76 1)))) (let ((?v_191 (and ?v_179 ?v_200)) (?v_192 (< x_0 0)) (?v_205 (or ?v_200 ?v_201)) (?v_206 (- 0 x_1))) (let ((?v_202 (* ?v_206 1000)) (?v_214 (- 0 x_6))) (let ((?v_203 (* ?v_214 1000)) (?v_215 (+ 0 x_8))) (let ((?v_216 (and ?v_201 (not (= ?v_215 0)))) (?v_217 (- 0 0)) (?v_2 (* x_34 2)) (?v_48 (- ?v_3 1)) (?v_50 (+ ?v_3 1)) (?v_51 (+ ?v_215 1)) (?v_52 (+ (+ x_7 x_7) x_8)) (?v_49 (* x_35 2)) (?v_56 (* x_36 2)) (?v_58 (* x_37 2)) (?v_60 (* x_38 2)) (?v_62 (* x_39 2)) (?v_64 (- x_47 x_52)) (?v_65 (- x_40 x_52)) (?v_66 (- x_41 x_52)) (?v_67 (- x_42 x_52)) (?v_68 (- x_43 x_52)) (?v_69 (- x_45 x_52)) (?v_70 (+ x_47 x_52)) (?v_71 (+ x_40 x_52)) (?v_72 (+ x_41 x_52)) (?v_73 (+ x_42 x_52)) (?v_74 (+ x_43 x_52)) (?v_75 (+ x_45 x_52)) (?v_83 (- x_15 x_104)) (?v_84 (- x_15 x_105)) (?v_85 (+ x_15 x_8)) (?v_94 (- x_46 x_97)) (?v_95 (- x_47 x_91)) (?v_97 (- x_48 x_98)) (?v_98 (- x_40 x_92)) (?v_100 (- x_49 x_99)) (?v_101 (- x_41 x_93)) (?v_103 (- x_50 x_100)) (?v_104 (- x_42 x_94)) (?v_106 (- x_51 x_101)) (?v_107 (- x_43 x_95)) (?v_109 (- x_44 x_102)) (?v_110 (- x_45 x_96)) (?v_111 (- x_46 x_21)) (?v_112 (- x_47 x_15)) (?v_113 (- x_48 x_24)) (?v_114 (- x_40 x_15)) (?v_115 (- x_49 x_27)) (?v_116 (- x_41 x_15)) (?v_117 (- x_50 x_30)) (?v_118 (- x_42 x_15)) (?v_119 (- x_51 x_33)) (?v_120 (- x_43 x_15)) (?v_121 (- x_44 x_16)) (?v_122 (- x_45 x_15)) (?v_148 (- x_21 x_97))) (let ((?v_125 (* ?v_148 1000)) (?v_126 (* (- x_21 x_102) 1000)) (?v_129 (* (- x_24 x_97) 1000)) (?v_130 (* (- x_24 x_102) 1000)) (?v_133 (* (- x_27 x_97) 1000)) (?v_134 (* (- x_27 x_102) 1000)) (?v_137 (* (- x_30 x_97) 1000)) (?v_138 (* (- x_30 x_102) 1000)) (?v_141 (* (- x_33 x_97) 1000)) (?v_142 (* (- x_33 x_102) 1000)) (?v_145 (* (- x_16 x_97) 1000)) (?v_163 (- x_16 x_102))) (let ((?v_146 (* ?v_163 1000)) (?v_149 (- x_15 x_91)) (?v_151 (- x_24 x_98)) (?v_152 (- x_15 x_92)) (?v_154 (- x_27 x_99)) (?v_155 (- x_15 x_93)) (?v_157 (- x_30 x_100)) (?v_158 (- x_15 x_94)) (?v_160 (- x_33 x_101)) (?v_161 (- x_15 x_95)) (?v_164 (- x_15 x_96)) (?v_165 (- x_20 x_21)) (?v_167 (- x_23 x_24)) (?v_169 (- x_26 x_27)) (?v_170 (- x_29 x_30)) (?v_171 (- x_32 x_33)) (?v_172 (- x_17 x_16)) (?v_181 (- x_1 x_1)) (?v_183 (- x_2 x_2)) (?v_185 (- x_3 x_3)) (?v_186 (- x_4 x_4)) (?v_187 (- x_5 x_5)) (?v_188 (- x_6 x_6)) (?v_189 (- x_1 0)) (?v_190 (- 1 ?v_76)) (?v_194 (- x_2 0)) (?v_196 (- x_3 0)) (?v_197 (- x_4 0)) (?v_198 (- x_5 0)) (?v_199 (- x_6 0)) (?v_207 (- ?v_76 1)) (?v_209 (- 0 x_2)) (?v_211 (- 0 x_3)) (?v_212 (- 0 x_4)) (?v_213 (- 0 x_5)) (?v_0 (+ x_0 (/ 999 1000))) (?v_1 (+ x_0 (/ 1001 1000))) (?v_166 (* (* x_8 999) (/ 1 1000))) (?v_168 (* (* x_8 1001) (/ 1 1000))) (?v_182 (* (* ?v_180 999) (/ 1 1000))) (?v_184 (* (* ?v_180 1001) (/ 1 1000)))) (let ((?v_193 (* (* ?v_190 999) (/ 1 1000))) (?v_195 (* (* ?v_190 1001) (/ 1 1000))) (?v_204 (and ?v_205 (or (not (>= (+ (+ (* (* (+ (+ (+ 1 (* ?v_202 (/ 1 999))) 1) (* ?v_203 (/ 1 999))) 1) (/ 1 2)) x_52) (/ 3001 1998)) 0)) (> (- (- (* (* (+ (+ (+ 1 (* ?v_202 (/ 1 1001))) 1) (* ?v_203 (/ 1 1001))) 1) (/ 1 2)) x_52) (/ 1 2)) 0)))) (?v_208 (* (* ?v_207 999) (/ 1 1000))) (?v_210 (* (* ?v_207 1001) (/ 1 1000))) (?v_218 (and ?v_201 (or (not (<= ?v_166 ?v_217)) (not (<= ?v_217 ?v_168)))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (<= x_7 0)) (not (<= x_8 0))) (not (<= x_52 0))) (not (< x_103 (+ x_52 (* (* (+ (* (* x_8 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (< x_104 (- (* (* (- (- x_8 x_103) 1) 999) (/ 1 2)) 1))) (not (< x_104 (* (* (+ (+ (+ x_7 x_52) x_103) (/ 1501 1000)) 1001) (/ 1 999))))) (not (<= x_105 0))) (<= x_105 (- x_7 (+ (+ x_52 (* (* (+ x_8 2) 1001) (/ 1 999))) (/ 1 2))))) (= x_0 0)) (<= ?v_0 x_1)) (<= x_1 ?v_1)) (<= ?v_0 x_2)) (<= x_2 ?v_1)) (<= ?v_0 x_3)) (<= x_3 ?v_1)) (<= ?v_0 x_4)) (<= x_4 ?v_1)) (<= ?v_0 x_5)) (<= x_5 ?v_1)) (<= ?v_0 x_6)) (<= x_6 ?v_1)) (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 (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_6)) (< x_0 x_53)) (<= x_53 x_1)) (<= x_53 x_2)) (<= x_53 x_3)) (<= x_53 x_4)) (<= x_53 x_5)) (<= x_53 x_6)) (or (or (or (or (or (= x_53 x_1) (= x_53 x_2)) (= x_53 x_3)) (= x_53 x_4)) (= x_53 x_5)) (= x_53 x_6))) ?v_54) ?v_13) ?v_20) ?v_27) ?v_34) ?v_41) ?v_5) ?v_14) ?v_21) ?v_28) ?v_35) ?v_42) ?v_4) ?v_15) ?v_22) ?v_29) ?v_36) ?v_43) ?v_55) ?v_16) ?v_23) ?v_30) ?v_37) ?v_44) ?v_10) ?v_17) ?v_24) ?v_31) ?v_38) ?v_45) ?v_9) ?v_18) ?v_25) ?v_32) ?v_39) ?v_46) ?v_11) ?v_19) ?v_26) ?v_33) ?v_40) ?v_47) (= x_54 1)) (= x_55 1)) (= x_56 1)) (= x_57 1)) (= x_58 1)) (= x_59 1)) (= x_60 1)) (= x_61 1)) (= x_62 1)) (= x_63 1)) (= x_64 1)) (= x_65 1)) (= x_66 1)) (= x_67 1)) (= x_68 1)) (= x_69 1)) (= x_70 1)) (= x_71 1)) (= x_72 1)) (= x_73 1)) (= x_74 1)) (= x_75 1)) (= x_76 1)) (= x_77 1)) (= x_78 1)) (= x_79 1)) (= x_80 1)) (= x_81 1)) (= x_82 1)) (= x_83 1)) (= x_84 1)) (= x_85 1)) (= x_86 1)) (= x_87 1)) (= x_88 1)) (= x_89 1)) (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 (and (and (or (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 (and (and (and (and (and (and (and (= x_0 x_1) (<= ?v_0 x_46)) (<= x_46 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_48 ?v_2)) (<= ?v_2 ?v_50)) ?v_8) ?v_4) (and (and (and ?v_7 (= x_47 ?v_51)) (= x_9 ?v_52)) ?v_5)) (and (and (and ?v_12 ?v_8) ?v_5) ?v_4))) (or (or (and (and (and ?v_6 (= x_21 x_0)) ?v_9) ?v_10) (and (and (and ?v_7 (= x_20 x_0)) (= x_19 (- x_47 1))) ?v_11)) (and (and (and ?v_12 ?v_11) ?v_9) ?v_10))) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47) (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_2) (<= ?v_0 x_48)) (<= x_48 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_48 ?v_49)) (<= ?v_49 ?v_50)) ?v_53) ?v_15) (and (and (and ?v_7 (= x_40 ?v_51)) (= x_10 ?v_52)) ?v_14)) (and (and (and ?v_12 ?v_53) ?v_14) ?v_15))) (or (or (and (and (and ?v_6 (= x_24 x_0)) ?v_18) ?v_17) (and (and (and ?v_7 (= x_23 x_0)) (= x_22 (- x_40 1))) ?v_19)) (and (and (and ?v_12 ?v_19) ?v_18) ?v_17))) ?v_54) ?v_5) ?v_4) ?v_55) ?v_10) ?v_9) ?v_11) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47)) (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_3) (<= ?v_0 x_49)) (<= x_49 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_48 ?v_56)) (<= ?v_56 ?v_50)) ?v_57) ?v_22) (and (and (and ?v_7 (= x_41 ?v_51)) (= x_11 ?v_52)) ?v_21)) (and (and (and ?v_12 ?v_57) ?v_21) ?v_22))) (or (or (and (and (and ?v_6 (= x_27 x_0)) ?v_25) ?v_24) (and (and (and ?v_7 (= x_26 x_0)) (= x_25 (- x_41 1))) ?v_26)) (and (and (and ?v_12 ?v_26) ?v_25) ?v_24))) ?v_54) ?v_5) ?v_4) ?v_55) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47)) (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_4) (<= ?v_0 x_50)) (<= x_50 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_48 ?v_58)) (<= ?v_58 ?v_50)) ?v_59) ?v_29) (and (and (and ?v_7 (= x_42 ?v_51)) (= x_12 ?v_52)) ?v_28)) (and (and (and ?v_12 ?v_59) ?v_28) ?v_29))) (or (or (and (and (and ?v_6 (= x_30 x_0)) ?v_32) ?v_31) (and (and (and ?v_7 (= x_29 x_0)) (= x_28 (- x_42 1))) ?v_33)) (and (and (and ?v_12 ?v_33) ?v_32) ?v_31))) ?v_54) ?v_5) ?v_4) ?v_55) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47)) (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_5) (<= ?v_0 x_51)) (<= x_51 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_48 ?v_60)) (<= ?v_60 ?v_50)) ?v_61) ?v_36) (and (and (and ?v_7 (= x_43 ?v_51)) (= x_13 ?v_52)) ?v_35)) (and (and (and ?v_12 ?v_61) ?v_35) ?v_36))) (or (or (and (and (and ?v_6 (= x_33 x_0)) ?v_39) ?v_38) (and (and (and ?v_7 (= x_32 x_0)) (= x_31 (- x_43 1))) ?v_40)) (and (and (and ?v_12 ?v_40) ?v_39) ?v_38))) ?v_54) ?v_5) ?v_4) ?v_55) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_41) ?v_42) ?v_43) ?v_44) ?v_45) ?v_46) ?v_47)) (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_6) (<= ?v_0 x_44)) (<= x_44 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_48 ?v_62)) (<= ?v_62 ?v_50)) ?v_63) ?v_43) (and (and (and ?v_7 (= x_45 ?v_51)) (= x_14 ?v_52)) ?v_42)) (and (and (and ?v_12 ?v_63) ?v_42) ?v_43))) (or (or (and (and (and ?v_6 (= x_16 x_0)) ?v_46) ?v_45) (and (and (and ?v_7 (= x_17 x_0)) (= x_18 (- x_45 1))) ?v_47)) (and (and (and ?v_12 ?v_47) ?v_46) ?v_45))) ?v_54) ?v_5) ?v_4) ?v_55) ?v_10) ?v_9) ?v_11) ?v_13) ?v_14) ?v_15) ?v_16) ?v_17) ?v_18) ?v_19) ?v_20) ?v_21) ?v_22) ?v_23) ?v_24) ?v_25) ?v_26) ?v_27) ?v_28) ?v_29) ?v_30) ?v_31) ?v_32) ?v_33) ?v_34) ?v_35) ?v_36) ?v_37) ?v_38) ?v_39) ?v_40)) (<= ?v_64 x_54)) (<= ?v_64 x_60)) (<= ?v_64 x_66)) (<= ?v_64 x_72)) (<= ?v_64 x_78)) (<= ?v_64 x_84)) (<= ?v_65 x_55)) (<= ?v_65 x_61)) (<= ?v_65 x_67)) (<= ?v_65 x_73)) (<= ?v_65 x_79)) (<= ?v_65 x_85)) (<= ?v_66 x_56)) (<= ?v_66 x_62)) (<= ?v_66 x_68)) (<= ?v_66 x_74)) (<= ?v_66 x_80)) (<= ?v_66 x_86)) (<= ?v_67 x_57)) (<= ?v_67 x_63)) (<= ?v_67 x_69)) (<= ?v_67 x_75)) (<= ?v_67 x_81)) (<= ?v_67 x_87)) (<= ?v_68 x_58)) (<= ?v_68 x_64)) (<= ?v_68 x_70)) (<= ?v_68 x_76)) (<= ?v_68 x_82)) (<= ?v_68 x_88)) (<= ?v_69 x_59)) (<= ?v_69 x_65)) (<= ?v_69 x_71)) (<= ?v_69 x_77)) (<= ?v_69 x_83)) (<= ?v_69 x_89)) (<= x_54 ?v_70)) (<= x_60 ?v_70)) (<= x_66 ?v_70)) (<= x_72 ?v_70)) (<= x_78 ?v_70)) (<= x_84 ?v_70)) (<= x_55 ?v_71)) (<= x_61 ?v_71)) (<= x_67 ?v_71)) (<= x_73 ?v_71)) (<= x_79 ?v_71)) (<= x_85 ?v_71)) (<= x_56 ?v_72)) (<= x_62 ?v_72)) (<= x_68 ?v_72)) (<= x_74 ?v_72)) (<= x_80 ?v_72)) (<= x_86 ?v_72)) (<= x_57 ?v_73)) (<= x_63 ?v_73)) (<= x_69 ?v_73)) (<= x_75 ?v_73)) (<= x_81 ?v_73)) (<= x_87 ?v_73)) (<= x_58 ?v_74)) (<= x_64 ?v_74)) (<= x_70 ?v_74)) (<= x_76 ?v_74)) (<= x_82 ?v_74)) (<= x_88 ?v_74)) (<= x_59 ?v_75)) (<= x_65 ?v_75)) (<= x_71 ?v_75)) (<= x_77 ?v_75)) (<= x_83 ?v_75)) (<= x_89 ?v_75)) (= x_53 x_0)))) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not ?v_77) (not ?v_78)) (not ?v_79)) (not ?v_80)) (not ?v_81)) (not ?v_82)) (= x_90 x_53)) (= x_91 x_47)) (= x_92 x_40)) (= x_93 x_41)) (= x_94 x_42)) (= x_95 x_43)) (= x_96 x_45)) (= x_97 x_46)) (= x_98 x_48)) (= x_99 x_49)) (= x_100 x_50)) (= x_101 x_51)) (= x_102 x_44)) (= x_15 ?v_176)) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or ?v_77 ?v_78) ?v_79) ?v_80) ?v_81) ?v_82) (= x_15 ?v_76)) (= x_90 x_0)) (= x_97 x_1)) (= x_98 x_2)) (= x_99 x_3)) (= x_100 x_4)) (= x_101 x_5)) (= x_102 x_6)) (= x_91 1)) (= x_92 1)) (= x_93 1)) (= x_94 1)) (= x_95 1)) (= x_96 1)))) (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 (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 (<= ?v_83 x_91)) (not (<= ?v_83 x_92))) (not (<= ?v_83 x_93))) (not (<= ?v_83 x_94))) (not (<= ?v_83 x_95))) (not (<= ?v_83 x_96))) (not (<= x_91 ?v_84))) (not (<= x_92 ?v_84))) (not (<= x_93 ?v_84))) (not (<= x_94 ?v_84))) (not (<= x_95 ?v_84))) (not (<= x_96 ?v_84))) (not (<= (- x_91 x_91) x_103))) (not (<= (- x_92 x_91) x_103))) (not (<= (- x_93 x_91) x_103))) (not (<= (- x_94 x_91) x_103))) (not (<= (- x_95 x_91) x_103))) (not (<= (- x_96 x_91) x_103))) (not (<= (- x_91 x_92) x_103))) (not (<= (- x_92 x_92) x_103))) (not (<= (- x_93 x_92) x_103))) (not (<= (- x_94 x_92) x_103))) (not (<= (- x_95 x_92) x_103))) (not (<= (- x_96 x_92) x_103))) (not (<= (- x_91 x_93) x_103))) (not (<= (- x_92 x_93) x_103))) (not (<= (- x_93 x_93) x_103))) (not (<= (- x_94 x_93) x_103))) (not (<= (- x_95 x_93) x_103))) (not (<= (- x_96 x_93) x_103))) (not (<= (- x_91 x_94) x_103))) (not (<= (- x_92 x_94) x_103))) (not (<= (- x_93 x_94) x_103))) (not (<= (- x_94 x_94) x_103))) (not (<= (- x_95 x_94) x_103))) (not (<= (- x_96 x_94) x_103))) (not (<= (- x_91 x_95) x_103))) (not (<= (- x_92 x_95) x_103))) (not (<= (- x_93 x_95) x_103))) (not (<= (- x_94 x_95) x_103))) (not (<= (- x_95 x_95) x_103))) (not (<= (- x_96 x_95) x_103))) (not (<= (- x_91 x_96) x_103))) (not (<= (- x_92 x_96) x_103))) (not (<= (- x_93 x_96) x_103))) (not (<= (- x_94 x_96) x_103))) (not (<= (- x_95 x_96) x_103))) (not (<= (- x_96 x_96) x_103))) (and (or ?v_87 (not (<= x_47 ?v_85))) (not ?v_124))) (and (or ?v_88 (not (<= x_40 ?v_85))) (not ?v_128))) (and (or ?v_89 (not (<= x_41 ?v_85))) (not ?v_132))) (and (or ?v_90 (not (<= x_42 ?v_85))) (not ?v_136))) (and (or ?v_91 (not (<= x_43 ?v_85))) (not ?v_140))) (and (or ?v_92 (not (<= x_45 ?v_85))) (not ?v_144))) (and (and (and (and (and ?v_87 ?v_88) ?v_89) ?v_90) ?v_91) ?v_92)) (and ?v_93 (or (not (<= (* (* ?v_95 999) (/ 1 1000)) ?v_94)) (not (<= ?v_94 (* (* ?v_95 1001) (/ 1 1000))))))) (and ?v_96 (or (not (<= (* (* ?v_98 999) (/ 1 1000)) ?v_97)) (not (<= ?v_97 (* (* ?v_98 1001) (/ 1 1000))))))) (and ?v_99 (or (not (<= (* (* ?v_101 999) (/ 1 1000)) ?v_100)) (not (<= ?v_100 (* (* ?v_101 1001) (/ 1 1000))))))) (and ?v_102 (or (not (<= (* (* ?v_104 999) (/ 1 1000)) ?v_103)) (not (<= ?v_103 (* (* ?v_104 1001) (/ 1 1000))))))) (and ?v_105 (or (not (<= (* (* ?v_107 999) (/ 1 1000)) ?v_106)) (not (<= ?v_106 (* (* ?v_107 1001) (/ 1 1000))))))) (and ?v_108 (or (not (<= (* (* ?v_110 999) (/ 1 1000)) ?v_109)) (not (<= ?v_109 (* (* ?v_110 1001) (/ 1 1000))))))) (and (and ?v_93 ?v_123) (or (or (< x_53 x_21) (not (<= (* (* ?v_112 999) (/ 1 1000)) ?v_111))) (not (<= ?v_111 (* (* ?v_112 1001) (/ 1 1000))))))) (and (and ?v_96 ?v_127) (or (or (< x_53 x_24) (not (<= (* (* ?v_114 999) (/ 1 1000)) ?v_113))) (not (<= ?v_113 (* (* ?v_114 1001) (/ 1 1000))))))) (and (and ?v_99 ?v_131) (or (or (< x_53 x_27) (not (<= (* (* ?v_116 999) (/ 1 1000)) ?v_115))) (not (<= ?v_115 (* (* ?v_116 1001) (/ 1 1000))))))) (and (and ?v_102 ?v_135) (or (or (< x_53 x_30) (not (<= (* (* ?v_118 999) (/ 1 1000)) ?v_117))) (not (<= ?v_117 (* (* ?v_118 1001) (/ 1 1000))))))) (and (and ?v_105 ?v_139) (or (or (< x_53 x_33) (not (<= (* (* ?v_120 999) (/ 1 1000)) ?v_119))) (not (<= ?v_119 (* (* ?v_120 1001) (/ 1 1000))))))) (and (and ?v_108 ?v_143) (or (or (< x_53 x_16) (not (<= (* (* ?v_122 999) (/ 1 1000)) ?v_121))) (not (<= ?v_121 (* (* ?v_122 1001) (/ 1 1000))))))) (and ?v_147 (or (not (<= x_34 (+ (+ (* (* (+ (+ (+ x_91 (* ?v_125 (/ 1 999))) x_96) (* ?v_126 (/ 1 999))) 1) (/ 1 2)) x_52) (/ 3001 1998)))) (< x_34 (- (- (* (* (+ (+ (+ x_91 (* ?v_125 (/ 1 1001))) x_96) (* ?v_126 (/ 1 1001))) 1) (/ 1 2)) x_52) (/ 1 2)))))) (and ?v_150 (or (not (<= x_35 (+ (+ (* (* (+ (+ (+ x_91 (* ?v_129 (/ 1 999))) x_96) (* ?v_130 (/ 1 999))) 1) (/ 1 2)) x_52) (/ 3001 1998)))) (< x_35 (- (- (* (* (+ (+ (+ x_91 (* ?v_129 (/ 1 1001))) x_96) (* ?v_130 (/ 1 1001))) 1) (/ 1 2)) x_52) (/ 1 2)))))) (and ?v_153 (or (not (<= x_36 (+ (+ (* (* (+ (+ (+ x_91 (* ?v_133 (/ 1 999))) x_96) (* ?v_134 (/ 1 999))) 1) (/ 1 2)) x_52) (/ 3001 1998)))) (< x_36 (- (- (* (* (+ (+ (+ x_91 (* ?v_133 (/ 1 1001))) x_96) (* ?v_134 (/ 1 1001))) 1) (/ 1 2)) x_52) (/ 1 2)))))) (and ?v_156 (or (not (<= x_37 (+ (+ (* (* (+ (+ (+ x_91 (* ?v_137 (/ 1 999))) x_96) (* ?v_138 (/ 1 999))) 1) (/ 1 2)) x_52) (/ 3001 1998)))) (< x_37 (- (- (* (* (+ (+ (+ x_91 (* ?v_137 (/ 1 1001))) x_96) (* ?v_138 (/ 1 1001))) 1) (/ 1 2)) x_52) (/ 1 2)))))) (and ?v_159 (or (not (<= x_38 (+ (+ (* (* (+ (+ (+ x_91 (* ?v_141 (/ 1 999))) x_96) (* ?v_142 (/ 1 999))) 1) (/ 1 2)) x_52) (/ 3001 1998)))) (< x_38 (- (- (* (* (+ (+ (+ x_91 (* ?v_141 (/ 1 1001))) x_96) (* ?v_142 (/ 1 1001))) 1) (/ 1 2)) x_52) (/ 1 2)))))) (and ?v_162 (or (not (<= x_39 (+ (+ (* (* (+ (+ (+ x_91 (* ?v_145 (/ 1 999))) x_96) (* ?v_146 (/ 1 999))) 1) (/ 1 2)) x_52) (/ 3001 1998)))) (< x_39 (- (- (* (* (+ (+ (+ x_91 (* ?v_145 (/ 1 1001))) x_96) (* ?v_146 (/ 1 1001))) 1) (/ 1 2)) x_52) (/ 1 2)))))) (and ?v_147 (or (not (<= (* (* ?v_149 999) (/ 1 1000)) ?v_148)) (not (<= ?v_148 (* (* ?v_149 1001) (/ 1 1000))))))) (and ?v_150 (or (not (<= (* (* ?v_152 999) (/ 1 1000)) ?v_151)) (not (<= ?v_151 (* (* ?v_152 1001) (/ 1 1000))))))) (and ?v_153 (or (not (<= (* (* ?v_155 999) (/ 1 1000)) ?v_154)) (not (<= ?v_154 (* (* ?v_155 1001) (/ 1 1000))))))) (and ?v_156 (or (not (<= (* (* ?v_158 999) (/ 1 1000)) ?v_157)) (not (<= ?v_157 (* (* ?v_158 1001) (/ 1 1000))))))) (and ?v_159 (or (not (<= (* (* ?v_161 999) (/ 1 1000)) ?v_160)) (not (<= ?v_160 (* (* ?v_161 1001) (/ 1 1000))))))) (and ?v_162 (or (not (<= (* (* ?v_164 999) (/ 1 1000)) ?v_163)) (not (<= ?v_163 (* (* ?v_164 1001) (/ 1 1000))))))) (and ?v_124 (not (= x_19 (+ x_34 x_8))))) (and ?v_128 (not (= x_22 (+ x_35 x_8))))) (and ?v_132 (not (= x_25 (+ x_36 x_8))))) (and ?v_136 (not (= x_28 (+ x_37 x_8))))) (and ?v_140 (not (= x_31 (+ x_38 x_8))))) (and ?v_144 (not (= x_18 (+ x_39 x_8))))) (and ?v_124 (or (not (<= ?v_166 ?v_165)) (not (<= ?v_165 ?v_168))))) (and ?v_128 (or (not (<= ?v_166 ?v_167)) (not (<= ?v_167 ?v_168))))) (and ?v_132 (or (not (<= ?v_166 ?v_169)) (not (<= ?v_169 ?v_168))))) (and ?v_136 (or (not (<= ?v_166 ?v_170)) (not (<= ?v_170 ?v_168))))) (and ?v_140 (or (not (<= ?v_166 ?v_171)) (not (<= ?v_171 ?v_168))))) (and ?v_144 (or (not (<= ?v_166 ?v_172)) (not (<= ?v_172 ?v_168))))) ?v_173) ?v_173) ?v_173) ?v_173) ?v_173) ?v_173) ?v_174) ?v_174) ?v_174) ?v_174) ?v_174) ?v_174) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_175) ?v_177) ?v_177) ?v_177) ?v_177) ?v_177) ?v_177) (and (and (and (and (and ?v_178 ?v_178) ?v_178) ?v_178) ?v_178) ?v_178)) (and ?v_179 (or (not (<= ?v_182 ?v_181)) (not (<= ?v_181 ?v_184))))) (and ?v_179 (or (not (<= ?v_182 ?v_183)) (not (<= ?v_183 ?v_184))))) (and ?v_179 (or (not (<= ?v_182 ?v_185)) (not (<= ?v_185 ?v_184))))) (and ?v_179 (or (not (<= ?v_182 ?v_186)) (not (<= ?v_186 ?v_184))))) (and ?v_179 (or (not (<= ?v_182 ?v_187)) (not (<= ?v_187 ?v_184))))) (and ?v_179 (or (not (<= ?v_182 ?v_188)) (not (<= ?v_188 ?v_184))))) (and ?v_191 (or (or ?v_192 (not (<= ?v_193 ?v_189))) (not (<= ?v_189 ?v_195))))) (and ?v_191 (or (or ?v_192 (not (<= ?v_193 ?v_194))) (not (<= ?v_194 ?v_195))))) (and ?v_191 (or (or ?v_192 (not (<= ?v_193 ?v_196))) (not (<= ?v_196 ?v_195))))) (and ?v_191 (or (or ?v_192 (not (<= ?v_193 ?v_197))) (not (<= ?v_197 ?v_195))))) (and ?v_191 (or (or ?v_192 (not (<= ?v_193 ?v_198))) (not (<= ?v_198 ?v_195))))) (and ?v_191 (or (or ?v_192 (not (<= ?v_193 ?v_199))) (not (<= ?v_199 ?v_195))))) ?v_204) ?v_204) ?v_204) ?v_204) ?v_204) ?v_204) (and ?v_205 (or (not (<= ?v_208 ?v_206)) (not (<= ?v_206 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_209)) (not (<= ?v_209 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_211)) (not (<= ?v_211 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_212)) (not (<= ?v_212 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_213)) (not (<= ?v_213 ?v_210))))) (and ?v_205 (or (not (<= ?v_208 ?v_214)) (not (<= ?v_214 ?v_210))))) ?v_216) ?v_216) ?v_216) ?v_216) ?v_216) ?v_216) ?v_218) ?v_218) ?v_218) ?v_218) ?v_218) ?v_218))))))))))))))))))))))))))
(check-sat)
(exit)