15.26/17.00	unsat
