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