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