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