p cnf 2 2 1 2 0 -2 0