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