mirror of
https://github.com/c-cube/sidekick.git
synced 2025-12-06 03:05:31 -05:00
438 lines
5.3 KiB
INI
438 lines
5.3 KiB
INI
c This Formular is generated by mcnf
|
|
c
|
|
c horn? no
|
|
c forced? no
|
|
c mixed sat? no
|
|
c clause length = 3
|
|
c
|
|
p cnf 100 430
|
|
79 -92 -71 0
|
|
-54 -11 3 0
|
|
1 -47 -17 0
|
|
-77 69 99 0
|
|
-34 100 16 0
|
|
-85 21 -93 0
|
|
6 -1 -89 0
|
|
17 94 -16 0
|
|
-9 49 8 0
|
|
-93 -49 -55 0
|
|
-39 -12 48 0
|
|
100 -59 -15 0
|
|
-24 -45 -100 0
|
|
-66 86 -29 0
|
|
-13 -38 26 0
|
|
-23 31 -28 0
|
|
96 23 -44 0
|
|
-94 54 40 0
|
|
73 76 3 0
|
|
79 62 -85 0
|
|
21 52 7 0
|
|
-34 17 -53 0
|
|
73 20 37 0
|
|
29 -85 -23 0
|
|
-78 -63 -33 0
|
|
38 87 12 0
|
|
75 68 -50 0
|
|
10 18 95 0
|
|
93 -58 -90 0
|
|
86 66 38 0
|
|
-79 65 92 0
|
|
-24 84 94 0
|
|
48 -20 -56 0
|
|
47 -59 43 0
|
|
12 -60 97 0
|
|
53 57 -89 0
|
|
70 -81 64 0
|
|
89 -11 58 0
|
|
77 36 85 0
|
|
-26 68 12 0
|
|
-27 2 24 0
|
|
41 -18 -2 0
|
|
-6 -49 -3 0
|
|
-5 -55 15 0
|
|
5 -94 92 0
|
|
-52 -95 -38 0
|
|
-97 5 -3 0
|
|
-91 -14 -11 0
|
|
-74 -81 43 0
|
|
12 -75 -6 0
|
|
-40 44 67 0
|
|
-63 16 36 0
|
|
28 -5 58 0
|
|
-26 -72 -14 0
|
|
-81 -71 59 0
|
|
58 -14 93 0
|
|
-56 54 28 0
|
|
-36 -47 46 0
|
|
26 -11 -16 0
|
|
-23 60 46 0
|
|
30 3 33 0
|
|
-35 -82 -76 0
|
|
3 8 42 0
|
|
93 -27 37 0
|
|
82 -88 76 0
|
|
-46 98 23 0
|
|
-1 55 32 0
|
|
71 -19 13 0
|
|
-38 -60 39 0
|
|
-90 -48 -92 0
|
|
85 -21 -58 0
|
|
-57 -100 33 0
|
|
92 -46 68 0
|
|
-17 -96 -94 0
|
|
-60 59 -8 0
|
|
-11 7 3 0
|
|
-47 -71 -1 0
|
|
-28 -51 -22 0
|
|
30 71 76 0
|
|
-84 86 3 0
|
|
-74 47 32 0
|
|
-78 61 -17 0
|
|
-55 -68 -25 0
|
|
56 93 -50 0
|
|
-75 -100 -61 0
|
|
2 64 -43 0
|
|
-80 -18 -96 0
|
|
51 -25 -94 0
|
|
83 -81 -22 0
|
|
-88 -97 -57 0
|
|
-67 -51 -96 0
|
|
-79 8 70 0
|
|
44 -55 52 0
|
|
9 -63 20 0
|
|
-27 63 -13 0
|
|
37 -94 50 0
|
|
-84 72 -48 0
|
|
81 89 -6 0
|
|
-72 -35 49 0
|
|
9 -92 87 0
|
|
-21 11 -7 0
|
|
-11 -26 72 0
|
|
10 -61 7 0
|
|
2 -66 67 0
|
|
-74 -66 -23 0
|
|
-73 7 -80 0
|
|
87 -75 -52 0
|
|
-55 15 76 0
|
|
71 74 75 0
|
|
-94 -96 29 0
|
|
27 -89 -32 0
|
|
86 -52 55 0
|
|
-6 51 24 0
|
|
-89 92 5 0
|
|
-70 -6 31 0
|
|
-23 -86 -100 0
|
|
-35 78 17 0
|
|
99 20 -64 0
|
|
-54 -91 -76 0
|
|
95 24 -93 0
|
|
37 -44 39 0
|
|
2 33 8 0
|
|
-31 22 42 0
|
|
-80 -98 -33 0
|
|
42 -51 10 0
|
|
87 12 -74 0
|
|
-55 -49 5 0
|
|
85 -98 -49 0
|
|
69 72 89 0
|
|
-88 69 -95 0
|
|
28 91 81 0
|
|
-73 71 77 0
|
|
-5 17 41 0
|
|
45 11 5 0
|
|
-78 100 73 0
|
|
24 -93 -25 0
|
|
78 -29 -75 0
|
|
-27 13 -32 0
|
|
-80 -50 -9 0
|
|
-92 -81 60 0
|
|
12 -75 -25 0
|
|
34 -60 -4 0
|
|
86 -96 88 0
|
|
93 44 -83 0
|
|
88 27 44 0
|
|
-48 -26 -1 0
|
|
-49 95 42 0
|
|
28 89 -6 0
|
|
48 -98 14 0
|
|
94 86 -75 0
|
|
-64 -80 -16 0
|
|
-46 -100 -73 0
|
|
98 -79 -63 0
|
|
-73 -41 -66 0
|
|
35 65 -49 0
|
|
99 65 60 0
|
|
-91 -74 -12 0
|
|
-37 -59 43 0
|
|
67 35 77 0
|
|
96 -55 12 0
|
|
-25 -62 78 0
|
|
97 66 79 0
|
|
71 -66 -98 0
|
|
49 -32 94 0
|
|
-72 60 68 0
|
|
-97 29 -94 0
|
|
-79 9 -35 0
|
|
-97 88 -30 0
|
|
54 -49 -27 0
|
|
60 46 -50 0
|
|
-60 -26 -81 0
|
|
-22 78 3 0
|
|
20 32 6 0
|
|
-43 80 55 0
|
|
59 86 75 0
|
|
61 73 29 0
|
|
35 47 5 0
|
|
-56 -22 -71 0
|
|
67 -13 76 0
|
|
51 40 87 0
|
|
-29 9 -73 0
|
|
-85 84 45 0
|
|
-29 76 70 0
|
|
-97 3 52 0
|
|
-73 -75 74 0
|
|
60 -28 -29 0
|
|
-32 -70 -62 0
|
|
-23 -89 -58 0
|
|
-32 -84 97 0
|
|
-17 -29 -97 0
|
|
11 -48 24 0
|
|
-18 -12 78 0
|
|
61 11 25 0
|
|
13 34 -97 0
|
|
31 34 -81 0
|
|
22 -34 -17 0
|
|
54 -90 -9 0
|
|
-69 30 6 0
|
|
7 -60 -42 0
|
|
56 99 92 0
|
|
5 -47 48 0
|
|
18 -47 -9 0
|
|
22 47 -7 0
|
|
-36 47 -14 0
|
|
36 5 81 0
|
|
-42 -44 53 0
|
|
9 82 -92 0
|
|
95 -29 -16 0
|
|
-55 -91 -2 0
|
|
51 3 -55 0
|
|
-37 -71 38 0
|
|
35 -68 -84 0
|
|
95 -79 -19 0
|
|
-65 34 64 0
|
|
-16 -53 -33 0
|
|
64 21 -33 0
|
|
-4 -45 59 0
|
|
-79 -64 22 0
|
|
71 38 35 0
|
|
-65 -20 -89 0
|
|
-60 -53 93 0
|
|
84 59 48 0
|
|
85 24 -81 0
|
|
7 91 -93 0
|
|
-79 -90 15 0
|
|
40 47 57 0
|
|
-35 -23 70 0
|
|
-99 -49 -39 0
|
|
34 61 -50 0
|
|
22 80 -64 0
|
|
-40 87 98 0
|
|
-8 54 59 0
|
|
92 34 71 0
|
|
89 -47 -85 0
|
|
-12 95 67 0
|
|
25 -70 100 0
|
|
58 -74 72 0
|
|
39 -42 -41 0
|
|
33 -60 -1 0
|
|
-4 -8 -68 0
|
|
-83 7 68 0
|
|
-100 87 -8 0
|
|
78 41 -100 0
|
|
-72 -82 30 0
|
|
45 -2 34 0
|
|
-10 54 22 0
|
|
11 36 -18 0
|
|
85 79 76 0
|
|
73 10 76 0
|
|
90 -10 -35 0
|
|
-11 -34 72 0
|
|
98 6 -57 0
|
|
-92 -97 74 0
|
|
12 71 -88 0
|
|
4 29 -24 0
|
|
16 43 -46 0
|
|
100 18 24 0
|
|
-6 27 -92 0
|
|
-84 95 5 0
|
|
-60 13 -52 0
|
|
56 33 3 0
|
|
67 -34 91 0
|
|
55 89 -1 0
|
|
-11 7 98 0
|
|
41 28 73 0
|
|
-78 77 -37 0
|
|
-46 85 36 0
|
|
-48 37 45 0
|
|
-85 -56 -36 0
|
|
6 100 -30 0
|
|
-6 21 -99 0
|
|
-30 -78 -35 0
|
|
-10 -19 -54 0
|
|
78 -24 -27 0
|
|
-48 95 -13 0
|
|
-81 -59 75 0
|
|
-95 69 60 0
|
|
70 58 61 0
|
|
15 -27 52 0
|
|
24 -17 -41 0
|
|
-12 73 38 0
|
|
-11 -33 97 0
|
|
-12 -62 93 0
|
|
100 70 -51 0
|
|
64 56 38 0
|
|
-13 -20 -54 0
|
|
-9 -90 79 0
|
|
-91 44 7 0
|
|
62 -29 -18 0
|
|
10 32 -12 0
|
|
64 45 79 0
|
|
-100 52 26 0
|
|
-92 -21 -51 0
|
|
-47 -44 -9 0
|
|
21 66 9 0
|
|
-91 -76 85 0
|
|
5 -93 79 0
|
|
-37 -63 30 0
|
|
-68 -7 56 0
|
|
-52 92 -77 0
|
|
-1 -15 -65 0
|
|
-14 87 51 0
|
|
1 53 83 0
|
|
-41 -7 50 0
|
|
-7 -34 12 0
|
|
73 -95 50 0
|
|
95 -94 20 0
|
|
66 87 89 0
|
|
91 -57 35 0
|
|
-61 60 51 0
|
|
-8 -15 40 0
|
|
91 -46 -15 0
|
|
47 56 86 0
|
|
-63 95 58 0
|
|
-14 -95 69 0
|
|
9 74 -26 0
|
|
69 22 -83 0
|
|
78 -69 -68 0
|
|
-75 67 27 0
|
|
85 -95 6 0
|
|
58 -35 42 0
|
|
-73 88 -40 0
|
|
38 98 -20 0
|
|
75 -85 -58 0
|
|
38 -41 53 0
|
|
61 -47 48 0
|
|
-20 -25 1 0
|
|
12 18 32 0
|
|
-97 -12 81 0
|
|
-36 -9 91 0
|
|
40 -46 -51 0
|
|
62 22 -64 0
|
|
-32 19 1 0
|
|
-86 38 41 0
|
|
-5 70 17 0
|
|
99 89 -61 0
|
|
-13 91 -79 0
|
|
-60 44 100 0
|
|
89 -93 77 0
|
|
-36 -64 82 0
|
|
68 58 19 0
|
|
-85 -19 39 0
|
|
44 54 -94 0
|
|
-83 2 -92 0
|
|
-72 66 -14 0
|
|
83 86 30 0
|
|
-50 -98 55 0
|
|
39 5 2 0
|
|
-31 17 -23 0
|
|
62 12 -86 0
|
|
-98 15 88 0
|
|
49 -26 78 0
|
|
75 91 27 0
|
|
-37 -69 59 0
|
|
31 22 16 0
|
|
-74 34 -60 0
|
|
-85 81 -13 0
|
|
87 -92 89 0
|
|
56 -35 -96 0
|
|
18 23 77 0
|
|
78 -14 -46 0
|
|
25 59 -58 0
|
|
36 7 -68 0
|
|
52 -76 -100 0
|
|
-3 7 -15 0
|
|
91 -17 67 0
|
|
-13 78 100 0
|
|
47 -51 26 0
|
|
-79 -26 21 0
|
|
-69 -76 -16 0
|
|
37 -45 71 0
|
|
44 -93 1 0
|
|
-62 10 66 0
|
|
-32 -2 67 0
|
|
-62 48 -14 0
|
|
31 -68 -12 0
|
|
24 -15 84 0
|
|
41 20 -58 0
|
|
47 -38 -82 0
|
|
52 8 66 0
|
|
-59 -6 44 0
|
|
84 90 -20 0
|
|
-48 -67 24 0
|
|
100 11 86 0
|
|
64 -52 -54 0
|
|
61 -39 -98 0
|
|
-40 -81 63 0
|
|
26 -37 76 0
|
|
54 90 -59 0
|
|
86 -66 -11 0
|
|
31 -54 29 0
|
|
-1 -99 -7 0
|
|
73 84 32 0
|
|
-96 87 12 0
|
|
12 11 -78 0
|
|
12 80 -26 0
|
|
-67 -8 83 0
|
|
-68 -43 -24 0
|
|
21 86 -43 0
|
|
45 -52 79 0
|
|
95 85 8 0
|
|
-4 -92 -24 0
|
|
26 32 37 0
|
|
6 -52 -13 0
|
|
-16 -29 -3 0
|
|
23 -46 -61 0
|
|
-46 -68 77 0
|
|
-63 80 73 0
|
|
26 -34 56 0
|
|
-90 -97 68 0
|
|
68 13 64 0
|
|
-15 -89 96 0
|
|
32 20 -29 0
|
|
-8 -44 -91 0
|
|
-2 -71 -69 0
|
|
-88 -30 72 0
|
|
-80 -73 -4 0
|
|
-25 -95 -81 0
|
|
10 -6 43 0
|
|
72 70 -95 0
|
|
-99 -27 87 0
|
|
-86 58 -17 0
|
|
49 58 -74 0
|
|
-29 21 77 0
|
|
-96 93 -14 0
|
|
47 32 -79 0
|
|
-77 -87 13 0
|
|
73 -24 3 0
|
|
-18 -82 -34 0
|
|
-39 49 -47 0
|