# solving
c Min unsat cost LB: 1, ts: 1.6041, CS: 1
c Min unsat cost LB: 2, ts: 1.6201, CS: 1
c Min unsat cost LB: 3, ts: 1.6321, CS: 1
c Min unsat cost LB: 4, ts: 1.6521, CS: 3
c Min unsat cost LB: 5, ts: 1.6681, CS: 1
c Min unsat cost LB: 6, ts: 1.6841, CS: 1
c Min unsat cost LB: 7, ts: 1.70011, CS: 1
c Min unsat cost LB: 8, ts: 1.72011, CS: 1
c Min unsat cost LB: 9, ts: 1.73611, CS: 1
c Min unsat cost LB: 10, ts: 1.75211, CS: 1
c Min unsat cost LB: 11, ts: 1.76811, CS: 1
c Min unsat cost LB: 12, ts: 1.78811, CS: 1
c Min unsat cost LB: 13, ts: 1.80411, CS: 2
c Min unsat cost LB: 14, ts: 1.82011, CS: 1
c Min unsat cost LB: 15, ts: 1.83611, CS: 2
c Min unsat cost LB: 16, ts: 1.85612, CS: 1
c Min unsat cost LB: 17, ts: 1.87212, CS: 1
c Min unsat cost LB: 18, ts: 1.88812, CS: 1
c Min unsat cost LB: 19, ts: 1.90412, CS: 1
c Min unsat cost LB: 20, ts: 1.92012, CS: 1
c Min unsat cost LB: 21, ts: 1.93612, CS: 1
c Min unsat cost LB: 22, ts: 1.95212, CS: 1
c Min unsat cost LB: 23, ts: 1.97212, CS: 1
c Min unsat cost LB: 24, ts: 1.98812, CS: 1
c Min unsat cost LB: 25, ts: 2.01613, CS: 1
c SAT found, ts: 2.06013
c Min unsat cost LB: 1, ts: 2.10413, CS: 1
c Min unsat cost LB: 2, ts: 2.13213, CS: 1
c Min unsat cost LB: 3, ts: 2.15213, CS: 3
c Min unsat cost LB: 4, ts: 2.17614, CS: 4
c Min unsat cost LB: 5, ts: 2.20014, CS: 3
c Min unsat cost LB: 6, ts: 2.22014, CS: 4
c Min unsat cost LB: 7, ts: 2.24414, CS: 3
c Min unsat cost LB: 8, ts: 2.26814, CS: 1
c Min unsat cost LB: 9, ts: 2.28814, CS: 1
c Min unsat cost LB: 10, ts: 2.31214, CS: 1
c Min unsat cost LB: 11, ts: 2.33615, CS: 3
c Min unsat cost LB: 12, ts: 2.35615, CS: 1
c Min unsat cost LB: 13, ts: 2.38015, CS: 3
c Min unsat cost LB: 14, ts: 2.40415, CS: 1
c Min unsat cost LB: 15, ts: 2.42815, CS: 3
c Min unsat cost LB: 16, ts: 2.45215, CS: 4
c Min unsat cost LB: 17, ts: 2.47215, CS: 2
c Min unsat cost LB: 18, ts: 2.49616, CS: 8
c Min unsat cost LB: 19, ts: 2.52016, CS: 4
c Min unsat cost LB: 20, ts: 2.54016, CS: 1
c Min unsat cost LB: 21, ts: 2.56016, CS: 4
c Min unsat cost LB: 22, ts: 2.58416, CS: 11
c Min unsat cost LB: 23, ts: 2.61216, CS: 3
c Min unsat cost LB: 24, ts: 2.63216, CS: 9
c Min unsat cost LB: 25, ts: 2.65617, CS: 1
c Min unsat cost LB: 26, ts: 2.68017, CS: 7
c Min unsat cost LB: 27, ts: 2.70017, CS: 1
c Min unsat cost LB: 28, ts: 2.72417, CS: 6
c Min unsat cost LB: 29, ts: 2.75217, CS: 13
c Min unsat cost LB: 30, ts: 2.77217, CS: 4
c Min unsat cost LB: 31, ts: 2.79617, CS: 4
c Min unsat cost LB: 32, ts: 2.82018, CS: 1
c Min unsat cost LB: 33, ts: 2.84418, CS: 1
c Min unsat cost LB: 34, ts: 2.86818, CS: 1
c Min unsat cost LB: 35, ts: 2.89218, CS: 1
c Min unsat cost LB: 36, ts: 2.91618, CS: 1
c Min unsat cost LB: 37, ts: 2.93618, CS: 2
c Min unsat cost LB: 38, ts: 2.96019, CS: 1
c Min unsat cost LB: 39, ts: 2.98419, CS: 4
c Min unsat cost LB: 40, ts: 3.00819, CS: 15
c Min unsat cost LB: 41, ts: 3.03219, CS: 7
c Min unsat cost LB: 42, ts: 3.05619, CS: 1
c Min unsat cost LB: 43, ts: 3.08019, CS: 4
c Min unsat cost LB: 44, ts: 3.10419, CS: 1
c Min unsat cost LB: 45, ts: 3.12419, CS: 3
c Min unsat cost LB: 46, ts: 3.1482, CS: 4
c Min unsat cost LB: 47, ts: 3.1722, CS: 1
c Min unsat cost LB: 48, ts: 3.1962, CS: 11
c Min unsat cost LB: 49, ts: 3.2202, CS: 8
c Min unsat cost LB: 50, ts: 3.2442, CS: 7
c Min unsat cost LB: 51, ts: 3.2682, CS: 2
c Min unsat cost LB: 52, ts: 3.29221, CS: 1
c Min unsat cost LB: 53, ts: 3.31621, CS: 3
c Min unsat cost LB: 54, ts: 3.34021, CS: 7
c Min unsat cost LB: 55, ts: 3.36421, CS: 1
c Min unsat cost LB: 56, ts: 3.38821, CS: 1
c Min unsat cost LB: 57, ts: 3.41221, CS: 3
c Min unsat cost LB: 58, ts: 3.43621, CS: 1
c Min unsat cost LB: 59, ts: 3.46022, CS: 2
c Min unsat cost LB: 60, ts: 3.48422, CS: 1
c Min unsat cost LB: 61, ts: 3.50822, CS: 3
c Min unsat cost LB: 62, ts: 3.53222, CS: 4
c Min unsat cost LB: 63, ts: 3.55222, CS: 3
c Min unsat cost LB: 64, ts: 3.57222, CS: 1
c Min unsat cost LB: 65, ts: 3.59622, CS: 4
c Min unsat cost LB: 66, ts: 3.62023, CS: 1
c Min unsat cost LB: 67, ts: 3.64423, CS: 1
c Min unsat cost LB: 68, ts: 3.66823, CS: 1
c Min unsat cost LB: 69, ts: 3.69223, CS: 1
c Min unsat cost LB: 70, ts: 3.71623, CS: 2
c Min unsat cost LB: 71, ts: 3.74023, CS: 2
c Min unsat cost LB: 72, ts: 3.76424, CS: 11
c Min unsat cost LB: 73, ts: 3.78824, CS: 3
c Min unsat cost LB: 74, ts: 3.81224, CS: 1
c Min unsat cost LB: 75, ts: 3.84024, CS: 3
c Min unsat cost LB: 76, ts: 3.86024, CS: 5
c Min unsat cost LB: 77, ts: 3.88424, CS: 1
c Min unsat cost LB: 78, ts: 3.90824, CS: 1
c Min unsat cost LB: 79, ts: 3.93224, CS: 7
c Min unsat cost LB: 80, ts: 3.96025, CS: 3
c Min unsat cost LB: 81, ts: 3.98425, CS: 1
c Min unsat cost LB: 82, ts: 4.00825, CS: 2
c Min unsat cost LB: 83, ts: 4.03225, CS: 13
c Min unsat cost LB: 84, ts: 4.05625, CS: 1
c Min unsat cost LB: 85, ts: 4.08026, CS: 5
c Min unsat cost LB: 86, ts: 4.10426, CS: 1
c Min unsat cost LB: 87, ts: 4.13226, CS: 1
c Min unsat cost LB: 88, ts: 4.15626, CS: 3
c Min unsat cost LB: 89, ts: 4.18026, CS: 1
c Min unsat cost LB: 90, ts: 4.20026, CS: 1
c Min unsat cost LB: 91, ts: 4.22426, CS: 7
c Min unsat cost LB: 92, ts: 4.24826, CS: 1
c Min unsat cost LB: 93, ts: 4.27227, CS: 4
c Min unsat cost LB: 94, ts: 4.30027, CS: 2
c Min unsat cost LB: 95, ts: 4.32027, CS: 3
c Min unsat cost LB: 96, ts: 4.34027, CS: 2
c Min unsat cost LB: 97, ts: 4.36427, CS: 19
c Min unsat cost LB: 98, ts: 4.38827, CS: 20
c Min unsat cost LB: 99, ts: 4.41228, CS: 1
c Min unsat cost LB: 100, ts: 4.43628, CS: 2
c Min unsat cost LB: 101, ts: 4.46028, CS: 3
c Min unsat cost LB: 102, ts: 4.48428, CS: 4
c Min unsat cost LB: 103, ts: 4.50828, CS: 3
c Min unsat cost LB: 104, ts: 4.53228, CS: 1
c Min unsat cost LB: 105, ts: 4.55628, CS: 3
c Min unsat cost LB: 106, ts: 4.58029, CS: 6
c Min unsat cost LB: 107, ts: 4.60429, CS: 1
c Min unsat cost LB: 108, ts: 4.62829, CS: 3
c Min unsat cost LB: 109, ts: 4.65229, CS: 2
c Min unsat cost LB: 110, ts: 4.67629, CS: 9
c Min unsat cost LB: 111, ts: 4.70029, CS: 3
c SAT found, ts: 4.72429
# solving time:4.7483--1.5561s
# sol printing (4.7483)
# sol printed