p cnf 4 5
1       0
2       0
3       0
-1      -2      4       0
-4      -3      0