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