c launch: /data/cnf/sc2014/app/8pipe_k.cnf.bz2
c host: atom19
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/8pipe_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/8pipe_k.cnf.bz2
c no embedded options
c found 'p cnf 35065 1332773' header
c read 35065 variables, 1332773 clauses, 3936683 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
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 --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
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=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
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 --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=6
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
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 --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
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 --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 35064 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 [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] AVG (--score=6)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   35064  1332772         0       0      0     0    0     0   41   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 6 at-most-one constraints of average size 3.2
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6 out of 6 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 10 variables
c [simpleprobe-1] all 35055 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [simpleprobe-1] 17648 variables remain 50% (17407 retained 50%)
c [simpleprobe-1] removed 0 variables, found 33586 hbrs, 0 units
c [unhide-1] limit 83276 based on 1332429 irredundant clauses
c [unhide-1-1] 0 units, 0 failed, 0 tauts, 0 hbrs, 0 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 35055 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 23138 not tried 66% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4032 = 12% variables out of 35055 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 1323956 negative 100.0% of 1324582 except 626 0.0%
c [phase-count-1] 154804 positive 11.7% of 1324582 except 1169778 88.3%
c [phase-count-1] less non-negative clauses 626 than limit 132400 (10.0%)
c [phase-count-1] non-pos/non-neg = 1169778/626 = 1868.65 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 31023 negative 100%
c [sort-queue-1] sorted 31023 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 31023 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 4032 variables 11.5% (31023 remain 88%)
c [simplification-1] removed 8190 irredundant clauses 0.6% (1324582 remain 99%)
c [simplification-1] maximum reduction of 12% = max (12%, 1%)
c [simplification-1] large reduction 12% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [treelook-1] limit 331145 based on 1324582 irredundant clauses
c [treelook-1] scheduled 27874 literals 45%
c [treelook-1] scheduling used 331641 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 331145 based on 1324582 irredundant clauses
c [treelook-1] used 487845 steps
c [treelook-1] 27870 literals remain 45%
c [treelook-1] 26854 variables remain to probed next time 87%
c [treelook-1] removed 0 variables, found 1 hbrs
c [basicprobe-1] limit 10596656 based on 1324582 irredundant clauses
c [basicprobe-1-0] 28323 probes remain 92% after last round
c [basicprobe-1-0] 145 units = 145 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 168 variables, found 355 hbrs
c [elim-2] 22982 variables 74% will be scheduled this time
c [elim-2] scheduled 22982 variables 74%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 16876 not tried 55% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 73 = 0% variables out of 22982 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 25454 enqueued variables after 1001 conflicts
c [score-dist-2] active 5328 (17%), one 0 (0%), zero 25454 (83%)
c [score-dist-2] max exp 511, different 9 (2%)
c [score-dist-2] median active exp 510, avg 509.9
c [simplification-2] removed 241 variables 0.8% (30782 remain 88%)
c [simplification-2] removed 12073 irredundant clauses 0.9% (1312509 remain 98%)
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 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21001 (soft 11001 + delta 10000)
c [simplification-2] new conflict limit 11001 (hard 21001)
c 
c [simplification-3] limit 11001 conflicts (hard 21001) hit after 11001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3 out of 3 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [simpleprobe-2] 16996 schedulable variables 55%
c [simpleprobe-2] limit 2625018 based on 1312509 irredundant clauses
c [simpleprobe-2] 16996 variables remain 55% (13786 retained 45%)
c [unhide-2] limit 82031 based on 1312509 irredundant clauses
c [unhide-2-2] 0 units, 0 failed, 300 tauts, 0 hbrs, 9466 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 30782 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 20177 not tried 66% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 282 = 1% variables out of 30782 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 16539 enqueued variables after 11001 conflicts
c [score-dist-3] active 13961 (46%), one 0 (0%), zero 16539 (54%)
c [score-dist-3] max exp 515, different 12 (2%)
c [score-dist-3] median active exp 514, avg 513.5
c [simplification-3] removed 282 variables 0.9% (30500 remain 87%)
c [simplification-3] removed 2919 irredundant clauses 0.2% (1309590 remain 98%)
c [simplification-3] maximum reduction of 1% = max (1%, 0%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 20000
c [simplification-3] penalized conflict interval 20000 = 1 * 20000
c [simplification-3] hard conflict limit 41001 (soft 31001 + delta 10000)
c [simplification-3] new conflict limit 31001 (hard 41001)
c 
c [simplification-4] limit 31001 conflicts (hard 41001) hit after 31004 conflicts
c [elim-4] 16872 variables 55% will be scheduled this time
c [elim-4] scheduled 16872 variables 55%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1075158520 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 248 variables 1% in round 1 in 245695264 steps
c [elim-4-1] backward subsumption/strengthening limit 245695200
c [elim-4-1-1] backward checking 13652 touched variables 45%
c [elim-4-1-1] incomplete backward checking 13649 remain 100%
c [elim-4-1] subsumed 0 and strengthened 219 clauses in 245697197 steps
c [elim-4-1] rescheduled 763 variables 3% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 4250398 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 248 = 1% variables out of 16872 scheduled
c [elim-4] 248 < 1/100 * 16872 = 168 considered unsuccessful
c [sort-queue-4] sorted 12307 enqueued variables after 31004 conflicts
c [score-dist-4] active 17945 (59%), one 0 (0%), zero 12307 (41%)
c [score-dist-4] max exp 516, different 12 (2%)
c [score-dist-4] median active exp 516, avg 515.3
c [simplification-4] removed 248 variables 0.8% (30252 remain 86%)
c [simplification-4] removed 4005 irredundant clauses 0.3% (1305582 remain 98%)
c [simplification-4] maximum reduction of 1% = max (1%, 0%)
c [simplification-4] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 76004 (soft 61004 + delta 15000)
c [simplification-4] new conflict limit 61004 (hard 76004)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   42.4   30251  1305581     50852   42345    908 31578   39   135   60  29%    545   50    7   22   33%
c -   45.8   30251  1305581     65785   19103    982 31585   16    57   50  27%      0  -32    8   22   38%
c i   45.8   30250  1305581     66223   19305    992 31590   15    54   51  27%      7  -34    8   22   34%
c 
c [simplification-5] limit 61004 conflicts (hard 76004) hit after 76004 conflicts
c [quatres-1] found 5051 quaternary clauses 10% in total
c [quatres-1-2] added 166 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 33548640 with penalty 0 = 0 + 0
c [ternres-1] all 30250 free variables schedulable
c [ternres-1] 8056 ternary resolvents (4 bin, 8052 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 0 xors of average arity 0.0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-2] limit 335486 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 27403 literals 45%
c [treelook-2] scheduling used 336784 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 335486 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 426288 steps
c [treelook-2] 27397 literals remain 45%
c [treelook-2] 24801 variables remain to probed next time 82%
c [treelook-2] removed 0 variables, found 8 hbrs
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 30250 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 670972800 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 53056 blocked clauses
c [cce-1] limit of 33548640 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 177
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 176
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 175
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 174
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 173
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 172
c [cce-1-1] eliminated 7 clauses out of 7 (100%) of length 171
c [cce-1-1] eliminated 9 clauses out of 9 (100%) of length 170
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 169
c [cce-1-1] eliminated 7 clauses out of 7 (100%) of length 168
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 167
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 166
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 165
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 164
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 163
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 161
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 160
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 159
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 158
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 157
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 156
c [cce-1-1] eliminated 8 clauses out of 8 (100%) of length 155
c [cce-1-1] eliminated 7 clauses out of 9 (78%) of length 154
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 153
c [cce-1-1] eliminated 5 clauses out of 7 (71%) of length 152
c [cce-1-1] eliminated 4 clauses out of 4 (100%) of length 151
c [cce-1-1] eliminated 2 clauses out of 4 (50%) of length 150
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 149
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 147
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 146
c [cce-1-1] eliminated 3 clauses out of 6 (50%) of length 145
c [cce-1-1] eliminated 5 clauses out of 5 (100%) of length 144
c [cce-1-1] eliminated 6 clauses out of 8 (75%) of length 143
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 142
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 148 large clauses in 33554557 steps
c [cce-1-1] allowing another 16777278 steps for small clauses
c [cce-1-1] scheduling 1178147 clauses = 1176587 binary + 1560 ternary
c [cce-1-1] tried to eliminate 321 small clauses 0%
c [cce-1-1] eliminated 9 binary clauses 0%
c [cce-1-1] eliminated 9 small clauses 0%
c [cce-1-1] eliminated 9 small clauses in 33549313 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 157 covered clauses in round 1
c [cce-1] eliminated 157 covered clauses in TOTAL during 1 rounds
c [cce-1] 157 < 1/100 * 1238718 = 12387 considered unsuccessful
c [bca-1] limit of 10000000 steps and 2477622 added (scaled 2)
c [bca-1] 36301 out of 60278 literals actually usable 60%
c [bca-1] added 12397 blocked clauses in 134102 steps
c [sweep-1] limit 2477122 based on 1238561 irredundant clauses
c [sweep-1-1] 574 pos 1.9% + 29564 neg 98.1% = 30138 sched 100.0% ret 0
c [sweep-1-1] 2505842 steps 52 queries 1708.77 avg class size
c [sweep-1-1] 1573 decisions 46 SAT calls 207.33 avg env size
c [sweep-1-1] 26963 variables remain 89% (3175 retained 11%)
c [decomp-10] removed 5 variables
c [sweep-1-1] removed 5 vars (0 failed, 5 eqs, 14 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 5 vars in TOTAL (1 rounds, 51 queries)
c [sort-queue-5] sorted 7295 enqueued variables after 76004 conflicts
c [score-dist-5] active 22838 (76%), one 0 (0%), zero 7295 (24%)
c [score-dist-5] max exp 518, different 11 (2%)
c [score-dist-5] median active exp 518, avg 517.5
c [simplification-5] removed 117 variables 0.4% (30133 remain 86%)
c [simplification-5] removed 67019 irredundant clauses 5.1% (1238561 remain 93%)
c [simplification-5] maximum reduction of 5% = max (0%, 5%)
c [simplification-5] large reduction 5% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 88004 (soft 78004 + delta 10000)
c [simplification-5] new conflict limit 78004 (hard 88004)
c 
c [simplification-6] limit 78004 conflicts (hard 88004) hit after 79872 conflicts
c [quatres-2] found 5026 quaternary clauses 9% in total
c [quatres-2-2] added 175 quaternary resolvents
c [ternres-2] limit 6989739 with penalty 0 = 0 + 0
c [ternres-2] all 30133 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 9192 variables remain 31% (20941 retained 69%)
c [card-3] limit 873717 penalty 2 = 2 + 0
c [card-3] found 2 at-most-one constraints of average size 3.5
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 873717 for elimination
c [card-3] 2 out of 2 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 34948695 penalty 0 = 0 + 0
c [basicprobe-2-0] 23977 probes remain 82% after last round
c [basicprobe-2-0] 578 units = 578 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 859 variables, found 1674 hbrs
c [bate-1] eliminated 91 asymmetric tautologies during probing
c [unhide-3] limit 87371 with penalty 4 = 2 + 2
c [unhide-3-3] 0 units, 1 failed, 6060 tauts, 0 hbrs, 4464 literals
c [block-2] scheduling all variables this time
c [block-2] scheduled 29273 variables 100%
c [block-2] limit of 69897391 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 126505 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 26589 variables 100%
c [elim-5] limit of 69897391 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 6617 not tried 25% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1267 = 5% variables out of 26589 scheduled
c [bca-2] limit of 10000000 steps and 2094042 added (scaled 2)
c [bca-2] 27624 out of 50646 literals actually usable 55%
c [bca-2] added 5692 blocked clauses in 115289 steps
c [sweep-2] limit 2096921 penalty 0 = 0 + 0
c [sweep-2-1] 405 pos 1.8% + 22417 neg 98.2% = 22822 sched 90.1% ret 2500
c [sweep-2-1] 2103792 steps 75 queries 1461.80 avg class size
c [sweep-2-1] 2126 decisions 61 SAT calls 199.13 avg env size
c [sweep-2-1] 19645 variables remain 78% (5677 retained 22%)
c [decomp-12] removed 13 variables
c [sweep-2-1] removed 13 vars (0 failed, 13 eqs, 30 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 13 vars in TOTAL (1 rounds, 74 queries)
c [sort-queue-6] sorted 3633 enqueued variables after 79872 conflicts
c [score-dist-6] active 21676 (86%), one 0 (0%), zero 3633 (14%)
c [score-dist-6] max exp 518, different 10 (2%)
c [score-dist-6] median active exp 518, avg 517.6
c [simplification-6] removed 4824 variables 16.0% (25309 remain 72%)
c [simplification-6] removed 194888 irredundant clauses 15.7% (1043672 remain 78%)
c [simplification-6] maximum reduction of 16% = max (16%, 16%)
c [simplification-6] large reduction 16% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 91872 (soft 81872 + delta 10000)
c [simplification-6] new conflict limit 81872 (hard 91872)
c 
c [simplification-7] limit 81872 conflicts (hard 91872) hit after 81872 conflicts
c [quatres-3] found 4718 quaternary clauses 9% in total
c [quatres-3-2] added 187 single-self-subsuming ternary resolvents
c [quatres-3-2] added 147 quaternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 0 xors of average arity 0.0
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-2] limit 1043657 based on 1043657 irredundant clauses
c [transred-2] removed 13 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 25309 variables 100%
c [block-3] limit of 71313157 steps penalty 0 = 0 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 2749 blocked clauses
c [block-3] 2749 < 1/100 * 1043652 = 10436 considered unsuccessful
c [cce-2] limit of 17828289 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 1 clauses out of 1 (100%) of length 149
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 141
c [cce-2-1] eliminated 2 clauses out of 3 (67%) of length 140
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 139
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 5 large clauses in 17835923 steps
c [cce-2-1] allowing another 8917961 steps for small clauses
c [cce-2-1] scheduling 985998 clauses = 984123 binary + 1875 ternary
c [cce-2-1] tried to eliminate 276 small clauses 0%
c [cce-2-1] eliminated 247 binary clauses 0%
c [cce-2-1] eliminated 247 small clauses 0%
c [cce-2-1] eliminated 247 small clauses in 17833534 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 252 covered clauses in round 1
c [cce-2] eliminated 252 covered clauses in TOTAL during 1 rounds
c [cce-2] 252 < 1/100 * 1040903 = 10409 considered unsuccessful
c [elim-6] 6611 variables 26% will be scheduled this time
c [elim-6] scheduled 6611 variables 26%
c [elim-6] limit of 142626314 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 475 variables 2% in round 1 in 132338940 steps
c [elim-6-1] backward subsumption/strengthening limit 10287374
c [elim-6-1-1] backward checking 8323 touched variables 33%
c [elim-6-1-1] incomplete backward checking 8350 remain 100%
c [elim-6-1] subsumed 0 and strengthened 99 clauses in 10287497 steps
c [elim-6] incomplete 59 not tried 0% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 475 = 7% variables out of 6611 scheduled
c [bca-3] limit of 10000000 steps and 2086618 added (scaled 2)
c [bca-3] 27009 out of 49668 literals actually usable 54%
c [bca-3] added 1010 blocked clauses in 127090 steps
c [sweep-3] limit 2139394 penalty 0 = 0 + 0
c [sweep-3-1] 400 pos 2.1% + 18792 neg 97.9% = 19192 sched 77.3% ret 5641
c [sweep-3-1] 2143126 steps 42 queries 1331.79 avg class size
c [sweep-3-1] 1403 decisions 38 SAT calls 171.32 avg env size
c [sweep-3-1] 18138 variables remain 73% (6695 retained 27%)
c [decomp-14] removed 4 variables
c [sweep-3-1] removed 4 vars (0 failed, 3 eqs, 10 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 4 vars in TOTAL (1 rounds, 41 queries)
c [sort-queue-7] sorted 3562 enqueued variables after 81872 conflicts
c [score-dist-7] active 21267 (86%), one 0 (0%), zero 3562 (14%)
c [score-dist-7] max exp 518, different 10 (2%)
c [score-dist-7] median active exp 518, avg 517.6
c [simplification-7] removed 480 variables 1.9% (24829 remain 71%)
c [simplification-7] removed 5120 irredundant clauses 0.5% (1038537 remain 78%)
c [simplification-7] maximum reduction of 2% = max (2%, 0%)
c [simplification-7] geometric conflict interval increment 10000 = 30000 / 3
c [simplification-7] new conflict interval 40000
c [simplification-7] penalized conflict interval 40000 = 1 * 40000
c [simplification-7] hard conflict limit 141872 (soft 121872 + delta 20000)
c [simplification-7] new conflict limit 121872 (hard 141872)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   79.6   24829  1038519    116607   24558   8474 40533   23    98   49  24%    439  -11   18   27   66%
c i   82.9   24828  1038515    136809   40872   8548 40554   10    27   54  37%    594  -66    6   23   25%
c 
c [simplification-8] limit 121872 conflicts (hard 141872) hit after 141872 conflicts
c [quatres-4] found 4886 quaternary clauses 6% in total
c [quatres-4-2] added 4 single-self-subsuming ternary resolvents
c [quatres-4-2] added 198 quaternary resolvents
c [ternres-3] limit 4946280 with penalty 1 = 1 + 0
c [ternres-3] 7579 schedulable variables 31%
c [ternres-3] 92 ternary resolvents (0 bin, 92 trn)
c [ternres-3] fully completed ternary resolution
c [decomp-15] removed 1 variables
c [unhide-4] limit 247314 with penalty 3 = 1 + 2
c [unhide-4-4] 0 units, 1 failed, 968 tauts, 0 hbrs, 18963 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 4 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 24827 variables 100%
c [elim-7] limit of 197851232 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 4657 not tried 19% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 39 = 0% variables out of 24827 scheduled
c [elim-7] 39 < 1/100 * 24827 = 248 considered unsuccessful
c [bca-4] limit of 10000000 steps and 2058185 added (scaled 2)
c [bca-4] 26157 out of 49578 literals actually usable 53%
c [bca-4] added 1848 blocked clauses in 126099 steps
c [sweep-4] limit 2967768 penalty 0 = 0 + 0
c [sweep-4-1] 326 pos 1.8% + 17787 neg 98.2% = 18113 sched 73.1% ret 6675
c [sweep-4-1] 3086299 steps 66 queries 802.23 avg class size
c [sweep-4-1] 1893 decisions 53 SAT calls 133.87 avg env size
c [sweep-4-1] 15842 variables remain 64% (8945 retained 36%)
c [decomp-16] removed 13 variables
c [sweep-4-1] removed 13 vars (0 failed, 12 eqs, 28 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 13 vars in TOTAL (1 rounds, 65 queries)
c [sort-queue-8] sorted 2355 enqueued variables after 141872 conflicts
c [score-dist-8] active 22420 (90%), one 0 (0%), zero 2355 (10%)
c [score-dist-8] max exp 519, different 10 (2%)
c [score-dist-8] median active exp 518, avg 518.0
c [simplification-8] removed 53 variables 0.2% (24775 remain 71%)
c [simplification-8] removed 14495 irredundant clauses 1.4% (1024020 remain 77%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 20000 = 40000 / 2
c [simplification-8] new conflict interval 60000
c [simplification-8] penalized conflict interval 60000 = 1 * 60000
c [simplification-8] hard conflict limit 231872 (soft 201872 + delta 30000)
c [simplification-8] new conflict limit 201872 (hard 231872)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   96.0   24774  1023983    162060   40964   7099 40796   19    83   53  23%    -30  -14    6   23   27%
c -  101.3   24773  1023940    183550   27757   7192 40806   25   114   48  22%    -24   13   20   24   83%
c i  102.3   24772  1023940    189005   32060   7239 40814   15    57   52  27%     59  -43    8   23   33%
c i  102.6   24771  1023939    190318   33034   7265 40820   18    90   52  20%   -222   -9   25   23  107%
c 
c [simplification-9] limit 201872 conflicts (hard 231872) hit after 210133 conflicts
c [quatres-5] found 4934 quaternary clauses 6% in total
c [quatres-5-1] removed 2 duplicate quaternary clauses
c [quatres-5-2] added 8 single-self-subsuming ternary resolvents
c [quatres-5-2] added 144 quaternary resolvents
c [ternres-4] limit 13597312 with penalty 0 = 0 + 0
c [ternres-4] all 24767 free variables schedulable
c [ternres-4] 149 ternary resolvents (1 bin, 148 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-17] removed 8 variables
c [simpleprobe-3] 13695 schedulable variables 55%
c [simpleprobe-3] limit 13597312 penalty 2 = 2 + 0
c [simpleprobe-3] 13782 variables remain 56% (10985 retained 44%)
c [simpleprobe-3] removed 0 variables, found 114 hbrs, 0 units
c [unhide-5] limit 679865 with penalty 2 = 0 + 2
c [unhide-5-5] 0 units, 0 failed, 5414 tauts, 0 hbrs, 10659 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 16 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 24767 variables 100%
c [block-4] limit of 67986560 steps penalty 1 = 1 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 122 blocked clauses
c [block-4] 122 < 1/100 * 1002259 = 10022 considered unsuccessful
c [bca-5] limit of 10000000 steps and 2015247 added (scaled 2)
c [bca-5] 23169 out of 49536 literals actually usable 47%
c [bca-5] added 656 blocked clauses in 126479 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 40791930 penalty 0 = 0 + 0
c [sweep-5-1] 270 pos 1.7% + 15568 neg 98.3% = 15838 sched 63.9% ret 8929
c [sweep-5-1] 40933503 steps 1001 queries 293.45 avg class size
c [sweep-5-1] 22766 decisions 451 SAT calls 183.02 avg env size
c [sweep-5-1] 5813 variables remain 23% (18925 retained 77%)
c [decomp-19] removed 589 variables
c [sweep-5-1] removed 589 vars (0 failed, 551 eqs, 1135 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 589 vars in TOTAL (1 rounds, 1000 queries)
c [sort-queue-9] sorted 1291 enqueued variables after 210133 conflicts
c [score-dist-9] active 22887 (95%), one 0 (0%), zero 1291 (5%)
c [score-dist-9] max exp 519, different 9 (2%)
c [score-dist-9] median active exp 519, avg 518.6
c [simplification-9] removed 589 variables 2.4% (24178 remain 69%)
c [simplification-9] removed 37193 irredundant clauses 3.6% (986740 remain 74%)
c [simplification-9] maximum reduction of 4% = max (2%, 4%)
c [simplification-9] geometric conflict interval increment 12000 = 60000 / 5
c [simplification-9] new conflict interval 72000
c [simplification-9] penalized conflict interval 72000 = 1 * 72000
c [simplification-9] hard conflict limit 318133 (soft 282133 + delta 36000)
c [simplification-9] new conflict limit 282133 (hard 318133)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  113.8   24177   986739    213540   40071   6231 41288   23   109   54  21%     52    5   24   23  103%
c i  113.9   24176   986739    213788   40275   6232 41289   23   110   54  21%    -22    7   28   23  120%
c -  116.9   24176   986738    234421   27263   6351 41305   14    27   47  52%     46  -66   13   21   61%
c i  117.5   24175   986738    238633   30796   6359 41305   11    23   50  50%    107  -66    7   21   34%
c i  121.7   24174   986738    266727   54455   6706 41319   12    42   54  28%    170  -31    6   19   35%
c -  123.0   24174   986738    273400   30249   6731 41323   14    46   47  31%   -150  -24   21   18  117%
c i  125.7   24173   986738    287814   41860   6997 41334   12    31   50  38%     82  -35    7   17   40%
c i  127.1   24172   986738    296939   49454   7125 41342   10    24   51  44%    -87  -39    7   17   45%
c i  129.1   24171   986738    308667   59324   7364 41348   11    30   54  36%    -26  -30    7   16   44%
c i  129.3   24169   986738    310006   60392   7401 41354   10    27   54  37%   -137  -31    6   16   39%
c i  129.3   24164   986738    310046   60411   7405 41356   10    27   54  37%   -139  -32    6   16   38%
c i  129.6   17661   986736    311196   61303   7411 41444   12    70   54  18%   -164   11   22   16  135%
c i  129.7   17658   986736    311644   61655   7413 41480   14    86   54  16%   -171   28   23   16  145%
c i  129.8   17657   986736    311737   61724   7413 41488   14    87   54  16%   -172   28   23   16  144%
c i  129.9   17656   986736    312053   61980   7415 41496   15    91   54  16%   -174   32   27   16  171%
c i  129.9   17655   986736    312107   62029   7415 41497   15    91   54  16%   -175   32   26   16  164%
c -  130.0   17655   986736    312292   30935   7415 41505   15    93   47  16%   -176   34   26   16  161%
c i  130.3   17654   986736    313652   31990   7421 41565   17   100   49  17%   -168   41   21   16  132%
c i  130.4   17653   986736    313895   32183   7421 41569   18   100   49  18%   -170   40   22   16  135%
c i  130.7   17652   986736    316503   34021   7430 41621   17    88   49  19%   -148   27   15   16   90%
c i  130.7   17651   986736    316531   34033   7431 41621   16    88   49  19%   -149   27   14   16   87%
c i  130.7   17650   986736    316677   34116   7435 41632   16    87   49  19%   -152   26   11   16   68%
c i  130.8   17649   986736    316946   34311   7442 41637   16    85   49  19%   -156   24   11   16   68%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i  130.8   17648   986736    316968   34317   7442 41637   16    85   49  19%   -156   24   11   16   67%
c i  130.8   17647   986736    317050   34356   7447 41639   16    84   49  19%   -157   22    9   16   57%
c i  130.8   17214   986736    317051   34356   7447 41639   16    84   49  19%   -157   22    9   16   57%
c i  130.8   17204   986736    317100   34394   7447 41639   16    83   49  19%   -158   22    9   16   54%
c i  130.8   17203   986736    317156   34418   7451 41644   15    82   49  19%   -159   21    8   16   49%
c i  130.8   16686   986736    317157   34418   7451 41644   15    82   49  19%   -159   21    8   16   49%
c i  130.8   16684   986736    317174   34421   7452 41646   15    82   49  19%   -159   20    8   16   47%
c i  130.8   16533   986736    317175   34421   7452 41646   15    82   49  19%   -159   20    8   16   47%
c i  130.8   16373   986736    317181   34421   7453 41647   15    81   49  19%   -159   20    7   16   46%
c i  130.8   16325   986736    317184   34419   7454 41647   15    81   49  19%   -159   20    7   16   46%
c 0  130.8   16259   986736    317184   34419   7454 41647   15    81   49  19%   -159   20    7   16   46%
c 
s UNSATISFIABLE
c
c bate: 91 basic ate = 0 trn 0% + 91 lrg 100% in 1 updates
c bcas: 5 count, 21603 added (2037 skipped), 629059 steps
c bkwd: tried 72272 clauses, 144426 lits, 2.00 lits/clause
c bkwd: checked 216428730 occs, 2994.64 occs/clause, 1498.54 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 318 large (0% self)
c blkd: 4 bces, 182432 removed, 30086646 resolutions, 95339319 steps
c blkd: 7607 blocking literals 11%, 2797 pure
c bump: 306582 bumped seen, 34042128 lits 111.0 on average
c card: 3 count, 0 units, 0 am1, 14644402 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 3 subsumed
c card: 11 at-most-one constraints found, average size 3.18
c card: 11 at-most-one constraints used 100%, average size 3.18
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 2 cces, 409 eliminated, 409 ate 100%, 0 abce 0%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 5269456 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 44 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 19 decompositions, 594 equivalent 2%
c deco: 1700 decision-only clauses 1%, 55% reduction
c decs: 3907218 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 9213 eliminated 26%, 26 pure 0%
c elms: 9 rounds, 1.3 rounds/bve
c elms: 2284 small 25%, 4106 large 45%
c elms: 2299 tried small, 2284 succeeded 99%, 15 failed 1%
c elms: 4956 subsumed, 245689 strengthened, 2992 blocked
c elms: 4489416 copies, 10748827 resolutions, 42667 ipos
c elms: 23896874 subchks, 8473940 strchks
c gaus: 2 extractions, 0 extracted, 0.0 size, 0 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 6273170 steps, 3136585 extr 50%, 0 elim 0%
c glue: 24.4 orig avg, 24.4 real avg, 4.3 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 36542 = 33700 simple 92% + 2837 trn 8% + 5 lrg 0%, 652 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 306582 clauses, 41.9 length
c lrnd: 12859296 lits = 25811763 orig - 12952467 removed 50%
c lrnd: 106118 uips 35%, 145561 flips 47%
c mins: 301482 mins 98%, 312 bin 0%, 3076 size 1%
c mins: 12627766 poisoned searches, 1581802 hits, 13% hit rate
c mins: 35899016 used twice searches, 4822675 hits, 13% hit rate
c move: moved 164845, 162982 bin 99%, 1863 trn 1%
c otfs: 10868 driving 15%, 61137 restarting 85%
c otfs: str 72005, 67869 red 94%, 4136 irr 6%
c otfs: str 72005, 0 bin 0%, 99 trn 0%, 71906 lrg 100%
c otfs: sub 418, 283 red 68%, 135 irr 32%
c otfs: sub 418, 0 bin 0%, 3 trn 1%, 415 lrg 99%
c phas: 1 computed, 31023 set, 0 pos (0%), 31023 neg (100%)
c prbs: 2 basic, 7618 probed, 723 failed, 0 lifted
c prbs: 3 simple, 66246 probed, 0 failed, 0 eqs
c prbs: 2 treelook, 10 probed, 0 failed, 0 lifted
c prom: 40450 locked 3% out of 1360197 tried
c prps: 379991594 props, 94 props/dec
c prps: 96% srch, 4% simp, 0% lkhd
c quat: 5 count, 830 quat, 199 self1, 0 self2, 4 dup
c queu: 9 sorted, 3907218 next (11133 steps 0.00)
c queu: 34180652 enq (312125171 steps 9.13), 34042128 deq 100%
c redc: 4064 clauses 15%, 26435 tried 8%, 20 sat 0%
c redc: 14289 lits 5%, 265712 tried 1%, 20 sat 0%
c redc: 685 times jump level reduced, 22.5 levels on average
c reds: 6 count, 52864.0 conflicts per reduce
c reds: 0 memlim 0%, 6 arith 100%
c reds: 157510 collected 84%, 28898 retired 16%
c rmbd: 2537 removed, 1403 red 55%
c rsts: 7510 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 9 count, 9 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 306582 count (310911 tried 1.0), 42656 sub out of 302129 (14.1%)
c swps: 5 count, 5 rounds, 1231 queries (246.2/round)
c swps: 649 sat calls, 3 unsat (0.4% success rate)
c swps: 29761 decisions 45.9, 266 conflicts 0.4
c swps; 488.3 avg class size, 181.6 avg environment size
c swps: 0 failed, 1217 impls, 584 equivs
c swp0: 408 type 0 queries, 478 unsat (117.2%), 178 sat (43.6%)
c swp1: 823 type 1 queries, 769 unsat (93.4%), 469 sat (57.0%)
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 time: 8427782 calls to obtain time
c tops: 8999 fixed 26%, 36 its, 8810.67 confs/it
c trds: 4 transitive reductions, 33 removed, 0 failed
c trds: 719 nodes, 10327 edges, 7044944 steps
c trim: 392116 words, 1.5 MB
c trnr: 4 count, 5 bin, 8292 trn, 41277588 steps
c unhd: 5 count, 5 rounds, 9906426 steps
c unhd: 6 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 2 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 12742 tauts, 19 bin 0%, 80 trn 1%, 1 lrg 0%
c unhd: 12742 tauts, 12642 stamp 99%, 1318 red 10%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 43552 str, 0 bin 0%, 562 trn 1%, 42990 lrg 99%, 30576 red 70%
c vars: 16259 remaining 46% and 18806 removed 54% out of 35065
c vars: 8999 fixed 26%, 9213 eliminated 26%, 594 equivalent 2%
c vsts: 1995603006 visits, 97% srch, 3% simp, 0% lkhd
c vsts: 5.3 search visits per propagation, 6082.2 per conflict
c wchs: 330273596 pushed, 23924024 enlarged, 72 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         302959        157510         28898       7632192       3500736        236765
c 
c  0 0         14679   5      1475   1         0   0   2919481  38    912773  26     19655   8     0.6
c  1 5          6886   2      1232   1       318   1    393732   5    219351   6     10084   4     0.2
c  2 6         30056  10      9842   6      1447   5    975272  13<   546913  16     38310  16     1.0
c  3 9         65800  22     32850  21      3641  13   1233621  16    686030  20<    55457  23     2.2
c  4 14        62747  21<    37286  24      4800  17    774121  10    423304  12     42570  18<    2.0
c  5 21        40853  13     24664  16<     4479  15    573505   8    309265   9     32015  14     1.9
c  6 30        29136  10     18019  11      4114  14<   294847   4    170322   5     21008   9     1.9
c  7 41        22587   7     14461   9      3760  13    205555   3    104424   3      9061   4     2.0
c  8 54        15404   5      9375   6      3084  11    140628   2     65139   2      4842   2     2.0
c  9 69         7425   2      4499   3      1601   6     78230   1     39012   1      1911   1     1.4
c 10 86         5116   2      3136   2      1089   4     39564   1     22072   1      1610   1     1.5
c 11 126        2224   1       669   0       543   2      3583   0      2112   0       239   0     0.7
c 12 230          46   0         2   0        22   0        53   0        19   0         3   0     0.0
c 
c avg                  4.4           4.8           5.6           2.3           2.7           3.6
c std                  2.3           2.0           2.2           2.4           2.3           2.0
c 
c   27.301  21% elim
c   14.170  11% block
c   10.302   8% probe
c    6.439   5% bump
c    3.140   2% sweep
c    2.686   2% decide
c    2.234   2% unhide
c    1.034   1% cce
c    1.022   1% bca
c 
c    1.722 < 1% rest (below)
c 
c    0.616   0% quatres
c    0.489   0% gauss
c    0.298   0% ternres
c    0.160   0% card
c    0.159   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    8.902   7% preprocessing    14%
c   55.771  43% inprocessing     86%
c ==================================
c   64.673  49% simplifying
c   66.137  51% search
c ==================================
c  130.811 100% all
c 
c        317184 conflicts,        2424.8 confs/sec
c          3778 ternaries,          84.0 confs/ternary
c           575 binaries,          551.6 confs/binary
c            36 iterations,       8810.7 confs/iteration
c 
c             6 reductions,          0.0 redus/sec,  52864.0 confs/reduction
c          7510 restarts,           57.4 rests/sec,     42.2 confs/restart
c       3907218 decisions,       29869.2 decis/sec,     12.3 decis/conflict
c     379991594 propagations,  2904894.5 props/sec,     97.3 props/decision
c 
c 130.8 seconds, 98.9 MB
c launch: done
