p cnf 3 3 a 1 0 e 2 3 0 -1 2 0 1 3 0 -2 -3 0