20.15/22.47	unsat
