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