This version of DPLL implements unit clause and non-chronological backtrack. The assignment is in lexicographical order.
Enter in the box below a series of clauses (one for each line), using alphanumeric characters to represent the variables, separating it using spaces. A dash (-) represents the negation symbol.
Tip: press "n" to advance to the next step
Solution:
Formula