proof by finding suitable instances and resolution I am trying to proof by resolution the following:  
1) Given a language with the binary relation symbols $<, <<, <<<$ and the binary function symbols $+, *$ and the constant symbols a, b,
proof by resolution that the following CNF is unsatisfiable:
$\{\{a+b < a*b\}; \{x_2 \not< y_2, x_2 + y_2 << x_2 * y_2\}; \{x_2 \not<< y_2, x_2 + y_2 <<< x_2 * y_2\}; \{x \not<<< y\}\}$ 
Hint: Find a set of instances without free variables of this clauses, that are propositionally unsatisfiable.  
I don't manage to find suitable instances of the clauses. Do you have any idea? 
2) Name a set of n clauses (with O(n) symbols) that is unsatisfiable, but whereby the smallest set of instances without free variables, that are propositionally unsatisfiable, does have more than O(n) symbols. 
I have no idea how such a set of clauses could look like. Hopefully it becomes more clear, when 1) is solved?  
I'd appreciate your help on this! :)
 A: 
proof by resolution that the following CNF is unsatisfiable:
$\{\{a+b < a*b\}; \{x_2 \not< y_2, x_2 + y_2 \ll x_2 * y_2\}; \{x_2 \not\ll y_2, x_2 + y_2 \lll x_2 * y_2\}; \{x \not\lll y\}\}$ 

You need to use $a+b < a*b$ in some other clause. The operator "$<$" only occurs in $x_2 \not< y_2$ so you should take $x_2=a+b, y_2=a*b$. The other instantiations follow the same reasoning. So you end up with clauses, 
\begin{align*} 
& a+b < a*b\\\\
& a+b \not< a*b\\
&   (a+b) + (a*b) \ll (a+b) * (a*b)\\\\
& (a+b) + (a*b) \not\ll (a+b) * (a*b)\\
&    ((a+b)+(a*b))+((a+b)*(a*b)) \lll ((a+b)+(a*b))*((a+b)*(a*b))\\\\
&    ((a+b)+(a*b))+((a+b)*(a*b)) \not\lll ((a+b)+(a*b))*((a+b)*(a*b))\\\\
\end{align*}
Applying the resolution method is now trivial. 

For question number 2 consider,
\begin{align*} 
 &\{a+b <_1 a*b\}\\
 %
 &\{x_k \not<_{(k-1)} y_k,\ x_k + y_k <_k x_k * y_k\}\quad 1<k<n\\
 &\{x_{n} \not<_{n-1}< y_{n}\}  
 \end{align*}
and to instantiate the free variables consider terms, 
 $s_0 = a$,
 $t_0 = b$,
 $s_k =s_{(k-1)}+t_{(k-1)}$ and
 $t_k =s_{(k-1)}*t_{(k-1)}$, 
and define substitutions $x_k/s_{k-1}$ and $y_k/t_{k-1}$ for $1<k<n$. The number of symbols grows exponentially with $k$ and therefore also with $n$.
