(set-option :produce-models true)
(set-option :opt.solution_prefix foo)
(set-logic QF_LIA)
(declare-fun var_1 () Int)
(declare-fun var_2 () Int)
(declare-fun var_3 () Int)
(declare-fun var_4 () Int)
(declare-fun var_5 () Bool)
(declare-fun var_6 () Int)
(declare-fun var_7 () Int)
(declare-fun var_8 () Int)
(declare-fun var_9 () Bool)
(declare-fun var_10 () Int)
(declare-fun var_11 () Int)
(declare-fun var_12 () Int)
(declare-fun var_13 () Bool)
(declare-fun var_14 () Int)
(declare-fun var_15 () Int)
(declare-fun var_16 () Int)
(declare-fun var_17 () Int)
(declare-fun var_18 () Int)
(declare-fun var_19 () Bool)
(declare-fun var_20 () Int)
(declare-fun var_21 () Int)
(declare-fun var_22 () Int)
(declare-fun var_23 () Bool)
(declare-fun var_24 () Int)
(declare-fun var_25 () Int)
(declare-fun var_26 () Int)
(declare-fun var_27 () Bool)
(declare-fun var_28 () Int)
(declare-fun var_29 () Bool)
(declare-fun var_30 () Bool)
(declare-fun var_31 () Bool)
(declare-fun var_32 () Bool)
(declare-fun var_33 () Bool)
(declare-fun var_34 () Bool)
(declare-fun var_35 () Bool)
(declare-fun var_36 () Bool)
(declare-fun var_37 () Bool)
(declare-fun var_38 () Bool)
(declare-fun var_39 () Bool)
(declare-fun var_40 () Bool)
(declare-fun var_41 () Bool)
(declare-fun var_42 () Bool)
(declare-fun var_43 () Bool)
(declare-fun var_44 () Bool)
(declare-fun var_45 () Bool)
(declare-fun var_46 () Bool)
(declare-fun var_47 () Bool)
(declare-fun var_48 () Bool)
(declare-fun var_49 () Bool)
(declare-fun var_50 () Bool)
(declare-fun var_51 () Bool)
(declare-fun var_52 () Bool)
(declare-fun var_53 () Bool)
(declare-fun var_54 () Bool)
(declare-fun var_55 () Bool)
(declare-fun var_56 () Bool)
(declare-fun var_57 () Bool)
(declare-fun var_58 () Bool)
(declare-fun var_59 () Bool)
(declare-fun var_60 () Bool)
(declare-fun var_61 () Bool)
(declare-fun var_62 () Bool)
(declare-fun var_63 () Bool)
(declare-fun var_64 () Bool)
(declare-fun var_65 () Bool)
(declare-fun var_66 () Bool)
(declare-fun var_67 () Bool)
(declare-fun var_68 () Bool)
(declare-fun var_69 () Bool)
(declare-fun var_70 () Bool)
(declare-fun var_71 () Bool)
(declare-fun var_72 () Bool)
(declare-fun var_73 () Bool)
(declare-fun var_74 () Bool)
(declare-fun var_75 () Bool)
(declare-fun var_76 () Bool)
(declare-fun var_77 () Bool)
(declare-fun var_78 () Bool)
(declare-fun var_79 () Bool)
(declare-fun var_80 () Bool)
(declare-fun var_81 () Bool)
(declare-fun var_82 () Bool)
(declare-fun var_83 () Bool)
(declare-fun var_84 () Bool)
(declare-fun var_85 () Bool)
(declare-fun var_86 () Bool)
(declare-fun var_87 () Bool)
(declare-fun var_88 () Bool)
(declare-fun var_89 () Bool)
(declare-fun var_90 () Bool)
(declare-fun var_91 () Bool)
(declare-fun var_92 () Bool)
(declare-fun var_93 () Bool)
(declare-fun var_94 () Bool)
(declare-fun var_95 () Bool)
(declare-fun var_96 () Bool)
(declare-fun var_97 () Bool)
(declare-fun var_98 () Bool)
(declare-fun var_99 () Bool)
(declare-fun var_100 () Bool)
(declare-fun var_101 () Bool)
(declare-fun var_102 () Bool)
(declare-fun var_103 () Bool)
(declare-fun var_104 () Bool)
(declare-fun var_105 () Bool)
(declare-fun var_106 () Bool)
(declare-fun var_107 () Bool)
(declare-fun var_108 () Bool)
(declare-fun var_109 () Bool)
(declare-fun var_110 () Bool)
(declare-fun var_111 () Bool)
(declare-fun var_112 () Bool)
(declare-fun var_113 () Bool)
(declare-fun var_114 () Bool)
(declare-fun var_115 () Bool)
(declare-fun var_116 () Bool)
(declare-fun var_117 () Bool)
(declare-fun var_118 () Bool)
(assert (and (and (>= var_2 1440) (and (<= var_2 2300) (and (>= var_1 6000) (<= var_1 24150)))) (and (>= var_16 1440) (and (<= var_16 2300) (and (>= var_15 6000) (<= var_15 24150))))))
(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (=> var_29 (= var_4 615)) (=> var_35 (= var_4 615))) (=> var_41 (= var_4 615))) (=> var_47 (= var_4 615))) (=> var_53 (= var_4 615))) (=> var_59 (= var_4 615))) (=> var_65 (= var_4 615))) (=> var_71 (= var_4 615))) (=> var_77 (= var_4 615))) (=> var_83 (= var_4 615))) (=> var_89 (= var_4 615))) (=> var_95 (= var_4 615))) (=> var_101 (= var_4 615))) (=> var_107 (= var_4 615))) (=> var_113 (= var_4 615))) (=> var_30 (= var_8 615))) (=> var_36 (= var_8 615))) (=> var_42 (= var_8 615))) (=> var_48 (= var_8 615))) (=> var_54 (= var_8 615))) (=> var_60 (= var_8 615))) (=> var_66 (= var_8 615))) (=> var_72 (= var_8 615))) (=> var_78 (= var_8 615))) (=> var_84 (= var_8 615))) (=> var_90 (= var_8 615))) (=> var_96 (= var_8 615))) (=> var_102 (= var_8 615))) (=> var_108 (= var_8 615))) (=> var_114 (= var_8 615))) (=> var_31 (= var_12 615))) (=> var_37 (= var_12 615))) (=> var_43 (= var_12 615))) (=> var_49 (= var_12 615))) (=> var_55 (= var_12 615))) (=> var_61 (= var_12 615))) (=> var_67 (= var_12 615))) (=> var_73 (= var_12 615))) (=> var_79 (= var_12 615))) (=> var_85 (= var_12 615))) (=> var_91 (= var_12 615))) (=> var_97 (= var_12 615))) (=> var_103 (= var_12 615))) (=> var_109 (= var_12 615))) (=> var_115 (= var_12 615))) (=> var_32 (= var_18 615))) (=> var_38 (= var_18 615))) (=> var_44 (= var_18 615))) (=> var_50 (= var_18 615))) (=> var_56 (= var_18 615))) (=> var_62 (= var_18 615))) (=> var_68 (= var_18 615))) (=> var_74 (= var_18 615))) (=> var_80 (= var_18 615))) (=> var_86 (= var_18 615))) (=> var_92 (= var_18 615))) (=> var_98 (= var_18 615))) (=> var_104 (= var_18 615))) (=> var_110 (= var_18 615))) (=> var_116 (= var_18 615))) (=> var_33 (= var_22 615))) (=> var_39 (= var_22 615))) (=> var_45 (= var_22 615))) (=> var_51 (= var_22 615))) (=> var_57 (= var_22 615))) (=> var_63 (= var_22 615))) (=> var_69 (= var_22 615))) (=> var_75 (= var_22 615))) (=> var_81 (= var_22 615))) (=> var_87 (= var_22 615))) (=> var_93 (= var_22 615))) (=> var_99 (= var_22 615))) (=> var_105 (= var_22 615))) (=> var_111 (= var_22 615))) (=> var_117 (= var_22 615))) (=> var_34 (= var_26 615))) (=> var_40 (= var_26 615))) (=> var_46 (= var_26 615))) (=> var_52 (= var_26 615))) (=> var_58 (= var_26 615))) (=> var_64 (= var_26 615))) (=> var_70 (= var_26 615))) (=> var_76 (= var_26 615))) (=> var_82 (= var_26 615))) (=> var_88 (= var_26 615))) (=> var_94 (= var_26 615))) (=> var_100 (= var_26 615))) (=> var_106 (= var_26 615))) (=> var_112 (= var_26 615))) (=> var_118 (= var_26 615))))
(assert (and (and (and (=> (not var_5) (= var_1 var_3)) (=> (not var_9) (= var_1 var_7))) (=> (not var_13) (= var_1 var_11))) (and (and (=> (not var_19) (= var_15 var_17)) (=> (not var_23) (= var_15 var_21))) (=> (not var_27) (= var_15 var_25)))))
(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or var_29 var_30) var_31) var_32) var_33) var_34) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_29) (not var_30)) (or (not var_29) (not var_31))) (or (not var_29) (not var_32))) (or (not var_29) (not var_33))) (or (not var_29) (not var_34))) (or (not var_30) (not var_31))) (or (not var_30) (not var_32))) (or (not var_30) (not var_33))) (or (not var_30) (not var_34))) (or (not var_31) (not var_32))) (or (not var_31) (not var_33))) (or (not var_31) (not var_34))) (or (not var_32) (not var_33))) (or (not var_32) (not var_34))) (or (not var_33) (not var_34)))) (and (or (or (or (or (or var_35 var_36) var_37) var_38) var_39) var_40) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_35) (not var_36)) (or (not var_35) (not var_37))) (or (not var_35) (not var_38))) (or (not var_35) (not var_39))) (or (not var_35) (not var_40))) (or (not var_36) (not var_37))) (or (not var_36) (not var_38))) (or (not var_36) (not var_39))) (or (not var_36) (not var_40))) (or (not var_37) (not var_38))) (or (not var_37) (not var_39))) (or (not var_37) (not var_40))) (or (not var_38) (not var_39))) (or (not var_38) (not var_40))) (or (not var_39) (not var_40))))) (and (or (or (or (or (or var_41 var_42) var_43) var_44) var_45) var_46) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_41) (not var_42)) (or (not var_41) (not var_43))) (or (not var_41) (not var_44))) (or (not var_41) (not var_45))) (or (not var_41) (not var_46))) (or (not var_42) (not var_43))) (or (not var_42) (not var_44))) (or (not var_42) (not var_45))) (or (not var_42) (not var_46))) (or (not var_43) (not var_44))) (or (not var_43) (not var_45))) (or (not var_43) (not var_46))) (or (not var_44) (not var_45))) (or (not var_44) (not var_46))) (or (not var_45) (not var_46))))) (and (or (or (or (or (or var_47 var_48) var_49) var_50) var_51) var_52) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_47) (not var_48)) (or (not var_47) (not var_49))) (or (not var_47) (not var_50))) (or (not var_47) (not var_51))) (or (not var_47) (not var_52))) (or (not var_48) (not var_49))) (or (not var_48) (not var_50))) (or (not var_48) (not var_51))) (or (not var_48) (not var_52))) (or (not var_49) (not var_50))) (or (not var_49) (not var_51))) (or (not var_49) (not var_52))) (or (not var_50) (not var_51))) (or (not var_50) (not var_52))) (or (not var_51) (not var_52))))) (and (or (or (or (or (or var_53 var_54) var_55) var_56) var_57) var_58) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_53) (not var_54)) (or (not var_53) (not var_55))) (or (not var_53) (not var_56))) (or (not var_53) (not var_57))) (or (not var_53) (not var_58))) (or (not var_54) (not var_55))) (or (not var_54) (not var_56))) (or (not var_54) (not var_57))) (or (not var_54) (not var_58))) (or (not var_55) (not var_56))) (or (not var_55) (not var_57))) (or (not var_55) (not var_58))) (or (not var_56) (not var_57))) (or (not var_56) (not var_58))) (or (not var_57) (not var_58))))) (and (or (or (or (or (or var_59 var_60) var_61) var_62) var_63) var_64) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_59) (not var_60)) (or (not var_59) (not var_61))) (or (not var_59) (not var_62))) (or (not var_59) (not var_63))) (or (not var_59) (not var_64))) (or (not var_60) (not var_61))) (or (not var_60) (not var_62))) (or (not var_60) (not var_63))) (or (not var_60) (not var_64))) (or (not var_61) (not var_62))) (or (not var_61) (not var_63))) (or (not var_61) (not var_64))) (or (not var_62) (not var_63))) (or (not var_62) (not var_64))) (or (not var_63) (not var_64))))) (and (or (or (or (or (or var_65 var_66) var_67) var_68) var_69) var_70) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_65) (not var_66)) (or (not var_65) (not var_67))) (or (not var_65) (not var_68))) (or (not var_65) (not var_69))) (or (not var_65) (not var_70))) (or (not var_66) (not var_67))) (or (not var_66) (not var_68))) (or (not var_66) (not var_69))) (or (not var_66) (not var_70))) (or (not var_67) (not var_68))) (or (not var_67) (not var_69))) (or (not var_67) (not var_70))) (or (not var_68) (not var_69))) (or (not var_68) (not var_70))) (or (not var_69) (not var_70))))) (and (or (or (or (or (or var_71 var_72) var_73) var_74) var_75) var_76) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_71) (not var_72)) (or (not var_71) (not var_73))) (or (not var_71) (not var_74))) (or (not var_71) (not var_75))) (or (not var_71) (not var_76))) (or (not var_72) (not var_73))) (or (not var_72) (not var_74))) (or (not var_72) (not var_75))) (or (not var_72) (not var_76))) (or (not var_73) (not var_74))) (or (not var_73) (not var_75))) (or (not var_73) (not var_76))) (or (not var_74) (not var_75))) (or (not var_74) (not var_76))) (or (not var_75) (not var_76))))) (and (or (or (or (or (or var_77 var_78) var_79) var_80) var_81) var_82) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_77) (not var_78)) (or (not var_77) (not var_79))) (or (not var_77) (not var_80))) (or (not var_77) (not var_81))) (or (not var_77) (not var_82))) (or (not var_78) (not var_79))) (or (not var_78) (not var_80))) (or (not var_78) (not var_81))) (or (not var_78) (not var_82))) (or (not var_79) (not var_80))) (or (not var_79) (not var_81))) (or (not var_79) (not var_82))) (or (not var_80) (not var_81))) (or (not var_80) (not var_82))) (or (not var_81) (not var_82))))) (and (or (or (or (or (or var_83 var_84) var_85) var_86) var_87) var_88) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_83) (not var_84)) (or (not var_83) (not var_85))) (or (not var_83) (not var_86))) (or (not var_83) (not var_87))) (or (not var_83) (not var_88))) (or (not var_84) (not var_85))) (or (not var_84) (not var_86))) (or (not var_84) (not var_87))) (or (not var_84) (not var_88))) (or (not var_85) (not var_86))) (or (not var_85) (not var_87))) (or (not var_85) (not var_88))) (or (not var_86) (not var_87))) (or (not var_86) (not var_88))) (or (not var_87) (not var_88))))) (and (or (or (or (or (or var_89 var_90) var_91) var_92) var_93) var_94) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_89) (not var_90)) (or (not var_89) (not var_91))) (or (not var_89) (not var_92))) (or (not var_89) (not var_93))) (or (not var_89) (not var_94))) (or (not var_90) (not var_91))) (or (not var_90) (not var_92))) (or (not var_90) (not var_93))) (or (not var_90) (not var_94))) (or (not var_91) (not var_92))) (or (not var_91) (not var_93))) (or (not var_91) (not var_94))) (or (not var_92) (not var_93))) (or (not var_92) (not var_94))) (or (not var_93) (not var_94))))) (and (or (or (or (or (or var_95 var_96) var_97) var_98) var_99) var_100) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_95) (not var_96)) (or (not var_95) (not var_97))) (or (not var_95) (not var_98))) (or (not var_95) (not var_99))) (or (not var_95) (not var_100))) (or (not var_96) (not var_97))) (or (not var_96) (not var_98))) (or (not var_96) (not var_99))) (or (not var_96) (not var_100))) (or (not var_97) (not var_98))) (or (not var_97) (not var_99))) (or (not var_97) (not var_100))) (or (not var_98) (not var_99))) (or (not var_98) (not var_100))) (or (not var_99) (not var_100))))) (and (or (or (or (or (or var_101 var_102) var_103) var_104) var_105) var_106) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_101) (not var_102)) (or (not var_101) (not var_103))) (or (not var_101) (not var_104))) (or (not var_101) (not var_105))) (or (not var_101) (not var_106))) (or (not var_102) (not var_103))) (or (not var_102) (not var_104))) (or (not var_102) (not var_105))) (or (not var_102) (not var_106))) (or (not var_103) (not var_104))) (or (not var_103) (not var_105))) (or (not var_103) (not var_106))) (or (not var_104) (not var_105))) (or (not var_104) (not var_106))) (or (not var_105) (not var_106))))) (and (or (or (or (or (or var_107 var_108) var_109) var_110) var_111) var_112) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_107) (not var_108)) (or (not var_107) (not var_109))) (or (not var_107) (not var_110))) (or (not var_107) (not var_111))) (or (not var_107) (not var_112))) (or (not var_108) (not var_109))) (or (not var_108) (not var_110))) (or (not var_108) (not var_111))) (or (not var_108) (not var_112))) (or (not var_109) (not var_110))) (or (not var_109) (not var_111))) (or (not var_109) (not var_112))) (or (not var_110) (not var_111))) (or (not var_110) (not var_112))) (or (not var_111) (not var_112))))) (and (or (or (or (or (or var_113 var_114) var_115) var_116) var_117) var_118) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (not var_113) (not var_114)) (or (not var_113) (not var_115))) (or (not var_113) (not var_116))) (or (not var_113) (not var_117))) (or (not var_113) (not var_118))) (or (not var_114) (not var_115))) (or (not var_114) (not var_116))) (or (not var_114) (not var_117))) (or (not var_114) (not var_118))) (or (not var_115) (not var_116))) (or (not var_115) (not var_117))) (or (not var_115) (not var_118))) (or (not var_116) (not var_117))) (or (not var_116) (not var_118))) (or (not var_117) (not var_118))))))
(assert (and (and (and (and (and (and (= (not (or (or (or (or (or (or (or (or (or (or (or (or (or (or var_29 var_35) var_41) var_47) var_53) var_59) var_65) var_71) var_77) var_83) var_89) var_95) var_101) var_107) var_113)) var_5) (= var_5 (and (= var_4 0) (and (= var_6 0) (= var_3 0))))) (and (= (not (or (or (or (or (or (or (or (or (or (or (or (or (or (or var_30 var_36) var_42) var_48) var_54) var_60) var_66) var_72) var_78) var_84) var_90) var_96) var_102) var_108) var_114)) var_9) (= var_9 (and (= var_8 0) (and (= var_10 0) (= var_7 0)))))) (and (= (not (or (or (or (or (or (or (or (or (or (or (or (or (or (or var_31 var_37) var_43) var_49) var_55) var_61) var_67) var_73) var_79) var_85) var_91) var_97) var_103) var_109) var_115)) var_13) (= var_13 (and (= var_12 0) (and (= var_14 0) (= var_11 0)))))) (and (= (not (or (or (or (or (or (or (or (or (or (or (or (or (or (or var_32 var_38) var_44) var_50) var_56) var_62) var_68) var_74) var_80) var_86) var_92) var_98) var_104) var_110) var_116)) var_19) (= var_19 (and (= var_18 0) (and (= var_20 0) (= var_17 0)))))) (and (= (not (or (or (or (or (or (or (or (or (or (or (or (or (or (or var_33 var_39) var_45) var_51) var_57) var_63) var_69) var_75) var_81) var_87) var_93) var_99) var_105) var_111) var_117)) var_23) (= var_23 (and (= var_22 0) (and (= var_24 0) (= var_21 0)))))) (and (= (not (or (or (or (or (or (or (or (or (or (or (or (or (or (or var_34 var_40) var_46) var_52) var_58) var_64) var_70) var_76) var_82) var_88) var_94) var_100) var_106) var_112) var_118)) var_27) (= var_27 (and (= var_26 0) (and (= var_28 0) (= var_25 0)))))))
(assert (and (and (and (and (and (= var_3 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (ite var_29 4050 0) (ite var_35 4050 0)) (ite var_41 4050 0)) (ite var_47 4050 0)) (ite var_53 4050 0)) (ite var_59 4050 0)) (ite var_65 4050 0)) (ite var_71 4050 0)) (ite var_77 4050 0)) (ite var_83 4050 0)) (ite var_89 4050 0)) (ite var_95 4050 0)) (ite var_101 4050 0)) (ite var_107 4050 0)) (ite var_113 4050 0)) var_6)) (= var_7 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (ite var_30 4050 0) (ite var_36 4050 0)) (ite var_42 4050 0)) (ite var_48 4050 0)) (ite var_54 4050 0)) (ite var_60 4050 0)) (ite var_66 4050 0)) (ite var_72 4050 0)) (ite var_78 4050 0)) (ite var_84 4050 0)) (ite var_90 4050 0)) (ite var_96 4050 0)) (ite var_102 4050 0)) (ite var_108 4050 0)) (ite var_114 4050 0)) var_10))) (= var_11 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (ite var_31 4050 0) (ite var_37 4050 0)) (ite var_43 4050 0)) (ite var_49 4050 0)) (ite var_55 4050 0)) (ite var_61 4050 0)) (ite var_67 4050 0)) (ite var_73 4050 0)) (ite var_79 4050 0)) (ite var_85 4050 0)) (ite var_91 4050 0)) (ite var_97 4050 0)) (ite var_103 4050 0)) (ite var_109 4050 0)) (ite var_115 4050 0)) var_14))) (= var_17 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (ite var_32 4050 0) (ite var_38 4050 0)) (ite var_44 4050 0)) (ite var_50 4050 0)) (ite var_56 4050 0)) (ite var_62 4050 0)) (ite var_68 4050 0)) (ite var_74 4050 0)) (ite var_80 4050 0)) (ite var_86 4050 0)) (ite var_92 4050 0)) (ite var_98 4050 0)) (ite var_104 4050 0)) (ite var_110 4050 0)) (ite var_116 4050 0)) var_20))) (= var_21 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (ite var_33 4050 0) (ite var_39 4050 0)) (ite var_45 4050 0)) (ite var_51 4050 0)) (ite var_57 4050 0)) (ite var_63 4050 0)) (ite var_69 4050 0)) (ite var_75 4050 0)) (ite var_81 4050 0)) (ite var_87 4050 0)) (ite var_93 4050 0)) (ite var_99 4050 0)) (ite var_105 4050 0)) (ite var_111 4050 0)) (ite var_117 4050 0)) var_24))) (= var_25 (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (+ (ite var_34 4050 0) (ite var_40 4050 0)) (ite var_46 4050 0)) (ite var_52 4050 0)) (ite var_58 4050 0)) (ite var_64 4050 0)) (ite var_70 4050 0)) (ite var_76 4050 0)) (ite var_82 4050 0)) (ite var_88 4050 0)) (ite var_94 4050 0)) (ite var_100 4050 0)) (ite var_106 4050 0)) (ite var_112 4050 0)) (ite var_118 4050 0)) var_28))))
(assert (and (= var_2 (+ (+ var_4 var_8) var_12)) (= var_16 (+ (+ var_18 var_22) var_26))))
(assert (and (and (and (and (and (>= var_6 0) (>= var_10 0)) (>= var_14 0)) (>= var_20 0)) (>= var_24 0)) (>= var_28 0)))
(minimize (+ (+ (+ (+ (+ var_6 var_10) var_14) var_20) var_24) var_28))
(check-sat)
(get-model)