20.34/22.76	unsat
