17.15/17.23	unsat
