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