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