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