17.45/17.58	unsat
