c Lingeling SAT Solver
c 
c Version bcj 78ebb8672540bde0a335aea946bbf32515157d5a
c 
c Copyright (C) 2010-2016 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Thu May 17 11:57:41 CEST 2018
c compiled Sun Dec  1 22:34:55 CET 2019
c 
c gcc (Ubuntu 7.4.0-1ubuntu1~18.04.1) 7.4.0
c -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
c -DNLGLFILES -DNLGLDEMA
c Linux Flensburg 4.15.0-70-generic x86_64
c 
c 
c  seconds         irredundant            redundant clauses   glue   iterations"      MB    stability
c          variables clauses conflicts  large ternary binary     jlevel       jlevel'  agility     tlevel
c 
c  S    0.0     369     9654         0       0      0     0    0     0      0     0    1   0     0      0
c 
c  seconds         irredundant            redundant clauses   glue   iterations"      MB    stability
c          variables clauses conflicts  large ternary binary     jlevel       jlevel'  agility     tlevel
c 
s SATISFIABLE
v -1 -2 -3 -4 -5 6 7 8 -9 10 11 12 -13 -14 -15 -16 17 -18 -19 -20 21 -22 -23 24
v 25 26 27 -28 -29 30 -31 -32 -33 -34 -35 -36 -37 -38 39 -40 -41 42 43 44 -45
v -46 -47 48 -49 -50 51 52 53 54 55 56 57 -58 59 -60 -61 -62 63 64 65 -66 -67
v -68 -69 -70 -71 72 73 74 -75 76 -77 -78 -79 -80 81 82 83 84 -85 -86 -87 -88
v -89 -90 -91 92 -93 -94 -95 -96 97 -98 99 100 101 -102 -103 104 -105 -106 -107
v 108 -109 -110 -111 -112 -113 -114 -115 116 117 118 -119 -120 -121 -122 -123
v -124 -125 126 -127 -128 -129 -130 -131 132 -133 -134 -135 -136 -137 -138 -139
v -140 -141 142 -143 -144 -145 -146 -147 -148 -149 -150 151 -152 -153 -154 -155
v -156 -157 -158 -159 -160 -161 -162 -163 -164 -165 -166 167 -168 -169 -170 -171
v -172 -173 174 175 176 -177 -178 -179 -180 -181 -182 -183 -184 -185 -186 -187
v -188 189 -190 -191 -192 -193 -194 -195 -196 -197 -198 -199 -200 -201 -202 -203
v -204 205 -206 207 -208 -209 -210 -211 -212 -213 214 -215 -216 -217 -218 -219
v -220 -221 -222 -223 -224 -225 -226 -227 -228 -229 -230 -231 -232 -233 -234
v -235 -236 -237 -238 -239 -240 -241 -242 -243 -244 -245 -246 -247 248 -249 -250
v -251 -252 -253 -254 -255 -256 -257 -258 -259 -260 -261 -262 -263 -264 -265
v -266 -267 -268 -269 -270 -271 -272 -273 -274 -275 -276 -277 -278 -279 -280
v -281 -282 -283 -284 -285 -286 -287 -288 -289 -290 -291 292 -293 -294 295 296
v 297 -298 -299 -300 -301 -302 -303 -304 -305 -306 -307 -308 -309 -310 -311 -312
v -313 -314 -315 -316 -317 -318 -319 -320 -321 -322 -323 -324 -325 -326 -327
v -328 -329 -330 -331 -332 -333 -334 -335 -336 -337 -338 -339 -340 -341 -342
v -343 -344 345 -346 -347 -348 -349 -350 -351 352 353 354 355 356 357 358 359
v 360 361 362 363 -364 -365 366 367 368 369 -370 -371 -372 -373 374 375 -376 377
v 378 0
c
c    0.036  22% simplifying
c    0.127  78% search
c ==================================
c    0.162 100% all
c 
c          5702 conflicts,       35099.6 confs/sec
c            28 ternaries,         203.6 confs/ternary
c             0 binaries,            0.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c             2 reductions,         12.3 redus/sec,   2851.0 confs/reduction
c             3 restarts,           18.5 rests/sec,   1900.7 confs/restart
c         19758 decisions,      121623.6 decis/sec,      3.5 decis/conflict
c        215222 propagations,  1324834.4 props/sec,     10.9 props/decision
c 
c 0.2 seconds, 1.6 MB