641.27/642.56	unsat
