Is it an open problem if generalized resolution is always possible? Let we have a 3CNF under following restriction: each variable occurs 3 times.

Then I apply generalized resolution (GR) (I don't know which name would fit more) technique (number of clauses can be arbitrary large, just an example):

$(x\lor A)\land(x\lor B)\land(\overline x\lor C)=(A\lor C)\land(B\lor C)$. Here $A,B,C$ are some clauses. Neither $A$ and $C$ nor $B$ and $C$ have opposing literals (like in original resolution, the reason is not to exponentially increase length of formula).

Is it an open problem if there is such a sequence of choices (which variable to choose for GR) that will return 'NO' if formula is unsatisfiable? Or there is a proof that some unsatisfiable formulas (with given restrictions) have no such sequences? Meaning that for every pair of literals $x,y$ on some step it will be possible to find a clause $(A\lor x\lor y)\land(B\lor\overline x\lor\overline y)$.

We assume that we can use any known polynomial technique such as unit propagation, absorption rules $(x\lor A)\land(\overline x\lor A)=A; A\land(x\lor A)=A$, pure literal rule (if variable always occur as positive or negative, remove all clauses where it is contained), changing equal literals, finding strongly connected components in a graph for 2-clauses, etc.
Resolution is refutation-complete. This means that if $S$ is a set of unsatisfiable clauses, then you can use resolution to derive the empty clause. Moreover, Resolution is sound, so you can only derive the empty clause if $S$ is unsatisfiable. Summarizing, given a set $S$ of clauses, you can use Resolution to derive the empty clause if and only if $S$ is unsatisfiable.

Unfortunately, sometimes generating the empty clause takes an exponential number of steps. Let $G$ be a random 4-regular graph on an odd number of vertices $n$, and let us associate with each of the $2n$ edges a variable. Consider the set of $\Theta(n)$ clauses stating that for every vertex, the XOR of the four variables corresponding to edges touching the vertex is 1. Since the number of vertices is odd, this set of clauses, known as a Tseitin contradiction, is unsatisfiable. Urquhart showed that with high probability, any Resolution refutation of this set of clauses has $2^{\Omega(n)}$ many lines (i.e., clauses); see Jakob Nordström's lecture notes.