57.30/58.54	unsat
