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