# solving
c SAT found, ts: 1.6001
c Min unsat cost LB: 1, ts: 1.6441, CS: 1
c Min unsat cost LB: 2, ts: 1.6601, CS: 1
c Min unsat cost LB: 3, ts: 1.6761, CS: 1
c Min unsat cost LB: 4, ts: 1.69611, CS: 3
c Min unsat cost LB: 5, ts: 1.71611, CS: 2
c Min unsat cost LB: 6, ts: 1.73211, CS: 4
c Min unsat cost LB: 7, ts: 1.75211, CS: 1
c Min unsat cost LB: 8, ts: 1.77211, CS: 2
c Min unsat cost LB: 9, ts: 1.78811, CS: 1
c Min unsat cost LB: 10, ts: 1.80811, CS: 2
c Min unsat cost LB: 11, ts: 1.82811, CS: 1
c Min unsat cost LB: 12, ts: 1.84811, CS: 1
c Min unsat cost LB: 13, ts: 1.86812, CS: 2
c Min unsat cost LB: 14, ts: 1.88412, CS: 1
c Min unsat cost LB: 15, ts: 1.90412, CS: 4
c Min unsat cost LB: 16, ts: 1.92412, CS: 3
c SAT found, ts: 1.94812
# solving time:1.96412--1.52409s
# sol printing (1.96412)
# sol printed