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