5.58/7.27	unsat
