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