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