0.27/0.64	unsat
