57.23/59.32	unsat
