All participating solvers will be executed on the same set of input problems.
Let m be the number of participating solvers. For each input problem we give points to each solver, according to whether the participant yields
The number of points a solver gets on a given input problem is calculated as follows:
Note that it is possible that an input problem indeed doesn't have a solution. In that case, (1) above is not possible, so the solvers that correctly say FAIL are ranked best.
It is also possible that the input universe is not consistent. In that case a solver is expected to turn that inconsistent universe into a consistent universe which satisfies the request.
The total score of a solver is the sum of the number of points obtained for all problems of the problem set. The solver with the minimal score wins.
If several solvers obtain the best total score then the winner is determined by choosing among those having obtained the best total score the one with the minimal total success time. The total success time of a solver is the sum of execution times of that solvers over all problems in case 1 (correct solution), plus f*timeout where f is the number of problems where the result of that solver is in one of the cases 2 (no solution) or 3 (wrong solution), and timeout is the time limit defined in the execution environment.