The smallest hard unsatisfiable instance xor-chain/x1_36 (106 variables, 844 literal occurrences) was submitted by Lintao Zhang and Sharad Malik.
The smallest hard satisfiable instance hgen2-v500-s1216665065 (500 variables, 5250 literal occurrences) was generated by Edward A. Hirsch's random instance generator hgen2.
Note that instances with fewer variables also remained unsolved, but the winner was determined by the total number of literal occurrences in the formula (note that a hard randomly generated formula in -CNF will have a much greater clauses/variables ratio, not to say about the length of its clauses).