Apply Resolution rule in this formula

Solution 1:

Only once you cannot obtain any new clauses can you stop and declare the set of statements to be satisfiable. And there are a bunch more resolutions you can (and therefore should) perform:

$(u_1 \lor u_3)$ resolves with $(\neg u_1 \lor \neg u_3)$ to get $(u_1 \lor \neg u_1)$

$(u_1 \lor u_3)$ resolves with $(\neg u_1 \lor \neg u_3)$ to get $(u_3 \lor \neg u_3)$

$(u_2 \lor u_3)$ resolves with $(\neg u_1 \lor \neg u_3)$ to get $(u_2 \lor \neg u_1)$

....

but yes, at some point you will find that there are no more new clauses that you can obtain, and then (and only then) you can stop.