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