5.27/6.17	unsat
