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