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