57.12/57.43	unsat
