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