c sample satisfiable formula
c (x1 or x2 or -x3) and (-x1 or x3) and (-x2 or x3) and (x1 or x2)
p cnf 3 4
1 2 -3 0
-1 3 0
-2 3 0
1 2 0