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