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