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