menage

UnitTests/unsat/QF_LRA/clocksynchro_4clocks.main_invar.base.smt2

-(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)
-(assert (let ((?v_27 (= x_30 x_4)) (?v_40 (= x_32 x_1)) (?v_13 (= x_34 x_2)) (?v_20 (= x_35 x_3)) (?v_67 (= x_7 x_11))) (let ((?v_63 (not ?v_67)) (?v_62 (+ (+ x_11 x_5) x_6))) (let ((?v_88 (= x_7 ?v_62)) (?v_70 (= x_8 x_11))) (let ((?v_64 (not ?v_70)) (?v_92 (= x_8 ?v_62)) (?v_73 (= x_9 x_11))) (let ((?v_65 (not ?v_73)) (?v_96 (= x_9 ?v_62)) (?v_76 (= x_10 x_11))) (let ((?v_66 (not ?v_76)) (?v_100 (= x_10 ?v_62)) (?v_87 (not (<= x_33 x_11))) (?v_91 (not (<= x_28 x_11))) (?v_95 (not (<= x_29 x_11))) (?v_99 (not (<= x_31 x_11)))) (let ((?v_103 (or ?v_87 ?v_88)) (?v_106 (or ?v_91 ?v_92)) (?v_109 (or ?v_95 ?v_96)) (?v_112 (or ?v_99 ?v_100)) (?v_5 (= x_24 0)) (?v_14 (= x_25 0)) (?v_21 (= x_26 0)) (?v_28 (= x_27 0)) (?v_4 (= x_7 x_5)) (?v_15 (= x_8 x_5)) (?v_22 (= x_9 x_5)) (?v_29 (= x_10 x_5)) (?v_41 (= x_33 1)) (?v_16 (= x_28 1)) (?v_23 (= x_29 1)) (?v_30 (= x_31 1)) (?v_10 (= x_15 0)) (?v_17 (= x_18 0)) (?v_24 (= x_21 0)) (?v_31 (= x_14 0)) (?v_9 (= x_16 0)) (?v_18 (= x_19 0)) (?v_25 (= x_22 0)) (?v_32 (= x_13 0)) (?v_11 (= x_17 0)) (?v_19 (= x_20 0)) (?v_26 (= x_23 0)) (?v_33 (= x_12 0)) (?v_6 (= 1 x_5)) (?v_3 (+ 1 1))) (let ((?v_8 (= x_33 ?v_3)) (?v_7 (= (+ x_5 x_6) 1))) (let ((?v_12 (and (not ?v_6) (not ?v_7))) (?v_39 (= x_28 ?v_3)) (?v_43 (= x_29 ?v_3)) (?v_45 (= x_31 ?v_3)) (?v_54 (+ x_0 x_5))) (let ((?v_55 (<= x_7 ?v_54)) (?v_56 (<= x_8 ?v_54)) (?v_57 (<= x_9 ?v_54)) (?v_58 (<= x_10 ?v_54)) (?v_121 (not (<= (- ?v_54 x_64) 1))) (?v_122 (not (>= (- ?v_54 x_65) 1))) (?v_128 (- 1 1))) (let ((?v_123 (not (<= ?v_128 x_63))) (?v_127 (= x_5 ?v_54))) (let ((?v_126 (not ?v_127)) (?v_124 (+ (+ ?v_54 x_5) x_6))) (let ((?v_145 (= x_5 ?v_124))) (let ((?v_125 (and (or ?v_126 (not (>= (+ ?v_54 x_6) 1))) (not ?v_145))) (?v_144 (not (>= ?v_54 1)))) (let ((?v_137 (and ?v_127 ?v_144)) (?v_138 (< x_0 0)) (?v_149 (or ?v_144 ?v_145)) (?v_150 (- 0 x_1))) (let ((?v_146 (* ?v_150 1000)) (?v_156 (- 0 x_4))) (let ((?v_147 (* ?v_156 1000)) (?v_157 (+ 0 x_6))) (let ((?v_158 (and ?v_145 (not (= ?v_157 0)))) (?v_159 (- 0 0)) (?v_2 (* x_24 2)) (?v_34 (- ?v_3 1)) (?v_36 (+ ?v_3 1)) (?v_37 (+ ?v_157 1)) (?v_38 (+ (+ x_5 x_5) x_6)) (?v_35 (* x_25 2)) (?v_42 (* x_26 2)) (?v_44 (* x_27 2)) (?v_46 (- x_33 x_36)) (?v_47 (- x_28 x_36)) (?v_48 (- x_29 x_36)) (?v_49 (- x_31 x_36)) (?v_50 (+ x_33 x_36)) (?v_51 (+ x_28 x_36)) (?v_52 (+ x_29 x_36)) (?v_53 (+ x_31 x_36)) (?v_59 (- x_11 x_64)) (?v_60 (- x_11 x_65)) (?v_61 (+ x_11 x_6)) (?v_68 (- x_32 x_59)) (?v_69 (- x_33 x_55)) (?v_71 (- x_34 x_60)) (?v_72 (- x_28 x_56)) (?v_74 (- x_35 x_61)) (?v_75 (- x_29 x_57)) (?v_77 (- x_30 x_62)) (?v_78 (- x_31 x_58)) (?v_79 (- x_32 x_17)) (?v_80 (- x_33 x_11)) (?v_81 (- x_34 x_20)) (?v_82 (- x_28 x_11)) (?v_83 (- x_35 x_23)) (?v_84 (- x_29 x_11)) (?v_85 (- x_30 x_12)) (?v_86 (- x_31 x_11)) (?v_104 (- x_17 x_59))) (let ((?v_89 (* ?v_104 1000)) (?v_90 (* (- x_17 x_62) 1000)) (?v_93 (* (- x_20 x_59) 1000)) (?v_94 (* (- x_20 x_62) 1000)) (?v_97 (* (- x_23 x_59) 1000)) (?v_98 (* (- x_23 x_62) 1000)) (?v_101 (* (- x_12 x_59) 1000)) (?v_113 (- x_12 x_62))) (let ((?v_102 (* ?v_113 1000)) (?v_105 (- x_11 x_55)) (?v_107 (- x_20 x_60)) (?v_108 (- x_11 x_56)) (?v_110 (- x_23 x_61)) (?v_111 (- x_11 x_57)) (?v_114 (- x_11 x_58)) (?v_115 (- x_16 x_17)) (?v_117 (- x_19 x_20)) (?v_119 (- x_22 x_23)) (?v_120 (- x_13 x_12)) (?v_129 (- x_1 x_1)) (?v_131 (- x_2 x_2)) (?v_133 (- x_3 x_3)) (?v_134 (- x_4 x_4)) (?v_135 (- x_1 0)) (?v_136 (- 1 ?v_54)) (?v_140 (- x_2 0)) (?v_142 (- x_3 0)) (?v_143 (- x_4 0)) (?v_151 (- ?v_54 1)) (?v_153 (- 0 x_2)) (?v_155 (- 0 x_3)) (?v_0 (+ x_0 (/ 999 1000))) (?v_1 (+ x_0 (/ 1001 1000))) (?v_116 (* (* x_6 999) (/ 1 1000))) (?v_118 (* (* x_6 1001) (/ 1 1000))) (?v_130 (* (* ?v_128 999) (/ 1 1000))) (?v_132 (* (* ?v_128 1001) (/ 1 1000)))) (let ((?v_139 (* (* ?v_136 999) (/ 1 1000))) (?v_141 (* (* ?v_136 1001) (/ 1 1000))) (?v_148 (and ?v_149 (or (not (>= (+ (+ (* (* (+ (+ (+ 1 (* ?v_146 (/ 1 999))) 1) (* ?v_147 (/ 1 999))) 1) (/ 1 2)) x_36) (/ 3001 1998)) 0)) (> (- (- (* (* (+ (+ (+ 1 (* ?v_146 (/ 1 1001))) 1) (* ?v_147 (/ 1 1001))) 1) (/ 1 2)) x_36) (/ 1 2)) 0)))) (?v_152 (* (* ?v_151 999) (/ 1 1000))) (?v_154 (* (* ?v_151 1001) (/ 1 1000))) (?v_160 (and ?v_145 (or (not (<= ?v_116 ?v_159)) (not (<= ?v_159 ?v_118)))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (<= x_5 0)) (not (<= x_6 0))) (not (<= x_36 0))) (not (< x_63 (+ x_36 (* (* (+ (* (* x_6 1) (/ 1 2)) 1) 1001) (/ 1 999)))))) (< x_64 (- (* (* (- (- x_6 x_63) 1) 999) (/ 1 2)) 1))) (not (< x_64 (* (* (+ (+ (+ x_5 x_36) x_63) (/ 1501 1000)) 1001) (/ 1 999))))) (not (<= x_65 0))) (<= x_65 (- x_5 (+ (+ x_36 (* (* (+ x_6 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)) (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 (< x_0 x_1) (< x_0 x_2)) (< x_0 x_3)) (< x_0 x_4)) (< x_0 x_37)) (<= x_37 x_1)) (<= x_37 x_2)) (<= x_37 x_3)) (<= x_37 x_4)) (or (or (or (= x_37 x_1) (= x_37 x_2)) (= x_37 x_3)) (= x_37 x_4))) ?v_40) ?v_13) ?v_20) ?v_27) ?v_5) ?v_14) ?v_21) ?v_28) ?v_4) ?v_15) ?v_22) ?v_29) ?v_41) ?v_16) ?v_23) ?v_30) ?v_10) ?v_17) ?v_24) ?v_31) ?v_9) ?v_18) ?v_25) ?v_32) ?v_11) ?v_19) ?v_26) ?v_33) (= x_38 1)) (= x_39 1)) (= x_40 1)) (= x_41 1)) (= x_42 1)) (= x_43 1)) (= x_44 1)) (= x_45 1)) (= x_46 1)) (= x_47 1)) (= x_48 1)) (= x_49 1)) (= x_50 1)) (= x_51 1)) (= x_52 1)) (= x_53 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 (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 (= x_0 x_1) (<= ?v_0 x_32)) (<= x_32 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_34 ?v_2)) (<= ?v_2 ?v_36)) ?v_8) ?v_4) (and (and (and ?v_7 (= x_33 ?v_37)) (= x_7 ?v_38)) ?v_5)) (and (and (and ?v_12 ?v_8) ?v_5) ?v_4))) (or (or (and (and (and ?v_6 (= x_17 x_0)) ?v_9) ?v_10) (and (and (and ?v_7 (= x_16 x_0)) (= x_15 (- x_33 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) (and (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_34)) (<= x_34 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_34 ?v_35)) (<= ?v_35 ?v_36)) ?v_39) ?v_15) (and (and (and ?v_7 (= x_28 ?v_37)) (= x_8 ?v_38)) ?v_14)) (and (and (and ?v_12 ?v_39) ?v_14) ?v_15))) (or (or (and (and (and ?v_6 (= x_20 x_0)) ?v_18) ?v_17) (and (and (and ?v_7 (= x_19 x_0)) (= x_18 (- x_28 1))) ?v_19)) (and (and (and ?v_12 ?v_19) ?v_18) ?v_17))) ?v_40) ?v_5) ?v_4) ?v_41) ?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)) (and (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_35)) (<= x_35 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_34 ?v_42)) (<= ?v_42 ?v_36)) ?v_43) ?v_22) (and (and (and ?v_7 (= x_29 ?v_37)) (= x_9 ?v_38)) ?v_21)) (and (and (and ?v_12 ?v_43) ?v_21) ?v_22))) (or (or (and (and (and ?v_6 (= x_23 x_0)) ?v_25) ?v_24) (and (and (and ?v_7 (= x_22 x_0)) (= x_21 (- x_29 1))) ?v_26)) (and (and (and ?v_12 ?v_26) ?v_25) ?v_24))) ?v_40) ?v_5) ?v_4) ?v_41) ?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)) (and (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_30)) (<= x_30 ?v_1)) (or (or (and (and (and (and ?v_6 (<= ?v_34 ?v_44)) (<= ?v_44 ?v_36)) ?v_45) ?v_29) (and (and (and ?v_7 (= x_31 ?v_37)) (= x_10 ?v_38)) ?v_28)) (and (and (and ?v_12 ?v_45) ?v_28) ?v_29))) (or (or (and (and (and ?v_6 (= x_12 x_0)) ?v_32) ?v_31) (and (and (and ?v_7 (= x_13 x_0)) (= x_14 (- x_31 1))) ?v_33)) (and (and (and ?v_12 ?v_33) ?v_32) ?v_31))) ?v_40) ?v_5) ?v_4) ?v_41) ?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_46 x_38)) (<= ?v_46 x_42)) (<= ?v_46 x_46)) (<= ?v_46 x_50)) (<= ?v_47 x_39)) (<= ?v_47 x_43)) (<= ?v_47 x_47)) (<= ?v_47 x_51)) (<= ?v_48 x_40)) (<= ?v_48 x_44)) (<= ?v_48 x_48)) (<= ?v_48 x_52)) (<= ?v_49 x_41)) (<= ?v_49 x_45)) (<= ?v_49 x_49)) (<= ?v_49 x_53)) (<= x_38 ?v_50)) (<= x_42 ?v_50)) (<= x_46 ?v_50)) (<= x_50 ?v_50)) (<= x_39 ?v_51)) (<= x_43 ?v_51)) (<= x_47 ?v_51)) (<= x_51 ?v_51)) (<= x_40 ?v_52)) (<= x_44 ?v_52)) (<= x_48 ?v_52)) (<= x_52 ?v_52)) (<= x_41 ?v_53)) (<= x_45 ?v_53)) (<= x_49 ?v_53)) (<= x_53 ?v_53)) (= x_37 x_0)))) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (not ?v_55) (not ?v_56)) (not ?v_57)) (not ?v_58)) (= x_54 x_37)) (= x_55 x_33)) (= x_56 x_28)) (= x_57 x_29)) (= x_58 x_31)) (= x_59 x_32)) (= x_60 x_34)) (= x_61 x_35)) (= x_62 x_30)) (= x_11 ?v_124)) (and (and (and (and (and (and (and (and (and (and (or (or (or ?v_55 ?v_56) ?v_57) ?v_58) (= x_11 ?v_54)) (= x_54 x_0)) (= x_59 x_1)) (= x_60 x_2)) (= x_61 x_3)) (= x_62 x_4)) (= x_55 1)) (= x_56 1)) (= x_57 1)) (= x_58 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 (not (<= ?v_59 x_55)) (not (<= ?v_59 x_56))) (not (<= ?v_59 x_57))) (not (<= ?v_59 x_58))) (not (<= x_55 ?v_60))) (not (<= x_56 ?v_60))) (not (<= x_57 ?v_60))) (not (<= x_58 ?v_60))) (not (<= (- x_55 x_55) x_63))) (not (<= (- x_56 x_55) x_63))) (not (<= (- x_57 x_55) x_63))) (not (<= (- x_58 x_55) x_63))) (not (<= (- x_55 x_56) x_63))) (not (<= (- x_56 x_56) x_63))) (not (<= (- x_57 x_56) x_63))) (not (<= (- x_58 x_56) x_63))) (not (<= (- x_55 x_57) x_63))) (not (<= (- x_56 x_57) x_63))) (not (<= (- x_57 x_57) x_63))) (not (<= (- x_58 x_57) x_63))) (not (<= (- x_55 x_58) x_63))) (not (<= (- x_56 x_58) x_63))) (not (<= (- x_57 x_58) x_63))) (not (<= (- x_58 x_58) x_63))) (and (or ?v_63 (not (<= x_33 ?v_61))) (not ?v_88))) (and (or ?v_64 (not (<= x_28 ?v_61))) (not ?v_92))) (and (or ?v_65 (not (<= x_29 ?v_61))) (not ?v_96))) (and (or ?v_66 (not (<= x_31 ?v_61))) (not ?v_100))) (and (and (and ?v_63 ?v_64) ?v_65) ?v_66)) (and ?v_67 (or (not (<= (* (* ?v_69 999) (/ 1 1000)) ?v_68)) (not (<= ?v_68 (* (* ?v_69 1001) (/ 1 1000))))))) (and ?v_70 (or (not (<= (* (* ?v_72 999) (/ 1 1000)) ?v_71)) (not (<= ?v_71 (* (* ?v_72 1001) (/ 1 1000))))))) (and ?v_73 (or (not (<= (* (* ?v_75 999) (/ 1 1000)) ?v_74)) (not (<= ?v_74 (* (* ?v_75 1001) (/ 1 1000))))))) (and ?v_76 (or (not (<= (* (* ?v_78 999) (/ 1 1000)) ?v_77)) (not (<= ?v_77 (* (* ?v_78 1001) (/ 1 1000))))))) (and (and ?v_67 ?v_87) (or (or (< x_37 x_17) (not (<= (* (* ?v_80 999) (/ 1 1000)) ?v_79))) (not (<= ?v_79 (* (* ?v_80 1001) (/ 1 1000))))))) (and (and ?v_70 ?v_91) (or (or (< x_37 x_20) (not (<= (* (* ?v_82 999) (/ 1 1000)) ?v_81))) (not (<= ?v_81 (* (* ?v_82 1001) (/ 1 1000))))))) (and (and ?v_73 ?v_95) (or (or (< x_37 x_23) (not (<= (* (* ?v_84 999) (/ 1 1000)) ?v_83))) (not (<= ?v_83 (* (* ?v_84 1001) (/ 1 1000))))))) (and (and ?v_76 ?v_99) (or (or (< x_37 x_12) (not (<= (* (* ?v_86 999) (/ 1 1000)) ?v_85))) (not (<= ?v_85 (* (* ?v_86 1001) (/ 1 1000))))))) (and ?v_103 (or (not (<= x_24 (+ (+ (* (* (+ (+ (+ x_55 (* ?v_89 (/ 1 999))) x_58) (* ?v_90 (/ 1 999))) 1) (/ 1 2)) x_36) (/ 3001 1998)))) (< x_24 (- (- (* (* (+ (+ (+ x_55 (* ?v_89 (/ 1 1001))) x_58) (* ?v_90 (/ 1 1001))) 1) (/ 1 2)) x_36) (/ 1 2)))))) (and ?v_106 (or (not (<= x_25 (+ (+ (* (* (+ (+ (+ x_55 (* ?v_93 (/ 1 999))) x_58) (* ?v_94 (/ 1 999))) 1) (/ 1 2)) x_36) (/ 3001 1998)))) (< x_25 (- (- (* (* (+ (+ (+ x_55 (* ?v_93 (/ 1 1001))) x_58) (* ?v_94 (/ 1 1001))) 1) (/ 1 2)) x_36) (/ 1 2)))))) (and ?v_109 (or (not (<= x_26 (+ (+ (* (* (+ (+ (+ x_55 (* ?v_97 (/ 1 999))) x_58) (* ?v_98 (/ 1 999))) 1) (/ 1 2)) x_36) (/ 3001 1998)))) (< x_26 (- (- (* (* (+ (+ (+ x_55 (* ?v_97 (/ 1 1001))) x_58) (* ?v_98 (/ 1 1001))) 1) (/ 1 2)) x_36) (/ 1 2)))))) (and ?v_112 (or (not (<= x_27 (+ (+ (* (* (+ (+ (+ x_55 (* ?v_101 (/ 1 999))) x_58) (* ?v_102 (/ 1 999))) 1) (/ 1 2)) x_36) (/ 3001 1998)))) (< x_27 (- (- (* (* (+ (+ (+ x_55 (* ?v_101 (/ 1 1001))) x_58) (* ?v_102 (/ 1 1001))) 1) (/ 1 2)) x_36) (/ 1 2)))))) (and ?v_103 (or (not (<= (* (* ?v_105 999) (/ 1 1000)) ?v_104)) (not (<= ?v_104 (* (* ?v_105 1001) (/ 1 1000))))))) (and ?v_106 (or (not (<= (* (* ?v_108 999) (/ 1 1000)) ?v_107)) (not (<= ?v_107 (* (* ?v_108 1001) (/ 1 1000))))))) (and ?v_109 (or (not (<= (* (* ?v_111 999) (/ 1 1000)) ?v_110)) (not (<= ?v_110 (* (* ?v_111 1001) (/ 1 1000))))))) (and ?v_112 (or (not (<= (* (* ?v_114 999) (/ 1 1000)) ?v_113)) (not (<= ?v_113 (* (* ?v_114 1001) (/ 1 1000))))))) (and ?v_88 (not (= x_15 (+ x_24 x_6))))) (and ?v_92 (not (= x_18 (+ x_25 x_6))))) (and ?v_96 (not (= x_21 (+ x_26 x_6))))) (and ?v_100 (not (= x_14 (+ x_27 x_6))))) (and ?v_88 (or (not (<= ?v_116 ?v_115)) (not (<= ?v_115 ?v_118))))) (and ?v_92 (or (not (<= ?v_116 ?v_117)) (not (<= ?v_117 ?v_118))))) (and ?v_96 (or (not (<= ?v_116 ?v_119)) (not (<= ?v_119 ?v_118))))) (and ?v_100 (or (not (<= ?v_116 ?v_120)) (not (<= ?v_120 ?v_118))))) ?v_121) ?v_121) ?v_121) ?v_121) ?v_122) ?v_122) ?v_122) ?v_122) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_123) ?v_125) ?v_125) ?v_125) ?v_125) (and (and (and ?v_126 ?v_126) ?v_126) ?v_126)) (and ?v_127 (or (not (<= ?v_130 ?v_129)) (not (<= ?v_129 ?v_132))))) (and ?v_127 (or (not (<= ?v_130 ?v_131)) (not (<= ?v_131 ?v_132))))) (and ?v_127 (or (not (<= ?v_130 ?v_133)) (not (<= ?v_133 ?v_132))))) (and ?v_127 (or (not (<= ?v_130 ?v_134)) (not (<= ?v_134 ?v_132))))) (and ?v_137 (or (or ?v_138 (not (<= ?v_139 ?v_135))) (not (<= ?v_135 ?v_141))))) (and ?v_137 (or (or ?v_138 (not (<= ?v_139 ?v_140))) (not (<= ?v_140 ?v_141))))) (and ?v_137 (or (or ?v_138 (not (<= ?v_139 ?v_142))) (not (<= ?v_142 ?v_141))))) (and ?v_137 (or (or ?v_138 (not (<= ?v_139 ?v_143))) (not (<= ?v_143 ?v_141))))) ?v_148) ?v_148) ?v_148) ?v_148) (and ?v_149 (or (not (<= ?v_152 ?v_150)) (not (<= ?v_150 ?v_154))))) (and ?v_149 (or (not (<= ?v_152 ?v_153)) (not (<= ?v_153 ?v_154))))) (and ?v_149 (or (not (<= ?v_152 ?v_155)) (not (<= ?v_155 ?v_154))))) (and ?v_149 (or (not (<= ?v_152 ?v_156)) (not (<= ?v_156 ?v_154))))) ?v_158) ?v_158) ?v_158) ?v_158) ?v_160) ?v_160) ?v_160) ?v_160))))))))))))))))))))))))
-(check-sat)
-(exit)