10.57/10.62	unsat
