17.45/17.57	unsat
