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