p cnf 4 3