ais6.cnf

c created by Generic SAT Encoder v1.0
p cnf 61 581
1 2 3 4 5 6 0
-1 -2 0
-1 -3 0
-1 -4 0
-1 -5 0
-1 -6 0
-2 -3 0
-2 -4 0
-2 -5 0
-2 -6 0
-3 -4 0
-3 -5 0
-3 -6 0
-4 -5 0
-4 -6 0
-5 -6 0
7 8 9 10 11 12 0
-7 -8 0
-7 -9 0
-7 -10 0
-7 -11 0
-7 -12 0
-8 -9 0
-8 -10 0
-8 -11 0
-8 -12 0
-9 -10 0
-9 -11 0
-9 -12 0
-10 -11 0
-10 -12 0
-11 -12 0
13 14 15 16 17 18 0
-13 -14 0
-13 -15 0
-13 -16 0
-13 -17 0
-13 -18 0
-14 -15 0
-14 -16 0
-14 -17 0
-14 -18 0
-15 -16 0
-15 -17 0
-15 -18 0
-16 -17 0
-16 -18 0
-17 -18 0
19 20 21 22 23 24 0
-19 -20 0
-19 -21 0
-19 -22 0
-19 -23 0
-19 -24 0
-20 -21 0
-20 -22 0
-20 -23 0
-20 -24 0
-21 -22 0
-21 -23 0
-21 -24 0
-22 -23 0
-22 -24 0
-23 -24 0
25 26 27 28 29 30 0
-25 -26 0
-25 -27 0
-25 -28 0
-25 -29 0
-25 -30 0
-26 -27 0
-26 -28 0
-26 -29 0
-26 -30 0
-27 -28 0
-27 -29 0
-27 -30 0
-28 -29 0
-28 -30 0
-29 -30 0
31 32 33 34 35 36 0
-31 -32 0
-31 -33 0
-31 -34 0
-31 -35 0
-31 -36 0
-32 -33 0
-32 -34 0
-32 -35 0
-32 -36 0
-33 -34 0
-33 -35 0
-33 -36 0
-34 -35 0
-34 -36 0
-35 -36 0
37 38 39 40 41 0
-37 -38 0
-37 -39 0
-37 -40 0
-37 -41 0
-38 -39 0
-38 -40 0
-38 -41 0
-39 -40 0
-39 -41 0
-40 -41 0
42 43 44 45 46 0
-42 -43 0
-42 -44 0
-42 -45 0
-42 -46 0
-43 -44 0
-43 -45 0
-43 -46 0
-44 -45 0
-44 -46 0
-45 -46 0
47 48 49 50 51 0
-47 -48 0
-47 -49 0
-47 -50 0
-47 -51 0
-48 -49 0
-48 -50 0
-48 -51 0
-49 -50 0
-49 -51 0
-50 -51 0
52 53 54 55 56 0
-52 -53 0
-52 -54 0
-52 -55 0
-52 -56 0
-53 -54 0
-53 -55 0
-53 -56 0
-54 -55 0
-54 -56 0
-55 -56 0
57 58 59 60 61 0
-57 -58 0
-57 -59 0
-57 -60 0
-57 -61 0
-58 -59 0
-58 -60 0
-58 -61 0
-59 -60 0
-59 -61 0
-60 -61 0
-1 -7 0
-2 -8 0
-3 -9 0
-4 -10 0
-5 -11 0
-6 -12 0
-1 -13 0
-2 -14 0
-3 -15 0
-4 -16 0
-5 -17 0
-6 -18 0
-1 -19 0
-2 -20 0
-3 -21 0
-4 -22 0
-5 -23 0
-6 -24 0
-1 -25 0
-2 -26 0
-3 -27 0
-4 -28 0
-5 -29 0
-6 -30 0
-1 -31 0
-2 -32 0
-3 -33 0
-4 -34 0
-5 -35 0
-6 -36 0
-7 -1 0
-8 -2 0
-9 -3 0
-10 -4 0
-11 -5 0
-12 -6 0
-7 -13 0
-8 -14 0
-9 -15 0
-10 -16 0
-11 -17 0
-12 -18 0
-7 -19 0
-8 -20 0
-9 -21 0
-10 -22 0
-11 -23 0
-12 -24 0
-7 -25 0
-8 -26 0
-9 -27 0
-10 -28 0
-11 -29 0
-12 -30 0
-7 -31 0
-8 -32 0
-9 -33 0
-10 -34 0
-11 -35 0
-12 -36 0
-13 -1 0
-14 -2 0
-15 -3 0
-16 -4 0
-17 -5 0
-18 -6 0
-13 -7 0
-14 -8 0
-15 -9 0
-16 -10 0
-17 -11 0
-18 -12 0
-13 -19 0
-14 -20 0
-15 -21 0
-16 -22 0
-17 -23 0
-18 -24 0
-13 -25 0
-14 -26 0
-15 -27 0
-16 -28 0
-17 -29 0
-18 -30 0
-13 -31 0
-14 -32 0
-15 -33 0
-16 -34 0
-17 -35 0
-18 -36 0
-19 -1 0
-20 -2 0
-21 -3 0
-22 -4 0
-23 -5 0
-24 -6 0
-19 -7 0
-20 -8 0
-21 -9 0
-22 -10 0
-23 -11 0
-24 -12 0
-19 -13 0
-20 -14 0
-21 -15 0
-22 -16 0
-23 -17 0
-24 -18 0
-19 -25 0
-20 -26 0
-21 -27 0
-22 -28 0
-23 -29 0
-24 -30 0
-19 -31 0
-20 -32 0
-21 -33 0
-22 -34 0
-23 -35 0
-24 -36 0
-25 -1 0
-26 -2 0
-27 -3 0
-28 -4 0
-29 -5 0
-30 -6 0
-25 -7 0
-26 -8 0
-27 -9 0
-28 -10 0
-29 -11 0
-30 -12 0
-25 -13 0
-26 -14 0
-27 -15 0
-28 -16 0
-29 -17 0
-30 -18 0
-25 -19 0
-26 -20 0
-27 -21 0
-28 -22 0
-29 -23 0
-30 -24 0
-25 -31 0
-26 -32 0
-27 -33 0
-28 -34 0
-29 -35 0
-30 -36 0
-31 -1 0
-32 -2 0
-33 -3 0
-34 -4 0
-35 -5 0
-36 -6 0
-31 -7 0
-32 -8 0
-33 -9 0
-34 -10 0
-35 -11 0
-36 -12 0
-31 -13 0
-32 -14 0
-33 -15 0
-34 -16 0
-35 -17 0
-36 -18 0
-31 -19 0
-32 -20 0
-33 -21 0
-34 -22 0
-35 -23 0
-36 -24 0
-31 -25 0
-32 -26 0
-33 -27 0
-34 -28 0
-35 -29 0
-36 -30 0
-37 -42 0
-38 -43 0
-39 -44 0
-40 -45 0
-41 -46 0
-37 -47 0
-38 -48 0
-39 -49 0
-40 -50 0
-41 -51 0
-37 -52 0
-38 -53 0
-39 -54 0
-40 -55 0
-41 -56 0
-37 -57 0
-38 -58 0
-39 -59 0
-40 -60 0
-41 -61 0
-42 -37 0
-43 -38 0
-44 -39 0
-45 -40 0
-46 -41 0
-42 -47 0
-43 -48 0
-44 -49 0
-45 -50 0
-46 -51 0
-42 -52 0
-43 -53 0
-44 -54 0
-45 -55 0
-46 -56 0
-42 -57 0
-43 -58 0
-44 -59 0
-45 -60 0
-46 -61 0
-47 -37 0
-48 -38 0
-49 -39 0
-50 -40 0
-51 -41 0
-47 -42 0
-48 -43 0
-49 -44 0
-50 -45 0
-51 -46 0
-47 -52 0
-48 -53 0
-49 -54 0
-50 -55 0
-51 -56 0
-47 -57 0
-48 -58 0
-49 -59 0
-50 -60 0
-51 -61 0
-52 -37 0
-53 -38 0
-54 -39 0
-55 -40 0
-56 -41 0
-52 -42 0
-53 -43 0
-54 -44 0
-55 -45 0
-56 -46 0
-52 -47 0
-53 -48 0
-54 -49 0
-55 -50 0
-56 -51 0
-52 -57 0
-53 -58 0
-54 -59 0
-55 -60 0
-56 -61 0
-57 -37 0
-58 -38 0
-59 -39 0
-60 -40 0
-61 -41 0
-57 -42 0
-58 -43 0
-59 -44 0
-60 -45 0
-61 -46 0
-57 -47 0
-58 -48 0
-59 -49 0
-60 -50 0
-61 -51 0
-57 -52 0
-58 -53 0
-59 -54 0
-60 -55 0
-61 -56 0
-1 -8 37 0
-1 -9 38 0
-1 -10 39 0
-1 -11 40 0
-1 -12 41 0
-2 -9 37 0
-2 -7 37 0
-2 -10 38 0
-2 -11 39 0
-2 -12 40 0
-3 -10 37 0
-3 -8 37 0
-3 -11 38 0
-3 -7 38 0
-3 -12 39 0
-4 -11 37 0
-4 -9 37 0
-4 -12 38 0
-4 -8 38 0
-4 -7 39 0
-5 -12 37 0
-5 -10 37 0
-5 -9 38 0
-5 -8 39 0
-5 -7 40 0
-6 -11 37 0
-6 -10 38 0
-6 -9 39 0
-6 -8 40 0
-6 -7 41 0
-7 -14 42 0
-7 -15 43 0
-7 -16 44 0
-7 -17 45 0
-7 -18 46 0
-8 -15 42 0
-8 -13 42 0
-8 -16 43 0
-8 -17 44 0
-8 -18 45 0
-9 -16 42 0
-9 -14 42 0
-9 -17 43 0
-9 -13 43 0
-9 -18 44 0
-10 -17 42 0
-10 -15 42 0
-10 -18 43 0
-10 -14 43 0
-10 -13 44 0
-11 -18 42 0
-11 -16 42 0
-11 -15 43 0
-11 -14 44 0
-11 -13 45 0
-12 -17 42 0
-12 -16 43 0
-12 -15 44 0
-12 -14 45 0
-12 -13 46 0
-13 -20 47 0
-13 -21 48 0
-13 -22 49 0
-13 -23 50 0
-13 -24 51 0
-14 -21 47 0
-14 -19 47 0
-14 -22 48 0
-14 -23 49 0
-14 -24 50 0
-15 -22 47 0
-15 -20 47 0
-15 -23 48 0
-15 -19 48 0
-15 -24 49 0
-16 -23 47 0
-16 -21 47 0
-16 -24 48 0
-16 -20 48 0
-16 -19 49 0
-17 -24 47 0
-17 -22 47 0
-17 -21 48 0
-17 -20 49 0
-17 -19 50 0
-18 -23 47 0
-18 -22 48 0
-18 -21 49 0
-18 -20 50 0
-18 -19 51 0
-19 -26 52 0
-19 -27 53 0
-19 -28 54 0
-19 -29 55 0
-19 -30 56 0
-20 -27 52 0
-20 -25 52 0
-20 -28 53 0
-20 -29 54 0
-20 -30 55 0
-21 -28 52 0
-21 -26 52 0
-21 -29 53 0
-21 -25 53 0
-21 -30 54 0
-22 -29 52 0
-22 -27 52 0
-22 -30 53 0
-22 -26 53 0
-22 -25 54 0
-23 -30 52 0
-23 -28 52 0
-23 -27 53 0
-23 -26 54 0
-23 -25 55 0
-24 -29 52 0
-24 -28 53 0
-24 -27 54 0
-24 -26 55 0
-24 -25 56 0
-25 -32 57 0
-25 -33 58 0
-25 -34 59 0
-25 -35 60 0
-25 -36 61 0
-26 -33 57 0
-26 -31 57 0
-26 -34 58 0
-26 -35 59 0
-26 -36 60 0
-27 -34 57 0
-27 -32 57 0
-27 -35 58 0
-27 -31 58 0
-27 -36 59 0
-28 -35 57 0
-28 -33 57 0
-28 -36 58 0
-28 -32 58 0
-28 -31 59 0
-29 -36 57 0
-29 -34 57 0
-29 -33 58 0
-29 -32 59 0
-29 -31 60 0
-30 -35 57 0
-30 -34 58 0
-30 -33 59 0
-30 -32 60 0
-30 -31 61 0
c end of file