c --subsume=0
c --eliminit=0
p cnf 5 8
-2 1 0
2 1 0
-3 -1 0
3 -1 0
1 4 5 0
-1 4 5 0
1 -4 -5 0
-1 -4 -5 0