Aim of this track is to solve small hard instances of past evaluations. A pool of about 50 instances will be selected, and solvers will be allowed a substantial CPU time budget. The requirements for the solvers are the same given for the main competition.

As for the main competition, authors of solvers are allowed to submit at most three solvers. We will set the CPU time limit to 12 hours and the memory limit at 2GB. At the end of the evaluation, we will rank the solvers by number of solved formulas and we will use CPU time to break ties.