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