17.15/17.20	unsat
