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