8.17/8.28	unsat
