c launch: /data/cnf/sc2014/app/atco_enc2_opt1_20_11.cnf.bz2
c host: atom11
c Lingeling SAT Solver
c 
c Version ayv 86bf266b9332599f1b876e28a02fe8427aeaa2db
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat Oct 11 12:11:52 CEST 2014
c compiled Sat Oct 11 12:11:52 CEST 2014
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -DNDBLSCR  -I../yalsat -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLPICOSAT
c -DNLGLDRUPLIG
c Linux cluster2 3.13.0-36-generic x86_64
c 
c piping '/data/cnf/sc2014/app/atco_enc2_opt1_20_11.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt1_20_11.cnf.bz2
c no embedded options
c found 'p cnf 461417 9776924' header
c read 461417 variables, 9776924 clauses, 35972702 literals in 0.00 seconds
c
c --abstime=0
c --actavgmax=112
c --actdblarithlim=3
c --actgeomlim=2
c --actgsdul=7
c --acts=2
c --actstdmax=112
c --actstdmin=10
c --actvlim=200000
c --agile=1
c --agilelim=30
c --agilesinint=100000
c --bate=1
c --batewait=2
c --bca=1
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bva=0
c --bias=2
c --binlocsdel=10
c --binsimpdel=2
c --bkwdscale=2
c --blkboost=10
c --blkboostvlim=1000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim=1000000
c --blkocclim1=100000
c --blkocclim2=10000
c --blkreleff=100
c --blkrtc=0
c --blksched2b2=0
c --blkschedmin=0
c --blkschedprod=0
c --blkschedpure=1
c --blkschedsum=1
c --blksmall=1
c --blksuccesslim=10000
c --blksuccessrat=1000
c --block=1
c --blockwait=1
c --boost=1
c --bumpbcplits=0
c --bumpclslits=0
c --bumpseenaftermin=0
c --bumpseenbeforemin=1
c --bumpseenlits=1
c --bumpseenminsize=3
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce=3
c --cceboost=10
c --cceboostvlim=1000000
c --cce2wait=1
c --cce3wait=2
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --cceonlyifstuck=0
c --ccereleff=20
c --ccertc=0
c --ccesuccesslim=10000
c --ccesuccessrat=1000
c --ccewait=2
c --cgrclsr=1
c --cgrclsrwait=2
c --cgreleff=1
c --cgrextand=1
c --cgrexteq=1
c --cgrextite=1
c --cgrextunits=1
c --cgrextxor=1
c --cgrmaxeff=8000000
c --cgrmaxority=20
c --cgrmineff=200000
c --cintinc=20000
c --cintincdiv=1
c --cintmaxhard=10000000
c --cintmaxsoft=1000000
c --cliff=1
c --cliffmaxeff=100000000
c --cliffmineff=10000000
c --cliffreleff=8
c --cliffwait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=30
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --drup=0
c --druplig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=40
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim=1000000
c --elmocclim1=1000
c --elmocclim2=100
c --elmreleff=200
c --elmroundlim=3
c --elmrtc=0
c --elmsched2b2=0
c --elmschediff=0
c --elmschedmin=0
c --elmschedprod=0
c --elmschedpure=1
c --elmschedsum=1
c --elmsuccesslim=1000
c --elmsuccessrat=1000
c --exitonabort=0
c --factmax=100000
c --factor=3
c --flipdur=10
c --flipint=10
c --flipldmod=4
c --fliplevels=6
c --flipping=1
c --fliptop=1
c --flipvlim=100000
c --force=0
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=3
c --gluescale=4
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --itlocsdel=100
c --itsimpdel=20
c --jwhred=1
c --keepmaxglue=1
c --lftmaxeff=20000000
c --lftmineff=500000
c --lftreleff=6
c --lftroundlim=5
c --lhbr=1
c --lift=1
c --liftlrg=3
c --liftwait=2
c --lkhd=2
c --lkhdmisifelmrtc=0
c --locs=0
c --locsboost=2
c --locscint=10000
c --locsdec=2
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsclim=1000000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxglue=2147483647
c --maxscorexp=500
c --mega=0
c --megaint=4
c --megawait=2
c --memlim=-1
c --minimize=2
c --minlocalgluelim=30
c --minrecgluelim=20
c --mocint=1000
c --move=2
c --otfs=1
c --otfsbump=0
c --otfsconf=0
c --penmax=4
c --phase=0
c --phaseflip=0
c --phasegluebit=0
c --phaseneginit=0
c --plain=0
c --plim=-1
c --prbasic=1
c --prbasicmaxeff=100000000
c --prbasicmineff=1000000
c --prbasicreleff=10
c --prbasicroundlim=9
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --psm=3
c --pure=1
c --randec=0
c --randecflipint=0
c --randecint=1000
c --rdp=0
c --rdpclslim=3
c --rdplim=100
c --rdpmaxeff=10000000
c --rdpmineff=10000
c --rdpmodelm=0
c --rdpreleff=2
c --rdpwait=2
c --redfixed=0
c --redinoutinc=100
c --redlbound=0
c --redlexpfac=10
c --redlinc=1000
c --redlinit=4000
c --redlmaxabs=1000000
c --redlmaxinc=200
c --redlmaxrel=300
c --redlminabs=500
c --redlmininc=10
c --redlminrel=10
c --redloutinc=10000
c --redoutclim=5000
c --redoutvlim=1000
c --reduce=2
c --rephase=1
c --rephaseinc=10000
c --restart=2
c --restartinit=0
c --restartint=5
c --restartintscale=0
c --reusetrail=1
c --rmincpen=4
c --rstinoutinc=110
c --saturating=70
c --scincinc=200
c --score=5
c --seed=0
c --simpdelay=0
c --simpen=0
c --simpidiv=3
c --simpinterdelay=2000
c --simpiscale=100
c --simplify=2
c --simprtc=5
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --tabr=3
c --tabrcfactor=2
c --tabrkeep=3
c --tabrvfactor=4
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=20
c --treelookfull=0
c --treelooklrg=1
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=1
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --verbose=1
c [freezer] frozen 0 variables out of 460708 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [init-scores] score increment factor 1.200000d+00 (--scincinc=200)
c [init-scores] maxium score limit 1.000000d+500 (--maxscorexp=500)
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c *    0.0  460708  9754664         0       0      0     0   1  0.0   0.0  628
c 
c [simplification-1] limit of 0 conflicts hit after 0 conflicts
c [card-1] limit 2438666 based on 9754664 irredundant clauses
c [card-1] found 54657 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2438666 for elimination
c [card-1] 54657 out of 54657 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 58740 variables
c [simpleprobe-1] all 402677 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 2398950 based on 9595800 irredundant clauses
c [decomp-2] removed 3 variables
c [simpleprobe-1] 402674 variables remain 100% (0 retained)
c [simpleprobe-1] removed 3 variables, found 18 hbrs, 0 units
c [unhide-1] limit 4797898 based on 9595797 irredundant clauses
c [unhide-1-1] 2 units, 3947 failed, 92989 tauts, 0 hbrs, 14211 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 396189 variables 100%
c [elim-1] boosting limit by 40
c [elim-1] limit of 50000000 steps penalty 4 = 0 + 4
c [elim-1] incomplete 392087 not tried 99% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 7976 = 2% variables out of 396189
c [phase-1] phase bias: 171307 positive 44%, 216906 negative 56%
c [simplification-1] removed 71081 variables 15.5% (388213 remain 84%)
c [simplification-1] removed 669945 irredundant clauses 6.9% (9084719 remain 93%)
c [simplification-1] maximum reduction of 15% = max (15%, 7%)
c [simplification-1] large reduction 15% >= 5% limit
c [simplification-1] new conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 2000 = 2 * 1000
c [simplification-1] new conflict limit 2000
c [cut-width] 1433931, max 2957499, min4 642926 at 75%, min10 282073 at 90%
c [cut-width] cut-width based bias 1
c [decision-order] bias 1, old 1
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   22.3  388213  9084719         5       1      3    12   7  2.4 1075.4  604
c R   22.3  388213  9084719        23      16      6    12   7  3.5 1060.8  604
c R   22.3  388213  9084719        64      53      7    12   9  7.3 1054.9  604
c R   22.4  388213  9084719       171     143     10    16   2  7.2 1011.4  604
c R   22.6  388213  9084719       422     376     16    19   2  7.9 934.4  604
c R   23.0  388213  9084719      1004     890     29    29   2  8.4 809.3  604
c 
c [simplification-2] limit of 2054 conflicts hit after 2056 conflicts
c [decomp-3] removed 25 variables
c [simpleprobe-2] all 388188 free variables schedulable
c [simpleprobe-2] limit 2271172 based on 9084688 irredundant clauses
c [simpleprobe-2] 388188 variables remain 100% (0 retained)
c [simpleprobe-2] removed 0 variables, found 39 hbrs, 0 units
c [treelook-1] limit 2271172 based on 9084688 irredundant clauses
c [treelook-1] scheduled 63924 literals 8%
c [treelook-1] scheduling used 2272189 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 2271172 based on 9084688 irredundant clauses
c [treelook-1] used 2538577 steps
c [treelook-1] 63895 literals remain 8%
c [treelook-1] 61764 variables remain to probed next time 16%
c [decomp-5] removed 2 variables
c [treelook-1] removed 2 variables, found 282 hbrs
c [basicprobe-1] limit 18169372 based on 9084686 irredundant clauses
c [basicprobe-1-0] 38134 probes remain 10% after last round
c [basicprobe-1-0] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 32 variables, found 25976 hbrs
c [unhide-2] limit 4542343 based on 9084686 irredundant clauses
c [unhide-2-2] 1 units, 0 failed, 4057 tauts, 0 hbrs, 9236 literals
c [elim-2] 388153 variables 100% will be scheduled this time
c [elim-2] scheduled 388153 variables 100%
c [elim-2] limit of 9084087 steps based on 9084087 irredundant clauses
c [elim-2] incomplete 386815 not tried 100% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 2632 = 1% variables out of 388153
c [phase-2] phase bias: 3838 positive 51%, 3636 negative 49%
c [simplification-2] removed 2692 variables 0.7% (385521 remain 84%)
c [simplification-2] removed 99830 irredundant clauses 1.1% (8984889 remain 92%)
c [simplification-2] maximum reduction of 1% = max (1%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 20000 = 2 * 10000
c [simplification-2] new conflict limit 22056
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   48.3  385521  8984889      2325    2134     41 14528   3  8.6 633.7  586
c -   50.4  385521  8984889      4952    2603     78 14544   2  8.8 453.8  587
c R   50.6  385521  8984889      5287    2911     79 14545   2  8.7 445.3  587
c -   53.2  385521  8984889      8438    3393    105 14561   4  9.1 330.3  587
c R   55.1  385521  8984889     11892    6697    123 14567   6  9.5 278.7  588
c -   55.6  385521  8984889     12337    4128    126 14569   2  9.6 269.4  587
c -   59.3  385521  8984889     16826    4904    140 14574   3  9.7 215.0  587
c -   63.1  385521  8984889     21933    5765    161 14582   3 10.0 176.1  587
c 
c [simplification-3] limit of 22164 conflicts hit after 22165 conflicts
c [card-2] limit 2246222 based on 8984889 irredundant clauses
c [card-2] found 53981 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 2246222 for elimination
c [card-2] 53981 out of 53981 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 840 variables
c [treelook-2] limit 2245873 based on 8983495 irredundant clauses
c [treelook-2] scheduled 67576 literals 9%
c [treelook-2] scheduling used 2270594 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 2245873 based on 8983495 irredundant clauses
c [treelook-2] used 3750603 steps
c [treelook-2] 67474 literals remain 9%
c [treelook-2] 22570 variables remain to probed next time 6%
c [decomp-7] removed 6 variables
c [treelook-2] removed 18 variables, found 543 hbrs
c [unhide-3] limit 4491705 based on 8983410 irredundant clauses
c [unhide-3-3] 0 units, 1 failed, 88462 tauts, 0 hbrs, 7741 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 384662 variables 100%
c [elim-3] limit of 28947563 steps penalty 3 = 0 + 3
c [elim-3] incomplete 380247 not tried 99% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 8565 = 2% variables out of 384662
c [rephase-1] after 22165 conflicts (new increment 20000, next 42165)
c [flushphases] 352114 phases reset
c [phase-3] phase bias: 12459 positive 80%, 3059 negative 20%
c [simplification-3] removed 9424 variables 2.4% (376097 remain 82%)
c [simplification-3] removed 373829 irredundant clauses 4.2% (8611060 remain 88%)
c [simplification-3] maximum reduction of 4% = max (2%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 14000
c [simplification-3] penalized conflict interval 28000 = 2 * 14000
c [simplification-3] new conflict limit 50165
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c R   83.9  376097  8611060     26348    9922    159 13351   4 10.4 162.3  564
c -   84.9  376097  8611060     27450    6485    165 13351   3 10.4 156.4  564
c -   89.6  376097  8611060     33629    7371    193 13355   4 10.4 133.1  564
c -   94.2  376097  8611060     40289    8242    210 13356   3 10.3 116.9  564
c -   99.6  376097  8611060     47479    9119    229 13366   3 10.4 102.1  564
c 
c [simplification-4] limit of 50195 conflicts hit after 50197 conflicts
c [decomp-8] removed 1177 variables
c [basicprobe-2] limit 17217420 based on 8608710 irredundant clauses
c [basicprobe-2-0] 44301 probes remain 12% after last round
c [basicprobe-2-0] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 10 variables, found 17429 hbrs
c [unhide-4] limit 4304355 based on 8608710 irredundant clauses
c [unhide-4-4] 0 units, 0 failed, 4581 tauts, 0 hbrs, 8819 literals
c [elim-4] 374910 variables 100% will be scheduled this time
c [elim-4] scheduled 374910 variables 100%
c [elim-4] limit of 64035456 steps penalty 3 = 0 + 3
c [elim-4] incomplete 368791 not tried 98% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 11788 = 3% variables out of 374910
c [rephase-2] after 50197 conflicts (new increment 40000, next 90197)
c [flushphases] 339804 phases reset
c [phase-4] phase bias: 14218 positive 83%, 2995 negative 17%
c [simplification-4] removed 12975 variables 3.4% (363122 remain 79%)
c [simplification-4] removed 555498 irredundant clauses 6.5% (8055562 remain 83%)
c [simplification-4] maximum reduction of 6% = max (3%, 6%)
c [simplification-4] large reduction 6% >= 5% limit
c [simplification-4] new conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 4000 = 2 * 2000
c [simplification-4] new conflict limit 54197
c 
c [simplification-5] limit of 54199 conflicts hit after 54199 conflicts
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 32222248 based on 8055562 irredundant clauses
c [ternres-1] all 363122 free variables schedulable
c [ternres-1] 1160 ternary resolvents (0 bin, 1160 trn)
c [ternres-1] 350908 variables remain 97% (12214 retained)
c [gauss-1] limit 4027781 based on 8055562 irredundant clauses
c [gauss-1] extracted 72 xors of average arity 2.0
c [gauss-1] connected 144 occurrences of 136 variables (average 1.1)
c [gauss-1] limit 4027781 based on 8055562 irredundant clauses
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 1930 variables
c [cgrclsr-1] limit 4025941 based on 8051882 irredundant clauses
c [cgrclsr-1] all 361192 free variables schedulable
c [cgrclsr-1] fully completed congruence closure
c [cgrclsr-1] removed 1 variables
c [lift-1] limit 2051507 with penalty 3 = 0 + 3
c [lift-1] using 344777 probes 95%
c [lift-1] 0 units, 2 impls, 0 eqs in 1 rounds
c [lift-1] 361138 variables remain 100% (53 retained)
c [cliff-1] limit of 16103762 steps based on 8051881 irredundant clauses
c [cliff-1] failed 0, lifted 0
c [transred-1] limit 8051881 based on 8051881 irredundant clauses
c [transred-1] removed 2456 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 361191 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 341917883 steps penalty 3 = 0 + 3
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 1570843 blocked clauses
c [cce-1] boosting limit by 10
c [cce-1] limit of 68383576 steps penalty 3 = 0 + 3
c [cce-1-1] eliminated 1 clauses out of 4570 (0%) of length 10
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 1 large clauses in 68383577 steps
c [cce-1-1] allowing another 34191788 steps for small clauses
c [cce-1] scheduling 663391 clauses = 593050 binary + 70341 ternary
c [cce-1] tried to eliminate 1772 small clauses 0%
c [cce-1] eliminated 284 small clauses 0%
c [cce-1] eliminated 278 binary clauses 0%
c [cce-1] eliminated 6 ternary clauses 0%
c [cce-1-1] eliminated 284 small clauses in 68383577 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 285 covered clauses in round 1
c [cce-1] eliminated 285 covered clauses in TOTAL during 1 rounds
c [cce-1] 285 < 1/1000 * 6479079 = 6479 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 329447 variables 100%
c [elim-5] limit of 68383576 steps penalty 3 = 0 + 3
c [elim-5] incomplete 128688 not tried 39% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 90890 = 28% variables out of 329447
c [bca-1] limit of 10000000 steps
c [bca-1] 474821 out of 477116 literals actually usable 100%
c [bca-1] added 22 blocked clauses in 1293447 steps
c [phase-5] phase bias: 11956 positive 37%, 20563 negative 63%
c [simplification-5] removed 124565 variables 34.3% (238557 remain 52%)
c [simplification-5] removed 1685188 irredundant clauses 20.9% (6370374 remain 65%)
c [simplification-5] maximum reduction of 34% = max (34%, 21%)
c [simplification-5] large reduction 34% >= 5% limit
c [simplification-5] new conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 4000 = 2 * 2000
c [simplification-5] new conflict limit 58199
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  148.4  238557  6370374     55376    9933   1137  6193   4 10.7  95.0  415
c R  149.4  238557  6370374     57817   12236   1140  6198   5 10.8  93.2  416
c 
c [simplification-6] limit of 58211 conflicts hit after 58211 conflicts
c [ternres-2] limit 25481496 based on 6370374 irredundant clauses
c [ternres-2] 230532 schedulable variables 97%
c [ternres-2] 795 ternary resolvents (0 bin, 795 trn)
c [ternres-2] 224107 variables remain 94% (14450 retained)
c [card-3] limit 1592593 based on 6370374 irredundant clauses
c [card-3] found 38657 at-most-one constraints of average size 3.3
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1592593 for elimination
c [card-3] 38657 out of 38657 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-10] removed 128 variables
c [simpleprobe-3] all 238429 free variables schedulable
c [simpleprobe-3] limit 7242866 penalty 4 = 1 + 3
c [decomp-11] removed 10 variables
c [simpleprobe-3] 234041 variables remain 98% (4378 retained)
c [simpleprobe-3] removed 10 variables, found 184 hbrs, 0 units
c [cgrclsr-2] limit 3185055 based on 6370111 irredundant clauses
c [cgrclsr-2] all 238419 free variables schedulable
c [cgrclsr-2] fully completed congruence closure
c [unhide-5] limit 3185055 based on 6370111 irredundant clauses
c [unhide-5-5] 0 units, 0 failed, 15048 tauts, 0 hbrs, 8269 literals
c [transred-2] limit 6342797 based on 6342797 irredundant clauses
c [transred-2] removed 1089 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 238419 variables 100%
c [block-2] limit of 36214333 steps penalty 3 = 0 + 3
c [block-2] incomplete 34961 not tried 15%
c [block-2] transition to [ all 1 rem 1 ] state
c [block-2] eliminated 46775 blocked clauses
c [elim-6] 128677 variables 54% will be scheduled this time
c [elim-6] scheduled 128677 variables 54%
c [elim-6] limit of 72428667 steps penalty 3 = 0 + 3
c [elim-6] incomplete 98832 not tried 41% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 566 = 0% variables out of 238419
c [bca-2] limit of 10000000 steps
c [bca-2] 473581 out of 475708 literals actually usable 100%
c [bca-2] added 27478 blocked clauses in 1936512 steps
c [phase-6] phase bias: 2352 positive 66%, 1218 negative 34%
c [simplification-6] removed 704 variables 0.3% (237853 remain 52%)
c [simplification-6] removed 78550 irredundant clauses 1.2% (6291824 remain 65%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 24000
c [simplification-6] penalized conflict interval 48000 = 2 * 24000
c [simplification-6] new conflict limit 106211
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  174.7  237853  6291824     63849   10847  36880 33797   4 10.8  85.6  414
c -  179.8  237853  6291824     72606   11738  36897 33799   3 10.8  77.7  414
c -  185.4  237853  6291824     82192   12758  36916 33802   5 10.8  71.3  414
c -  192.0  237853  6291824     92407   13756  36928 33806   4 10.8  65.5  414
c -  198.3  237853  6291824    102882   14649  36936 33815   5 10.9  60.8  414
c 
c [simplification-7] limit of 106255 conflicts hit after 106255 conflicts
c [ternres-3] limit 25167296 based on 6291824 irredundant clauses
c [ternres-3] 223444 schedulable variables 94%
c [ternres-3] 558 ternary resolvents (0 bin, 558 trn)
c [ternres-3] 216997 variables remain 91% (20856 retained)
c [gauss-2] limit 3145912 based on 6291824 irredundant clauses
c [gauss-2] extracted 250 xors of average arity 2.9
c [gauss-2] connected 730 occurrences of 724 variables (average 1.0)
c [gauss-2] limit 3145912 based on 6291824 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-12] removed 806 variables
c [treelook-3] limit 1572566 based on 6290266 irredundant clauses
c [treelook-3] scheduled 41403 literals 9%
c [treelook-3] scheduling used 1587776 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1572566 based on 6290266 irredundant clauses
c [treelook-3] used 1589780 steps
c [treelook-3] 41372 literals remain 9%
c [treelook-3] 7893 variables remain to probed next time 3%
c [treelook-3] removed 0 variables, found 856 hbrs
c [lift-2] limit 1572566 based on 6290266 irredundant clauses
c [lift-2] using 206978 probes 87%
c [lift-2] 0 units, 0 impls, 1 eqs in 1 rounds
c [lift-2] 236975 variables remain 100% (71 retained)
c [lift-2] removed 1 variables
c [cliff-2] limit of 12580530 steps based on 6290265 irredundant clauses
c [cliff-2] failed 0, lifted 0
c [transred-3] limit 6290265 based on 6290265 irredundant clauses
c [transred-3] removed 907 transitive binary clauses
c [block-3] 34961 variables 15% will be scheduled this time
c [block-3] scheduled 34961 variables 15%
c [block-3] limit of 65990516 steps penalty 3 = 0 + 3
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [cce-2] limit of 6599051 steps penalty 4 = 1 + 3
c [cce-2-1] incomplete large round (ABCE)
c [cce-2-1] allowing another 3299526 steps for small clauses
c [cce-2] scheduling 517857 clauses = 494687 binary + 23170 ternary
c [cce-2] tried to eliminate 84 small clauses 0%
c [cce-2] eliminated 14 small clauses 0%
c [cce-2] eliminated 13 binary clauses 0%
c [cce-2] eliminated 1 ternary clauses 0%
c [cce-2-1] eliminated 14 small clauses in 6599052 steps
c [cce-2-1] incomplete small round (ABCE)
c [cce-2-1] eliminated 14 covered clauses in round 1
c [cce-2] eliminated 14 covered clauses in TOTAL during 1 rounds
c [cce-2] 14 < 1/1000 * 6289572 = 6289 considered unsuccessful
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 237046 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 0 + 3
c [elim-7] incomplete 102347 not tried 43% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 112 = 0% variables out of 237046
c [elim-7] 112 < 1/1000 * 237046 = 237 considered unsuccessful
c [bca-3] limit of 10000000 steps
c [bca-3] 471507 out of 473870 literals actually usable 100%
c [bca-3] added 3073 blocked clauses in 1941394 steps
c [rephase-3] after 106255 conflicts (new increment 80000, next 186255)
c [flushphases] 221930 phases reset
c [phase-7] phase bias: 560 positive 79%, 150 negative 21%
c [simplification-7] removed 919 variables 0.4% (236934 remain 51%)
c [simplification-7] removed 3854 irredundant clauses 0.1% (6287970 remain 64%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 24000
c [simplification-7] new conflict interval 48000
c [simplification-7] penalized conflict interval 96000 = 2 * 48000
c [simplification-7] new conflict limit 202255
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  227.6  236934  6287970    113849   15492  37254 37596   5 11.0  57.8  415
c -  233.1  236934  6287970    125711   16356  37261 37597   6 11.0  55.3  415
c R  233.2  236934  6287970    126010   16614  37261 37597   4 11.0  55.2  415
c -  240.3  236934  6287970    137770   17306  37275 37602   6 11.0  51.9  415
c -  247.7  236934  6287970    150488   18300  37291 37604   7 11.0  48.9  415
c -  255.2  236934  6287970    163629   19225  37299 37609   5 11.0  46.4  415
c -  263.4  236934  6287970    177422   20196  37314 37612   5 11.1  44.1  415
c -  271.4  236934  6287970    191882   21175  37340 37617   4 11.2  42.4  415
c 
c [simplification-8] limit of 202309 conflicts hit after 202309 conflicts
c [ternres-4] limit 25151880 based on 6287970 irredundant clauses
c [ternres-4] 216162 schedulable variables 91%
c [ternres-4] 982 ternary resolvents (0 bin, 982 trn)
c [ternres-4] 209875 variables remain 89% (27059 retained)
c [decomp-14] removed 3 variables
c [basicprobe-3] limit 12575934 based on 6287967 irredundant clauses
c [basicprobe-3-0] 67697 probes remain 29% after last round
c [basicprobe-3-0] removed 0 variables, found 5922 hbrs
c [bate-1] eliminated 419 asymmetric tautologies during probing
c [cgrclsr-3] limit 3143774 based on 6287548 irredundant clauses
c [cgrclsr-3] all 236931 free variables schedulable
c [cgrclsr-3] fully completed congruence closure
c [cgrclsr-3] removed 10 variables
c [lift-3] limit 2500000 with penalty 3 = 0 + 3
c [lift-3] using 206729 probes 87%
c [lift-3] 0 units, 1 impls, 4 eqs in 1 rounds
c [lift-3] 236800 variables remain 100% (117 retained)
c [lift-3] removed 4 variables
c [transred-4] limit 6287537 based on 6287537 irredundant clauses
c [transred-4] removed 1053 transitive binary clauses
c [bca-4] limit of 10000000 steps
c [bca-4] 471264 out of 473836 literals actually usable 99%
c [bca-4] added 1 blocked clauses in 1953917 steps
c [rephase-4] after 202309 conflicts (new increment 160000, next 362309)
c [flushphases] 221914 phases reset
c [phase-8] phase bias: 689 positive 68%, 317 negative 32%
c [simplification-8] removed 17 variables 0.0% (236917 remain 51%)
c [simplification-8] removed 1023 irredundant clauses 0.0% (6286947 remain 64%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 48000
c [simplification-8] new conflict interval 96000
c [simplification-8] penalized conflict interval 192000 = 2 * 96000
c [simplification-8] new conflict limit 394309
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  292.1  236917  6286947    206761   22241  38422 43451   4 11.2  40.5  416
c -  301.1  236917  6286947    222164   23246  38428 43453   4 11.2  39.0  416
c -  310.6  236917  6286947    238323   24217  38434 43456   7 11.2  37.6  416
c -  317.3  236917  6286947    254910   25232  38436 43458   9 11.2  36.8  416
c -  324.7  236917  6286947    272405   26260  38445 43460   8 11.1  35.8  416
c R  324.8  236917  6286947    272501   26356  38445 43460   8 11.1  35.8  417
c -  335.6  236917  6286947    289817   27234  38452 43461   3 11.1  34.6  416
c -  346.8  236917  6286947    308031   28243  38464 43466   4 11.1  33.4  416
c -  358.3  236917  6286947    327029   29329  38472 43467   6 11.2  32.5  416
c -  370.3  236917  6286947    346437   30420  38481 43468   4 11.2  31.6  416
c -  383.1  236917  6286947    366517   31582  38495 43469   3 11.2  30.7  416
c -  395.0  236917  6286947    387000   32755  38502 43473   3 11.2  30.1  416
c 
c [simplification-9] limit of 394355 conflicts hit after 394355 conflicts
c [ternres-5] limit 25147788 based on 6286947 irredundant clauses
c [ternres-5] 209860 schedulable variables 89%
c [ternres-5] 798 ternary resolvents (0 bin, 798 trn)
c [ternres-5] 203559 variables remain 86% (33358 retained)
c [decomp-15] removed 203 variables
c [simpleprobe-4] 232366 schedulable variables 98%
c [simpleprobe-4] limit 25000000 penalty 3 = 0 + 3
c [decomp-16] removed 12 variables
c [simpleprobe-4] 197548 variables remain 83% (39154 retained)
c [simpleprobe-4] removed 12 variables, found 2164 hbrs, 0 units
c [cgrclsr-4] limit 3143378 based on 6286756 irredundant clauses
c [cgrclsr-4] all 236702 free variables schedulable
c [cgrclsr-4] fully completed congruence closure
c [lift-4] limit 2500000 with penalty 3 = 0 + 3
c [lift-4] using 206459 probes 87%
c [lift-4] 0 units, 0 impls, 1 eqs in 1 rounds
c [lift-4] 236545 variables remain 100% (156 retained)
c [lift-4] removed 1 variables
c [unhide-6] limit 3143377 based on 6286755 irredundant clauses
c [unhide-6-6] 0 units, 0 failed, 3489 tauts, 0 hbrs, 11729 literals
c [transred-5] limit 6286603 based on 6286603 irredundant clauses
c [transred-5] removed 883 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 236701 variables 100%
c [block-4] limit of 50000000 steps penalty 4 = 1 + 3
c [block-4] incomplete 10143 not tried 4%
c [block-4] transition to [ all 1 rem 1 ] state
c [block-4] eliminated 396 blocked clauses
c [block-4] 396 < 1/1000 * 6286072 = 6286 considered unsuccessful
c [elim-8] 98683 variables 42% will be scheduled this time
c [elim-8] scheduled 98683 variables 42%
c [elim-8] limit of 50000000 steps penalty 4 = 1 + 3
c [elim-8] incomplete 93751 not tried 40% in round 1
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 136 = 0% variables out of 236701
c [elim-8] 136 < 1/1000 * 236701 = 236 considered unsuccessful
c [bca-5] limit of 10000000 steps
c [bca-5] 470466 out of 473132 literals actually usable 99%
c [bca-5] added 109 blocked clauses in 1961637 steps
c [rephase-5] after 394355 conflicts (new increment 320000, next 714355)
c [flushphases] 221579 phases reset
c [phase-9] phase bias: 502 positive 61%, 323 negative 39%
c [simplification-9] removed 352 variables 0.1% (236565 remain 51%)
c [simplification-9] removed 1595 irredundant clauses 0.0% (6285352 remain 64%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 96000
c [simplification-9] new conflict interval 192000
c [simplification-9] penalized conflict interval 384000 = 2 * 192000
c [simplification-9] new conflict limit 778355
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  429.4  236565  6285352    408159   33881  39266 41293   4 11.2  29.5  418
c -  442.7  236565  6285352    429692   35028  39275 41295   5 11.2  28.9  418
c -  456.5  236565  6285352    451883   36128  39283 41297   9 11.2  28.3  418
c -  470.9  236565  6285352    474599   37304  39288 41299   4 11.2  27.7  418
c -  485.5  236565  6285352    497697   38417  39300 41302   4 11.3  27.2  418
c -  497.1  236565  6285352    521083   39473  39300 41303   5 11.3  27.0  418
c -  505.8  236565  6285352    544579   40426  39303 41303   5 11.4  26.8  418
c -  515.6  236565  6285352    569359   41389  39304 41305   9 11.3  26.6  418
c R  521.4  236565  6285352    586305   57250  39305 41305   8 11.3  26.4  421
c -  527.3  236565  6285352    594377   42342  39308 41305   5 11.3  26.3  418
c -  544.9  236565  6285352    620600   43652  39315 41305   3 11.3  25.8  418
c -  563.3  236565  6285352    647865   44940  39338 41310   4 11.3  25.4  418
c -  581.2  236565  6285352    674936   46153  39347 41311   5 11.3  25.1  418
c -  597.9  236565  6285352    702432   47229  39356 41313   5 11.4  24.8  418
c -  615.6  236565  6285352    730795   48461  39373 41318   4 11.4  24.5  418
c -  635.1  236565  6285352    759600   49641  39378 41321   4 11.4  24.2  418
c 
c [simplification-10] limit of 778413 conflicts hit after 778413 conflicts
c [ternres-6] limit 25141408 based on 6285352 irredundant clauses
c [ternres-6] 203251 schedulable variables 86%
c [ternres-6] 815 ternary resolvents (0 bin, 815 trn)
c [ternres-6] 197085 variables remain 83% (39480 retained)
c [card-4] limit 2832976 penalty 6 = 3 + 3
c [card-4] found 41222 at-most-one constraints of average size 3.2
c [card-4] found 100 at-most-two constraints of average size 8.3
c [card-4] using previous limit 2832976 for elimination
c [card-4] 41321 out of 41322 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 3142676 based on 6285352 irredundant clauses
c [gauss-3] extracted 310 xors of average arity 3.0
c [gauss-3] connected 928 occurrences of 925 variables (average 1.0)
c [gauss-3] limit 3142676 based on 6285352 irredundant clauses
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 20 variables
c [lift-5] limit 2500000 with penalty 3 = 0 + 3
c [lift-5] using 206257 probes 87%
c [lift-5] 0 units, 2 impls, 1 eqs in 1 rounds
c [lift-5] 236340 variables remain 100% (204 retained)
c [lift-5] removed 1 variables
c [cliff-3] limit of 12570628 steps based on 6285314 irredundant clauses
c [cliff-3] failed 0, lifted 0
c [transred-6] limit 6285314 based on 6285314 irredundant clauses
c [transred-6] removed 770 transitive binary clauses
c [cce-3] limit of 22663813 steps penalty 5 = 2 + 3
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 11331907 steps for small clauses
c [cce-3] scheduling 5763784 clauses = 491157 binary + 5272627 ternary
c [cce-3] tried to eliminate 268 small clauses 0%
c [cce-3] eliminated 53 small clauses 0%
c [cce-3] eliminated 4 binary clauses 0%
c [cce-3] eliminated 49 ternary clauses 0%
c [cce-3-1] eliminated 53 small clauses in 22663814 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 53 covered clauses in round 1
c [cce-3] eliminated 53 covered clauses in TOTAL during 1 rounds
c [cce-3] 53 < 1/1000 * 6284859 = 6284 considered unsuccessful
c [bca-6] limit of 10000000 steps
c [bca-6] 470083 out of 473090 literals actually usable 99%
c [bca-6] added 0 blocked clauses in 1988289 steps
c [rephase-6] after 778413 conflicts (new increment 640000, next 1418413)
c [flushphases] 221561 phases reset
c [phase-10] phase bias: 247 positive 80%, 60 negative 20%
c [simplification-10] removed 21 variables 0.0% (236544 remain 51%)
c [simplification-10] removed 546 irredundant clauses 0.0% (6284806 remain 64%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 192000
c [simplification-10] new conflict interval 384000
c [simplification-10] penalized conflict interval 768000 = 2 * 384000
c [simplification-10] new conflict limit 1546413
c 
c  seconds         irredundant          redundant clauses agility   height
c          variables clauses conflicts large ternary binary    glue         MB
c 
c -  666.5  236544  6284806    788782   50841  40247 41267   3 11.4  23.9  420
c -  686.3  236544  6284806    818557   52058  40253 41267   4 11.4  23.6  420
c -  699.8  236544  6284806    848709   53154  40259 41271   5 11.5  23.6  420
c -  720.8  236544  6284806    880093   54319  40270 41271   3 11.5  23.3  420
c -  741.0  236544  6284806    911414   55477  40279 41275   5 11.5  23.1  420
c -  761.1  236544  6284806    943261   56636  40286 41276   9 11.5  22.9  420
c -  782.6  236544  6284806    975947   57825  40292 41276   5 11.5  22.7  420
c -  804.1  236544  6284806   1009100   59013  40297 41276   7 11.5  22.5  420
c -  825.3  236544  6284806   1042589   60275  40302 41276   7 11.6  22.4  420
c -  850.0  236544  6284806   1077153   61554  40312 41276   8 11.6  22.2  420
c -  868.2  236544  6284806   1111116   62729  40315 41276   5 11.6  22.1  420
c -  882.4  236544  6284806   1145730   64144  40319 41276   4 11.6  22.1  420
c -  899.7  236544  6284806   1181726   65605  40327 41278   9 11.6  22.0  420
c -  914.9  236544  6284806   1217728   66992  40331 41278  10 11.5  21.9  420
c -  930.6  236544  6284806   1254333   68135  40335 41282   6 11.5  21.8  420
c R  930.8  236544  6284806   1254785   68556  40335 41282   6 11.5  21.8  422
c -  958.4  236544  6284806   1292231   69398  40343 41282   5 11.5  21.6  421
c -  984.5  236544  6284806   1330335   70595  40352 41282   4 11.6  21.5  421
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 419 basic ate = 100 trn 24% + 319 lrg 76% in 1 updates
c bcas: 6 count, 30683 added (24861 skipped), 11075196 steps
c bkwd: tried 0 clauses, 0 lits, 0.00 lits/clause
c bkwd: checked 0 occs, 0.00 occs/clause, 0.00 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 0 large (0% self)
c blkd: 4 bces, 1618014 removed, 58790866 resolutions, 263207511 steps
c blkd: 41457 blocking literals 4%, 31744 pure
c bvas: 0 bvas, 0 added, 0 removed
c card: 4 count, 0 units, 0 am1, 18230285 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 393424 subsumed
c card: 188517 at-most-one constraints found, average size 3.10
c card: 188517 at-most-one constraints used 100%, average size 3.10
c card: 100 at-most-two constraints found, average size 8.35
c card: 99 at-most-two constraints used 99%, average size 8.33
c cces: 3 cces, 352 eliminated, 302 ate 86%, 50 abce 14%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c cgrs: 4 count, 13498168 esteps, 161629 csteps
c cgrs: 11 eqs, 0 units
c cgrs: 0 matched (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 0 simplified (0 ands 0%, 0 xors 0%, 0 ites 0%)
c cgrs: 6169 extracted (5541 ands 90%, 456 xors 7%, 172 ites 3%)
c clff: 3 cliffs, 0 lifted, 0 failed
c clff: 8958 decisions, 41279860 steps
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 45749626 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 47 gcs, 0 rescored clauses, 705 rescored vars
c dcps: 17 decompositions, 61800 equivalent 13%
c deco: 3392 decision-only clauses 0%, 54% reduction
c decs: 2336301 decision, 0 random 0.000%, 0 flipped 0.000%
c decs: 0 flipped 0.000% (in 0 phases)
c elms: 8 elims, 154409 eliminated 33%
c elms: 8 rounds, 1.0 rounds/bve
c elms: 49121 small 32%, 73544 large 48%
c elms: 66806 tried small, 49121 succeeded 74%, 17685 failed 26%
c elms: 176200 subsumed, 7759 strengthened, 0 blocked
c elms: 10261389 copies, 9136222 resolutions, 1050092 ipos
c elms: 37645868 subchks, 5049807 strchks
c frcs: 0 computed, 0 - 0 average min-cut range
c gaus: 3 extractions, 632 extracted, 2.9 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 20645494 steps, 10322747 extr 50%, 2452 elim 0%
c glue: 11.6 orig avg, 11.5 real avg, 3.1 scaled avg
c glue: 0 maxscaledglue=15 (0%)
c hbrs: 54842 = 2405 simple + 52186 trn 4% + 251 lrg 95%, 9224 sub 0%
c hght: 21 average, 1.86 height/glue
c ints: 36073 luby (9322106 steps), 0 inout (0 steps)
c lift: 5 phases, 1335 probed (446 level1 33%, 889 level2 67%)
c lift: 0 units, 7 equivalences, 5 implications
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1341354 clauses, 25.1 length
c lrnd: 420399 uips 31%, 839911 flips 63%
c mega: 0 count, 0 failed, 0 rounds
c mins: 33680296 learned lits, 29% minimized
c mins: 1320709 mins 98%, 205 bin 0%, 17048 size 1%, 3392 deco 0%
c move: moved 1341354, 5081 bin 0%, 74358 trn 6%, 0 lrg 0%
c otfs: str 5427 dyn (5369 red, 58 irr) 1768 drv 33%, 3659 rst 67%
c otfs: sub 33 dyn (33 red, 0 irr)
c phas: 10 computed, 467355 set, 218128 pos (47%), 249227 neg (53%)
c prbs: 3 basic, 32931 probed, 6 failed, 0 lifted
c prbs: 4 simple, 275069 probed, 0 failed, 13 eqs
c prbs: 3 treelook, 144 probed, 1 failed, 0 lifted
c prps: 1438810723 props, 614 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c psns: 44627015 searches, 5420453 hits, 12% hit rate
c rdps: 0 count, 0 units, 0 bin, 0 trn, 0 steps
c rdps: 0 partial eliminations, 0 bounded 0%
c rdps: 0 resolutions, 0 size 0%, 0 model 0%
c reds: 65 count, 0 reset, 0 acts 0%
c reds: 0 geom 0%, 0 glue useless 0%
c reds: 0 memlim 0%, 65 arith 100%, 0 double 0%
c rmbd: 47332 removed, 1499 red 3%
c rphs: 6 recomputed phases
c rsts: 35624 restarts 99%, 449 skipped 1%
c rsts: 0 saturating 0%, 0 agile 0%, 449 reuse 100%
c rsts: 36.9 avg interval, 36.9 scaled, 1.0 factor
c rsts: 14804 kept 41.6% average 19.1%
c simp: 10 count (10 confs 100%, 0 irr 0%, 0 vars 0%)
c subl: 1341354 count (584643 tried 0.4), 88176 sub out of 1340423 (6.6%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c tabr: 0 count
c tops: 8664 fixed 2%, 0 its, 0.00 confs/it
c trvs: 98232609207 traversals, 100% srch, 0% simp, 0% lkhd
c trvs: 68.4 search traversals per propagation, 73060.8 per conflict
c trvs: 1.6 search traversals per search visit
c trds: 6 transitive reductions, 7158 removed, 0 failed
c trds: 620655 nodes, 654390 edges, 39544783 steps
c trim: 1172703 words, 4.5 MB
c trnr: 6 count, 0 bin, 5108 trn, 158312117 steps
c unhd: 6 count, 6 rounds, 166853631 steps
c unhd: 1386 non-trivial sccs of average size 2.1
c unhd: 3 units, 3 bin, 0 trn, 0 lrg
c unhd: 3948 failed, 3946 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 208626 tauts, 238 bin 0%, 77459 trn 37%, 4272 lrg 2%
c unhd: 208626 tauts, 126657 stamp 61%, 51026 red 24%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 60005 str, 3 bin 0%, 35124 trn 59%, 24878 lrg 41%, 21255 red 35%
c vars: 236544 remaining 51% and 224873 removed 49% out of 461417
c vars: 8664 fixed 2%, 154409 eliminated 33%, 61800 equivalent 13%
c vsts: 62086692643 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 43.2 search visits per propagation, 46148.9 per conflict
c wchs: 4500777000 pushed, 95759162 enlarged, 83 defrags
c 
c scaledglue  added       reduced       forcing      resolved     conflicts
c 
c all   1340423 100   1169649 100  30564846 100  11206201 100    525281 100
c 
c  0      37053   3         0   0  20814475  68   5962658  53    262755  50 
c  1      59503   4     24687   2   6786861  22<  2229009  20<   119805  23<
c  2     287241  21    279829  24   1294470   4    899391   8     40144   8 
c  3     443947  33<   412663  35<   934845   3   1038934   9     43899   8 
c  4     373368  28    328582  28    541426   2    786839   7     39950   8 
c  5     130225  10    117191  10    179647   1    270426   2     17421   3 
c  6       8938   1      6627   1     12918   0     18653   0      1286   0 
c  7        148   0        70   0       204   0       291   0        21   0 
c  8          0   0         0   0         0   0         0   0         0   0 
c  9          0   0         0   0         0   0         0   0         0   0 
c 10          0   0         0   0         0   0         0   0         0   0 
c 11          0   0         0   0         0   0         0   0         0   0 
c 12          0   0         0   0         0   0         0   0         0   0 
c 13          0   0         0   0         0   0         0   0         0   0 
c 14          0   0         0   0         0   0         0   0         0   0 
c 15          0   0         0   0         0   0         0   0         0   0 
c 
c avg             3.1           3.2           0.5           1.0           1.1
c std             1.2           1.0           0.9           1.4           1.5
c 
c   51.046   5% gc
c   44.182   4% decomp
c   34.782   4% elim
c   31.378   3% probe
c   30.647   3% analysis
c   26.676   3% defrag
c   20.203   2% unhide
c   14.531   1% block
c   10.837   1% transred
c   10.084   1% bca
c    9.566   1% lift
c    9.425   1% cgrclsr
c    9.187   1% bump
c    7.301   1% phase
c    7.198   1% cce
c    4.994   1% reduce
c    4.392   0% restart
c    4.309   0% gauss
c    3.822   0% mincls
c    2.370   0% card
c    1.860   0% decide
c    1.599   0% ternres
c    1.172   0% cliff
c    0.274   0% cutwidth
c    0.000   0% backward
c    0.000   0% bva
c    0.000   0% force
c    0.000   0% locs
c    0.000   0% mega
c    0.000   0% rdp
c    0.000   0% tabularasa
c ----------------------------------
c   16.830   2% probe simple     54%
c    1.851   0% probe basic       6%
c   12.696   1% probe tree-look  40%
c ==================================
c   22.143   2% preprocessing    11%
c  179.926  18% inprocessing     89%
c ==================================
c  202.070  20% simplifying
c  790.922  80% search
c ==================================
c  992.999 100% all
c 
c 2336301 decisions, 2352.8 decisions/sec
c 1343122 conflicts, 1352.6 conflicts/sec
c 1438810723 propagations, 1.4 megaprops/sec
c 993.0 seconds, 995.7 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
