# solving
c SAT found, ts: 1.6761
c Min unsat cost LB: 1, ts: 1.74011, CS: 1
c Min unsat cost LB: 2, ts: 1.76811, CS: 1
c Min unsat cost LB: 3, ts: 1.80011, CS: 1
c Min unsat cost LB: 4, ts: 1.82811, CS: 3
c Min unsat cost LB: 5, ts: 1.86012, CS: 2
c Min unsat cost LB: 6, ts: 1.88412, CS: 4
c Min unsat cost LB: 7, ts: 1.90012, CS: 1
c Min unsat cost LB: 8, ts: 1.92012, CS: 2
c Min unsat cost LB: 9, ts: 1.94012, CS: 1
c Min unsat cost LB: 10, ts: 1.96012, CS: 2
c Min unsat cost LB: 11, ts: 1.97612, CS: 1
c Min unsat cost LB: 12, ts: 1.99212, CS: 1
c Min unsat cost LB: 13, ts: 2.01213, CS: 2
c Min unsat cost LB: 14, ts: 2.03213, CS: 1
c Min unsat cost LB: 15, ts: 2.04813, CS: 4
c Min unsat cost LB: 16, ts: 2.06813, CS: 3
c SAT found, ts: 2.08813
# solving time:2.10413--1.5601s
# sol printing (2.10413)
# sol printed