Propositional Logic - Resolution Strategies I need help understanding these resolution strategies.

1) Set of support 
  2) Linear input 

Let's assume $\mathcal{S} = \{ C_1, ... ,C_n\}$ is our set of clauses.
and we want to derive / prove the conclusion clause $G$ (via resolution).
So we will add the negate of the conclusion clause $\lnot G$ to our clauses.

Question 1:
How does the Set of support strategy work?
  How does the Linear input strategy work?
Question 2:
What are the pros and cons of each strategy? 
  Why would u prefer to choose SoS and why would you prefer to chose Linear input?

Would really appreciate help, my exam is tomorrow, thanks.
 A: Resolution Strategies:
Set of support:
The set of support partitions all clauses into two sets, the set of support and auxiliary set.
We initialize the auxiliary set to be the set S (our starting set of clauses).
We initialize the set of support to be the negated conclusion ~G.
Our resolution will always use at least 1 clause from the set of support.
All clauses derived by such action will be added to the set of support.
+This strategy is complete.
Linear
Linear derivation of $G$ from $S$ is a finite sequence of clauses $R_0,...R_k=G$ such that $R_0\in S$ and each $R_i$ with $1\le i \le k$ is a resolvent of $R_{i-1}$ and a clause $G_i\in S \cup \{R_0,...,R_{i-2}\}$
+This strategy  is complete.
Input
At least one of the two parent clauses is in $S$.
+Reduces the size of the search space.
+Easy to implement and is efficient.
-Is ONLY complete for Horn clauses.
Linear input
Apply both liner and input strategy together.
+Efficient
-This is sound but not complete.
-Only complete for Horn clauses.

So basically we will use the set of support strategy if $S$ has non-horn clauses. Otherwise we can use the linear input strategy which is more efficient.
