5.27/5.51	unsat
