17.46/19.55	unsat
