617.93/623.57	unsat
