/ Test /

Record Case Detail

Notes

This function is in beta test. Please help improve it in the issues here.

Stderr


        

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!