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