An easy case of SAT that is not easy for tree resolution
It sounds like you are interested in all-different constraints (and your last sentence is on the right track).  These are non-trivial instances of the pigeonhole principle, where the number of pigeons is not necessarily greater than the number of holes, and in addition some pigeons may be barred from some of the holes.

All-different constraints can be decided by matching in low-order polynomial time.


Jean-Charles Régin, A filtering algorithm for constraints of difference in CSPs, AAAI 1994, 362–367.
D. E. Knuth and A. Raghunathan, The problem of compatible representatives, SIAM J. Discrete Math. 5 422–427, 1992.  doi:10.1137/0405033


When all-different constraints are expressed (using one of several encodings) as SAT instances, then conflict-driven clause learning usually quickly finds a solution if it exists.  However, pure resolution for the PHP has to build a superpolynomially large set of clauses to show that the instance is unsatisfiable.  This bound clearly holds for this more general problem.  On the other hand, recall that Cook's encoding of the PHP allows polynomial-sized extended resolution refutations.


S. A. Cook, A short proof of the pigeon hole principle using extended resolution, SIGACT News 8 28–32, 1976.  doi:10.1145/1008335.1008338


Recent work along these lines is Chapter 5 of Sergi Oliva's thesis, which formed the basis of a paper with Alberto Atserias at CCC 2013.

I expect you are aware of Cook's classic result, so perhaps you meant to restrict the power of the proof system in your third condition?