CNF resolution refutation. The last line of input is the query whose negation is added, then resolution derives a contradiction (UNSATISFIABLE) or exhausts the search (SATISFIABLE).
Literals: plain variable or ~variable for negation. Each line is one clause.
Result