15.64/17.30	unsat
