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