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