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