17.57/17.90	unsat
