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