19.45/21.53	unsat
