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