17.24/17.55	unsat
