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