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