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