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