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