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