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