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