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