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