c launch: /data/cnf/sc2014/app/004-22-144.cnf.bz2
c host: atom32
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/004-22-144.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/004-22-144.cnf.bz2
c no embedded options
c found 'p cnf 4128 126564' header
c read 4128 variables, 126564 clauses, 833818 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=5
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 3605 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] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
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    3605    72259         0       0      0     0    0     0    4   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 3 at-most-one constraints of average size 3.0
c [card-1] found 6 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 9 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 803 variables
c [simpleprobe-1] all 3325 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 20000000 penalty 0 = 0 + 0
c [decomp-2] removed 138 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 138 variables, found 15 hbrs, 36 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 653 tauts, 0 hbrs, 22 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3187 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1-1] eliminated 79 variables 2% in round 1 in 2582178 steps
c [elim-1-1] backward subsumption/strengthening limit 2582100
c [elim-1-1-1] backward checking 1318 touched variables 41%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 12 and strengthened 57 clauses in 768446 steps
c [elim-1-1] rescheduled 108 variables 3% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 92159 steps
c [elim-1-2] backward subsumption/strengthening limit 92100
c [elim-1-2-1] backward checking 20 touched variables 1%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 92101 steps
c [elim-1-2] fully rescheduled 3105 variables 97%
c [elim-1-3] no variable eliminated in round 3 in 2207822 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 82 = 3% variables out of 3187 scheduled
c [phase-count-1] 57804 negative 99.1% of 58339 except 535 0.9%
c [phase-count-1] 57561 positive 98.7% of 58339 except 778 1.3%
c [phase-1] phase bias: 1333 positive 43%, 1772 negative 57%
c [sort-queue-1] sorted 3105 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 3105 (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 397 variables 11.3% (3105 remain 86%)
c [simplification-1] removed 13920 irredundant clauses 19.3% (58339 remain 81%)
c [simplification-1] maximum reduction of 19% = max (11%, 19%)
c [simplification-1] large reduction 19% >= 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 1000 conflicts
c [decomp-3] removed 2 variables
c [simpleprobe-2] all 3103 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 1 variables
c [simpleprobe-2] 993 variables remain 32% (2109 retained 68%)
c [simpleprobe-2] removed 1 variables, found 4 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6204 literals 100%
c [treelook-1] scheduling used 253709 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300105 steps
c [treelook-1] 4918 literals remain 79%
c [treelook-1] 3083 variables remain to probed next time 99%
c [treelook-1] removed 0 variables, found 20 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 327 sched 11%, 1 failed, 0 lifted, 2 hbrs
c [decomp-6] removed 1 variables
c [basicprobe-1-1] 325 sched 10%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-1] removed 1 variables, found 2 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3101 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 500000000 steps penalty 0 = 0 + 0
c [block-1] fully completed
c [block-1] transition to [ all 0 rem 0 ] state
c [block-1] eliminated 95 blocked clauses
c [block-1] 95 < 1/100 * 58314 = 583 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2841 clauses out of 17214 (17%) of length 7
c [cce-1-1] eliminated 338 clauses out of 17065 (2%) of length 6
c [cce-1-1] eliminated 2220 clauses out of 12671 (18%) of length 5
c [cce-1-1] eliminated 531 clauses out of 6419 (8%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 5930 large clauses in 26971843 steps
c [cce-1-1] allowing another 13485921 steps for small clauses
c [cce-1-1] scheduling 765 clauses = 210 binary + 555 ternary
c [cce-1-1] tried to eliminate 765 small clauses 100%
c [cce-1-1] eliminated 4 binary clauses 2%
c [cce-1-1] eliminated 66 ternary clauses 12%
c [cce-1-1] eliminated 70 small clauses 9%
c [cce-1-1] eliminated 70 small clauses in 13633388 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 6000 covered clauses in round 1
c [cce-1-2] eliminated 39 clauses out of 14373 (0%) of length 7
c [cce-1-2] incomplete large round (ABCE)
c [cce-1-2] eliminated 39 large clauses in 16366625 steps
c [cce-1-2] allowing another 8183312 steps for small clauses
c [cce-1-2] scheduling 695 clauses = 206 binary + 489 ternary
c [cce-1-2] tried to eliminate 695 small clauses 100%
c [cce-1-2] completed small round (ABCE)
c [cce-1-2] eliminated 39 covered clauses in round 2
c [cce-1-3] incomplete large round (ABCE)
c [cce-1-3] allowing another 4020241 steps for small clauses
c [cce-1-3] scheduling 695 clauses = 206 binary + 489 ternary
c [cce-1-3] tried to eliminate 695 small clauses 100%
c [cce-1-3] completed small round (ABCE)
c [cce-1-3] eliminated 0 covered clauses in round 3
c [cce-1] eliminated 6039 covered clauses in TOTAL during 3 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3101 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 428 not tried 14% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 13 = 0% variables out of 3101 scheduled
c [elim-2] 13 < 1/100 * 3101 = 31 considered unsuccessful
c [bca-1] limit of 10000000 steps and 104296 added (scaled 2)
c [bca-1] 4453 out of 6178 literals actually usable 72%
c [bca-1] added 0 blocked clauses in 28700 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1420 pos 46.0% + 1668 neg 54.0% = 3088 sched 100.0% ret 0
c [sweep-1-1] 442339 steps 534 queries 150.75 avg class size
c [sweep-1-1] 8213 decisions 531 SAT calls 21.70 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-7] removed 4 variables
c [sweep-1-1] removed 4 vars (0 failed, 3 eqs, 4 impls)
c [sweep-1-2] 1419 pos 46.0% + 1665 neg 54.0% = 3084 sched 100.0% ret 0
c [sweep-1-2] 422321 steps 530 queries 147.66 avg class size
c [sweep-1-2] 8146 decisions 531 SAT calls 21.42 avg env size
c [sweep-1-2] fully completed sweeping round
c [decomp-8] removed 4 variables
c [sweep-1-2] removed 4 vars (0 failed, 2 eqs, 4 impls)
c [sweep-1-3] 1418 pos 46.0% + 1662 neg 54.0% = 3080 sched 100.0% ret 0
c [sweep-1-3] 135873 steps 153 queries 559.97 avg class size
c [sweep-1-3] 2233 decisions 152 SAT calls 21.99 avg env size
c [sweep-1-3] 2210 variables remain 72% (869 retained 28%)
c [decomp-9] removed 1 variables
c [sweep-1-3] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-1] removed 9 vars in TOTAL (3 rounds, 1214 queries)
c [sort-queue-2] sorted 282 enqueued variables after 1000 conflicts
c [score-dist-2] active 2797 (91%), one 0 (0%), zero 282 (9%)
c [score-dist-2] max exp 594, different 394 (66%)
c [score-dist-2] median active exp 469, avg 435.5
c [simplification-2] removed 26 variables 0.8% (3079 remain 85%)
c [simplification-2] removed 6463 irredundant clauses 11.1% (51872 remain 72%)
c [simplification-2] maximum reduction of 11% = max (1%, 11%)
c [simplification-2] large reduction 11% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13000 (soft 3000 + delta 10000)
c [simplification-2] new conflict limit 3000 (hard 13000)
c 
c [simplification-3] limit 3000 conflicts (hard 13000) hit after 3001 conflicts
c [quatres-1] found 6601 quaternary clauses 13% in total
c [quatres-1-1] added 18 double-self-subsuming ternary resolvents
c [quatres-1-2] added 103 single-self-subsuming ternary resolvents
c [quatres-1-2] added 386 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 3079 free variables schedulable
c [ternres-1] 250 ternary resolvents (14 bin, 236 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] no at-most-one constraint found
c [card-2] found 8 at-most-two constraints of average size 4.1
c [card-2] using previous limit 1000000 for elimination
c [card-2] 8 out of 8 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 3364 xors of average arity 5.0
c [gauss-1] connected 16670 occurrences of 771 variables (average 21.6)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 3 failed, 77 tauts, 0 hbrs, 119 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 7 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 178 clauses out of 17094 (1%) of length 6
c [cce-2-1] eliminated 20 clauses out of 10539 (0%) of length 5
c [cce-2-1] eliminated 41 clauses out of 5928 (1%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 239 large clauses in 24062013 steps
c [cce-2-1] allowing another 12031006 steps for small clauses
c [cce-2-1] scheduling 737 clauses = 233 binary + 504 ternary
c [cce-2-1] tried to eliminate 737 small clauses 100%
c [cce-2-1] eliminated 2 binary clauses 1%
c [cce-2-1] eliminated 13 ternary clauses 3%
c [cce-2-1] eliminated 15 small clauses 2%
c [cce-2-1] eliminated 19 small clauses in 12175526 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 258 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 8912246 steps for small clauses
c [cce-2-2] scheduling 722 clauses = 231 binary + 491 ternary
c [cce-2-2] tried to eliminate 722 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 258 covered clauses in TOTAL during 2 rounds
c [cce-2] 258 < 1/100 * 51866 = 518 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1076 pos 48.7% + 1133 neg 51.3% = 2209 sched 71.8% ret 869
c [sweep-2-1] 371545 steps 460 queries 124.77 avg class size
c [sweep-2-1] 7327 decisions 463 SAT calls 22.32 avg env size
c [sweep-2-1] fully completed sweeping round
c [decomp-11] removed 1 variables
c [sweep-2-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2-2] 1490 pos 48.4% + 1587 neg 51.6% = 3077 sched 100.0% ret 0
c [sweep-2-2] 433863 steps 505 queries 146.47 avg class size
c [sweep-2-2] 8181 decisions 507 SAT calls 23.02 avg env size
c [sweep-2-2] fully completed sweeping round
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-2-3] 1490 pos 48.4% + 1587 neg 51.6% = 3077 sched 100.0% ret 0
c [sweep-2-3] 195351 steps 195 queries 366.93 avg class size
c [sweep-2-3] 3393 decisions 195 SAT calls 25.86 avg env size
c [sweep-2-3] 1691 variables remain 55% (1386 retained 45%)
c [sweep-2-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] 1 < 1/1000 * 3078 = 3 considered unsuccessful
c [sweep-2] removed 1 vars in TOTAL (3 rounds, 1157 queries)
c [sort-queue-3] sorted 264 enqueued variables after 3001 conflicts
c [score-dist-3] active 2813 (91%), one 168 (5%), zero 96 (3%)
c [score-dist-3] max exp 841, different 399 (47%)
c [score-dist-3] median active exp 728, avg 682.7
c [simplification-3] removed 2 variables 0.1% (3077 remain 85%)
c [simplification-3] removed 271 irredundant clauses 0.5% (51600 remain 71%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23001 (soft 13001 + delta 10000)
c [simplification-3] new conflict limit 13001 (hard 23001)
c 
c [simplification-4] limit 13001 conflicts (hard 23001) hit after 13003 conflicts
c [quatres-2] found 7841 quaternary clauses 15% in total
c [quatres-2-1] added 37 double-self-subsuming ternary resolvents
c [quatres-2-2] added 254 single-self-subsuming ternary resolvents
c [quatres-2-2] added 430 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3077 free variables schedulable
c [ternres-2] 125 ternary resolvents (18 bin, 107 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3379 literals 55%
c [treelook-2] scheduling used 150104 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150058 steps
c [treelook-2] 2704 literals remain 44%
c [treelook-2] 2570 variables remain to probed next time 84%
c [treelook-2] removed 0 variables, found 10 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 154 tauts, 0 hbrs, 240 literals
c [transred-2] limit 238881 with penalty 0 = 0 + 0
c [transred-2] removed 6 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3077 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [elim-3] 428 variables 14% will be scheduled this time
c [elim-3] scheduled 428 variables 14%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 149 not tried 5% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 428 scheduled
c [bca-2] limit of 10000000 steps and 103540 added (scaled 2)
c [bca-2] 576 out of 6156 literals actually usable 9%
c [bca-2] added 0 blocked clauses in 17037 steps
c [sort-queue-4] sorted 814 enqueued variables after 13003 conflicts
c [score-dist-4] active 2263 (74%), one 759 (25%), zero 55 (2%)
c [score-dist-4] max exp 791, different 269 (34%)
c [score-dist-4] median active exp 719, avg 677.1
c [simplification-4] removed 0 variables 0.0% (3077 remain 85%)
c [simplification-4] removed 80 irredundant clauses 0.2% (51520 remain 71%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 58003 (soft 43003 + delta 15000)
c [simplification-4] new conflict limit 43003 (hard 58003)
c 
c [simplification-5] limit 43003 conflicts (hard 58003) hit after 43003 conflicts
c [quatres-3] found 9818 quaternary clauses 16% in total
c [quatres-3-1] added 47 double-self-subsuming ternary resolvents
c [quatres-3-2] added 395 single-self-subsuming ternary resolvents
c [quatres-3-2] added 399 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3077 free variables schedulable
c [ternres-3] 261 ternary resolvents (35 bin, 226 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1035 xors of average arity 4.6
c [gauss-2] connected 4791 occurrences of 302 variables (average 15.9)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-16] removed 2 variables
c [basicprobe-2] limit 6128970 penalty 0 = 0 + 0
c [basicprobe-2-0] 511 sched 17%, 1 failed, 0 lifted, 10 hbrs
c [decomp-17] removed 1 variables
c [basicprobe-2-1] 516 sched 17%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-2] 516 sched 17%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-2] fully completed probing
c [basicprobe-2-2] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-2-2] removed 1 variables, found 11 hbrs
c [bate-1] eliminated 12 asymmetric tautologies during probing
c [transred-3] limit 1225794 with penalty 0 = 0 + 0
c [transred-3] removed 17 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 5 clauses out of 17160 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 5 large clauses in 15000022 steps
c [cce-3-1] allowing another 7500011 steps for small clauses
c [cce-3-1] scheduling 792 clauses = 269 binary + 523 ternary
c [cce-3-1] tried to eliminate 792 small clauses 100%
c [cce-3-1] eliminated 7 ternary clauses 1%
c [cce-3-1] eliminated 7 small clauses 1%
c [cce-3-1] eliminated 7 small clauses in 7681414 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 12 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3659314 steps for small clauses
c [cce-3-2] scheduling 785 clauses = 269 binary + 516 ternary
c [cce-3-2] tried to eliminate 785 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 12 covered clauses in TOTAL during 2 rounds
c [cce-3] 12 < 1/100 * 51496 = 514 considered unsuccessful
c [sweep-3] limit 500000 penalty 1 = 1 + 0
c [sweep-3-1] 868 pos 51.4% + 822 neg 48.6% = 1690 sched 55.0% ret 1384
c [sweep-3-1] 503053 steps 159 queries 122.16 avg class size
c [sweep-3-1] 8593 decisions 158 SAT calls 97.42 avg env size
c [sweep-3-1] 398 variables remain 13% (2676 retained 87%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 158 queries)
c [sort-queue-5] sorted 417 enqueued variables after 43003 conflicts
c [score-dist-5] active 2657 (86%), one 376 (12%), zero 41 (1%)
c [score-dist-5] max exp 725, different 270 (37%)
c [score-dist-5] median active exp 659, avg 616.4
c [simplification-5] removed 3 variables 0.1% (3074 remain 85%)
c [simplification-5] removed 36 irredundant clauses 0.1% (51484 remain 71%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30000
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] hard conflict limit 133003 (soft 103003 + delta 30000)
c [simplification-5] new conflict limit 103003 (hard 133003)
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 -   14.5    3074    51484     75126   28229   2915   205   12   268   15   5%    693   98   13    7  187%
c 
c [simplification-6] limit 103003 conflicts (hard 133003) hit after 103003 conflicts
c [quatres-4] found 12793 quaternary clauses 18% in total
c [quatres-4-1] removed 4 duplicate quaternary clauses
c [quatres-4-1] added 45 double-self-subsuming ternary resolvents
c [quatres-4-2] added 458 single-self-subsuming ternary resolvents
c [quatres-4-2] added 422 quaternary resolvents
c [ternres-4] limit 4053725 with penalty 0 = 0 + 0
c [ternres-4] all 3074 free variables schedulable
c [ternres-4] 164 ternary resolvents (10 bin, 154 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 506715 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 23 at-most-two constraints of average size 4.1
c [card-3] using previous limit 506715 for elimination
c [card-3] 25 out of 26 constraints (96%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [simpleprobe-3] 984 schedulable variables 32%
c [simpleprobe-3] limit 16214900 penalty 0 = 0 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 39 hbrs, 0 units
c [unhide-4] limit 405372 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 312 tauts, 0 hbrs, 2111 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 22 transitive binary clauses
c [sort-queue-6] sorted 230 enqueued variables after 103003 conflicts
c [score-dist-6] active 2844 (93%), one 222 (7%), zero 8 (0%)
c [score-dist-6] max exp 638, different 234 (37%)
c [score-dist-6] median active exp 591, avg 523.9
c [simplification-6] removed 0 variables 0.0% (3074 remain 85%)
c [simplification-6] removed 0 irredundant clauses 0.0% (51484 remain 71%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 60000
c [simplification-6] new conflict interval 120000
c [simplification-6] penalized conflict interval 120000 = 1 * 120000
c [simplification-6] hard conflict limit 283003 (soft 223003 + delta 60000)
c [simplification-6] new conflict limit 223003 (hard 283003)
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 -   25.1    3074    51484    129409   35742   3762   261   14   283   17   5%    880   56   13   10  128%
c -   36.0    3074    51484    182730   44127   4032   264   15   304   18   5%    960   48   18   13  143%
c 
c [simplification-7] limit 223003 conflicts (hard 283003) hit after 223003 conflicts
c [quatres-5] found 16615 quaternary clauses 19% in total
c [quatres-5-1] removed 12 duplicate quaternary clauses
c [quatres-5-1] added 36 double-self-subsuming ternary resolvents
c [quatres-5-2] added 424 single-self-subsuming ternary resolvents
c [quatres-5-2] added 316 quaternary resolvents
c [ternres-5] limit 10388942 with penalty 0 = 0 + 0
c [ternres-5] all 3074 free variables schedulable
c [ternres-5] 96 ternary resolvents (2 bin, 94 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 12 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3074 variables 100%
c [block-3] limit of 25972355 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3074 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1038894205 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 4 variables 0% in round 1 in 37296208 steps
c [elim-4-1] backward subsumption/strengthening limit 37296200
c [elim-4-1-1] backward checking 913 touched variables 30%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 6 clauses in 586893 steps
c [elim-4-1] rescheduled 18 variables 1% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 65108 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 4 = 0% variables out of 3074 scheduled
c [elim-4] 4 < 1/100 * 3074 = 30 considered unsuccessful
c [bca-3] limit of 10000000 steps and 103114 added (scaled 2)
c [bca-3] 2 out of 6142 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 82455 steps
c [sort-queue-7] sorted 36 enqueued variables after 223003 conflicts
c [score-dist-7] active 3034 (99%), one 36 (1%), zero 0 (0%)
c [score-dist-7] max exp 531, different 227 (43%)
c [score-dist-7] median active exp 481, avg 460.4
c [simplification-7] removed 4 variables 0.1% (3070 remain 85%)
c [simplification-7] removed 177 irredundant clauses 0.3% (51307 remain 71%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 120000
c [simplification-7] new conflict interval 240000
c [simplification-7] penalized conflict interval 240000 = 1 * 240000
c [simplification-7] hard conflict limit 583003 (soft 463003 + delta 120000)
c [simplification-7] new conflict limit 463003 (hard 583003)
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 -   45.9    3070    51307    234553   44891   4725   249   16   286   18   6%    995   10   17   14  117%
c -   54.9    3070    51307    292861   53914   4853   253   18   312   19   6%   1012   20   17   16  105%
c -   63.6    3070    51307    348044   59971   4953   253   19   318   13   6%   1019   15   20   17  117%
c -   72.5    3070    51307    402351   64364   5040   253   20   312   21   6%   1022   -1   22   19  119%
c -   81.1    3070    51307    457021   68426   5093   253   21   341   21   6%   1023   22   17   20   87%
c 
c [simplification-8] limit 463003 conflicts (hard 583003) hit after 463003 conflicts
c [quatres-6] found 20798 quaternary clauses 19% in total
c [quatres-6-1] removed 36 duplicate quaternary clauses
c [quatres-6-1] added 26 double-self-subsuming ternary resolvents
c [quatres-6-2] added 313 single-self-subsuming ternary resolvents
c [quatres-6-2] added 268 quaternary resolvents
c [ternres-6] limit 20768585 with penalty 0 = 0 + 0
c [ternres-6] all 3070 free variables schedulable
c [ternres-6] 41 ternary resolvents (2 bin, 39 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1038429 penalty 2 = 2 + 0
c [gauss-3] extracted 178 xors of average arity 3.0
c [gauss-3] connected 534 occurrences of 38 variables (average 14.1)
c [gauss-3] limit 1038429 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 9 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 259607312 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 13 clauses out of 17566 (0%) of length 6
c [cce-4-1] eliminated 47 clauses out of 10612 (0%) of length 5
c [cce-4-1] eliminated 82 clauses out of 5580 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 142 large clauses in 23610736 steps
c [cce-4-1] allowing another 11805368 steps for small clauses
c [cce-4-1] scheduling 4491 clauses = 295 binary + 4196 ternary
c [cce-4-1] tried to eliminate 4491 small clauses 100%
c [cce-4-1] eliminated 3 binary clauses 1%
c [cce-4-1] eliminated 1003 ternary clauses 24%
c [cce-4-1] eliminated 1006 small clauses 22%
c [cce-4-1] eliminated 1006 small clauses in 12953994 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 1148 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 11662542 steps for small clauses
c [cce-4-2] scheduling 3485 clauses = 292 binary + 3193 ternary
c [cce-4-2] tried to eliminate 3485 small clauses 100%
c [cce-4-2] completed small round (ATE)
c [cce-4-2] eliminated 0 covered clauses in round 2
c [cce-4] eliminated 1148 covered clauses in TOTAL during 2 rounds
c [sweep-4] limit 1557643 penalty 2 = 2 + 0
c [sweep-4-1] 184 pos 46.2% + 214 neg 53.8% = 398 sched 13.0% ret 2672
c [sweep-4-1] 393133 steps 108 queries 19.83 avg class size
c [sweep-4-1] 6122 decisions 107 SAT calls 109.31 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-2] 1602 pos 52.2% + 1468 neg 47.8% = 3070 sched 100.0% ret 0
c [sweep-4-2] 991940 steps 220 queries 95.68 avg class size
c [sweep-4-2] 14098 decisions 219 SAT calls 125.08 avg env size
c [sweep-4-2] fully completed sweeping round
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-3] 1602 pos 52.2% + 1468 neg 47.8% = 3070 sched 100.0% ret 0
c [sweep-4-3] 178135 steps 38 queries 403.16 avg class size
c [sweep-4-3] 2828 decisions 37 SAT calls 178.03 avg env size
c [sweep-4-3] 2257 variables remain 74% (813 retained 26%)
c [sweep-4-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (3 rounds, 363 queries)
c [sort-queue-8] sorted 6 enqueued variables after 463003 conflicts
c [score-dist-8] active 3064 (100%), one 6 (0%), zero 0 (0%)
c [score-dist-8] max exp 787, different 208 (26%)
c [score-dist-8] median active exp 747, avg 733.5
c [simplification-8] removed 0 variables 0.0% (3070 remain 85%)
c [simplification-8] removed 1149 irredundant clauses 2.2% (50158 remain 69%)
c [simplification-8] maximum reduction of 2% = max (0%, 2%)
c [simplification-8] geometric conflict interval increment 80000 = 240000 / 3
c [simplification-8] new conflict interval 320000
c [simplification-8] penalized conflict interval 320000 = 1 * 320000
c [simplification-8] hard conflict limit 943003 (soft 783003 + delta 160000)
c [simplification-8] new conflict limit 783003 (hard 943003)
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 -   90.8    3070    50158    512151   71540   6486   252   22   345   14   6%   1024   20   21   21   99%
c -   99.4    3070    50158    568540   76069   6505   253   24   339   22   7%   1024    6   27   22  119%
c -  108.1    3070    50158    624723   80091   6531   253   25   353   23   7%   1024   10   27   23  117%
c -  116.9    3070    50158    681008   84513   6556   254   25   353   23   7%   1024    5   26   25  106%
c -  125.8    3070    50158    736387   88014   6578   255   28   350   24   8%   1024   -1   32   26  123%
c 
c [simplification-9] limit 783003 conflicts (hard 943003) hit after 783004 conflicts
c [quatres-7] found 23025 quaternary clauses 18% in total
c [quatres-7-1] removed 53 duplicate quaternary clauses
c [quatres-7-1] added 10 double-self-subsuming ternary resolvents
c [quatres-7-2] added 132 single-self-subsuming ternary resolvents
c [quatres-7-2] added 136 quaternary resolvents
c [ternres-7] limit 35671975 with penalty 0 = 0 + 0
c [ternres-7] all 3070 free variables schedulable
c [ternres-7] 12 ternary resolvents (0 bin, 12 trn)
c [ternres-7] fully completed ternary resolution
c [treelook-3] limit 891799 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 5229 literals 85%
c [treelook-3] scheduling used 699178 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 891799 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 891869 steps
c [treelook-3] 1175 literals remain 19%
c [treelook-3] 1145 variables remain to probed next time 37%
c [treelook-3] removed 0 variables, found 12 hbrs
c [unhide-5] limit 1783598 with penalty 2 = 2 + 0
c [unhide-5-6] 0 units, 0 failed, 113 tauts, 0 hbrs, 15770 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 8 transitive binary clauses
c [sort-queue-9] sorted 11 enqueued variables after 783004 conflicts
c [score-dist-9] active 3059 (100%), one 11 (0%), zero 0 (0%)
c [score-dist-9] max exp 585, different 221 (38%)
c [score-dist-9] median active exp 552, avg 499.6
c [simplification-9] removed 0 variables 0.0% (3070 remain 85%)
c [simplification-9] removed 0 irredundant clauses 0.0% (50158 remain 69%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 320000
c [simplification-9] new conflict interval 640000
c [simplification-9] penalized conflict interval 640000 = 1 * 640000
c [simplification-9] hard conflict limit 1743004 (soft 1423004 + delta 320000)
c [simplification-9] new conflict limit 1423004 (hard 1743004)
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 -  135.3    3070    50158    791930   92172   6654   259   28   369   24   7%   1024   11   26   27   98%
c -  144.2    3070    50158    846431   96132   6664   259   30   367   16   8%   1024    7   33   28  117%
c -  152.8    3070    50158    900549   99184   6671   259   29   378   16   8%   1024   11   28   29   99%
c -  161.6    3070    50158    954631  102132   6678   259   31   352   26   9%   1024  -11   34   30  116%
c -  170.3    3070    50158   1008962  105168   6683   259   30   354   26   8%   1024  -10   32   30  106%
c -  179.2    3070    50158   1063441  108300   6687   259   31   353   17   9%   1024  -10   25   31   82%
c -  188.0    3070    50158   1117881  110951   6692   259   30   370   17   8%   1024    4   23   31   74%
c -  196.9    3070    50158   1172742  113812   6698   259   32   379   17   8%   1024   11   33   32  105%
c -  206.2    3070    50158   1227492  115793   6703   259   33   375   18   9%   1024    5   37   32  115%
c -  215.3    3070    50158   1283179  118244   6707   259   33   371   18   9%   1024    0   39   32  120%
c -  224.9    3070    50158   1339376  120586   6711   259   33   375   28   9%   1024    3   28   33   87%
c -  234.6    3070    50158   1396177  122481   6720   259   32   356   28   9%   1024  -13   29   33   89%
c 
c [simplification-10] limit 1423004 conflicts (hard 1743004) hit after 1423004 conflicts
c [quatres-8] found 25011 quaternary clauses 17% in total
c [quatres-8-1] removed 89 duplicate quaternary clauses
c [quatres-8-1] added 5 double-self-subsuming ternary resolvents
c [quatres-8-2] added 68 single-self-subsuming ternary resolvents
c [quatres-8-2] added 113 quaternary resolvents
c [ternres-8] limit 70391101 with penalty 0 = 0 + 0
c [ternres-8] all 3070 free variables schedulable
c [ternres-8] 38 ternary resolvents (0 bin, 38 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 4399443 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 14 at-most-two constraints of average size 4.0
c [card-4] using previous limit 4399443 for elimination
c [card-4] 16 out of 16 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [basicprobe-3] limit 351955506 penalty 0 = 0 + 0
c [basicprobe-3-0] 592 sched 19%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-0] fully completed probing
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 1 transitive binary clauses
c [cce-5] limit of 175977753 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 2 clauses out of 17630 (0%) of length 6
c [cce-5-1] eliminated 4 clauses out of 10560 (0%) of length 5
c [cce-5-1] eliminated 11 clauses out of 5507 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 17 large clauses in 25725085 steps
c [cce-5-1] allowing another 12862542 steps for small clauses
c [cce-5-1] scheduling 3486 clauses = 292 binary + 3194 ternary
c [cce-5-1] tried to eliminate 3486 small clauses 100%
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 17 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 12828614 steps for small clauses
c [cce-5-2] scheduling 3486 clauses = 292 binary + 3194 ternary
c [cce-5-2] tried to eliminate 3486 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 17 covered clauses in TOTAL during 2 rounds
c [cce-5] 17 < 1/100 * 50158 = 501 considered unsuccessful
c [sort-queue-10] sorted 9 enqueued variables after 1423004 conflicts
c [score-dist-10] active 3061 (100%), one 9 (0%), zero 0 (0%)
c [score-dist-10] max exp 1001, different 259 (26%)
c [score-dist-10] median active exp 942, avg 904.2
c [simplification-10] removed 0 variables 0.0% (3070 remain 85%)
c [simplification-10] removed 17 irredundant clauses 0.0% (50141 remain 69%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 640000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] hard conflict limit 2923004 (soft 2423004 + delta 500000)
c [simplification-10] new conflict limit 2423004 (hard 2923004)
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 -  246.0    3070    50141   1453847  125256   6830   258   35   374   18   9%   1024    2   36   33  108%
c -  256.1    3070    50141   1511383  127527   6834   258   34   387   19   9%   1024   10   33   34   98%
c -  266.3    3070    50141   1569412  130224   6838   258   35   369   19   9%   1024   -6   30   35   87%
c -  276.6    3070    50141   1627315  131901   6842   258   35   370   19   9%   1024   -6   35   35  102%
c -  287.3    3070    50141   1686339  133956   6848   258   35   382   30   9%   1024    8   30   35   85%
c -  298.2    3070    50141   1745794  135699   6853   258   36   373   30  10%   1024   -6   33   35   94%
c -  309.1    3070    50141   1806319  138917   6857   258   36   379   31  10%   1024    4   38   36  108%
c -  319.9    3070    50141   1866238  140810   6861   258   36   374   20  10%   1024   -1   38   36  106%
c -  330.8    3070    50141   1926927  143129   6862   258   36   385   20   9%   1024   10   42   36  115%
c -  341.9    3070    50141   1987801  145018   6863   258   37   375   20  10%   1024   -2   32   37   86%
c -  353.0    3070    50141   2049100  147261   6867   258   38   372   32  10%   1024   -6   41   37  110%
c -  364.6    3070    50141   2110706  149312   6871   258   40   385   21  10%   1024    6   35   38   91%
c -  375.8    3070    50141   2172610  151328   6872   258   40   390   21  10%   1024    7   46   39  120%
c -  387.5    3070    50141   2235035  152531   6876   258   37   382   21  10%   1024   -0   38   39   98%
c -  399.3    3070    50141   2298617  154895   6877   258   39   369   21  11%   1024  -15   46   39  118%
c -  411.1    3070    50141   2362329  157015   6879   258   38   398   21  10%   1024   16   36   39   92%
c 
c [simplification-11] limit 2423004 conflicts (hard 2923004) hit after 2426092 conflicts
c [quatres-9] found 26559 quaternary clauses 15% in total
c [quatres-9-1] removed 108 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 32 single-self-subsuming ternary resolvents
c [quatres-9-2] added 65 quaternary resolvents
c [ternres-9] limit 135633101 with penalty 0 = 0 + 0
c [ternres-9] all 3070 free variables schedulable
c [ternres-9] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-9] fully completed ternary resolution
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 0 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 3070 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 3070 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 1 variables 0% in round 1 in 36086528 steps
c [elim-5-1] backward subsumption/strengthening limit 36086500
c [elim-5-1-1] backward checking 267 touched variables 9%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 177642 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 1 = 0% variables out of 3070 scheduled
c [elim-5] 1 < 1/100 * 3070 = 30 considered unsuccessful
c [bca-4] limit of 10000000 steps and 100782 added (scaled 2)
c [bca-4] 1 out of 6140 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 220015 steps
c [sort-queue-11] sorted 7 enqueued variables after 2426092 conflicts
c [score-dist-11] active 3062 (100%), one 7 (0%), zero 0 (0%)
c [score-dist-11] max exp 915, different 274 (30%)
c [score-dist-11] median active exp 850, avg 810.0
c [simplification-11] removed 1 variables 0.0% (3069 remain 85%)
c [simplification-11] removed 0 irredundant clauses 0.0% (50141 remain 69%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] hard conflict limit 3926092 (soft 3426092 + delta 500000)
c [simplification-11] new conflict limit 3426092 (hard 3926092)
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 -  424.1    3069    50141   2426550  158836   6902   257   37   377   21  10%   1024   -6   33   39   85%
c -  436.1    3069    50141   2490953  160807   6902   257   38   378   22  10%   1024   -2   42   39  109%
c -  448.4    3069    50141   2556023  162716   6905   257   37   385   22  10%   1024    6   32   39   83%
c -  461.0    3069    50141   2621490  163760   6905   257   40   372   22  11%   1024  -10   48   39  123%
c -  474.0    3069    50141   2688295  165541   6905   257   41   378   22  11%   1024   -4   38   40   96%
c -  486.8    3069    50141   2755818  168307   6906   257   40   398   23  10%   1024   16   39   40   97%
c -  499.7    3069    50141   2823017  170140   6908   257   39   382   35  10%   1024    3   31   40   79%
c -  512.9    3069    50141   2890996  171588   6913   257   38   389   23  10%   1024    5   29   39   74%
c -  526.4    3069    50141   2959971  173162   6916   257   41   397   23  10%   1024   16   46   40  116%
c -  540.4    3069    50141   3029773  175492   6917   257   43   389   23  11%   1024   11   55   40  138%
c -  554.1    3069    50141   3099653  177191   6920   257   39   389   37  10%   1024    8   32   40   81%
c -  568.2    3069    50141   3170185  179057   6922   257   40   383   37  11%   1024   -0   35   40   86%
c -  582.4    3069    50141   3241216  179953   6922   257   40   385   24  10%   1024    2   39   40   97%
c -  597.0    3069    50141   3313731  181866   6922   257   43   384   24  11%   1024   -1   47   40  116%
c -  611.8    3069    50141   3386725  184297   6923   257   41   378   24  11%   1024   -6   45   40  113%
c 
c [simplification-12] limit 3426092 conflicts (hard 3926092) hit after 3429918 conflicts
c [quatres-10] found 27378 quaternary clauses 14% in total
c [quatres-10-1] removed 96 duplicate quaternary clauses
c [quatres-10-1] added 1 double-self-subsuming ternary resolvents
c [quatres-10-2] added 19 single-self-subsuming ternary resolvents
c [quatres-10-2] added 47 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 3069 free variables schedulable
c [ternres-10] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 5252861 penalty 3 = 3 + 0
c [gauss-4] extracted 4091 xors of average arity 5.2
c [gauss-4] connected 21429 occurrences of 848 variables (average 25.3)
c [gauss-4] limit 5252861 penalty 3 = 3 + 0
c [gauss-4] connected 2037 occurrences of 848 variables (average 2.4)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] all 3069 free variables schedulable
c [simpleprobe-4] limit 100000000 penalty 1 = 1 + 0
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 0 variables, found 31 hbrs, 0 units
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 78792928 penalty 3 = 3 + 0
c [sweep-5-1] 1070 pos 47.4% + 1186 neg 52.6% = 2256 sched 73.5% ret 813
c [sweep-5-1] 1920405 steps 169 queries 49.41 avg class size
c [sweep-5-1] 15830 decisions 169 SAT calls 753.80 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 1473 pos 48.0% + 1596 neg 52.0% = 3069 sched 100.0% ret 0
c [sweep-5-2] 1936574 steps 187 queries 98.13 avg class size
c [sweep-5-2] 17404 decisions 186 SAT calls 748.59 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 1473 pos 48.0% + 1596 neg 52.0% = 3069 sched 100.0% ret 0
c [sweep-5-3] 1984388 steps 190 queries 87.86 avg class size
c [sweep-5-3] 17928 decisions 189 SAT calls 787.29 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 543 queries)
c [sort-queue-12] sorted 17 enqueued variables after 3429918 conflicts
c [score-dist-12] active 3052 (99%), one 17 (1%), zero 0 (0%)
c [score-dist-12] max exp 752, different 238 (32%)
c [score-dist-12] median active exp 700, avg 674.0
c [simplification-12] removed 0 variables 0.0% (3069 remain 85%)
c [simplification-12] removed 0 irredundant clauses 0.0% (50141 remain 69%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] new conflict interval 2000000
c [simplification-12] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-12] hard conflict limit 6429918 (soft 5429918 + delta 1000000)
c [simplification-12] new conflict limit 5429918 (hard 6429918)
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 -  628.6    3069    50141   3459621  186074   6949   288   40   387   24  10%   1024    5   39   40   97%
c -  643.5    3069    50141   3533163  188417   6951   288   39   397   24  10%   1024   16   37   41   92%
c -  658.7    3069    50141   3606709  189680   6953   288   41   383   25  11%   1024    2   42   41  104%
c -  674.2    3069    50141   3681497  191745   6953   288   41   382   25  11%   1024    4   47   41  114%
c -  689.5    3069    50141   3756644  193849   6955   288   41   387   25  11%   1024    6   35   41   85%
c -  705.2    3069    50141   3831848  195378   6958   288   41   394   39  10%   1024    8   50   41  121%
c -  720.7    3069    50141   3907851  197490   6960   288   43   374   25  12%   1024  -12   42   42  100%
c -  736.8    3069    50141   3984240  198590   6961   288   41   384   25  11%   1024    5   30   41   73%
c -  753.7    3069    50141   4061843  200055   6964   288   41   392   26  11%   1024   12   46   41  110%
c -  770.1    3069    50141   4140470  201709   6965   288   43   376   26  11%   1024   -5   35   41   86%
c -  786.6    3069    50141   4219777  204008   6967   288   40   366   26  11%   1024  -15   33   41   80%
c -  803.8    3069    50141   4299080  204750   6968   288   40   383   26  11%   1024    1   42   41  102%
c -  821.3    3069    50141   4380116  207530   6970   288   39   367   26  11%   1024  -14   42   41  103%
c -  839.3    3069    50141   4460742  207994   6971   288   42   398   26  10%   1024   14   34   41   82%
c -  857.1    3069    50141   4543478  210806   6972   288   42   377   27  11%   1024   -5   47   41  114%
c -  875.0    3069    50141   4625887  213280   6974   288   40   389   27  10%   1024    9   39   41   95%
c -  893.6    3069    50141   4708087  214139   6976   288   42   389   27  11%   1024    5   52   41  126%
c -  912.3    3069    50141   4791812  216616   6978   288   44   375   27  12%   1024   -5   47   42  112%
c -  930.7    3069    50141   4875473  218713   6978   288   43   386   27  11%   1024    4   41   42   98%
c -  949.2    3069    50141   4959388  220072   6978   288   40   385   28  10%   1024    4   33   42   79%
c -  968.6    3069    50141   5044280  221663   6980   288   43   395   28  11%   1024   10   38   42   90%
c -  987.5    3069    50141   5130109  223491   6983   288   41   375   28  11%   1024   -8   39   42   93%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 12 basic ate = 10 trn 83% + 2 lrg 17% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 348207 steps
c bkwd: tried 6188 clauses, 12326 lits, 1.99 lits/clause
c bkwd: checked 570260 occs, 92.16 occs/clause, 46.26 occs/lit
c bkwd: subsumed 0 binary, 4 ternary, 9 large
c bkwd: strengthened 0 binary, 4 ternary (100% self), 59 large (0% self)
c blkd: 4 bces, 95 removed, 2487360 resolutions, 5232942 steps
c blkd: 32 blocking literals 0%, 0 pure
c bump: 5157218 bumped seen, 520604566 lits 100.9 on average
c card: 4 count, 0 units, 0 am1, 8141104 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1404 subsumed
c card: 8 at-most-one constraints found, average size 3.00
c card: 8 at-most-one constraints used 100%, average size 3.00
c card: 51 at-most-two constraints found, average size 4.08
c card: 50 at-most-two constraints used 98%, average size 4.08
c cces: 5 cces, 7470 eliminated, 7430 ate 99%, 40 abce 1%
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: 960382 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 51 gcs, 0 rescored clauses, 2713 rescored vars
c dcps: 35 decompositions, 251 equivalent 6%
c deco: 6045 decision-only clauses 0%, 43% reduction
c decs: 32291702 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 99 eliminated 2%, 0 pure 0%
c elms: 9 rounds, 1.8 rounds/bve
c elms: 99 small 100%, 0 large 0%
c elms: 1836 tried small, 100 succeeded 5%, 1736 failed 95%
c elms: 2345 subsumed, 2906 strengthened, 3 blocked
c elms: 1070732 copies, 2500465 resolutions, 503068 ipos
c elms: 202329 subchks, 147748 strchks
c gaus: 4 extractions, 8668 extracted, 5.0 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 1 gc, 18583066 steps, 9291533 extr 50%, 287430 elim 2%
c glue: 35.7 orig avg, 35.7 real avg, 5.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 163 = 89 simple 55% + 62 trn 38% + 12 lrg 7%, 6 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5157218 clauses, 74.6 length
c lrnd: 384601794 lits = 408520647 orig - 23918853 removed 6%
c lrnd: 2308401 uips 45%, 2305106 flips 45%
c mins: 4805583 mins 93%, 47 bin 0%, 334564 size 7%
c mins: 309654971 poisoned searches, 28680873 hits, 9% hit rate
c mins: 620606843 used twice searches, 116127727 hits, 19% hit rate
c move: moved 1371, 9 bin 1%, 1362 trn 99%
c otfs: 33386 driving 47%, 37112 restarting 53%
c otfs: str 70498, 68862 red 98%, 1636 irr 2%
c otfs: str 70498, 0 bin 0%, 137 trn 0%, 70361 lrg 100%
c otfs: sub 491, 484 red 99%, 7 irr 1%
c otfs: sub 491, 0 bin 0%, 22 trn 4%, 469 lrg 96%
c phas: 1 computed, 3105 set, 1333 pos (43%), 1772 neg (57%)
c prbs: 3 basic, 5573 probed, 2 failed, 0 lifted
c prbs: 4 simple, 19484 probed, 36 failed, 137 eqs
c prbs: 3 treelook, 6015 probed, 0 failed, 0 lifted
c prom: 841401 locked 17% out of 5038782 tried
c prps: 572925463 props, 18 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 10 count, 2582 quat, 2198 self1, 227 self2, 406 dup
c queu: 12 sorted, 32291702 next (12385230 steps 0.38)
c queu: 528872712 enq (554472354 steps 1.05), 520604566 deq 98%
c redc: 584 clauses 0%, 514829 tried 10%, 2 sat 0%
c redc: 606 lits 0%, 4242064 tried 1%, 2 sat 0%
c redc: 26 times jump level reduced, 18.5 levels on average
c reds: 78 count, 66509.3 conflicts per reduce
c reds: 0 memlim 0%, 78 arith 100%
c reds: 3411435 collected 70%, 1433947 retired 30%
c rmbd: 32 removed, 18 red 56%
c rsts: 36290 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 12 count, 12 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5157218 count (9925015 tried 1.9), 26387 sub out of 5155039 (0.5%)
c swps: 5 count, 13 rounds, 3435 queries (264.2/round)
c swps: 3444 sat calls, 15 unsat (0.8% success rate)
c swps: 120296 decisions 34.9, 2876 conflicts 0.8
c swps; 159.7 avg class size, 153.8 avg environment size
c swps: 0 failed, 14 impls, 5 equivs
c swp0: 1141 type 0 queries, 27 unsat (2.4%), 1141 sat (100.0%)
c swp1: 2294 type 1 queries, 166 unsat (7.2%), 2289 sat (99.8%)
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: 74903537 calls to obtain time
c tops: 709 fixed 17%, 0 its, 0.00 confs/it
c trds: 9 transitive reductions, 82 removed, 0 failed
c trds: 55061 nodes, 4457 edges, 6461 steps
c trim: 197963 words, 0.8 MB
c trnr: 10 count, 81 bin, 910 trn, 17797470 steps
c unhd: 5 count, 6 rounds, 2674814 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 3 failed, 3 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 1309 tauts, 0 bin 0%, 980 trn 75%, 297 lrg 23%
c unhd: 1309 tauts, 32 stamp 2%, 805 red 61%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 18262 str, 0 bin 0%, 102 trn 1%, 18160 lrg 99%, 18174 red 100%
c vars: 3069 remaining 74% and 1059 removed 26% out of 4128
c vars: 709 fixed 17%, 99 eliminated 2%, 251 equivalent 6%
c vsts: 36005064888 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 62.9 search visits per propagation, 6938.6 per conflict
c wchs: 10179245807 pushed, 13329049 enlarged, 1103 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5157621       3411435       1433947     238469335      51051308       2560101
c 
c  0 0        186307   4       305   0         0   0 192389467  81< 37159428  73   1853163  72     5.8
c  1 5        219075   4     90639   3    106464   7  25216118  11   5506755  11<   299736  12<    0.7
c  2 6        727718  14    406839  12    291290  20  11379196   5   3183007   6    160059   6     1.3
c  3 9        771738  15    500101  15    258103  18   3246550   1   1421762   3     57670   2     0.9
c  4 14       678251  13    479280  14    188353  13   1945752   1   1037732   2     43273   2     1.3
c  5 21       568196  11<   412959  12    146030  10<  1259412   1    738153   1     31886   1     1.7
c  6 30       462060   9    342520  10<   111955   8    829988   0    517561   1     23734   1     2.1
c  7 41       384941   7    291502   9     87115   6    600696   0    393399   1     19705   1     2.7
c  8 54       322075   6    248118   7     68286   5    460283   0    311016   1     17092   1     3.2
c  9 69       267188   5    208941   6     53044   4    365351   0    253249   0     14999   1     3.7
c 10 86       379366   7    295865   9     74451   5    512661   0    357660   1     24548   1     8.0
c 11 126      178531   3    128504   4     44824   3    246528   0    161135   0     13334   1     6.2
c 12 230       12175   0      5862   0      4032   0     17333   0     10451   0       902   0     0.6
c 
c avg                  5.0           5.5           4.6           0.4           0.8           0.8
c std                  2.9           2.8           2.8           1.2           1.8           1.9
c 
c   65.845   7% bump
c   21.505   2% decide
c    2.598   0% cce
c 
c    6.226 < 1% rest (below)
c 
c    2.035   0% elim
c    1.547   0% sweep
c    1.354   0% rescore
c    0.998   0% probe
c    0.811   0% quatres
c    0.479   0% block
c    0.365   0% unhide
c    0.346   0% gauss
c    0.125   0% card
c    0.105   0% ternres
c    0.080   0% bca
c    0.014   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.513   0% preprocessing     5%
c   10.236   1% inprocessing     95%
c ==================================
c   10.748   1% simplifying
c  989.194  99% search
c ==================================
c  999.942 100% all
c 
c       5187728 conflicts,        5188.0 confs/sec
c          1845 ternaries,        2811.8 confs/ternary
c            72 binaries,        72051.8 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            78 reductions,          0.1 redus/sec,  66509.3 confs/reduction
c         36290 restarts,           36.3 rests/sec,    143.0 confs/restart
c      32291702 decisions,       32293.6 decis/sec,      6.2 decis/conflict
c     572925463 propagations,   572958.6 props/sec,     17.7 props/decision
c 
c 999.9 seconds, 106.2 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
