616.17/618.87	unsat
