80.23/80.37	unsat
