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