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