27.23/32.31	unsat
