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