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