# Propositional resolution: the correct way to proceed

I'm trying to solve the following exercise:

using resolution, tell whether the following formula can be proven:

F = {( L $\wedge$ V) $\rightarrow$ H, L $\rightarrow$ V , L } entails (V $\wedge$ H).

I know that the propositional resolution procedure consists of proving that F $\wedge$ $\neg$ (V $\wedge$ H) is unsatisfiable, therefore I'm actually working on this set of clauses (in clausal normal form):

{ ($\neg$ L,$\neg$V,H )$_{1}$, ($\neg$ L,V )$_{2}$, ( L )$_{3}$, ($\neg$ V,$\neg$ H )$_{4}$ }.

My question comes out here indeed: is there an exactly way to keep pairs of clauses for resolving them? I mean, my opinion is that the following procedure is right:

1. from 1 and 2 comes out ($\neg$L, H)$_{5}$;

2. from 5 and 4 comes out ($\neg$L, $\neg$V)$_{6}$;

3. from 2 and 6 comes out ($\neg$L)$_{7}$ and so
4. from 3 and 7 comes out {} which means that F entails (V $\wedge$ H).

Is this a correct way to go or is there a precise way that I did not understand (about how considering the pair of clauses to solve)?

\begin{align} &~\{ (\neg L,\neg V,H )_{1}, (\neg L,V )_{2}, ( L )_{3}, (\neg V,\neg H )_{4} \} \\ ~& ~\{\color{grey}{(L)_3}, (\neg V, \neg H)_{4}, (\neg V, H )_{5}, (V)_{6}\} & \because \{1, 2\}\vdash 5, \{2, 3\}\vdash 6 \\ ~&~\{\color{grey}{(L)_3, (V)_{6}},(\neg H)_{7}, (H)_{8}\} & \because \{4,6\}\vdash 7, \{5,6\}\vdash 8 \\ ~&~ \{\} & \because \{7,8\}\vdash \bot \\ \therefore ~&~ \{ (\neg L,\neg V,H )_{1}, (\neg L,V )_{2}, ( L )_{3}\}\vdash \{(V),(H)\}\end{align}
PS: hopefully you noticed that $( L \wedge V) \leftrightarrow H$ is $(\neg L\vee \neg V\vee H)\wedge(\neg H\vee(L\wedge V))$ and so the clausal form of $F$ is: $$F=\{(\neg L, \neg V, H)_{1},(\neg H, L)_{1.1},(\neg H, V)_{1.2}, (\neg L,V )_{2}, ( L )_{3}\}$$