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