54.52/57.22	unsat
