927.20/930.58	unsat
