17.42/17.56	unsat
