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