5.27/5.52	unsat
