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