c an ALC problem
p cnf 15 332
1 -2 3 -1 -4 2 0
1 -2 3 -5 -4 2 0
1 -2 3 -6 -4 2 0
1 -2 3 -7 -4 2 0
5 -2 3 -1 -4 2 0
5 -2 3 -5 -4 2 0
5 -2 3 -6 -4 2 0
5 -2 3 -7 -4 2 0
6 -2 3 -1 -4 2 0
6 -2 3 -5 -4 2 0
6 -2 3 -6 -4 2 0
6 -2 3 -7 -4 2 0
7 -2 3 -1 -4 2 0
7 -2 3 -5 -4 2 0
7 -2 3 -6 -4 2 0
7 -2 3 -7 -4 2 0
1 -2 3 -1 -4 7 0
1 -2 3 -5 -4 7 0
1 -2 3 -6 -4 7 0
1 -2 3 -7 -4 7 0
5 -2 3 -1 -4 7 0
5 -2 3 -5 -4 7 0
5 -2 3 -6 -4 7 0
5 -2 3 -7 -4 7 0
6 -2 3 -1 -4 7 0
6 -2 3 -5 -4 7 0
6 -2 3 -6 -4 7 0
6 -2 3 -7 -4 7 0
-2 3 -1 -4 7 0
-2 3 -5 -4 7 0
-2 3 -6 -4 7 0
-2 3 -7 -4 7 0
1 -2 3 -1 -8 2 0
1 -2 3 -5 -8 2 0
1 -2 3 -6 -8 2 0
1 -2 3 -7 -8 2 0
5 -2 3 -1 -8 2 0
5 -2 3 -5 -8 2 0
5 -2 3 -6 -8 2 0
5 -2 3 -7 -8 2 0
6 -2 3 -1 -8 2 0
6 -2 3 -5 -8 2 0
6 -2 3 -6 -8 2 0
6 -2 3 -7 -8 2 0
7 -2 3 -1 -8 2 0
7 -2 3 -5 -8 2 0
7 -2 3 -6 -8 2 0
7 -2 3 -7 -8 2 0
1 -2 3 -1 -9 2 0
1 -2 3 -5 -9 2 0
1 -2 3 -6 -9 2 0
1 -2 3 -7 -9 2 0
5 -2 3 -1 -9 2 0
5 -2 3 -5 -9 2 0
5 -2 3 -6 -9 2 0
5 -2 3 -7 -9 2 0
6 -2 3 -1 -9 2 0
6 -2 3 -5 -9 2 0
6 -2 3 -6 -9 2 0
6 -2 3 -7 -9 2 0
7 -2 3 -1 -9 2 0
7 -2 3 -5 -9 2 0
7 -2 3 -6 -9 2 0
7 -2 3 -7 -9 2 0
1 -2 3 -1 -10 2 0
1 -2 3 -5 -10 2 0
1 -2 3 -6 -10 2 0
1 -2 3 -7 -10 2 0
5 -2 3 -1 -10 2 0
5 -2 3 -5 -10 2 0
5 -2 3 -6 -10 2 0
5 -2 3 -7 -10 2 0
6 -2 3 -1 -10 2 0
6 -2 3 -5 -10 2 0
6 -2 3 -6 -10 2 0
6 -2 3 -7 -10 2 0
7 -2 3 -1 -10 2 0
7 -2 3 -5 -10 2 0
7 -2 3 -6 -10 2 0
7 -2 3 -7 -10 2 0
1 -2 3 -1 -11 2 0
1 -2 3 -5 -11 2 0
1 -2 3 -6 -11 2 0
1 -2 3 -7 -11 2 0
5 -2 3 -1 -11 2 0
5 -2 3 -5 -11 2 0
5 -2 3 -6 -11 2 0
5 -2 3 -7 -11 2 0
6 -2 3 -1 -11 2 0
6 -2 3 -5 -11 2 0
6 -2 3 -6 -11 2 0
6 -2 3 -7 -11 2 0
7 -2 3 -1 -11 2 0
7 -2 3 -5 -11 2 0
7 -2 3 -6 -11 2 0
7 -2 3 -7 -11 2 0
1 -2 3 -1 -8 7 0
1 -2 3 -5 -8 7 0
1 -2 3 -6 -8 7 0
1 -2 3 -7 -8 7 0
5 -2 3 -1 -8 7 0
5 -2 3 -5 -8 7 0
5 -2 3 -6 -8 7 0
5 -2 3 -7 -8 7 0
6 -2 3 -1 -8 7 0
6 -2 3 -5 -8 7 0
6 -2 3 -6 -8 7 0
6 -2 3 -7 -8 7 0
-2 3 -1 -8 7 0
-2 3 -5 -8 7 0
-2 3 -6 -8 7 0
-2 3 -7 -8 7 0
1 -2 3 -1 -9 7 0
1 -2 3 -5 -9 7 0
1 -2 3 -6 -9 7 0
1 -2 3 -7 -9 7 0
5 -2 3 -1 -9 7 0
5 -2 3 -5 -9 7 0
5 -2 3 -6 -9 7 0
5 -2 3 -7 -9 7 0
6 -2 3 -1 -9 7 0
6 -2 3 -5 -9 7 0
6 -2 3 -6 -9 7 0
6 -2 3 -7 -9 7 0
-2 3 -1 -9 7 0
-2 3 -5 -9 7 0
-2 3 -6 -9 7 0
-2 3 -7 -9 7 0
1 -2 3 -1 -10 7 0
1 -2 3 -5 -10 7 0
1 -2 3 -6 -10 7 0
1 -2 3 -7 -10 7 0
5 -2 3 -1 -10 7 0
5 -2 3 -5 -10 7 0
5 -2 3 -6 -10 7 0
5 -2 3 -7 -10 7 0
6 -2 3 -1 -10 7 0
6 -2 3 -5 -10 7 0
6 -2 3 -6 -10 7 0
6 -2 3 -7 -10 7 0
-2 3 -1 -10 7 0
-2 3 -5 -10 7 0
-2 3 -6 -10 7 0
-2 3 -7 -10 7 0
1 -2 3 -1 -11 7 0
1 -2 3 -5 -11 7 0
1 -2 3 -6 -11 7 0
1 -2 3 -7 -11 7 0
5 -2 3 -1 -11 7 0
5 -2 3 -5 -11 7 0
5 -2 3 -6 -11 7 0
5 -2 3 -7 -11 7 0
6 -2 3 -1 -11 7 0
6 -2 3 -5 -11 7 0
6 -2 3 -6 -11 7 0
6 -2 3 -7 -11 7 0
-2 3 -1 -11 7 0
-2 3 -5 -11 7 0
-2 3 -6 -11 7 0
-2 3 -7 -11 7 0
1 12 3 -1 -4 2 0
1 12 3 -5 -4 2 0
1 12 3 -6 -4 2 0
1 12 3 -7 -4 2 0
5 12 3 -1 -4 2 0
5 12 3 -5 -4 2 0
5 12 3 -6 -4 2 0
5 12 3 -7 -4 2 0
6 12 3 -1 -4 2 0
6 12 3 -5 -4 2 0
6 12 3 -6 -4 2 0
6 12 3 -7 -4 2 0
7 12 3 -1 -4 2 0
7 12 3 -5 -4 2 0
7 12 3 -6 -4 2 0
7 12 3 -7 -4 2 0
1 12 3 -1 -4 7 0
1 12 3 -5 -4 7 0
1 12 3 -6 -4 7 0
1 12 3 -7 -4 7 0
5 12 3 -1 -4 7 0
5 12 3 -5 -4 7 0
5 12 3 -6 -4 7 0
5 12 3 -7 -4 7 0
6 12 3 -1 -4 7 0
6 12 3 -5 -4 7 0
6 12 3 -6 -4 7 0
6 12 3 -7 -4 7 0
12 3 -1 -4 7 0
12 3 -5 -4 7 0
12 3 -6 -4 7 0
12 3 -7 -4 7 0
1 12 3 -1 -8 2 0
1 12 3 -5 -8 2 0
1 12 3 -6 -8 2 0
1 12 3 -7 -8 2 0
5 12 3 -1 -8 2 0
5 12 3 -5 -8 2 0
5 12 3 -6 -8 2 0
5 12 3 -7 -8 2 0
6 12 3 -1 -8 2 0
6 12 3 -5 -8 2 0
6 12 3 -6 -8 2 0
6 12 3 -7 -8 2 0
7 12 3 -1 -8 2 0
7 12 3 -5 -8 2 0
7 12 3 -6 -8 2 0
7 12 3 -7 -8 2 0
1 12 3 -1 -9 2 0
1 12 3 -5 -9 2 0
1 12 3 -6 -9 2 0
1 12 3 -7 -9 2 0
5 12 3 -1 -9 2 0
5 12 3 -5 -9 2 0
5 12 3 -6 -9 2 0
5 12 3 -7 -9 2 0
6 12 3 -1 -9 2 0
6 12 3 -5 -9 2 0
6 12 3 -6 -9 2 0
6 12 3 -7 -9 2 0
7 12 3 -1 -9 2 0
7 12 3 -5 -9 2 0
7 12 3 -6 -9 2 0
7 12 3 -7 -9 2 0
1 12 3 -1 -10 2 0
1 12 3 -5 -10 2 0
1 12 3 -6 -10 2 0
1 12 3 -7 -10 2 0
5 12 3 -1 -10 2 0
5 12 3 -5 -10 2 0
5 12 3 -6 -10 2 0
5 12 3 -7 -10 2 0
6 12 3 -1 -10 2 0
6 12 3 -5 -10 2 0
6 12 3 -6 -10 2 0
6 12 3 -7 -10 2 0
7 12 3 -1 -10 2 0
7 12 3 -5 -10 2 0
7 12 3 -6 -10 2 0
7 12 3 -7 -10 2 0
1 12 3 -1 -11 2 0
1 12 3 -5 -11 2 0
1 12 3 -6 -11 2 0
1 12 3 -7 -11 2 0
5 12 3 -1 -11 2 0
5 12 3 -5 -11 2 0
5 12 3 -6 -11 2 0
5 12 3 -7 -11 2 0
6 12 3 -1 -11 2 0
6 12 3 -5 -11 2 0
6 12 3 -6 -11 2 0
6 12 3 -7 -11 2 0
7 12 3 -1 -11 2 0
7 12 3 -5 -11 2 0
7 12 3 -6 -11 2 0
7 12 3 -7 -11 2 0
1 12 3 -1 -8 7 0
1 12 3 -5 -8 7 0
1 12 3 -6 -8 7 0
1 12 3 -7 -8 7 0
5 12 3 -1 -8 7 0
5 12 3 -5 -8 7 0
5 12 3 -6 -8 7 0
5 12 3 -7 -8 7 0
6 12 3 -1 -8 7 0
6 12 3 -5 -8 7 0
6 12 3 -6 -8 7 0
6 12 3 -7 -8 7 0
12 3 -1 -8 7 0
12 3 -5 -8 7 0
12 3 -6 -8 7 0
12 3 -7 -8 7 0
1 12 3 -1 -9 7 0
1 12 3 -5 -9 7 0
1 12 3 -6 -9 7 0
1 12 3 -7 -9 7 0
5 12 3 -1 -9 7 0
5 12 3 -5 -9 7 0
5 12 3 -6 -9 7 0
5 12 3 -7 -9 7 0
6 12 3 -1 -9 7 0
6 12 3 -5 -9 7 0
6 12 3 -6 -9 7 0
6 12 3 -7 -9 7 0
12 3 -1 -9 7 0
12 3 -5 -9 7 0
12 3 -6 -9 7 0
12 3 -7 -9 7 0
1 12 3 -1 -10 7 0
1 12 3 -5 -10 7 0
1 12 3 -6 -10 7 0
1 12 3 -7 -10 7 0
5 12 3 -1 -10 7 0
5 12 3 -5 -10 7 0
5 12 3 -6 -10 7 0
5 12 3 -7 -10 7 0
6 12 3 -1 -10 7 0
6 12 3 -5 -10 7 0
6 12 3 -6 -10 7 0
6 12 3 -7 -10 7 0
12 3 -1 -10 7 0
12 3 -5 -10 7 0
12 3 -6 -10 7 0
12 3 -7 -10 7 0
1 12 3 -1 -11 7 0
1 12 3 -5 -11 7 0
1 12 3 -6 -11 7 0
1 12 3 -7 -11 7 0
5 12 3 -1 -11 7 0
5 12 3 -5 -11 7 0
5 12 3 -6 -11 7 0
5 12 3 -7 -11 7 0
6 12 3 -1 -11 7 0
6 12 3 -5 -11 7 0
6 12 3 -6 -11 7 0
6 12 3 -7 -11 7 0
12 3 -1 -11 7 0
12 3 -5 -11 7 0
12 3 -6 -11 7 0
12 3 -7 -11 7 0
-5 0
2 -12 0
-3 0
1 0
13 8 0
14 9 0
4 10 0
15 11 0
-2 -1 0
-2 -5 0
-2 -6 0
-2 -7 0