p cnf 2 2 1 -2 0 -1 0