20.57/23.95	unsat
