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