21.35/22.87	unsat
