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