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