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