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