6.1.1.3 Propositional calculus

Problem: Prove the non-satisfiability (or satisfiability) of the following sets of clauses by using the resolution method. Apply an arbitrary order of enumeration of clauses, as well as, at the instruction of the teacher, one of the following strategies: preference for monomials, linear, level saturation. \[ \{(q \vee \neg \tau),(\neg q \vee \neg \tau),(q \vee \tau),(\neg p \vee \neg \tau), \neg q\} . \]