Interesting small SAT problems?
In general, you can look at hard combinatorial instances. If 50 variables is not a hard limit, try e.g., an instance arising from combinatorial block design having 105 variables described in [1]. The actual instance in DIMACS format is here provided by the authors. For the instance, the authors write in [1] that: "We issue a challenge for any solver to solve it in less than one day."

Something that will be not as hard, but still not entirely trivial is coloring Mycielski graphs. These are graphs with clique number 2, but the chromatic number can be arbitrarily large. Again, if 50 variables is really a hard limit, it seems the largest Mycielski graphs you can consider is the Grötzsch graph if you use the obvious encoding to CNF. The obvious encoding will have 33 variables if you test for 3-colorability (UNSAT), and 44 variables if you test for 4-colorability (SAT). 



[1] Van Gelder, Allen, and Ivor Spence. "Zero-one designs produce small hard SAT instances." Theory and Applications of Satisfiability Testing–SAT 2010. Springer Berlin Heidelberg, 2010. 388-397.