is the prover$()$ function. You will be implementing the two$-$pointer

method $($same as level saturation$),$ using the set$-$of$-$support strategy.

Here$$s a description of the algorithm$1$:

$1.$ Initialize the two pointers $($simply$,$ the clause index$)$ so that you will be using the set$-$of$-$support

strategy. This can be done in the following way.

$$ Set the $$inner loop$$ pointer to the front of the list of clauses.

$$ Set the $$outer loop$$ pointer to the first clause resulting