0.58/0.64	unsat
