5.07/5.57	unsat
