58.02/58.12	unsat
