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