5.27/5.30	unsat
