An easy case of SAT that is not easy for tree resolution Is there a natural class $C$ of CNF formulas - preferably one that has previously been studied in the literature - with the following properties:


$C$ is an easy case of SAT, like e.g. Horn or 2-CNF, i.e., membership in $C$ can be tested in polynomial time, and formulas $F\in C$ can be tested for satisfiability in polynomial time. 
Unsatisfiable formulas $F\in C$ are not known to have short (polynomial size) tree-like resolution refutations. Even better would be: there are unsatisfiable formulas in $C$ for which a super-polynomial lower bound for tree-like resolution is known. 
On the other hand, unsatisfiable formulas in $C$ are known to have short proofs in some stronger proof system, e.g. in dag-like resolution or some even stronger system. 


$C$ should not be too sparse, i.e., contain many formulas with $n$ variables, for every (or at least for most values of) $n\in \mathbb{N}$. It should also be non-trivial, in the sense of containing satisfiable as well as unsatisfiable formulas.

The following approach to solving an arbitrary CNF formula $F$ should be meaningful: find a partial assignment $\alpha$ s.t. the residual formula $F\alpha$ is in $C$, and then apply the polynomial time algorithm for formulas in $C$ to $F\alpha$. Therefore I would like other answers besides the all-different constraints from the currently accepted answer, as I think it is rare that an arbitrary formula will become an all-different constraint after applying a restriction.
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?