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