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