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