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