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