15.46/17.30	unsat
