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