uf100-041.cnf 5.2 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441
  1. c This Formular is generated by mcnf
  2. c
  3. c horn? no
  4. c forced? no
  5. c mixed sat? no
  6. c clause length = 3
  7. c
  8. p cnf 100 430
  9. -22 2 65 0
  10. -10 -20 40 0
  11. 47 81 -6 0
  12. -35 82 44 0
  13. 39 -76 -42 0
  14. -7 77 97 0
  15. 78 54 52 0
  16. -55 -68 100 0
  17. -13 15 6 0
  18. 92 -40 -2 0
  19. 29 60 -32 0
  20. 58 8 29 0
  21. 29 80 -18 0
  22. -53 52 13 0
  23. -84 99 54 0
  24. -40 -59 -66 0
  25. -48 -41 4 0
  26. 26 79 8 0
  27. -41 60 98 0
  28. -68 2 22 0
  29. -26 -92 -93 0
  30. 44 -16 93 0
  31. -45 -28 87 0
  32. 12 -72 81 0
  33. 31 78 -69 0
  34. 42 -1 -89 0
  35. 82 -92 -70 0
  36. 46 -2 -19 0
  37. 60 -66 65 0
  38. -88 27 17 0
  39. 52 84 28 0
  40. -19 3 -95 0
  41. -79 -50 54 0
  42. -90 -43 -73 0
  43. 93 70 94 0
  44. -36 78 19 0
  45. -67 37 43 0
  46. -13 -3 -97 0
  47. 73 89 21 0
  48. 13 34 -73 0
  49. -43 79 -76 0
  50. 2 -9 -30 0
  51. -91 81 -56 0
  52. -66 -19 -43 0
  53. -91 -77 -19 0
  54. 61 -26 -41 0
  55. -30 88 -91 0
  56. -13 22 -40 0
  57. -23 -75 -6 0
  58. -50 52 46 0
  59. -30 76 55 0
  60. 52 -41 -29 0
  61. 1 -12 -82 0
  62. 27 -3 65 0
  63. 2 -19 -79 0
  64. 77 -16 -69 0
  65. -72 -37 22 0
  66. 59 79 33 0
  67. -30 -46 -15 0
  68. -22 79 -1 0
  69. -93 2 -3 0
  70. -42 4 24 0
  71. 84 61 -80 0
  72. 28 31 44 0
  73. 25 46 99 0
  74. 13 -39 -27 0
  75. 2 42 -62 0
  76. 26 88 25 0
  77. 3 -32 -56 0
  78. -67 98 -26 0
  79. 90 35 9 0
  80. -75 -51 -36 0
  81. 2 43 24 0
  82. -10 -78 -5 0
  83. -22 -48 -10 0
  84. -78 -6 -90 0
  85. 68 -5 50 0
  86. 2 -82 -47 0
  87. -75 -97 71 0
  88. -64 -74 69 0
  89. 54 38 -45 0
  90. -43 99 -4 0
  91. 96 3 -65 0
  92. 36 -3 -48 0
  93. -27 45 73 0
  94. -35 72 71 0
  95. -78 58 100 0
  96. 65 -44 4 0
  97. 81 21 34 0
  98. -27 54 -61 0
  99. 32 -84 -50 0
  100. 4 41 -23 0
  101. 4 86 16 0
  102. -39 94 22 0
  103. 88 49 -3 0
  104. -26 -80 -36 0
  105. -41 -86 -39 0
  106. 35 -93 -45 0
  107. -51 38 -52 0
  108. 21 98 -22 0
  109. 74 70 49 0
  110. 7 86 17 0
  111. 5 83 -98 0
  112. -7 -83 36 0
  113. -32 -75 -43 0
  114. -22 -72 57 0
  115. 1 87 88 0
  116. 22 -36 -19 0
  117. -18 92 -33 0
  118. 98 81 -61 0
  119. -27 55 30 0
  120. -85 26 96 0
  121. -8 64 -27 0
  122. -1 -39 -9 0
  123. -50 69 56 0
  124. -16 -56 -43 0
  125. -84 6 -48 0
  126. -64 -11 -39 0
  127. -67 94 26 0
  128. 71 -97 -83 0
  129. 40 2 83 0
  130. 85 -26 -83 0
  131. -5 -84 -97 0
  132. 61 71 10 0
  133. 7 -14 -6 0
  134. -73 2 30 0
  135. -90 86 75 0
  136. 30 31 27 0
  137. 85 -78 20 0
  138. -28 10 49 0
  139. -32 11 68 0
  140. 77 98 91 0
  141. 78 -54 -69 0
  142. 15 -63 54 0
  143. 78 -12 -58 0
  144. 65 -3 -77 0
  145. 49 66 86 0
  146. 78 -92 63 0
  147. -22 11 -4 0
  148. -24 23 -98 0
  149. 48 13 -72 0
  150. -13 94 26 0
  151. -8 -11 31 0
  152. 12 -77 -37 0
  153. -1 -75 -4 0
  154. 68 4 65 0
  155. 99 41 4 0
  156. -64 48 46 0
  157. -20 30 79 0
  158. 38 45 -5 0
  159. -93 10 -65 0
  160. -68 -47 -33 0
  161. -7 34 19 0
  162. 54 48 66 0
  163. -63 -41 -53 0
  164. -29 74 -6 0
  165. 85 -99 -100 0
  166. 88 75 5 0
  167. 43 81 -80 0
  168. -17 77 23 0
  169. -65 -73 77 0
  170. 24 -50 -5 0
  171. -94 -54 -48 0
  172. 31 3 -56 0
  173. 92 -28 -45 0
  174. 17 62 94 0
  175. -55 76 -6 0
  176. -72 -96 27 0
  177. 1 -59 57 0
  178. 2 -98 -70 0
  179. 33 -56 21 0
  180. 26 42 -23 0
  181. 9 -91 61 0
  182. -36 -61 75 0
  183. -17 -72 43 0
  184. -45 20 -92 0
  185. 12 -70 19 0
  186. -99 9 -28 0
  187. 75 -80 49 0
  188. 94 -88 -91 0
  189. -73 -18 97 0
  190. -42 94 11 0
  191. 98 -26 -20 0
  192. -14 58 43 0
  193. 80 -1 70 0
  194. -9 -92 -44 0
  195. -14 -68 97 0
  196. -72 20 -27 0
  197. -10 -61 32 0
  198. 51 68 46 0
  199. 68 -14 -11 0
  200. -97 -100 52 0
  201. 100 45 -65 0
  202. 16 51 -29 0
  203. 92 -72 -64 0
  204. -56 -60 -82 0
  205. 50 -67 68 0
  206. 47 -59 85 0
  207. 79 1 -77 0
  208. -2 -39 -70 0
  209. 33 -32 -21 0
  210. 82 47 58 0
  211. -90 94 -76 0
  212. -100 -84 61 0
  213. 74 -92 47 0
  214. 5 89 -54 0
  215. -16 86 98 0
  216. -91 -24 39 0
  217. -27 98 -87 0
  218. -48 -8 -41 0
  219. 95 -52 -17 0
  220. 35 -41 65 0
  221. -99 -98 -49 0
  222. -91 -93 19 0
  223. 72 14 42 0
  224. -75 99 57 0
  225. 59 -53 52 0
  226. -33 60 24 0
  227. -73 -15 -12 0
  228. -26 -63 -92 0
  229. 71 49 95 0
  230. -39 100 65 0
  231. 16 55 86 0
  232. -58 -9 23 0
  233. 47 -24 -77 0
  234. 34 -62 100 0
  235. 41 28 -39 0
  236. 31 -33 -16 0
  237. 25 -29 -60 0
  238. 62 -44 -83 0
  239. -88 16 35 0
  240. -27 -84 -50 0
  241. 27 19 -100 0
  242. -94 58 -100 0
  243. -12 66 41 0
  244. 67 -91 -38 0
  245. -24 -4 -64 0
  246. 40 96 70 0
  247. 11 -31 -61 0
  248. 8 -96 32 0
  249. 71 -56 26 0
  250. -88 -80 -7 0
  251. -2 92 71 0
  252. 75 -43 39 0
  253. 1 61 19 0
  254. -67 -79 64 0
  255. 95 74 -99 0
  256. 77 -27 -43 0
  257. -55 72 -16 0
  258. 16 7 29 0
  259. 42 -5 16 0
  260. 24 -91 -75 0
  261. 72 68 26 0
  262. 88 -69 95 0
  263. 73 77 7 0
  264. -39 -52 50 0
  265. 55 79 37 0
  266. -28 -73 96 0
  267. -76 -75 77 0
  268. -70 -51 15 0
  269. -22 90 76 0
  270. -17 98 11 0
  271. -81 55 -83 0
  272. -85 -83 44 0
  273. 99 -22 73 0
  274. 38 -20 -15 0
  275. -45 -8 -56 0
  276. 66 41 37 0
  277. -18 -100 -26 0
  278. -84 -60 -100 0
  279. -81 10 17 0
  280. 53 68 -16 0
  281. 90 88 16 0
  282. -69 54 -31 0
  283. -72 -99 51 0
  284. -69 36 -33 0
  285. 93 -84 23 0
  286. -83 81 -34 0
  287. -29 -75 24 0
  288. -50 42 -38 0
  289. -23 -81 -28 0
  290. 10 -59 42 0
  291. 78 49 13 0
  292. 81 76 -94 0
  293. -44 -85 5 0
  294. 73 -7 -97 0
  295. -59 71 -21 0
  296. 33 -82 -36 0
  297. -65 -74 -59 0
  298. 22 21 -78 0
  299. 43 -75 69 0
  300. 2 33 1 0
  301. 9 66 -86 0
  302. -26 75 51 0
  303. -77 -54 -50 0
  304. -16 -22 -26 0
  305. 15 -63 -33 0
  306. 19 92 31 0
  307. 82 61 16 0
  308. 62 -20 -2 0
  309. -63 -90 -2 0
  310. 88 89 25 0
  311. 86 23 1 0
  312. -58 9 97 0
  313. 21 2 61 0
  314. 3 -75 -24 0
  315. -68 -50 -86 0
  316. 1 -56 11 0
  317. 38 30 -46 0
  318. 74 24 89 0
  319. -68 -48 76 0
  320. 88 -20 -73 0
  321. 13 -12 73 0
  322. -51 13 56 0
  323. -58 -39 30 0
  324. 59 -32 7 0
  325. 37 4 -32 0
  326. 71 27 -1 0
  327. 54 -92 97 0
  328. 51 33 80 0
  329. 82 65 -17 0
  330. -67 -53 -92 0
  331. -47 94 -81 0
  332. -43 26 -61 0
  333. -2 -34 -23 0
  334. 92 -40 -21 0
  335. -69 37 -22 0
  336. 41 59 83 0
  337. 85 91 43 0
  338. 18 45 77 0
  339. 96 17 74 0
  340. 86 -93 -80 0
  341. -97 93 -51 0
  342. 96 98 90 0
  343. -82 -60 76 0
  344. -92 95 18 0
  345. -9 97 -35 0
  346. 81 -1 -80 0
  347. 29 75 90 0
  348. 50 -94 -92 0
  349. 26 44 -85 0
  350. 86 18 -91 0
  351. -9 86 -95 0
  352. -82 -45 -48 0
  353. -4 13 54 0
  354. -85 64 -49 0
  355. -63 93 -75 0
  356. 49 22 -66 0
  357. -17 -92 -27 0
  358. -25 -66 2 0
  359. 83 44 3 0
  360. -88 75 3 0
  361. 42 77 39 0
  362. 89 -36 40 0
  363. 6 25 67 0
  364. 47 86 -70 0
  365. -59 -5 -57 0
  366. 78 8 -62 0
  367. 64 4 16 0
  368. -5 25 40 0
  369. -98 78 27 0
  370. 50 86 48 0
  371. -91 25 22 0
  372. 32 5 -41 0
  373. 63 -13 85 0
  374. -44 82 94 0
  375. -14 98 -7 0
  376. -76 94 79 0
  377. -34 77 23 0
  378. 35 -87 43 0
  379. 35 33 -8 0
  380. -50 -18 -55 0
  381. -10 -54 -52 0
  382. 7 -85 -74 0
  383. 61 94 -86 0
  384. 30 -48 7 0
  385. 94 -26 28 0
  386. -7 -92 60 0
  387. 56 87 -95 0
  388. 28 -76 -47 0
  389. -87 8 -6 0
  390. 4 -39 -7 0
  391. -38 -94 -80 0
  392. 8 7 -45 0
  393. 56 -64 37 0
  394. -62 -63 -23 0
  395. -49 -60 -7 0
  396. 45 28 88 0
  397. 82 33 -47 0
  398. 87 -90 46 0
  399. -38 54 84 0
  400. 27 69 -99 0
  401. 27 -69 18 0
  402. -54 74 75 0
  403. 83 87 -100 0
  404. 50 48 -45 0
  405. -72 -34 -33 0
  406. -61 94 27 0
  407. -21 -62 -92 0
  408. 5 -44 -79 0
  409. 96 -21 36 0
  410. 4 -26 77 0
  411. 95 57 37 0
  412. 39 -56 -7 0
  413. 22 -56 -13 0
  414. 90 -55 -5 0
  415. 68 98 -85 0
  416. 87 29 -38 0
  417. -68 87 -28 0
  418. -43 39 -34 0
  419. 39 -28 49 0
  420. -2 -21 -41 0
  421. 67 -50 -4 0
  422. 76 41 -40 0
  423. 81 57 95 0
  424. -8 -51 61 0
  425. 99 -96 -34 0
  426. 15 -48 47 0
  427. 71 27 -60 0
  428. -66 11 32 0
  429. -93 -33 -94 0
  430. 67 87 -82 0
  431. 98 -41 -11 0
  432. 64 29 89 0
  433. 99 -5 -28 0
  434. -73 58 -85 0
  435. 53 -77 -60 0
  436. 98 75 -26 0
  437. -71 83 -13 0
  438. 76 5 56 0
  439. %
  440. 0