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