58.27/58.47	unsat
