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