27.86/27.97	unsat
