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