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