p cnf 3 10000
1 -2 0
2 -3 0
3 -1 0
1 2 3 0
-1 -2 -3 0