uf150-024.cnf 8.6 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656
  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 150 645
  9. -18 82 -78 0
  10. -115 -82 146 0
  11. -121 8 -70 0
  12. 146 136 125 0
  13. -137 -26 74 0
  14. -12 -95 150 0
  15. 20 45 110 0
  16. -43 7 -81 0
  17. 75 147 -113 0
  18. -55 -22 -4 0
  19. 47 132 -25 0
  20. 75 -92 150 0
  21. 109 -150 43 0
  22. -16 -36 39 0
  23. -106 -140 95 0
  24. 39 15 -47 0
  25. 18 136 60 0
  26. -53 129 -16 0
  27. 138 34 -13 0
  28. 100 -117 87 0
  29. 110 114 -69 0
  30. 126 45 -115 0
  31. 51 -114 67 0
  32. 46 14 56 0
  33. 22 143 -89 0
  34. 27 32 62 0
  35. 8 102 -6 0
  36. 94 126 -103 0
  37. -53 80 -98 0
  38. 111 -24 116 0
  39. -43 -116 -64 0
  40. -144 7 -73 0
  41. -139 143 -62 0
  42. -26 55 25 0
  43. 96 123 -49 0
  44. 94 64 -105 0
  45. 129 12 111 0
  46. 137 -150 3 0
  47. 144 -117 60 0
  48. -44 -35 46 0
  49. 82 40 -131 0
  50. -140 -26 10 0
  51. -110 -64 -19 0
  52. 118 -105 76 0
  53. -101 -16 -50 0
  54. 63 40 -35 0
  55. 42 65 108 0
  56. -71 -124 98 0
  57. -50 -55 -15 0
  58. 140 32 -3 0
  59. 35 -90 150 0
  60. -2 -26 139 0
  61. -143 -148 127 0
  62. 150 -136 117 0
  63. 150 -101 -81 0
  64. -113 -25 48 0
  65. 36 96 -57 0
  66. 27 -47 130 0
  67. 66 -137 53 0
  68. 82 150 -115 0
  69. 120 -114 129 0
  70. -49 -112 18 0
  71. 88 13 -119 0
  72. 135 -82 -92 0
  73. 52 46 -92 0
  74. -120 27 -58 0
  75. 21 93 -94 0
  76. -111 137 -91 0
  77. -35 -39 38 0
  78. 69 -128 -47 0
  79. 103 113 131 0
  80. -143 -81 119 0
  81. -15 80 3 0
  82. -62 44 96 0
  83. -101 -88 -150 0
  84. -102 51 105 0
  85. -108 -53 96 0
  86. -92 -3 145 0
  87. -1 -20 46 0
  88. -118 70 -4 0
  89. 109 -18 2 0
  90. 79 -58 -115 0
  91. -90 75 107 0
  92. -87 -19 85 0
  93. 48 82 122 0
  94. 3 7 56 0
  95. 66 149 63 0
  96. -134 113 -121 0
  97. -4 -134 -8 0
  98. -141 14 -54 0
  99. 1 68 109 0
  100. -62 136 27 0
  101. -21 -150 13 0
  102. -130 92 44 0
  103. 110 -20 -24 0
  104. 116 133 -6 0
  105. -102 101 -62 0
  106. 29 -96 77 0
  107. -102 66 -107 0
  108. 4 14 -6 0
  109. -116 142 121 0
  110. -47 -17 109 0
  111. -36 24 130 0
  112. -127 16 132 0
  113. -70 14 48 0
  114. 64 -6 -67 0
  115. 43 -23 -149 0
  116. 36 -16 -17 0
  117. 81 104 -97 0
  118. -97 108 121 0
  119. -69 -97 -18 0
  120. -118 24 -17 0
  121. -110 -61 -12 0
  122. 58 6 -93 0
  123. -111 13 -88 0
  124. -93 76 68 0
  125. -104 -29 -72 0
  126. -116 -104 -8 0
  127. 117 -137 88 0
  128. -39 102 17 0
  129. 97 -126 100 0
  130. -63 40 39 0
  131. -81 -125 136 0
  132. -20 -69 52 0
  133. -111 -17 144 0
  134. -1 -90 -2 0
  135. -111 -16 -127 0
  136. 32 79 110 0
  137. -82 -36 -131 0
  138. 25 -103 -124 0
  139. 44 81 56 0
  140. -133 -142 25 0
  141. 94 23 -103 0
  142. -116 -122 -4 0
  143. 55 -130 99 0
  144. 145 -42 -109 0
  145. -60 69 -132 0
  146. 107 121 145 0
  147. 27 -140 -7 0
  148. -26 141 -91 0
  149. -2 14 130 0
  150. -101 124 135 0
  151. 55 14 133 0
  152. -85 -99 -147 0
  153. -52 -4 -74 0
  154. 81 -130 107 0
  155. -126 -41 144 0
  156. -122 -27 -64 0
  157. -111 -11 84 0
  158. -40 -3 66 0
  159. 56 -77 -23 0
  160. 33 113 -3 0
  161. -78 -45 -3 0
  162. 126 109 89 0
  163. 121 105 42 0
  164. -78 -124 -114 0
  165. 63 19 -62 0
  166. 41 -123 29 0
  167. 121 -90 136 0
  168. -98 119 6 0
  169. -27 82 47 0
  170. 90 94 -51 0
  171. 136 -49 69 0
  172. 41 -61 -122 0
  173. -78 68 -88 0
  174. 6 83 22 0
  175. -84 12 146 0
  176. -81 149 -52 0
  177. 31 -53 54 0
  178. 121 -7 -90 0
  179. 148 -95 80 0
  180. 72 80 13 0
  181. -72 -144 24 0
  182. 116 23 89 0
  183. -42 146 -25 0
  184. 128 51 58 0
  185. 59 142 133 0
  186. -97 -131 41 0
  187. -6 -69 -56 0
  188. -113 -129 -75 0
  189. 100 -88 -29 0
  190. 60 -53 -90 0
  191. -89 70 -130 0
  192. 12 -46 -1 0
  193. 147 -102 66 0
  194. -50 37 -114 0
  195. -26 -103 -10 0
  196. -115 84 -53 0
  197. 27 -74 -138 0
  198. 115 138 79 0
  199. 56 109 -53 0
  200. -127 62 49 0
  201. 119 -143 127 0
  202. -115 -113 -102 0
  203. -104 -90 7 0
  204. 40 -107 76 0
  205. 35 -54 -70 0
  206. 139 75 -90 0
  207. -125 -124 90 0
  208. 5 67 -132 0
  209. -35 -90 -86 0
  210. 131 32 132 0
  211. -13 41 -138 0
  212. 80 -26 -122 0
  213. 62 -107 2 0
  214. -23 -3 -141 0
  215. 37 -93 20 0
  216. 83 -7 111 0
  217. 69 -38 -41 0
  218. 120 96 127 0
  219. -36 67 19 0
  220. 32 -122 -27 0
  221. 133 -121 58 0
  222. 121 117 -107 0
  223. -136 144 -41 0
  224. 141 42 22 0
  225. 17 -68 -22 0
  226. 140 100 107 0
  227. 117 -123 3 0
  228. 18 -120 21 0
  229. 14 -72 -70 0
  230. -85 -98 -23 0
  231. 92 129 -90 0
  232. -84 142 66 0
  233. -114 -82 -19 0
  234. -12 4 -23 0
  235. 36 -123 51 0
  236. 49 20 -139 0
  237. -2 -37 146 0
  238. 51 34 64 0
  239. -47 28 -36 0
  240. 14 -39 -40 0
  241. -121 137 -99 0
  242. 40 -56 -31 0
  243. -81 -45 15 0
  244. 7 -127 -67 0
  245. 33 118 -22 0
  246. -3 -11 126 0
  247. -95 10 -86 0
  248. -108 -126 123 0
  249. -11 126 -29 0
  250. -60 -51 -100 0
  251. 69 -125 -1 0
  252. 74 -21 130 0
  253. 88 -104 -150 0
  254. -113 87 -95 0
  255. 123 74 -14 0
  256. 63 -73 112 0
  257. 33 39 59 0
  258. 37 135 -8 0
  259. -6 -7 21 0
  260. -62 120 -108 0
  261. 62 105 -34 0
  262. -60 51 -39 0
  263. 23 -100 -71 0
  264. -115 -142 -121 0
  265. -20 -3 -88 0
  266. -90 140 -84 0
  267. 123 72 2 0
  268. 97 -63 -13 0
  269. -132 57 -141 0
  270. 70 62 84 0
  271. 136 -129 150 0
  272. 21 -74 -84 0
  273. -86 31 -36 0
  274. -98 -29 -35 0
  275. -19 51 139 0
  276. -113 -43 -6 0
  277. 125 134 -30 0
  278. 32 92 144 0
  279. -45 137 70 0
  280. -7 93 101 0
  281. 22 -8 51 0
  282. 133 94 147 0
  283. -125 -33 -93 0
  284. -9 144 120 0
  285. -129 80 137 0
  286. -87 -96 38 0
  287. -150 -105 -101 0
  288. -149 91 -135 0
  289. 74 -68 78 0
  290. 86 124 81 0
  291. -103 -139 100 0
  292. -148 -126 -26 0
  293. 51 120 -83 0
  294. 120 134 59 0
  295. -49 112 -28 0
  296. -134 -137 70 0
  297. 6 125 -20 0
  298. -24 124 110 0
  299. 96 130 4 0
  300. -58 76 142 0
  301. -16 -39 -12 0
  302. -129 128 113 0
  303. -140 -32 9 0
  304. -119 -84 147 0
  305. -2 -145 100 0
  306. 18 96 44 0
  307. -17 9 144 0
  308. 14 -147 34 0
  309. 40 64 105 0
  310. 61 38 -36 0
  311. 15 -49 -61 0
  312. 74 95 -99 0
  313. -69 -88 103 0
  314. -124 150 -112 0
  315. 119 -96 36 0
  316. 120 121 115 0
  317. 121 102 136 0
  318. -26 87 -147 0
  319. -26 -12 -105 0
  320. 134 58 87 0
  321. 85 32 13 0
  322. -91 -33 141 0
  323. -136 -129 -95 0
  324. 88 -131 -145 0
  325. -33 -101 141 0
  326. 12 -55 -84 0
  327. 64 -45 -28 0
  328. 63 -106 108 0
  329. -141 26 45 0
  330. 70 101 -113 0
  331. 113 -81 -138 0
  332. 41 17 -137 0
  333. 48 -134 63 0
  334. -70 -132 -26 0
  335. -126 -37 -44 0
  336. 22 -59 -43 0
  337. -102 145 -13 0
  338. -45 -110 66 0
  339. -108 -34 38 0
  340. -77 124 -41 0
  341. -82 -84 -46 0
  342. -120 -44 145 0
  343. -64 -25 -16 0
  344. 36 90 15 0
  345. -78 -149 136 0
  346. 106 50 131 0
  347. -1 -143 -117 0
  348. 52 39 -122 0
  349. 49 -54 -44 0
  350. 75 55 -116 0
  351. -107 -129 133 0
  352. -10 -130 -149 0
  353. 73 -27 11 0
  354. 149 142 82 0
  355. -9 129 -113 0
  356. 57 -145 -114 0
  357. 45 91 73 0
  358. 16 139 74 0
  359. -54 32 9 0
  360. 44 82 -42 0
  361. -142 112 74 0
  362. -48 -45 95 0
  363. -18 -104 149 0
  364. -108 33 -64 0
  365. 30 62 -69 0
  366. 150 60 -86 0
  367. 78 64 131 0
  368. 32 -51 22 0
  369. -62 99 34 0
  370. 111 95 113 0
  371. -4 -16 -91 0
  372. 25 17 19 0
  373. -74 -70 -103 0
  374. -97 -11 -43 0
  375. -32 -96 53 0
  376. -25 129 85 0
  377. -71 -93 -40 0
  378. -141 -22 -147 0
  379. -37 64 -106 0
  380. -37 75 36 0
  381. -9 94 140 0
  382. 116 129 -149 0
  383. -82 58 -118 0
  384. -25 -38 149 0
  385. -71 -4 118 0
  386. -117 102 130 0
  387. 13 10 -16 0
  388. -109 97 -141 0
  389. 12 49 -29 0
  390. 53 100 -149 0
  391. 56 -22 -43 0
  392. -72 141 -96 0
  393. 21 111 -56 0
  394. 3 49 129 0
  395. 26 -111 107 0
  396. 115 37 34 0
  397. 94 -143 3 0
  398. 149 -101 116 0
  399. -135 -114 -52 0
  400. -121 20 71 0
  401. -90 9 88 0
  402. -135 -109 -1 0
  403. -142 146 -32 0
  404. 110 -35 -107 0
  405. 121 119 -41 0
  406. -135 22 29 0
  407. -93 -146 -38 0
  408. 71 139 -1 0
  409. -137 73 101 0
  410. 119 -38 22 0
  411. -101 69 -58 0
  412. 17 119 -91 0
  413. 23 -117 -72 0
  414. -17 -131 -33 0
  415. 18 -97 140 0
  416. -76 57 142 0
  417. 79 -52 136 0
  418. 102 128 -150 0
  419. 134 -17 -124 0
  420. -118 2 49 0
  421. 31 -117 -61 0
  422. 40 29 -148 0
  423. 58 150 -82 0
  424. 51 7 -98 0
  425. 127 -140 -83 0
  426. -30 -128 90 0
  427. 37 40 -69 0
  428. 138 123 -116 0
  429. -150 -81 146 0
  430. -29 -82 -8 0
  431. 85 -137 -83 0
  432. -65 -113 122 0
  433. 100 134 9 0
  434. 55 -52 119 0
  435. 67 -29 -5 0
  436. -28 -75 98 0
  437. 42 -14 -137 0
  438. 50 97 118 0
  439. 97 -66 72 0
  440. -138 -31 -100 0
  441. 104 -132 -14 0
  442. 76 -134 -126 0
  443. -46 -69 13 0
  444. -50 -146 104 0
  445. -102 -142 124 0
  446. -47 78 77 0
  447. -23 -2 -14 0
  448. -131 -44 -54 0
  449. -26 47 -130 0
  450. -3 113 81 0
  451. 40 -103 117 0
  452. 74 -123 20 0
  453. -140 14 59 0
  454. -8 57 -22 0
  455. -140 -30 42 0
  456. -7 -39 -21 0
  457. -129 13 -114 0
  458. 3 -11 -98 0
  459. -104 -1 -14 0
  460. -86 -127 110 0
  461. 45 99 83 0
  462. 56 50 34 0
  463. 104 -49 65 0
  464. 8 64 59 0
  465. 101 -125 -22 0
  466. 105 146 -63 0
  467. -60 -116 -33 0
  468. 149 -89 -129 0
  469. 121 147 2 0
  470. -74 119 -14 0
  471. -59 134 111 0
  472. -105 81 -137 0
  473. 67 -22 61 0
  474. -134 -56 47 0
  475. 25 -8 33 0
  476. -4 -12 45 0
  477. -135 88 147 0
  478. 94 142 -43 0
  479. -55 20 -33 0
  480. 15 29 -126 0
  481. 109 71 90 0
  482. 70 -20 -11 0
  483. -87 -85 -77 0
  484. -106 -143 -134 0
  485. -106 109 -17 0
  486. -9 -116 5 0
  487. 21 -39 59 0
  488. 117 41 135 0
  489. -7 -126 67 0
  490. -129 -69 -119 0
  491. -80 -8 90 0
  492. 124 127 98 0
  493. 82 124 -93 0
  494. 140 24 88 0
  495. 66 -143 -120 0
  496. -9 68 -126 0
  497. -7 125 58 0
  498. -6 89 39 0
  499. -61 145 -80 0
  500. 49 -117 86 0
  501. -137 -9 -141 0
  502. -44 113 -118 0
  503. 18 72 63 0
  504. 112 -82 -63 0
  505. 135 -129 -80 0
  506. -144 -134 88 0
  507. -128 -140 6 0
  508. -69 109 144 0
  509. -49 127 96 0
  510. 74 2 -4 0
  511. 83 66 -134 0
  512. 63 -28 69 0
  513. -140 40 -119 0
  514. -149 69 -110 0
  515. -120 -104 130 0
  516. -123 40 117 0
  517. -35 121 46 0
  518. -115 29 -57 0
  519. 67 -11 147 0
  520. -4 74 -130 0
  521. 34 -19 126 0
  522. 18 -10 5 0
  523. -81 78 -71 0
  524. 65 -77 94 0
  525. 87 -106 122 0
  526. -4 -122 37 0
  527. 13 140 -21 0
  528. -61 -134 62 0
  529. 64 -36 -149 0
  530. 55 -33 -57 0
  531. -43 -104 -117 0
  532. -91 -95 -79 0
  533. 95 23 -115 0
  534. -78 68 121 0
  535. -27 129 100 0
  536. 79 -47 -3 0
  537. 134 67 -30 0
  538. 44 -122 14 0
  539. 94 -55 84 0
  540. -130 -7 -137 0
  541. -129 19 38 0
  542. -65 -47 -80 0
  543. -85 2 78 0
  544. 116 103 -110 0
  545. 58 146 97 0
  546. 35 53 -55 0
  547. 86 98 -15 0
  548. 122 126 -125 0
  549. 104 -41 -87 0
  550. -3 147 99 0
  551. -136 -76 40 0
  552. -84 -57 -22 0
  553. -71 -74 -119 0
  554. -74 -38 -40 0
  555. -140 125 -90 0
  556. -74 -91 -39 0
  557. -121 -21 54 0
  558. -137 40 75 0
  559. -59 83 -110 0
  560. 90 -60 -62 0
  561. 143 72 -17 0
  562. -29 -6 -125 0
  563. 84 -135 -134 0
  564. 80 -149 -76 0
  565. 127 37 55 0
  566. -115 -59 125 0
  567. 86 119 16 0
  568. -4 -134 -148 0
  569. 131 -71 86 0
  570. -52 -86 -69 0
  571. -9 89 -45 0
  572. 144 5 103 0
  573. 21 69 -137 0
  574. 106 -36 48 0
  575. -74 -143 93 0
  576. 128 -108 -6 0
  577. -6 -84 -80 0
  578. -112 -114 -63 0
  579. -76 -87 -4 0
  580. 131 51 88 0
  581. -140 20 -143 0
  582. 71 48 -18 0
  583. 146 118 74 0
  584. 26 -143 -141 0
  585. 125 96 18 0
  586. -98 9 -80 0
  587. 24 -75 19 0
  588. 2 -71 142 0
  589. -129 4 51 0
  590. -87 8 -112 0
  591. -15 -17 -139 0
  592. -65 131 -68 0
  593. -108 -24 63 0
  594. 7 77 -45 0
  595. 73 -132 86 0
  596. 14 101 -21 0
  597. 144 110 -108 0
  598. -54 -150 -3 0
  599. 7 106 27 0
  600. 130 -85 -54 0
  601. -69 -132 -91 0
  602. 67 127 -95 0
  603. 3 91 -137 0
  604. -105 -64 41 0
  605. -53 95 -139 0
  606. 97 78 88 0
  607. -22 -83 -48 0
  608. -103 -109 -26 0
  609. 25 69 -147 0
  610. -119 103 57 0
  611. 63 6 143 0
  612. -71 64 92 0
  613. -53 133 -7 0
  614. 11 96 -39 0
  615. 119 -129 -41 0
  616. -91 -148 -105 0
  617. 92 69 -61 0
  618. -81 89 -73 0
  619. -57 28 -91 0
  620. 34 4 80 0
  621. -23 119 13 0
  622. 124 144 -80 0
  623. 125 107 55 0
  624. -43 101 -99 0
  625. 84 80 137 0
  626. 28 26 134 0
  627. -51 126 29 0
  628. -96 135 12 0
  629. 72 75 7 0
  630. -4 141 -132 0
  631. -5 31 10 0
  632. 23 -121 -138 0
  633. -105 46 133 0
  634. 22 -117 -90 0
  635. 80 -140 -138 0
  636. 46 -134 -22 0
  637. 66 145 63 0
  638. 51 -150 -59 0
  639. -48 138 70 0
  640. -135 94 47 0
  641. -113 -50 -10 0
  642. -76 20 126 0
  643. 1 124 -21 0
  644. -12 54 -124 0
  645. 139 -27 -82 0
  646. 61 -111 -135 0
  647. 51 20 109 0
  648. 47 8 5 0
  649. 54 78 -66 0
  650. -14 148 -133 0
  651. 31 92 -16 0
  652. 63 -56 -89 0
  653. -70 -100 -53 0
  654. %
  655. 0