283.03/283.52	unsat
