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