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