Resolution vs Nondeterministic Search Problems It is well known that each resolution refutation $\Pi$ for an unsatisfiable CNF formula $F = C_1\wedge C_2 \wedge ... \wedge C_m$ over variables $X$ can  be translated in polynomial time (in the size of $\Pi$) into a deterministic branching program $P$ solving the following search problem: 

1) $P$ has one source node and one sink node for each clause $C_i$. 

2) For each assingment $\alpha:X\rightarrow  \{0,1\}$ there is a consistent path in $P$ from the 
source node to some sink node associated with a clause that is falsified  by $\alpha$. 

Question: 
Is there a proof system strictly stronger than resolution where each proof $\Pi$ can be translated in polynomial time (in the size of $\Pi$) into a not necessarily deterministic branching program $P$ solving the search problem above?
If I understood correctly the question, the so-called Buss-Pudlak game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 http://math.cas.cz/%7Epudlak/howtolie.ps). The queries are formulas (not just variables). The tree is also completely deterministic. 

Other decision trees that correspond to different propositional proof systems exist: e.g., Linear Decision Trees correspond to Res(lin) refutations (cf., http://www.csc.kth.se/~sokolovd/files/papers/splitting.pdf and http://cs.rhul.ac.uk/home/tzameret/Res-Lin-Two.pdf). But there are many other examples (cf., Tonian Pitassi's work on CP-like proof systems).