I know that resolution is refutation complete, but what can we conclude if a resolution procedure leads to a situation with no more chance to operate the resolution?
Given a propositional formula which we want to check its satisfiability,
( a + b ) ( ¬a + c )
after one resolution the formula become
( a + b ) ( ¬a + c ) ( b + c )
what can we conclude at this point?