87.53/87.72	unsat
