17.48/20.53	unsat
