c status 10
c --eliminateclslim=0
c --eliminateinit=0
c --subsumeclslim=0
p cnf 11 10
2 8 5 0
-2 10 0
5 10 0
7 1 -4 0
6 7 8 0
-1 0
11 3 0
4 -11 0
-3 -9 0
-3 9 0