87.57/87.73	unsat
