This only works when feeding the data forward. When SAT-solving (i.e. working backwards), each clause has multiple possible inputs, meaning there is nothing to resolve away.
When you say "clause", do you mean a disjunction of literals in propositional logic? Because if so, I don't understand what you mean. Clauses don't have inputs. And when you say "resolve away", do you mean applying the resolution rule?
