c an ALC problem
p cnf 5 7
1 2 3 0
1 2 4 0
5 2 3 0
5 2 4 0
-5 0
-2 0
-3 0