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