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