uf50-082.cnf 2.7 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229
  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 50 218
  9. 10 23 50 0
  10. -3 -32 -12 0
  11. -43 -22 -47 0
  12. 29 -43 -47 0
  13. 47 -44 -39 0
  14. -43 37 4 0
  15. 31 -16 -50 0
  16. 36 38 41 0
  17. 7 14 -16 0
  18. 19 48 38 0
  19. 6 11 12 0
  20. 14 42 31 0
  21. -4 42 -10 0
  22. -14 -12 -46 0
  23. 23 2 45 0
  24. -35 14 -24 0
  25. -11 -36 -25 0
  26. 14 -2 -22 0
  27. -5 -10 39 0
  28. -47 11 -24 0
  29. -4 -5 46 0
  30. -10 11 4 0
  31. -15 -16 -4 0
  32. 13 -45 -9 0
  33. -24 -41 -7 0
  34. 29 35 -31 0
  35. -43 21 -41 0
  36. -47 19 -8 0
  37. 49 18 -42 0
  38. 4 -43 26 0
  39. 37 -18 41 0
  40. -47 -34 21 0
  41. -29 -26 -44 0
  42. 34 -25 -17 0
  43. -10 -36 28 0
  44. -41 -33 -34 0
  45. 32 -47 -10 0
  46. 28 -12 -15 0
  47. -20 33 -15 0
  48. -21 17 -33 0
  49. -15 43 11 0
  50. -25 6 -7 0
  51. -24 35 -1 0
  52. -29 25 -31 0
  53. 40 -31 5 0
  54. 1 -45 49 0
  55. -22 18 -28 0
  56. 17 26 19 0
  57. -16 -43 49 0
  58. -35 -26 40 0
  59. -46 49 14 0
  60. -16 31 -25 0
  61. -28 -25 3 0
  62. 21 7 -9 0
  63. 29 -38 20 0
  64. 38 22 16 0
  65. -8 32 5 0
  66. 9 -2 -37 0
  67. -28 -18 -35 0
  68. -30 -16 26 0
  69. -16 21 -25 0
  70. 6 29 -22 0
  71. 23 -19 -47 0
  72. 37 -7 -11 0
  73. -10 22 -14 0
  74. 38 36 -18 0
  75. 3 -22 -18 0
  76. 20 5 -47 0
  77. 10 1 33 0
  78. -19 31 46 0
  79. -28 4 2 0
  80. 35 -19 41 0
  81. -30 -13 -27 0
  82. -2 38 41 0
  83. 9 26 43 0
  84. 21 -35 -13 0
  85. -42 14 -48 0
  86. -4 45 -2 0
  87. 21 22 17 0
  88. 23 16 50 0
  89. -25 41 42 0
  90. 16 -5 36 0
  91. 2 41 46 0
  92. 34 41 -38 0
  93. 25 -24 -10 0
  94. 32 -13 -21 0
  95. -45 -15 39 0
  96. -31 -29 -16 0
  97. -43 16 -27 0
  98. -25 40 -2 0
  99. -14 46 4 0
  100. 17 -13 -18 0
  101. -31 -23 24 0
  102. 32 42 -21 0
  103. -36 -47 -27 0
  104. -28 -43 36 0
  105. 35 -43 17 0
  106. 47 29 -32 0
  107. -25 5 -22 0
  108. 33 -48 40 0
  109. -50 -14 -13 0
  110. 40 -29 -32 0
  111. -15 -27 -8 0
  112. -27 21 -35 0
  113. -42 49 -46 0
  114. 1 -6 -44 0
  115. -1 -30 -17 0
  116. 11 -50 24 0
  117. -49 22 40 0
  118. -31 -12 5 0
  119. 7 43 18 0
  120. -39 7 6 0
  121. 50 24 -27 0
  122. -16 41 -36 0
  123. 31 22 46 0
  124. 13 7 -25 0
  125. 1 19 -21 0
  126. -9 7 -18 0
  127. 31 -40 -28 0
  128. 8 19 10 0
  129. -10 -38 -31 0
  130. -17 1 11 0
  131. -31 16 -24 0
  132. 36 -32 -37 0
  133. 2 4 45 0
  134. 35 17 7 0
  135. 7 17 -18 0
  136. -34 -29 9 0
  137. -19 11 43 0
  138. -34 12 -13 0
  139. -29 -34 -39 0
  140. 50 1 17 0
  141. 37 43 10 0
  142. 39 -32 -9 0
  143. -4 50 40 0
  144. 26 -2 11 0
  145. -18 -36 6 0
  146. -35 -26 -12 0
  147. 11 34 16 0
  148. -46 8 5 0
  149. 8 -32 24 0
  150. -23 17 -45 0
  151. 48 -35 10 0
  152. 43 40 -39 0
  153. 12 -5 1 0
  154. 38 -48 11 0
  155. 37 4 -14 0
  156. 13 38 7 0
  157. 14 8 -1 0
  158. -33 21 45 0
  159. -36 8 39 0
  160. -15 9 -28 0
  161. -27 36 -20 0
  162. -46 -21 44 0
  163. -40 24 -30 0
  164. 37 7 47 0
  165. -50 -18 27 0
  166. -9 23 -37 0
  167. -14 2 8 0
  168. 38 -29 -47 0
  169. -9 7 33 0
  170. 33 27 -28 0
  171. -18 46 15 0
  172. 10 -3 -21 0
  173. -34 37 4 0
  174. -16 -17 11 0
  175. -49 -32 46 0
  176. 5 9 14 0
  177. -27 -14 18 0
  178. -24 -13 5 0
  179. 30 -8 41 0
  180. 5 11 -32 0
  181. 11 38 -6 0
  182. 29 -21 31 0
  183. 22 42 30 0
  184. -22 35 50 0
  185. 32 -25 -15 0
  186. 50 38 -25 0
  187. 38 -32 -48 0
  188. 21 11 -28 0
  189. 11 47 -17 0
  190. -20 6 -5 0
  191. -22 18 19 0
  192. 24 -9 -2 0
  193. -6 -48 -3 0
  194. -15 8 -23 0
  195. 11 38 2 0
  196. 46 -43 37 0
  197. -35 -13 -17 0
  198. -28 39 -41 0
  199. -7 37 46 0
  200. -26 -29 2 0
  201. -46 39 17 0
  202. 40 37 18 0
  203. -50 40 -41 0
  204. 36 48 -24 0
  205. 41 -44 40 0
  206. -13 -26 -29 0
  207. -35 -15 3 0
  208. -42 37 43 0
  209. 9 2 33 0
  210. 8 -11 10 0
  211. -37 24 -1 0
  212. 16 15 -38 0
  213. -48 38 -33 0
  214. 38 6 -21 0
  215. 30 16 50 0
  216. 41 -37 22 0
  217. -38 2 -45 0
  218. 43 -41 17 0
  219. -9 50 -41 0
  220. 20 1 11 0
  221. 41 45 -11 0
  222. 20 -3 49 0
  223. 48 39 -43 0
  224. 17 -20 36 0
  225. 2 -18 8 0
  226. -37 -28 6 0
  227. %
  228. 0