20.46/20.55	unsat
