Notes
This function is in beta test. Please help improve it in the issues
here.
Your Answer
Start deductive solver for: (-x0 | -x1) & (-x0 | x1) & (x0 | x1) & (x0 | -x1) Make decision x0 = 0: (1) & (1) & (x1) & (-x1) Unit propagate x1 = 1: (1) & (1) & (1) & (0) Reverse previous decision x0 = 1: (-x1) & (x1) & (1) & (1) Unit propagate x1 = 0: (1) & (0) & (1) & (1) The expression is unSAT! Bye!
JOJ Answer
Start deductive solver for: (-x0 | -x1) & (-x0 | x1) & (x0 | x1) & (x0 | -x1) Make decision x0 = 0: (1) & (1) & (x1) & (-x1) Unit propagate x1 = 1: (1) & (1) & (1) & (0) Reverse previous decision x0 = 1: (-x1) & (x1) & (1) & (1) Unit propagate x1 = 0: (1) & (0) & (1) & (1) The expression is unSAT! Bye!