Record Case Detail

Notes

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

Stderr


        

Hints

Your answer may be identical to the JOJ answer in the first several lines.

However, you will still get Wrong Answer because the complete output may be longer and there might be errors in the future lines.

Please double check your code to solve this problem and try again.

Your Answer

Start deductive solver for:
(-x0 | -x1) & (-x0 | x1) & (x0 | x1) & (x0 | -x1)
The expression is SAT!
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!