18.45/20.56	unsat
