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