p cnf 3 2
1 2 3 0
1 2 0