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