23.86/26.39	unsat
