Consider a first$-$order language having individual symbols $a_0,a_1,a_2,$dots, variables $x_0,x_1,x_2,$dots,

and a binary relation symbol, G$.$ Let

${}_1=\{G(a_0,a_1)\}$

${}_2=\{AA{x}_{i}AA{x}_{i+1}AA{x}_{i+2}(G(x_i,x_{i+1})G(x_{i+1},x_{i+2}))|i0\}$

$={}_1{}_2$

$($a$)$ Prove rigourously that, for any $i0,G(a_i,a_{i+1})$ can be produced by resolution from

$.$

Remark: This proves that resolution on the set $$ can continue forever, always pro$-$

ducing new formulas.