84 lines
839 B
INI
84 lines
839 B
INI
c pigeonhole PHP(6,5), UNSAT
|
|
p cnf 30 81
|
|
1 2 3 4 5 0
|
|
6 7 8 9 10 0
|
|
11 12 13 14 15 0
|
|
16 17 18 19 20 0
|
|
21 22 23 24 25 0
|
|
26 27 28 29 30 0
|
|
-1 -6 0
|
|
-1 -11 0
|
|
-1 -16 0
|
|
-1 -21 0
|
|
-1 -26 0
|
|
-6 -11 0
|
|
-6 -16 0
|
|
-6 -21 0
|
|
-6 -26 0
|
|
-11 -16 0
|
|
-11 -21 0
|
|
-11 -26 0
|
|
-16 -21 0
|
|
-16 -26 0
|
|
-21 -26 0
|
|
-2 -7 0
|
|
-2 -12 0
|
|
-2 -17 0
|
|
-2 -22 0
|
|
-2 -27 0
|
|
-7 -12 0
|
|
-7 -17 0
|
|
-7 -22 0
|
|
-7 -27 0
|
|
-12 -17 0
|
|
-12 -22 0
|
|
-12 -27 0
|
|
-17 -22 0
|
|
-17 -27 0
|
|
-22 -27 0
|
|
-3 -8 0
|
|
-3 -13 0
|
|
-3 -18 0
|
|
-3 -23 0
|
|
-3 -28 0
|
|
-8 -13 0
|
|
-8 -18 0
|
|
-8 -23 0
|
|
-8 -28 0
|
|
-13 -18 0
|
|
-13 -23 0
|
|
-13 -28 0
|
|
-18 -23 0
|
|
-18 -28 0
|
|
-23 -28 0
|
|
-4 -9 0
|
|
-4 -14 0
|
|
-4 -19 0
|
|
-4 -24 0
|
|
-4 -29 0
|
|
-9 -14 0
|
|
-9 -19 0
|
|
-9 -24 0
|
|
-9 -29 0
|
|
-14 -19 0
|
|
-14 -24 0
|
|
-14 -29 0
|
|
-19 -24 0
|
|
-19 -29 0
|
|
-24 -29 0
|
|
-5 -10 0
|
|
-5 -15 0
|
|
-5 -20 0
|
|
-5 -25 0
|
|
-5 -30 0
|
|
-10 -15 0
|
|
-10 -20 0
|
|
-10 -25 0
|
|
-10 -30 0
|
|
-15 -20 0
|
|
-15 -25 0
|
|
-15 -30 0
|
|
-20 -25 0
|
|
-20 -30 0
|
|
-25 -30 0
|