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