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