17.35/17.40	unsat
