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