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