c launch: /data/cnf/sc2014/app/13pipe_q0_k.cnf.bz2
c host: atom21
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/13pipe_q0_k.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/13pipe_q0_k.cnf.bz2
c no embedded options
c found 'p cnf 176066 5761591' header
c read 176066 variables, 5761591 clauses, 17114087 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 176065 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  176065  5761590         0       0      0     0    0     0  166   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 1440397 based on 5761590 irredundant clauses
c [card-1] found 2 at-most-one constraints of average size 3.0
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 1440397 for elimination
c [card-1] 2 out of 2 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 15 variables
c [simpleprobe-1] all 176051 free variables schedulable
c [simpleprobe-1] boosting simple probing limit by 10
c [simpleprobe-1] limit 11520314 based on 5760157 irredundant clauses
c [simpleprobe-1] 155283 variables remain 88% (20768 retained 12%)
c [simpleprobe-1] removed 0 variables, found 4180 hbrs, 0 units
c [unhide-1] limit 360009 based on 5760157 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 176051 variables 100%
c [elim-1] limit of 5760157 steps based on 5760157 irredundant clauses
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 171945 not tried 98% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 4092 = 2% variables out of 176051 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 5750533 negative 100.0% of 5751973 except 1440 0.0%
c [phase-count-1] 779389 positive 13.5% of 5751973 except 4972584 86.5%
c [phase-count-1] less non-negative clauses 1440 than limit 575100 (10.0%)
c [phase-count-1] non-pos/non-neg = 4972584/1440 = 3453.18 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 171959 negative 100%
c [sort-queue-1] sorted 171959 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 171959 (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 4092 variables 2.3% (171959 remain 98%)
c [simplification-1] removed 9617 irredundant clauses 0.2% (5751973 remain 100%)
c [simplification-1] maximum reduction of 2% = max (2%, 0%)
c [simplification-1] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-1] new conflict interval 6666
c [simplification-1] penalized conflict interval 6666 = 1 * 6666
c [simplification-1] hard conflict limit 16666 (soft 6666 + delta 10000)
c [simplification-1] new conflict limit 6666 (hard 16666)
c 
c [simplification-2] limit of 100 binary hit after 100 binaries
c [treelook-1] limit 1437993 based on 5751973 irredundant clauses
c [treelook-1] scheduled 101318 literals 29%
c [treelook-1] scheduling used 1438041 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 1437993 based on 5751973 irredundant clauses
c [treelook-1] used 1770550 steps
c [treelook-1] 101295 literals remain 29%
c [treelook-1] 95240 variables remain to probed next time 55%
c [treelook-1] removed 0 variables, found 14 hbrs
c [basicprobe-1] limit 46015784 based on 5751973 irredundant clauses
c [basicprobe-1-0] 87889 probes remain 51% after last round
c [basicprobe-1-0] 83 units = 83 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 83 variables, found 41044 hbrs
c [elim-2] 171862 variables 100% will be scheduled this time
c [elim-2] scheduled 171862 variables 100%
c [elim-2] limit of 5732773 steps based on 5732773 irredundant clauses
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 166635 not tried 97% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 5227 = 3% variables out of 171862 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 157502 enqueued variables after 1179 conflicts
c [score-dist-2] active 9147 (5%), one 0 (0%), zero 157502 (95%)
c [score-dist-2] max exp 512, different 9 (2%)
c [score-dist-2] median active exp 509, avg 509.3
c [simplification-2] removed 5310 variables 3.1% (166649 remain 95%)
c [simplification-2] removed 29708 irredundant clauses 0.5% (5722265 remain 99%)
c [simplification-2] maximum reduction of 3% = max (3%, 1%)
c [simplification-2] forced so keeping old conflict interval 6666
c [simplification-2] conflict limit remains at 6666 (hard 16666)
c [simplification-2] new binary interval 1000
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   25.1  166648  5722265      5288    4091    404 40664   33   384  188   8%     64  364   34    4  959%
c i   25.4  166647  5722265      5523    4266    414 40682   33   374  188   9%     51  353   44    4 1179%
c i   26.2  166646  5722265      5987    4707    421 40686   35   398  188   9%     33  374   42    4 1044%
c i   26.2  166645  5722265      5989    4707    421 40687   35   398  188   9%     33  374   42    4 1036%
c i   26.2  166644  5722265      5991    4707    421 40688   35   398  188   9%     32  374   42    4 1028%
c i   26.2  166643  5722265      5993    4707    421 40689   35   398  188   9%     32  373   41    4 1020%
c i   26.2  166642  5722265      5994    4707    421 40689   35   398  188   9%     32  373   41    4 1016%
c 
c [simplification-3] limit 6691 conflicts (hard 16666) hit after 6693 conflicts
c [card-2] limit 1430566 based on 5722265 irredundant clauses
c [card-2] found 2 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1430566 for elimination
c [card-2] 2 out of 2 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-5] removed 3372 variables
c [simpleprobe-2] 144053 schedulable variables 88%
c [simpleprobe-2] limit 11354848 based on 5677424 irredundant clauses
c [simpleprobe-2] 144501 variables remain 89% (18776 retained 11%)
c [simpleprobe-2] removed 0 variables, found 3277 hbrs, 0 units
c [unhide-2] limit 354839 based on 5677424 irredundant clauses
c [unhide-2-2] 0 units, 1 failed, 86 tauts, 0 hbrs, 7317 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 163276 variables 100%
c [elim-3] limit of 9415792 steps penalty 3 = 0 + 3
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 156207 not tried 96% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 7069 = 4% variables out of 163276 scheduled
c [elim-3] considered successful since not run to completion yet
c [sort-queue-3] sorted 109828 enqueued variables after 6693 conflicts
c [score-dist-3] active 46379 (30%), one 0 (0%), zero 109828 (70%)
c [score-dist-3] max exp 514, different 11 (2%)
c [score-dist-3] median active exp 513, avg 512.8
c [simplification-3] removed 10209 variables 6.1% (156207 remain 89%)
c [simplification-3] removed 59399 irredundant clauses 1.0% (5662866 remain 98%)
c [simplification-3] maximum reduction of 6% = max (6%, 1%)
c [simplification-3] large reduction 6% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 18693 (soft 8693 + delta 10000)
c [simplification-3] new conflict limit 8693 (hard 18693)
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   34.8  156206  5662866      7093    5577    482 36365   41   402  186  10%     16  372   57    5 1150%
c i   34.8  156205  5662866      7103    5575    483 36366   41   402  186  10%     15  371   55    5 1124%
c 
c [simplification-4] limit 8694 conflicts (hard 18693) hit after 8694 conflicts
c [decomp-7] removed 4214 variables
c [unhide-3] limit 350114 based on 5601834 irredundant clauses
c [unhide-3-3] 0 units, 0 failed, 373 tauts, 0 hbrs, 5501 literals
c [elim-4] 151983 variables 100% will be scheduled this time
c [elim-4] scheduled 151983 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 225367725 steps penalty 3 = 0 + 3
c [elim-4] rescheduling of touched variables disabled
c [elim-4] incomplete 90791 not tried 60% in round 1
c [elim-4] transition to [ all 0 rem 1 ] state
c [elim-4] eliminated 54280 = 36% variables out of 151983 scheduled
c [elim-4] considered successful since not run to completion yet
c [sort-queue-4] sorted 75576 enqueued variables after 8694 conflicts
c [score-dist-4] active 22137 (23%), one 0 (0%), zero 75576 (77%)
c [score-dist-4] max exp 515, different 12 (2%)
c [score-dist-4] median active exp 514, avg 513.3
c [simplification-4] removed 58204 variables 37.3% (97713 remain 55%)
c [simplification-4] removed 171550 irredundant clauses 3.0% (5491316 remain 95%)
c [simplification-4] maximum reduction of 37% = max (37%, 3%)
c [simplification-4] large reduction 37% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 20694 (soft 10694 + delta 10000)
c [simplification-4] new conflict limit 10694 (hard 20694)
c 
c [simplification-5] limit 10694 conflicts (hard 20694) hit after 10694 conflicts
c [quatres-1] found 24439 quaternary clauses 11% in total
c [quatres-1-2] added 1747 quaternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 21965264 based on 5491316 irredundant clauses
c [ternres-1] all 97713 free variables schedulable
c [ternres-1] 1996 ternary resolvents (0 bin, 1996 trn)
c [ternres-1] 8632 variables remain 9% (89081 retained 91%)
c [gauss-1] limit 2745658 based on 5491316 irredundant clauses
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 1372829 based on 5491316 irredundant clauses
c [treelook-2] scheduled 89592 literals 46%
c [treelook-2] scheduling used 1372983 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 1372829 based on 5491316 irredundant clauses
c [treelook-2] used 1444491 steps
c [treelook-2] 89580 literals remain 46%
c [treelook-2] 80573 variables remain to probed next time 82%
c [treelook-2] removed 0 variables, found 126 hbrs
c [transred-1] limit 5491316 based on 5491316 irredundant clauses
c [transred-1] removed 0 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 97713 variables 100%
c [block-1] boosting limit by 10
c [block-1] limit of 65019566 steps penalty 3 = 0 + 3
c [block-1] incomplete 13225 not tried 14%
c [block-1] transition to [ all 1 rem 1 ] state
c [block-1] eliminated 101972 blocked clauses
c [block-1] considered successful since not run to completion yet
c [cce-1] limit of 5389344 steps based on 5389344 irredundant clauses
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] allowing another 2694897 steps for small clauses
c [cce-1-1] scheduling 5137011 clauses = 5136360 binary + 651 ternary
c [cce-1-1] tried to eliminate 23 small clauses 0%
c [cce-1-1] eliminated 1 binary clauses 0%
c [cce-1-1] eliminated 1 small clauses 0%
c [cce-1-1] eliminated 1 small clauses in 5398499 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 1 covered clauses in round 1
c [cce-1] eliminated 1 covered clauses in TOTAL during 1 rounds
c [cce-1] 1 < 1/100 * 5389344 = 53893 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 96429 variables 100%
c [elim-5] limit of 13003913 steps penalty 3 = 0 + 3
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 87594 not tried 91% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 1393 = 1% variables out of 96429 scheduled
c [bca-1] limit of 10000000 steps and 10775288 added (scaled 2)
c [bca-1] 171613 out of 190074 literals actually usable 90%
c [bca-1] added 275 blocked clauses in 540502 steps
c [sweep-1] limit 10774788 based on 5387394 irredundant clauses
c [sweep-1-1] 1942 pos 2.0% + 93094 neg 98.0% = 95036 sched 100.0% ret 0
c [sweep-1-1] 10778329 steps 310 queries 3628.35 avg class size
c [sweep-1-1] 9880 decisions 297 SAT calls 270.52 avg env size
c [sweep-1-1] 38779 variables remain 41% (56251 retained 59%)
c [decomp-10] removed 24 variables
c [sweep-1-1] removed 24 vars (0 failed, 18 eqs, 48 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 24 vars in TOTAL (1 rounds, 309 queries)
c [sort-queue-5] sorted 72204 enqueued variables after 10694 conflicts
c [score-dist-5] active 22808 (24%), one 0 (0%), zero 72204 (76%)
c [score-dist-5] max exp 515, different 12 (2%)
c [score-dist-5] median active exp 514, avg 513.8
c [simplification-5] removed 2701 variables 2.8% (95012 remain 54%)
c [simplification-5] removed 106189 irredundant clauses 1.9% (5385127 remain 93%)
c [simplification-5] maximum reduction of 3% = max (3%, 2%)
c [simplification-5] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-5] new conflict interval 11666
c [simplification-5] penalized conflict interval 11666 = 1 * 11666
c [simplification-5] hard conflict limit 32360 (soft 22360 + delta 10000)
c [simplification-5] new conflict limit 22360 (hard 32360)
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   69.2   95011  5385127     11597    9700   3198 22698   45   459  179  10%     50  401   41    8  528%
c i   70.3   95010  5385127     13125   10736   3410 22774   44   406  179  11%     18  339   38    8  452%
c i   70.7   94883  5385127     13679   11206   3439 22796   43   413  179  10%     10  344   38    9  432%
c 
c [simplification-6] limit of 1829 ternary hit after 1829 ternaries
c [quatres-2] found 23732 quaternary clauses 12% in total
c [quatres-2-2] added 153 quaternary resolvents
c [ternres-2] limit 21540508 based on 5385127 irredundant clauses
c [ternres-2] 8343 schedulable variables 9%
c [ternres-2] 743 ternary resolvents (0 bin, 743 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 1346281 based on 5385127 irredundant clauses
c [card-3] found 1 at-most-one constraints of average size 4.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1346281 for elimination
c [card-3] 1 out of 1 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 154 variables
c [basicprobe-2] limit 42911104 based on 5363888 irredundant clauses
c [basicprobe-2-0] 76623 probes remain 81% after last round
c [basicprobe-2-0] 154 units = 154 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 240 variables, found 9990 hbrs
c [unhide-4] limit 335243 based on 5363888 irredundant clauses
c [unhide-4-4] 0 units, 0 failed, 142 tauts, 0 hbrs, 48852 literals
c [block-2] 12824 variables 14% will be scheduled this time
c [block-2] scheduled 12824 variables 14%
c [block-2] limit of 8397985 steps penalty 3 = 0 + 3
c [block-2] incomplete 12838 not tried 14%
c [block-2] transition to [ all 0 rem 1 ] state
c [block-2] eliminated 11727 blocked clauses
c [block-2] considered successful since not run to completion yet
c [elim-6] 86955 variables 92% will be scheduled this time
c [elim-6] scheduled 86955 variables 92%
c [elim-6] limit of 16795970 steps penalty 3 = 0 + 3
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 84509 not tried 89% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 1029 = 1% variables out of 86955 scheduled
c [bca-2] limit of 10000000 steps and 10595647 added (scaled 2)
c [bca-2] 163610 out of 186802 literals actually usable 88%
c [bca-2] added 21346 blocked clauses in 547556 steps
c [sweep-2] limit 10595010 based on 5297505 irredundant clauses
c [sweep-2-1] 1029 pos 2.7% + 36524 neg 97.3% = 37553 sched 40.2% ret 55847
c [sweep-2-1] 10598680 steps 382 queries 2512.06 avg class size
c [sweep-2-1] 13571 decisions 377 SAT calls 255.19 avg env size
c [sweep-2-1] 19819 variables remain 21% (73556 retained 79%)
c [decomp-12] removed 68 variables
c [sweep-2-1] removed 68 vars (0 failed, 7 eqs, 24 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 68 vars in TOTAL (1 rounds, 381 queries)
c [sort-queue-6] sorted 66836 enqueued variables after 18877 conflicts
c [score-dist-6] active 26496 (28%), one 0 (0%), zero 66836 (72%)
c [score-dist-6] max exp 516, different 13 (3%)
c [score-dist-6] median active exp 515, avg 514.6
c [simplification-6] removed 1551 variables 1.6% (93332 remain 53%)
c [simplification-6] removed 101848 irredundant clauses 1.9% (5283279 remain 92%)
c [simplification-6] maximum reduction of 2% = max (2%, 2%)
c [simplification-6] forced so keeping old conflict interval 11666
c [simplification-6] conflict limit remains at 22360 (hard 32360)
c [simplification-6] new ternary interval 10000
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   87.3   93331  5283279     19703   15436   4335 54430   41   380  180  11%     70  283   34   12  292%
c i   89.5   93187  5283279     21967   17222   4546 54508   43   421  180  10%     20  315   40   13  316%
c 
c [simplification-7] limit 22360 conflicts (hard 32360) hit after 22361 conflicts
c [quatres-3] found 23384 quaternary clauses 13% in total
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [quatres-3-2] added 580 quaternary resolvents
c [ternres-3] limit 21133116 based on 5283279 irredundant clauses
c [ternres-3] all 93187 free variables schedulable
c [ternres-3] 174 ternary resolvents (0 bin, 174 trn)
c [ternres-3] 19628 variables remain 21% (73559 retained 79%)
c [gauss-2] limit 2641639 based on 5283279 irredundant clauses
c [gauss-2] extracted 1 xors of average arity 2.0
c [gauss-2] connected 2 occurrences of 2 variables (average 1.0)
c [gauss-2] limit 2629168 based on 5258337 irredundant clauses
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-13] removed 45 variables
c [transred-2] limit 5258247 based on 5258247 irredundant clauses
c [transred-2] removed 1 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 93142 variables 100%
c [block-3] limit of 9392004 steps penalty 3 = 0 + 3
c [block-3] incomplete 44538 not tried 48%
c [block-3] transition to [ all 1 rem 1 ] state
c [block-3] eliminated 1306 blocked clauses
c [block-3] considered successful since not run to completion yet
c [cce-2] limit of 5256940 steps based on 5256940 irredundant clauses
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 2628552 steps for small clauses
c [cce-2-1] scheduling 5037285 clauses = 5035096 binary + 2189 ternary
c [cce-2-1] tried to eliminate 17 small clauses 0%
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 0 covered clauses in round 1
c [cce-2] eliminated 0 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 93123 variables 100%
c [elim-7] limit of 18784009 steps penalty 3 = 0 + 3
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 83421 not tried 90% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 813 = 1% variables out of 93123 scheduled
c [elim-7] 813 < 1/100 * 93123 = 931 considered unsuccessful
c [bca-3] limit of 10000000 steps and 10521850 added (scaled 2)
c [bca-3] 158598 out of 184622 literals actually usable 86%
c [bca-3] added 17 blocked clauses in 530990 steps
c [sweep-3] limit 10510540 based on 5255270 irredundant clauses
c [sweep-3-1] 636 pos 3.4% + 18292 neg 96.6% = 18928 sched 20.5% ret 73382
c [sweep-3-1] 10524435 steps 358 queries 1809.58 avg class size
c [sweep-3-1] 14153 decisions 351 SAT calls 208.26 avg env size
c [sweep-3-1] 13326 variables remain 14% (78669 retained 86%)
c [decomp-14] removed 444 variables
c [sweep-3-1] removed 444 vars (0 failed, 11 eqs, 21 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 444 vars in TOTAL (1 rounds, 357 queries)
c [sort-queue-7] sorted 63742 enqueued variables after 22361 conflicts
c [score-dist-7] active 28124 (31%), one 0 (0%), zero 63742 (69%)
c [score-dist-7] max exp 516, different 13 (3%)
c [score-dist-7] median active exp 515, avg 515.0
c [simplification-7] removed 1321 variables 1.4% (91866 remain 52%)
c [simplification-7] removed 99074 irredundant clauses 1.9% (5184205 remain 90%)
c [simplification-7] maximum reduction of 2% = max (1%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 18332
c [simplification-7] penalized conflict interval 18332 = 1 * 18332
c [simplification-7] hard conflict limit 50693 (soft 40693 + delta 10000)
c [simplification-7] new conflict limit 40693 (hard 50693)
c 
c [simplification-8] limit 40693 conflicts (hard 50693) hit after 40693 conflicts
c [quatres-4] found 21905 quaternary clauses 13% in total
c [quatres-4-2] added 5 single-self-subsuming ternary resolvents
c [quatres-4-2] added 397 quaternary resolvents
c [ternres-4] limit 20736820 based on 5184205 irredundant clauses
c [ternres-4] 19343 schedulable variables 21%
c [ternres-4] 765 ternary resolvents (0 bin, 765 trn)
c [ternres-4] fully completed ternary resolution
c [transred-3] limit 5184205 based on 5184205 irredundant clauses
c [transred-3] removed 2 transitive binary clauses
c [block-4] 12388 variables 13% will be scheduled this time
c [block-4] scheduled 12388 variables 13%
c [block-4] limit of 14614582 steps penalty 3 = 0 + 3
c [block-4] incomplete 12393 not tried 13%
c [block-4] transition to [ all 0 rem 1 ] state
c [block-4] eliminated 30254 blocked clauses
c [block-4] considered successful since not run to completion yet
c [bca-4] limit of 10000000 steps and 10319217 added (scaled 2)
c [bca-4] 146009 out of 182802 literals actually usable 80%
c [bca-4] added 18 blocked clauses in 495725 steps
c [sweep-4] limit 10307898 based on 5153949 irredundant clauses
c [sweep-4-1] 633 pos 4.8% + 12591 neg 95.2% = 13224 sched 14.5% ret 78176
c [sweep-4-1] 10318441 steps 315 queries 1867.44 avg class size
c [sweep-4-1] 14983 decisions 301 SAT calls 308.21 avg env size
c [sweep-4-1] 10932 variables remain 12% (79434 retained 88%)
c [decomp-16] removed 1686 variables
c [sweep-4-1] removed 1686 vars (0 failed, 19 eqs, 34 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 1686 vars in TOTAL (1 rounds, 314 queries)
c [sort-queue-8] sorted 53706 enqueued variables after 40693 conflicts
c [score-dist-8] active 36008 (40%), one 0 (0%), zero 53706 (60%)
c [score-dist-8] max exp 517, different 14 (3%)
c [score-dist-8] median active exp 516, avg 515.9
c [simplification-8] removed 2152 variables 2.3% (89714 remain 51%)
c [simplification-8] removed 238976 irredundant clauses 4.6% (4945229 remain 86%)
c [simplification-8] maximum reduction of 5% = max (2%, 5%)
c [simplification-8] large reduction 5% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 52693 (soft 42693 + delta 10000)
c [simplification-8] new conflict limit 42693 (hard 52693)
c 
c [simplification-9] limit 42693 conflicts (hard 52693) hit after 42693 conflicts
c [quatres-5] found 19128 quaternary clauses 13% in total
c [quatres-5-2] added 122 single-self-subsuming ternary resolvents
c [quatres-5-2] added 785 quaternary resolvents
c [ternres-5] limit 19780908 based on 4945227 irredundant clauses
c [ternres-5] all 89714 free variables schedulable
c [ternres-5] 596 ternary resolvents (0 bin, 596 trn)
c [ternres-5] 27334 variables remain 30% (62380 retained 70%)
c [simpleprobe-3] 79792 schedulable variables 89%
c [simpleprobe-3] limit 9890454 based on 4945227 irredundant clauses
c [simpleprobe-3] 80086 variables remain 89% (9628 retained 11%)
c [simpleprobe-3] removed 0 variables, found 2532 hbrs, 0 units
c [unhide-5] limit 309076 based on 4945227 irredundant clauses
c [unhide-5-5] 0 units, 0 failed, 5901 tauts, 0 hbrs, 3556 literals
c [transred-4] limit 4935803 based on 4935803 irredundant clauses
c [transred-4] removed 2 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 89714 variables 100%
c [block-5] limit of 29901443 steps penalty 2 = 0 + 2
c [block-5] incomplete 16421 not tried 18%
c [block-5] transition to [ all 1 rem 1 ] state
c [block-5] eliminated 36170 blocked clauses
c [block-5] considered successful since not run to completion yet
c [elim-8] 80385 variables 90% will be scheduled this time
c [elim-8] scheduled 80385 variables 90%
c [elim-8] boosting limit by 20
c [elim-8] limit of 598028872 steps penalty 3 = 1 + 2
c [elim-8] rescheduling of touched variables disabled
c [elim-8] incomplete 18549 not tried 21% in round 1
c [elim-8] transition to [ all 0 rem 1 ] state
c [elim-8] eliminated 5515 = 7% variables out of 80385 scheduled
c [bca-5] limit of 10000000 steps and 9740096 added (scaled 2)
c [bca-5] 135927 out of 167376 literals actually usable 81%
c [bca-5] added 883 blocked clauses in 442052 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 9728768 based on 4864384 irredundant clauses
c [sweep-5-1] 289 pos 4.2% + 6576 neg 95.8% = 6865 sched 8.2% ret 76822
c [sweep-5-1] 9739750 steps 469 queries 975.38 avg class size
c [sweep-5-1] 24948 decisions 443 SAT calls 306.12 avg env size
c [sweep-5-1] 4728 variables remain 6% (78581 retained 94%)
c [decomp-19] removed 549 variables
c [sweep-5-1] removed 549 vars (0 failed, 25 eqs, 33 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 549 vars in TOTAL (1 rounds, 468 queries)
c [sort-queue-9] sorted 50154 enqueued variables after 42693 conflicts
c [score-dist-9] active 32984 (40%), one 0 (0%), zero 50154 (60%)
c [score-dist-9] max exp 517, different 14 (3%)
c [score-dist-9] median active exp 516, avg 516.0
c [simplification-9] removed 6576 variables 7.3% (83138 remain 47%)
c [simplification-9] removed 164958 irredundant clauses 3.3% (4780271 remain 83%)
c [simplification-9] maximum reduction of 7% = max (7%, 3%)
c [simplification-9] large reduction 7% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 54693 (soft 44693 + delta 10000)
c [simplification-9] new conflict limit 44693 (hard 54693)
c 
c [simplification-10] limit 44693 conflicts (hard 54693) hit after 44693 conflicts
c [quatres-6] found 14650 quaternary clauses 8% in total
c [quatres-6-2] added 107 single-self-subsuming ternary resolvents
c [quatres-6-2] added 1027 quaternary resolvents
c [ternres-6] limit 19121084 based on 4780271 irredundant clauses
c [ternres-6] 25197 schedulable variables 30%
c [ternres-6] 3401 ternary resolvents (0 bin, 3401 trn)
c [ternres-6] 1 variables remain 0% (83137 retained 100%)
c [card-4] limit 1195067 based on 4780271 irredundant clauses
c [card-4] no at-most-one constraint found
c [card-4] no at-most-two constraint found
c [gauss-3] limit 2390135 based on 4780271 irredundant clauses
c [gauss-3] extracted 0 xors of average arity 0.0
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-5] limit 4780271 based on 4780271 irredundant clauses
c [transred-5] removed 1 transitive binary clauses
c [block-6] 11048 variables 13% will be scheduled this time
c [block-6] scheduled 11048 variables 13%
c [block-6] limit of 30708892 steps penalty 2 = 0 + 2
c [block-6] incomplete 11199 not tried 13%
c [block-6] transition to [ all 0 rem 1 ] state
c [block-6] eliminated 72058 blocked clauses
c [block-6] considered successful since not run to completion yet
c [cce-3] limit of 4708212 steps based on 4708212 irredundant clauses
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] allowing another 2355109 steps for small clauses
c [cce-3-1] scheduling 4528464 clauses = 4510470 binary + 17994 ternary
c [cce-3-1] tried to eliminate 4 small clauses 0%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 1 small clauses 0%
c [cce-3-1] eliminated 1 small clauses in 4708547 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1 covered clauses in round 1
c [cce-3] eliminated 1 covered clauses in TOTAL during 1 rounds
c [cce-3] 1 < 1/100 * 4708212 = 47082 considered unsuccessful
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 81948 variables 100%
c [elim-9] limit of 61417784 steps penalty 2 = 0 + 2
c [elim-9] rescheduling of touched variables disabled
c [elim-9] incomplete 69024 not tried 84% in round 1
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 1131 = 1% variables out of 81948 scheduled
c [bca-6] limit of 10000000 steps and 9423565 added (scaled 2)
c [bca-6] 129228 out of 161636 literals actually usable 80%
c [bca-6] added 30853 blocked clauses in 495480 steps
c [sweep-6] limit 9411796 based on 4705898 irredundant clauses
c [sweep-6-1] 196 pos 5.2% + 3574 neg 94.8% = 3770 sched 4.7% ret 77047
c [sweep-6-1] 9473418 steps 327 queries 542.06 avg class size
c [sweep-6-1] 25135 decisions 317 SAT calls 380.87 avg env size
c [sweep-6-1] 2685 variables remain 3% (78132 retained 97%)
c [decomp-21] removed 10 variables
c [sweep-6-1] removed 10 vars (0 failed, 10 eqs, 14 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 10 vars in TOTAL (1 rounds, 326 queries)
c [sort-queue-10] sorted 48546 enqueued variables after 44693 conflicts
c [score-dist-10] active 32261 (40%), one 0 (0%), zero 48546 (60%)
c [score-dist-10] max exp 517, different 14 (3%)
c [score-dist-10] median active exp 516, avg 516.0
c [simplification-10] removed 2331 variables 2.8% (80807 remain 46%)
c [simplification-10] removed 74521 irredundant clauses 1.6% (4705750 remain 82%)
c [simplification-10] maximum reduction of 3% = max (3%, 2%)
c [simplification-10] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-10] new conflict interval 23332
c [simplification-10] penalized conflict interval 23332 = 1 * 23332
c [simplification-10] hard conflict limit 79691 (soft 68025 + delta 11666)
c [simplification-10] new conflict limit 68025 (hard 79691)
c 
c [simplification-11] limit 68025 conflicts (hard 79691) hit after 68026 conflicts
c [quatres-7] found 13539 quaternary clauses 8% in total
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [quatres-7-2] added 315 quaternary resolvents
c [ternres-7] limit 18822996 based on 4705749 irredundant clauses
c [ternres-7] 1 schedulable variables 0%
c [ternres-7] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-7] fully completed ternary resolution
c [transred-6] limit 4705749 based on 4705749 irredundant clauses
c [transred-6] removed 0 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 80807 variables 100%
c [block-7] limit of 43862173 steps penalty 2 = 0 + 2
c [block-7] incomplete 12816 not tried 16%
c [block-7] transition to [ all 1 rem 1 ] state
c [block-7] eliminated 84190 blocked clauses
c [elim-10] 17783 variables 22% will be scheduled this time
c [elim-10] scheduled 17783 variables 22%
c [elim-10] limit of 87724346 steps penalty 2 = 0 + 2
c [elim-10] rescheduling of touched variables disabled
c [elim-10] incomplete 12226 not tried 15% in round 1
c [elim-10] transition to [ all 0 rem 1 ] state
c [elim-10] eliminated 67 = 0% variables out of 17783 scheduled
c [elim-10] 67 < 1/100 * 17783 = 177 considered unsuccessful
c [bca-7] limit of 10000000 steps and 9255526 added (scaled 2)
c [bca-7] 118277 out of 158858 literals actually usable 74%
c [bca-7] added 128 blocked clauses in 404582 steps
c [sweep-7] limit 9228330 based on 4614165 irredundant clauses
c [sweep-7-1] 402 pos 15.0% + 2281 neg 85.0% = 2683 sched 3.4% ret 76745
c [sweep-7-1] 9262849 steps 193 queries 477.61 avg class size
c [sweep-7-1] 13328 decisions 178 SAT calls 318.48 avg env size
c [sweep-7-1] 2176 variables remain 3% (77252 retained 97%)
c [decomp-23] removed 11 variables
c [sweep-7-1] removed 11 vars (0 failed, 15 eqs, 15 impls)
c [sweep-7] 11 < 1/1000 * 79428 = 79 considered unsuccessful
c [sweep-7] removed 11 vars in TOTAL (1 rounds, 192 queries)
c [sort-queue-11] sorted 41587 enqueued variables after 68026 conflicts
c [score-dist-11] active 37830 (48%), one 0 (0%), zero 41587 (52%)
c [score-dist-11] max exp 518, different 14 (3%)
c [score-dist-11] median active exp 517, avg 516.6
c [simplification-11] removed 1390 variables 1.7% (79417 remain 45%)
c [simplification-11] removed 91766 irredundant clauses 2.0% (4613983 remain 80%)
c [simplification-11] maximum reduction of 2% = max (2%, 2%)
c [simplification-11] geometric conflict interval increment 7777 = 23332 / 3
c [simplification-11] new conflict interval 31109
c [simplification-11] penalized conflict interval 31109 = 1 * 31109
c [simplification-11] hard conflict limit 114689 (soft 99135 + delta 15554)
c [simplification-11] new conflict limit 99135 (hard 114689)
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 -  197.8   79417  4613983     71397   18434   9638 35821   57   737  163   8%    530  450   60   33  185%
c 
c [simplification-12] limit 99135 conflicts (hard 114689) hit after 99209 conflicts
c [quatres-8] found 13879 quaternary clauses 8% in total
c [quatres-8-2] added 347 quaternary resolvents
c [treelook-3] limit 1153495 based on 4613983 irredundant clauses
c [treelook-3] scheduled 77275 literals 49%
c [treelook-3] scheduling used 1154018 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 1153495 based on 4613983 irredundant clauses
c [treelook-3] used 1256167 steps
c [treelook-3] 77269 literals remain 49%
c [treelook-3] 69658 variables remain to probed next time 88%
c [block-8] 10677 variables 13% will be scheduled this time
c [block-8] scheduled 10677 variables 13%
c [block-8] limit of 62470162 steps penalty 2 = 0 + 2
c [block-8] incomplete 10178 not tried 13%
c [block-8] transition to [ all 0 rem 1 ] state
c [block-8] eliminated 175273 blocked clauses
c [bca-8] limit of 10000000 steps and 8904680 added (scaled 2)
c [bca-8] 117189 out of 152956 literals actually usable 77%
c [bca-8] added 159 blocked clauses in 394973 steps
c [sort-queue-12] sorted 36037 enqueued variables after 99209 conflicts
c [score-dist-12] active 40440 (53%), one 0 (0%), zero 36037 (47%)
c [score-dist-12] max exp 518, different 14 (3%)
c [score-dist-12] median active exp 517, avg 517.0
c [simplification-12] removed 2940 variables 3.7% (76477 remain 43%)
c [simplification-12] removed 175273 irredundant clauses 3.8% (4438710 remain 77%)
c [simplification-12] maximum reduction of 4% = max (4%, 4%)
c [simplification-12] geometric conflict interval increment 6221 = 31109 / 5
c [simplification-12] new conflict interval 37330
c [simplification-12] penalized conflict interval 37330 = 1 * 37330
c [simplification-12] hard conflict limit 155204 (soft 136539 + delta 18665)
c [simplification-12] new conflict limit 136539 (hard 155204)
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 -  230.3   76477  4438710    118233   25969  10533 35495   47   332  161  14%    782   -8   50   45  110%
c 
c [simplification-13] limit 136539 conflicts (hard 155204) hit after 155206 conflicts
c [quatres-9] found 14262 quaternary clauses 8% in total
c [quatres-9-2] added 2 single-self-subsuming ternary resolvents
c [quatres-9-2] added 214 quaternary resolvents
c [ternres-8] limit 17754840 based on 4438710 irredundant clauses
c [ternres-8] all 76477 free variables schedulable
c [ternres-8] 270 ternary resolvents (0 bin, 270 trn)
c [ternres-8] 38919 variables remain 51% (37558 retained 49%)
c [basicprobe-3] limit 36022417 penalty 2 = 0 + 2
c [basicprobe-3-0] 61131 probes remain 80% after last round
c [basicprobe-3-0] 51 units = 51 failed (100%) + 0 lifted (0%)
c [basicprobe-3-0] removed 51 variables, found 8941 hbrs
c [unhide-6] limit 277419 based on 4438710 irredundant clauses
c [unhide-6-6] 0 units, 0 failed, 934 tauts, 0 hbrs, 93329 literals
c [transred-7] limit 4423493 based on 4423493 irredundant clauses
c [transred-7] removed 0 transitive binary clauses
c [block-9] scheduling all variables this time
c [block-9] scheduled 76426 variables 100%
c [block-9] limit of 72044835 steps penalty 2 = 0 + 2
c [block-9] incomplete 10220 not tried 13%
c [block-9] transition to [ all 1 rem 1 ] state
c [block-9] eliminated 157286 blocked clauses
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 73769 variables 100%
c [elim-11] limit of 72044835 steps penalty 3 = 1 + 2
c [elim-11] rescheduling of touched variables disabled
c [elim-11] incomplete 43083 not tried 58% in round 1
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 179 = 0% variables out of 73769 scheduled
c [elim-11] 179 < 1/100 * 73769 = 737 considered unsuccessful
c [bca-9] limit of 10000000 steps and 8559031 added (scaled 2)
c [bca-9] 108406 out of 147182 literals actually usable 74%
c [bca-9] added 264 blocked clauses in 387659 steps
c [sweep-8] limit 8531692 based on 4265846 irredundant clauses
c [sweep-8-1] 148 pos 7.0% + 1968 neg 93.0% = 2116 sched 2.9% ret 71474
c [sweep-8-1] 8588954 steps 233 queries 390.38 avg class size
c [sweep-8-1] 20126 decisions 230 SAT calls 395.45 avg env size
c [sweep-8-1] 1540 variables remain 2% (72050 retained 98%)
c [decomp-26] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 2 eqs, 4 impls)
c [sweep-8] 2 < 1/1000 * 73590 = 73 considered unsuccessful
c [sweep-8] removed 2 vars in TOTAL (1 rounds, 232 queries)
c [sort-queue-13] sorted 30510 enqueued variables after 155206 conflicts
c [score-dist-13] active 43078 (59%), one 0 (0%), zero 30510 (41%)
c [score-dist-13] max exp 519, different 14 (3%)
c [score-dist-13] median active exp 518, avg 517.5
c [simplification-13] removed 2889 variables 3.8% (73588 remain 42%)
c [simplification-13] removed 172864 irredundant clauses 3.9% (4265846 remain 74%)
c [simplification-13] maximum reduction of 4% = max (4%, 4%)
c [simplification-13] geometric conflict interval increment 7466 = 37330 / 5
c [simplification-13] new conflict interval 44796
c [simplification-13] penalized conflict interval 44796 = 1 * 44796
c [simplification-13] hard conflict limit 222400 (soft 200002 + delta 22398)
c [simplification-13] new conflict limit 200002 (hard 222400)
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 -  256.8   73588  4265846    162131   29320  11182 42100   38   270  159  14%    900  -23   48   41  116%
c -  266.4   73588  4265845    199074   28707  11697 42564   37   211  159  17%    954  -67   46   40  116%
c 
c [simplification-14] limit 200002 conflicts (hard 222400) hit after 221594 conflicts
c [quatres-10] found 14888 quaternary clauses 9% in total
c [quatres-10-2] added 377 single-self-subsuming ternary resolvents
c [quatres-10-2] added 273 quaternary resolvents
c [ternres-9] limit 17063380 based on 4265845 irredundant clauses
c [ternres-9] 37444 schedulable variables 51%
c [ternres-9] 398 ternary resolvents (3 bin, 395 trn)
c [ternres-9] 1 variables remain 0% (73587 retained 100%)
c [gauss-4] limit 2132922 based on 4265845 irredundant clauses
c [gauss-4] extracted 0 xors of average arity 0.0
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-27] removed 1 variables
c [block-10] 9209 variables 13% will be scheduled this time
c [block-10] scheduled 9209 variables 13%
c [block-10] limit of 82195351 steps penalty 2 = 0 + 2
c [block-10] incomplete 7942 not tried 11%
c [block-10] transition to [ all 0 rem 1 ] state
c [block-10] eliminated 269263 blocked clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 51372094 steps penalty 5 = 3 + 2
c [cce-4-1] eliminated 3 clauses out of 5 (60%) of length 351
c [cce-4-1] eliminated 2 clauses out of 4 (50%) of length 350
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 349
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 6 large clauses in 51374706 steps
c [cce-4-1] allowing another 25687353 steps for small clauses
c [cce-4-1] scheduling 3821188 clauses = 3814975 binary + 6213 ternary
c [cce-4-1] tried to eliminate 252 small clauses 0%
c [cce-4-1] eliminated 14 binary clauses 0%
c [cce-4-1] eliminated 14 small clauses 0%
c [cce-4-1] eliminated 14 small clauses in 51372813 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 20 covered clauses in round 1
c [cce-4] eliminated 20 covered clauses in TOTAL during 1 rounds
c [cce-4] 20 < 1/100 * 3996582 = 39965 considered unsuccessful
c [bca-10] limit of 10000000 steps and 8020595 added (scaled 2)
c [bca-10] 98867 out of 138314 literals actually usable 71%
c [bca-10] added 9 blocked clauses in 366696 steps
c [sort-queue-14] sorted 21850 enqueued variables after 221594 conflicts
c [score-dist-14] active 47306 (68%), one 0 (0%), zero 21850 (32%)
c [score-dist-14] max exp 519, different 13 (2%)
c [score-dist-14] median active exp 518, avg 517.9
c [simplification-14] removed 4432 variables 6.0% (69156 remain 39%)
c [simplification-14] removed 269283 irredundant clauses 6.3% (3996562 remain 69%)
c [simplification-14] maximum reduction of 6% = max (6%, 6%)
c [simplification-14] large reduction 6% >= 5% limit
c [simplification-14] next conflict interval 2215 = min (221594/100, 44796)
c [simplification-14] penalized conflict interval 2215 = 1 * 2215
c [simplification-14] hard conflict limit 233809 (soft 223809 + delta 10000)
c [simplification-14] new conflict limit 223809 (hard 233809)
c 
c [simplification-15] limit 223809 conflicts (hard 233809) hit after 233810 conflicts
c [quatres-11] found 14733 quaternary clauses 9% in total
c [quatres-11-1] added 2 double-self-subsuming ternary resolvents
c [quatres-11-2] added 4 single-self-subsuming ternary resolvents
c [quatres-11-2] added 111 quaternary resolvents
c [ternres-10] limit 15986240 based on 3996560 irredundant clauses
c [ternres-10] 1 schedulable variables 0%
c [ternres-10] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 999140 based on 3996560 irredundant clauses
c [card-5] found 1 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 999140 for elimination
c [card-5] 1 out of 1 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [block-11] scheduling all variables this time
c [block-11] scheduled 69156 variables 100%
c [block-11] limit of 83802614 steps penalty 2 = 0 + 2
c [block-11] incomplete 5598 not tried 8%
c [block-11] transition to [ all 1 rem 1 ] state
c [block-11] eliminated 286497 blocked clauses
c [bca-11] limit of 10000000 steps and 7447602 added (scaled 2)
c [bca-11] 94364 out of 136002 literals actually usable 69%
c [bca-11] added 12426 blocked clauses in 383120 steps
c [sort-queue-15] sorted 20212 enqueued variables after 233810 conflicts
c [score-dist-15] active 47788 (70%), one 0 (0%), zero 20212 (30%)
c [score-dist-15] max exp 519, different 13 (2%)
c [score-dist-15] median active exp 518, avg 518.0
c [simplification-15] removed 1156 variables 1.7% (68000 remain 39%)
c [simplification-15] removed 286497 irredundant clauses 7.2% (3710063 remain 64%)
c [simplification-15] maximum reduction of 7% = max (2%, 7%)
c [simplification-15] large reduction 7% >= 5% limit
c [simplification-15] next conflict interval 2338 = min (233810/100, 44796)
c [simplification-15] penalized conflict interval 2338 = 1 * 2338
c [simplification-15] hard conflict limit 246148 (soft 236148 + delta 10000)
c [simplification-15] new conflict limit 236148 (hard 246148)
c 
c [simplification-16] limit 236148 conflicts (hard 246148) hit after 236166 conflicts
c [quatres-12] found 14684 quaternary clauses 9% in total
c [quatres-12-2] added 1 single-self-subsuming ternary resolvents
c [quatres-12-2] added 89 quaternary resolvents
c [transred-8] limit 3710063 based on 3710063 irredundant clauses
c [transred-8] removed 3 transitive binary clauses
c [block-12] 5590 variables 8% will be scheduled this time
c [block-12] scheduled 5590 variables 8%
c [block-12] limit of 84257301 steps penalty 2 = 0 + 2
c [block-12] fully completed
c [block-12] transition to [ all 0 rem 0 ] state
c [block-12] eliminated 163294 blocked clauses
c [elim-12] 10498 variables 16% will be scheduled this time
c [elim-12] scheduled 10498 variables 16%
c [elim-12] limit of 42128650 steps penalty 4 = 2 + 2
c [elim-12] rescheduling of touched variables disabled
c [elim-12] incomplete 8155 not tried 12% in round 1
c [elim-12] transition to [ all 0 rem 1 ] state
c [elim-12] eliminated 488 = 5% variables out of 10498 scheduled
c [elim-12] 488 < 1/100 * 10498 = 104 considered unsuccessful
c [bca-12] limit of 10000000 steps and 7126005 added (scaled 2)
c [bca-12] 92272 out of 134240 literals actually usable 69%
c [bca-12] added 4470 blocked clauses in 401403 steps
c [sweep-9] limit 7092316 based on 3546158 irredundant clauses
c [sweep-9-1] 116 pos 7.6% + 1420 neg 92.4% = 1536 sched 2.3% ret 65583
c [sweep-9-1] 7100190 steps 200 queries 275.31 avg class size
c [sweep-9-1] 15325 decisions 183 SAT calls 359.35 avg env size
c [sweep-9-1] 1099 variables remain 2% (66020 retained 98%)
c [decomp-30] removed 12 variables
c [sweep-9-1] removed 12 vars (0 failed, 17 eqs, 17 impls)
c [sweep-9] 12 < 1/1000 * 67119 = 67 considered unsuccessful
c [sweep-9] removed 12 vars in TOTAL (1 rounds, 199 queries)
c [sort-queue-16] sorted 19342 enqueued variables after 236166 conflicts
c [score-dist-16] active 47765 (71%), one 0 (0%), zero 19342 (29%)
c [score-dist-16] max exp 519, different 13 (2%)
c [score-dist-16] median active exp 519, avg 518.0
c [simplification-16] removed 893 variables 1.3% (67107 remain 38%)
c [simplification-16] removed 163919 irredundant clauses 4.4% (3546144 remain 62%)
c [simplification-16] maximum reduction of 4% = max (1%, 4%)
c [simplification-16] geometric conflict interval increment 8959 = 44796 / 5
c [simplification-16] new conflict interval 53755
c [simplification-16] penalized conflict interval 53755 = 1 * 53755
c [simplification-16] hard conflict limit 316798 (soft 289921 + delta 26877)
c [simplification-16] new conflict limit 289921 (hard 316798)
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 -  309.5   67107  3546144    240017   31033  13000 222614   41   400  154  10%    986  147   54   38  143%
c -  321.8   67107  3546142    280274   32291  13710 222961   27   173  154  16%   1004  -88   16   37   43%
c 
c [simplification-17] limit 289921 conflicts (hard 316798) hit after 290743 conflicts
c [quatres-13] found 14928 quaternary clauses 9% in total
c [quatres-13-2] added 5 single-self-subsuming ternary resolvents
c [quatres-13-2] added 151 quaternary resolvents
c [ternres-11] limit 14184568 based on 3546142 irredundant clauses
c [ternres-11] all 67107 free variables schedulable
c [ternres-11] 20 ternary resolvents (0 bin, 20 trn)
c [ternres-11] 38013 variables remain 57% (29094 retained 43%)
c [simpleprobe-4] 60002 schedulable variables 89%
c [simpleprobe-4] limit 7092284 based on 3546142 irredundant clauses
c [simpleprobe-4] 60298 variables remain 90% (6809 retained 10%)
c [simpleprobe-4] removed 0 variables, found 3215 hbrs, 0 units
c [block-13] scheduling all variables this time
c [block-13] scheduled 67107 variables 100%
c [block-13] limit of 94881095 steps penalty 2 = 0 + 2
c [block-13] fully completed
c [block-13] transition to [ all 0 rem 0 ] state
c [block-13] eliminated 286 blocked clauses
c [block-13] 286 < 1/100 * 3546142 = 35461 considered unsuccessful
c [bca-13] limit of 10000000 steps and 7127636 added (scaled 2)
c [bca-13] 92635 out of 134216 literals actually usable 69%
c [bca-13] added 2 blocked clauses in 393622 steps
c [sort-queue-17] sorted 16566 enqueued variables after 290743 conflicts
c [score-dist-17] active 50541 (75%), one 0 (0%), zero 16566 (25%)
c [score-dist-17] max exp 520, different 14 (3%)
c [score-dist-17] median active exp 519, avg 518.4
c [simplification-17] removed 0 variables 0.0% (67107 remain 38%)
c [simplification-17] removed 286 irredundant clauses 0.0% (3545856 remain 62%)
c [simplification-17] maximum reduction of 0% = max (0%, 0%)
c [simplification-17] full geometric conflict interval increment 53755
c [simplification-17] new conflict interval 107510
c [simplification-17] penalized conflict interval 107510 = 1 * 107510
c [simplification-17] hard conflict limit 452008 (soft 398253 + delta 53755)
c [simplification-17] new conflict limit 398253 (hard 452008)
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 -  350.1   67107  3545851    322376   34342  14468 226737   34   287  154  12%   1013   36   30   34   88%
c i  356.6   67106  3545851    352923   59870  14677 226758   14    22  161  63%   1017 -167    8   28   29%
c -  360.8   67106  3545851    363179   35815  14815 226960   26   228  154  11%  -3474   37   33   28  116%
c i  360.8   67105  3545851    363202   35835  14816 226960   26   228  156  11%  -3472   37   33   28  117%
c -  384.9   67105  3545851    404880   35303  15693 227423   61   297  155  20%  -1443   26   47   41  116%
c 
c [simplification-18] limit 398253 conflicts (hard 452008) hit after 452008 conflicts
c [quatres-14] found 14884 quaternary clauses 10% in total
c [quatres-14-1] added 1 double-self-subsuming ternary resolvents
c [quatres-14-2] added 3 single-self-subsuming ternary resolvents
c [quatres-14-2] added 331 quaternary resolvents
c [ternres-12] limit 14183404 based on 3545851 irredundant clauses
c [ternres-12] 38011 schedulable variables 57%
c [ternres-12] 53 ternary resolvents (0 bin, 53 trn)
c [ternres-12] 10506 variables remain 16% (56599 retained 84%)
c [decomp-33] removed 3 variables
c [unhide-7] limit 221419 based on 3542708 irredundant clauses
c [unhide-7-7] 0 units, 0 failed, 21442 tauts, 0 hbrs, 4866 literals
c [transred-9] limit 3520018 based on 3520018 irredundant clauses
c [transred-9] removed 6 transitive binary clauses
c [bca-14] limit of 10000000 steps and 7075959 added (scaled 2)
c [bca-14] 91811 out of 134210 literals actually usable 68%
c [bca-14] added 3 blocked clauses in 398334 steps
c [sort-queue-18] sorted 13550 enqueued variables after 452008 conflicts
c [score-dist-18] active 53554 (80%), one 0 (0%), zero 13550 (20%)
c [score-dist-18] max exp 520, different 13 (2%)
c [score-dist-18] median active exp 520, avg 519.2
c [simplification-18] removed 1 variables 0.0% (67104 remain 38%)
c [simplification-18] removed 25834 irredundant clauses 0.7% (3520017 remain 61%)
c [simplification-18] maximum reduction of 1% = max (0%, 1%)
c [simplification-18] geometric conflict interval increment 53755 = 107510 / 2
c [simplification-18] new conflict interval 161265
c [simplification-18] penalized conflict interval 161265 = 1 * 161265
c [simplification-18] hard conflict limit 693905 (soft 613273 + delta 80632)
c [simplification-18] new conflict limit 613273 (hard 693905)
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 -  401.9   67104  3520017    457910   38638  14649 227324   24   129  155  18%    -74  -78   17   36   48%
c i  404.5   67103  3520017    469456   47316  14721 227330   15   102  160  14%    103  -95    8   33   24%
c -  418.6   67095  3520009    502902   39553  15485 227446   23   126  157  18%   -541 -110   16   34   47%
c i  419.5   67094  3520009    506058   41937  15509 227455   19   112  162  17%   -468 -119   12   33   37%
c i  419.5   67092  3520009    506059   41937  15509 227455   19   112  162  17%   -468 -120   12   33   37%
c i  437.7   67090  3520005    543067   71929  16327 227786   19   130  174  15%   -154 -146   10   35   29%
c -  439.7   67090  3520005    549510   40241  16512 227859   27   245  157  11%   -575  -28   26   34   74%
c -  454.8   67090  3520003    598789   43245  17504 228257   24   155  157  15%    269  -94   11   31   35%
c i  455.0   67089  3520003    599921   44146  17513 228264   20   124  161  16%    282 -124    7   30   24%
c i  457.5   67087  3519996    605632   49074  17664 228343   33   289  163  11%   -479   42   38   31  121%
c i  460.2   67086  3519996    615962   57920  17720 228402   31   189  167  17%   -341  -56   35   31  114%
c i  460.6   67085  3519996    617328   58994  17732 228410   31   177  168  17%   -430  -67   33   31  106%
c i  461.9   67084  3519996    621817   62668  17824 228485   29   177  169  17%   -393  -64   25   31   82%
c i  464.3   67083  3519996    631646   71288  17845 228504   20   102  171  19%   -258 -123   14   29   47%
c i  464.3   67082  3519996    631647   71288  17845 228504   20   102  171  19%   -258 -123   14   29   47%
c i  465.8   67081  3519996    637111   75697  17880 228521   20    68  175  30%   -298 -147   18   28   64%
c i  466.0   67080  3519996    637562   75944  17883 228522   20    66  175  30%   -320 -149   14   28   51%
c i  466.0   67079  3519996    637826   76047  17892 228527   19    63  175  31%   -328 -150   15   28   52%
c -  468.4   67079  3519996    644009   44320  18026 228676   27   203  157  13%   -255   -3   40   28  142%
c i  470.0   67078  3519996    648619   48132  18075 228782   25   202  163  13%   -168   -4    7   28   26%
c 
c [simplification-19] limit 613293 conflicts (hard 693905) hit after 667386 conflicts
c [quatres-15] found 11093 quaternary clauses 12% in total
c [quatres-15-1] added 1 double-self-subsuming ternary resolvents
c [quatres-15-2] added 228 single-self-subsuming ternary resolvents
c [quatres-15-2] added 381 quaternary resolvents
c [ternres-13] limit 17399522 with penalty 2 = 0 + 2
c [ternres-13] 10498 schedulable variables 16%
c [ternres-13] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-13] fully completed ternary resolution
c [gauss-5] limit 1759997 based on 3519995 irredundant clauses
c [gauss-5] extracted 0 xors of average arity 0.0
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-34] removed 1 variables
c [transred-10] limit 3468973 based on 3468973 irredundant clauses
c [transred-10] removed 2 transitive binary clauses
c [block-14] scheduling all variables this time
c [block-14] scheduled 67067 variables 100%
c [block-14] limit of 86997612 steps penalty 3 = 1 + 2
c [block-14] fully completed
c [block-14] transition to [ all 0 rem 0 ] state
c [block-14] eliminated 487 blocked clauses
c [block-14] 487 < 1/100 * 3468972 = 34689 considered unsuccessful
c [cce-5] limit of 5437350 steps penalty 6 = 4 + 2
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 386
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 385
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 383
c [cce-5-1] eliminated 4 clauses out of 4 (100%) of length 382
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 380
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 379
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 378
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 377
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 376
c [cce-5-1] eliminated 3 clauses out of 3 (100%) of length 375
c [cce-5-1] eliminated 2 clauses out of 2 (100%) of length 373
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 22 large clauses in 5438017 steps
c [cce-5-1] allowing another 2719008 steps for small clauses
c [cce-5-1] scheduling 3325050 clauses = 3312132 binary + 12918 ternary
c [cce-5-1] tried to eliminate 6 small clauses 0%
c [cce-5-1] eliminated 3 binary clauses 0%
c [cce-5-1] eliminated 3 small clauses 0%
c [cce-5-1] eliminated 3 small clauses in 5437365 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 25 covered clauses in round 1
c [cce-5] eliminated 25 covered clauses in TOTAL during 1 rounds
c [cce-5] 25 < 1/100 * 3468485 = 34684 considered unsuccessful
c [bca-15] limit of 10000000 steps and 6972846 added (scaled 2)
c [bca-15] 87168 out of 134136 literals actually usable 65%
c [bca-15] added 3510 blocked clauses in 374606 steps
c [sort-queue-19] sorted 8841 enqueued variables after 667386 conflicts
c [score-dist-19] active 58226 (87%), one 0 (0%), zero 8841 (13%)
c [score-dist-19] max exp 521, different 14 (3%)
c [score-dist-19] median active exp 521, avg 520.2
c [simplification-19] removed 1 variables 0.0% (67067 remain 38%)
c [simplification-19] removed 51535 irredundant clauses 1.5% (3468460 remain 60%)
c [simplification-19] maximum reduction of 1% = max (0%, 1%)
c [simplification-19] geometric conflict interval increment 80632 = 161265 / 2
c [simplification-19] new conflict interval 241897
c [simplification-19] penalized conflict interval 241897 = 1 * 241897
c [simplification-19] hard conflict limit 1030231 (soft 909283 + delta 120948)
c [simplification-19] new conflict limit 909283 (hard 1030231)
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 -  510.8   67067  3468459    706482   35367  12568 232666   16    50  153  32%    460 -172   14   31   46%
c i  511.7   67066  3468459    710394   38415  12591 232674   13    32  157  40%    493 -180    9   30   31%
c i  511.7   67065  3468459    710395   38415  12591 232674   13    32  157  40%    492 -180    9   30   31%
c -  531.8   67065  3468453    757076   38781  13475 233004   23   131  154  18%    282 -116   18   34   52%
c i  535.8   67064  3468453    775692   54237  13514 233015   14    23  160  58%    466 -177    8   29   28%
c i  541.3   67063  3468452    794682   70499  13617 233178   15    28  162  54%   -169 -148   10   27   37%
c i  541.3   67045  3468452    794683   70499  13617 233178   15    28  162  54%   -170 -148   10   27   37%
c i  544.2   67041  3468452    798573   73692  13738 233270   37   238  163  16%   -378   62   52   28  183%
c -  547.1   67041  3468452    804749   41150  13936 233432   34   243  154  14%   -314   61   29   29  101%
c i  553.5   67040  3468450    823117   55464  14385 233500   18   112  161  16%     13  -77    8   28   29%
c i  553.5   67039  3468450    823118   55464  14385 233500   18   112  161  16%     12  -77    8   28   29%
c 
c [simplification-20] limit of 8328 binary hit after 8610 binaries
c [quatres-16] found 9510 quaternary clauses 9% in total
c [quatres-16-2] added 790 single-self-subsuming ternary resolvents
c [quatres-16-2] added 348 quaternary resolvents
c [ternres-14] limit 21131358 with penalty 2 = 0 + 2
c [ternres-14] all 67039 free variables schedulable
c [ternres-14] 850 ternary resolvents (1 bin, 849 trn)
c [ternres-14] 12795 variables remain 19% (54244 retained 81%)
c [decomp-35] removed 76 variables
c [transred-11] limit 3408742 based on 3408742 irredundant clauses
c [transred-11] removed 4 transitive binary clauses
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 66991 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 3519 variables 5% in round 1 in 979892437 steps
c [elim-13-1] backward subsumption/strengthening limit 979892400
c [elim-13-1-1] backward checking 11238 touched variables 17%
c [elim-13-1-1] incomplete backward checking 11470 remain 102%
c [elim-13-1] subsumed 0 and strengthened 777 clauses in 979892621 steps
c [elim-13-1] rescheduled 2420 variables 4% by backward subsumption
c [elim-13-2] eliminated 5 variables 0% in round 2 in 190869525 steps
c [elim-13-2] backward subsumption/strengthening limit 190869500
c [elim-13-2-1] backward checking 11476 touched variables 17%
c [elim-13-2-1] incomplete backward checking 11476 remain 100%
c [elim-13-2] subsumed 0 and strengthened 66 clauses in 190869754 steps
c [elim-13-2] rescheduled 577 variables 1% by backward subsumption
c [elim-13-3] no variable eliminated in round 3 in 10173892 steps
c [elim-13] fully completed in 3 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 3524 = 5% variables out of 66991 scheduled
c [bca-16] limit of 10000000 steps and 6836735 added (scaled 2)
c [bca-16] 83679 out of 126936 literals actually usable 66%
c [bca-16] added 24686 blocked clauses in 359115 steps
c [sweep-10] limit 6799054 based on 3399527 irredundant clauses
c [sweep-10-1] 220 pos 21.2% + 816 neg 78.8% = 1036 sched 1.6% ret 62431
c [sweep-10-1] 6832759 steps 274 queries 139.97 avg class size
c [sweep-10-1] 18053 decisions 267 SAT calls 225.00 avg env size
c [sweep-10-1] 455 variables remain 1% (62995 retained 99%)
c [decomp-36] removed 23 variables
c [sweep-10-1] removed 23 vars (0 failed, 6 eqs, 12 impls)
c [sweep-10] 23 < 1/1000 * 63467 = 63 considered unsuccessful
c [sweep-10] removed 23 vars in TOTAL (1 rounds, 273 queries)
c [sort-queue-20] sorted 3922 enqueued variables after 843650 conflicts
c [score-dist-20] active 59522 (94%), one 0 (0%), zero 3922 (6%)
c [score-dist-20] max exp 521, different 11 (2%)
c [score-dist-20] median active exp 521, avg 520.5
c [simplification-20] removed 3595 variables 5.4% (63444 remain 36%)
c [simplification-20] removed 70148 irredundant clauses 2.0% (3398300 remain 59%)
c [simplification-20] maximum reduction of 5% = max (5%, 2%)
c [simplification-20] forced so keeping old conflict interval 241897
c [simplification-20] conflict limit remains at 909313 (hard 1030231)
c [simplification-20] new binary interval 10000
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  627.0   63443  3398275    860695   48684   8911 96186   30   209  154  14%    235    0   34   30  114%
c i  628.2   63438  3398274    864655   51770   9002 96256   29   212  158  14%   -268    3   10   30   34%
c i  628.2   63433  3398274    864656   51770   9002 96256   29   212  158  14%   -268    3   10   30   34%
c -  641.0   63433  3398237    895102   34812   9883 96605   41   227  148  18%    165   -1   38   32  119%
c i  643.8   63432  3398237    905881   43158  10115 96620   15    72  152  21%    295 -145    7   30   23%
c i  652.2   63430  3398233    934851   66073  10669 96878   11    42  161  27%    135 -148    7   27   26%
c i  652.8   61548  3398230    935979   66861  10677 97089   15   168  161   9%   -149  -20   31   27  115%
c i  652.8   61547  3398230    935985   66866  10677 97089   15   168  161   9%   -150  -21   30   27  113%
c i  652.8   61546  3398230    935987   66867  10677 97089   15   168  161   9%   -150  -21   30   27  112%
c i  653.2   61545  3398230    937295   67819  10696 97140   18   163  162  11%   -246  -25   32   27  119%
c i  653.3   61544  3398230    937661   68105  10705 97147   18   161  162  11%   -259  -27   21   27   76%
c i  653.3   61543  3398230    937734   68141  10711 97151   18   159  162  11%   -261  -29   18   27   66%
c i  653.3   61542  3398230    938026   68384  10707 97158   18   154  162  12%   -268  -34   19   27   71%
c i  653.3   61541  3398230    938050   68395  10707 97159   18   154  162  12%   -268  -34   18   27   69%
c i  653.4   61540  3398230    938335   68565  10717 97170   18   149  162  12%   -273  -39   15   27   57%
c i  653.6   61539  3398230    938657   68816  10715 97181   20   157  162  12%   -276  -31   36   27  132%
c i  653.6   61538  3398230    938811   68938  10717 97189   20   156  162  13%   -278  -32   32   27  117%
c i  653.6   61537  3398230    938812   68938  10717 97189   20   156  162  13%   -278  -32   31   27  117%
c i  653.6   61536  3398230    938813   68938  10717 97189   20   156  162  13%   -278  -32   31   27  116%
c i  653.6   61535  3398230    938814   68938  10717 97189   20   156  162  13%   -278  -32   31   27  116%
c i  653.6   61534  3398230    938830   68951  10718 97189   20   155  162  13%   -278  -33   30   27  112%
c i  653.6   61533  3398230    938836   68952  10718 97190   20   155  162  13%   -278  -33   30   27  110%
c i  653.6   61532  3398230    938837   68952  10718 97190   20   155  162  13%   -278  -33   29   27  109%
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  653.9   61531  3398230    939501   69421  10723 97226   21   158  162  13%   -278  -29   27   27  101%
c i  653.9   61530  3398230    939502   69421  10723 97226   21   158  162  13%   -278  -29   27   27  101%
c i  653.9   61529  3398230    939503   69421  10723 97226   21   158  162  13%   -278  -29   27   27  100%
c i  653.9   61528  3398230    939504   69421  10723 97226   21   158  162  13%   -278  -29   27   27  100%
c i  653.9   61527  3398230    939507   69423  10723 97226   21   158  162  13%   -278  -29   27   27   99%
c i  653.9   61526  3398230    939508   69423  10723 97226   21   158  162  13%   -278  -29   27   27   99%
c i  654.1   61525  3398230    940280   70000  10729 97276   23   164  162  14%   -277  -23   39   27  143%
c i  654.1   61524  3398230    940356   70044  10731 97286   23   164  162  14%   -277  -23   37   27  137%
c i  654.4   61523  3398230    941124   70510  10739 97361   25   167  162  15%   -274  -19   31   27  116%
c i  654.4   61521  3398230    941134   70516  10741 97361   25   167  162  15%   -274  -20   31   27  113%
c i  654.4   61520  3398230    941135   70516  10741 97361   25   167  162  15%   -274  -20   31   27  113%
c i  654.4   61519  3398230    941137   70517  10741 97361   25   167  162  15%   -274  -20   30   27  112%
c i  654.4   61518  3398230    941138   70517  10741 97361   25   167  162  15%   -274  -20   30   27  112%
c i  654.4   61517  3398230    941142   70519  10741 97361   25   167  162  15%   -274  -20   30   27  111%
c i  654.4   61516  3398230    941144   70520  10740 97362   25   167  162  15%   -274  -20   30   27  110%
c i  654.8   61515  3398230    942043   71217  10745 97421   26   174  163  15%   -270  -13   36   27  131%
c i  654.8   61514  3398230    942044   71216  10745 97422   26   174  163  15%   -270  -13   35   27  131%
c i  654.8   61513  3398230    942045   71216  10745 97422   26   174  163  15%   -270  -13   35   27  130%
c i  654.8   61512  3398230    942048   71213  10745 97425   26   174  163  15%   -270  -13   35   27  130%
c i  654.8   61511  3398230    942050   71212  10745 97426   26   174  163  15%   -270  -13   35   27  129%
c i  654.8   61510  3398230    942150   71277  10746 97431   26   173  163  15%   -270  -14   32   27  119%
c i  654.8   61509  3398230    942159   71284  10746 97431   26   173  163  15%   -270  -14   32   27  118%
c i  654.9   61508  3398230    942369   71447  10749 97438   26   171  163  15%   -270  -16   27   27  100%
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  654.9   61507  3398230    942380   71455  10749 97438   26   170  163  15%   -270  -16   27   27   99%
c i  654.9   61506  3398230    942480   71529  10749 97439   26   172  163  15%   -270  -15   31   27  114%
c i  654.9   61505  3398230    942481   71529  10749 97439   26   172  163  15%   -270  -15   31   27  114%
c i  654.9   61504  3398230    942482   71529  10749 97439   26   172  163  15%   -270  -15   31   27  113%
c i  655.0   61503  3398230    942608   71636  10751 97443   26   172  163  15%   -270  -15   29   27  108%
c i  655.1   61502  3398230    943241   72049  10758 97452   26   163  163  16%   -267  -23   18   27   68%
c i  655.1   61501  3398230    943245   72051  10758 97452   26   163  163  16%   -267  -24   18   27   67%
c i  655.1   61500  3398230    943253   72056  10758 97452   26   163  163  16%   -267  -24   18   27   66%
c i  655.1   61499  3398230    943298   72091  10759 97453   26   163  163  16%   -267  -23   18   27   65%
c i  655.1   61498  3398230    943304   72090  10758 97457   26   163  163  16%   -267  -23   18   27   65%
c i  655.1   61497  3398230    943308   72091  10758 97458   26   163  163  16%   -267  -23   18   27   65%
c i  655.1   61496  3398230    943315   72095  10758 97459   26   163  163  16%   -267  -23   18   27   65%
c i  655.1   61495  3398230    943333   72105  10758 97459   26   163  163  16%   -267  -24   18   27   67%
c i  655.1   61494  3398230    943339   72107  10758 97459   26   162  163  16%   -267  -24   18   27   67%
c i  655.2   61493  3398230    943674   72309  10761 97476   25   155  163  16%   -266  -31   19   27   69%
c i  655.2   61492  3398230    943714   72338  10762 97477   25   155  163  16%   -266  -31   19   27   70%
c i  655.2   61491  3398230    943715   72338  10762 97477   25   155  163  16%   -266  -31   19   27   70%
c i  655.2   61490  3398230    943716   72338  10762 97477   25   155  163  16%   -266  -31   19   27   70%
c i  655.2   61489  3398230    943718   72339  10762 97477   25   155  163  16%   -266  -31   19   27   69%
c i  655.2   61488  3398230    943728   72341  10762 97478   25   155  163  16%   -266  -31   18   27   68%
c i  655.3   61487  3398230    944092   72647  10762 97487   26   165  163  15%   -265  -21   33   27  122%
c i  655.7   61486  3398230    945265   73518  10776 97563   26   172  163  15%   -256  -14   31   27  115%
c i  655.7   61485  3398230    945349   73566  10780 97565   26   171  163  15%   -256  -15   26   27   96%
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  655.7   61484  3398230    945350   73566  10780 97565   26   171  163  15%   -256  -15   26   27   96%
c i  655.7   61483  3398230    945352   73565  10780 97566   26   171  163  15%   -256  -15   26   27   96%
c i  655.8   61482  3398230    945512   73688  10780 97583   26   170  163  15%   -256  -16   26   27   95%
c i  655.9   61481  3398230    945855   73929  10781 97604   26   168  163  15%   -256  -18   21   27   78%
c i  655.9   61480  3398230    945945   73978  10781 97607   26   166  163  15%   -256  -19   24   27   90%
c i  655.9   61479  3398230    945947   73977  10782 97608   26   166  163  15%   -256  -19   24   27   89%
c i  655.9   61478  3398230    945948   73976  10782 97609   26   166  163  15%   -256  -19   24   27   89%
c i  655.9   61477  3398230    945950   73977  10782 97609   26   166  163  15%   -256  -19   24   27   88%
c i  655.9   61476  3398230    946099   74086  10785 97614   25   163  163  15%   -256  -23   18   27   65%
c i  656.1   61475  3398230    946632   74453  10797 97620   23   149  163  16%   -254  -36   10   27   38%
c i  656.1   61474  3398230    946633   74453  10797 97620   23   149  163  16%   -254  -36   10   27   37%
c i  656.1   61473  3398230    946636   74454  10797 97620   23   149  163  16%   -254  -36   10   27   37%
c i  656.2   61472  3398228    946941   74687  10799 97627   25   168  163  15%   -253  -17   37   27  137%
c i  656.2   61471  3398207    947080   74727  10799 97637   26   165  163  16%   -253  -20   40   27  146%
c i  656.2   61470  3398207    947081   74727  10799 97637   26   165  163  16%   -253  -20   39   27  146%
c i  656.2   61469  3398207    947082   74727  10799 97637   26   165  163  16%   -253  -20   39   27  145%
c i  656.2   61468  3398207    947083   74727  10799 97637   26   165  163  16%   -253  -20   39   27  145%
c i  656.2   61467  3398207    947084   74727  10799 97637   26   165  163  16%   -253  -20   39   27  144%
c i  656.2   61466  3398207    947124   74746  10799 97642   26   164  163  16%   -253  -21   35   27  130%
c i  656.2   61465  3398207    947131   74750  10799 97642   26   164  163  16%   -253  -22   34   27  128%
c i  656.4   61464  3398196    947431   74951  10804 97652   26   168  163  15%   -252  -17   31   27  117%
c i  656.4   61463  3398185    947546   74986  10804 97660   26   165  163  16%   -252  -20   35   27  128%
c i  656.4   61462  3398185    947548   74986  10804 97660   26   165  163  16%   -252  -20   35   27  128%
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  656.4   61461  3398185    947549   74986  10804 97660   26   165  163  16%   -252  -20   34   27  127%
c i  656.4   61460  3398185    947550   74986  10804 97660   26   165  163  16%   -252  -20   34   27  127%
c i  656.4   61459  3398185    947551   74986  10804 97660   26   165  163  16%   -252  -20   34   27  126%
c i  656.4   61458  3398185    947568   74993  10805 97662   26   164  163  16%   -252  -21   33   27  121%
c i  656.5   61457  3398185    947953   75258  10808 97665   26   158  163  16%   -251  -27   23   27   84%
c i  656.7   61456  3398185    948767   75827  10817 97723   25   159  163  16%   -245  -26   16   27   58%
c i  656.8   61455  3398185    948929   75922  10816 97736   25   158  163  16%   -245  -27   14   27   53%
c i  656.8   61454  3398185    948936   75926  10816 97737   24   158  163  16%   -245  -27   14   27   52%
c i  656.8   61453  3398185    949011   75983  10817 97739   24   158  163  15%   -245  -27   15   27   55%
c i  656.8   61452  3398185    949152   76055  10825 97754   24   154  163  16%   -245  -30   12   27   46%
c i  656.8   61434  3398185    949155   76057  10825 97754   24   154  163  16%   -245  -31   12   27   45%
c i  656.8   61433  3398185    949156   76057  10825 97754   24   154  163  16%   -245  -31   12   27   45%
c i  656.9   61432  3398185    949248   76123  10827 97760   23   151  163  16%   -245  -33   10   27   38%
c i  656.9   61431  3398185    949282   76139  10830 97765   23   150  163  16%   -245  -34    9   27   35%
c i  656.9   61407  3398185    949295   76142  10832 97769   23   150  163  16%   -245  -35    9   27   34%
c i  656.9   61406  3398185    949297   76143  10832 97769   23   150  163  16%   -245  -35    9   27   34%
c i  656.9   61373  3398185    949300   76145  10832 97769   23   150  163  16%   -245  -35    9   27   33%
c 0  656.9   60478  3398185    949300   76145  10832 97769   23   150  163  16%   -245  -35    9   27   33%
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 
s UNSATISFIABLE
c
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 16 count, 99049 added (44703 skipped), 6916415 steps
c bkwd: tried 445964 clauses, 891087 lits, 2.00 lits/clause
c bkwd: checked 859636023 occs, 1927.59 occs/clause, 964.70 occs/lit
c bkwd: subsumed 0 binary, 0 ternary, 0 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 843 large (0% self)
c blkd: 14 bces, 1390063 removed, 121579575 resolutions, 674629767 steps
c blkd: 40743 blocking literals 12%, 16549 pure
c bump: 902015 bumped seen, 113130647 lits 125.4 on average
c card: 5 count, 0 units, 0 am1, 72223634 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 21 subsumed
c card: 6 at-most-one constraints found, average size 3.33
c card: 6 at-most-one constraints used 100%, average size 3.33
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: 5 cces, 47 eliminated, 46 ate 98%, 1 abce 2%
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: 22875678 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 98 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 36 decompositions, 8238 equivalent 5%
c deco: 5865 decision-only clauses 1%, 56% reduction
c decs: 26272401 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 13 elims, 101356 eliminated 58%, 565 pure 1%
c elms: 15 rounds, 1.2 rounds/bve
c elms: 60044 small 59%, 24198 large 24%
c elms: 60185 tried small, 60044 succeeded 100%, 141 failed 0%
c elms: 2937 subsumed, 277022 strengthened, 0 blocked
c elms: 11827169 copies, 30006432 resolutions, 1227913 ipos
c elms: 86244377 subchks, 47617990 strchks
c gaus: 5 extractions, 1 extracted, 2.0 size, 2 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 24106976 steps, 12053488 extr 50%, 3 elim 0%
c glue: 34.9 orig avg, 34.9 real avg, 5.2 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 78741 = 13204 simple 17% + 65429 trn 83% + 108 lrg 0%, 1339 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 902015 clauses, 62.8 length
c lrnd: 56620259 lits = 83722912 orig - 27102653 removed 32%
c lrnd: 336648 uips 37%, 411308 flips 46%
c mins: 876740 mins 97%, 9683 bin 1%, 8976 size 1%
c mins: 116712318 poisoned searches, 8545775 hits, 7% hit rate
c mins: 187980382 used twice searches, 20692494 hits, 11% hit rate
c move: moved 1313638, 1310011 bin 100%, 3627 trn 0%
c otfs: 48095 driving 15%, 281789 restarting 85%
c otfs: str 329884, 317137 red 96%, 12747 irr 4%
c otfs: str 329884, 0 bin 0%, 1571 trn 0%, 328313 lrg 100%
c otfs: sub 1262, 1092 red 87%, 170 irr 13%
c otfs: sub 1262, 0 bin 0%, 9 trn 1%, 1253 lrg 99%
c phas: 1 computed, 171959 set, 0 pos (0%), 171959 neg (100%)
c prbs: 3 basic, 22384 probed, 288 failed, 0 lifted
c prbs: 4 simple, 234116 probed, 0 failed, 0 eqs
c prbs: 3 treelook, 41 probed, 0 failed, 0 lifted
c prom: 108427 locked 3% out of 3897112 tried
c prps: 2324585223 props, 87 props/dec
c prps: 98% srch, 2% simp, 0% lkhd
c quat: 16 count, 7249 quat, 1647 self1, 4 self2, 2 dup
c queu: 20 sorted, 26272401 next (33631 steps 0.00)
c queu: 114389183 enq (1501613884 steps 13.13), 113130647 deq 99%
c redc: 8227 clauses 12%, 68413 tried 7%, 124 sat 0%
c redc: 39323 lits 6%, 674003 tried 1%, 124 sat 0%
c redc: 2582 times jump level reduced, 40.0 levels on average
c reds: 18 count, 52738.9 conflicts per reduce
c reds: 0 memlim 0%, 18 arith 100%
c reds: 526852 collected 85%, 93063 retired 15%
c rmbd: 11506 removed, 421 red 4%
c rsts: 16854 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: 20 count, 17 confs 85%, 0 vars 0%
c simp: 0 its 0%, 2 bin 10%, 1 trns 5%
c subl: 902015 count (1401950 tried 1.6), 107027 sub out of 870929 (12.3%)
c swps: 10 count, 10 rounds, 3051 queries (305.1/round)
c swps: 2944 sat calls, 24 unsat (0.3% success rate)
c swps: 169502 decisions 57.6, 810 conflicts 0.3
c swps; 1387.0 avg class size, 296.3 avg environment size
c swps: 0 failed, 222 impls, 130 equivs
c swp0: 1015 type 0 queries, 54 unsat (5.3%), 996 sat (98.1%)
c swp1: 2036 type 1 queries, 352 unsat (17.3%), 1925 sat (94.5%)
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: 54349323 calls to obtain time
c tops: 5994 fixed 3%, 147 its, 6457.82 confs/it
c trds: 11 transitive reductions, 21 removed, 0 failed
c trds: 1414 nodes, 42543 edges, 48899962 steps
c trim: 1751499 words, 6.7 MB
c trnr: 14 count, 4 bin, 9273 trn, 188799767 steps
c unhd: 7 count, 7 rounds, 49704583 steps
c unhd: 76 non-trivial sccs of average size 2.1
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 1 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 28878 tauts, 37 bin 0%, 108 trn 0%, 515 lrg 2%
c unhd: 28878 tauts, 28218 stamp 98%, 1256 red 4%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 163421 str, 0 bin 0%, 1144 trn 1%, 162277 lrg 99%, 109095 red 67%
c vars: 60478 remaining 34% and 115588 removed 66% out of 176066
c vars: 5994 fixed 3%, 101356 eliminated 58%, 8238 equivalent 5%
c vsts: 9420285341 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 4.1 search visits per propagation, 9759.4 per conflict
c wchs: 1282374213 pushed, 91112756 enlarged, 154 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         878178        526852         93063      28279919      10317368        764424
c 
c  0 0         38449   4      3384   1         0   0  12432806  44   2788243  27     52741   7     1.3
c  1 5         18542   2      6723   1      2328   3   1274058   5    680256   7     27285   4     0.5
c  2 6         60646   7     28772   5      6508   7   3164178  11<  1404315  14     83627  11     1.4
c  3 9        101207  12     56682  11      9849  11   3916382  14   1397218  14<   119098  16     2.5
c  4 14       138846  16     90753  17     11113  12   3301511  12   1229856  12    120291  16<    2.9
c  5 21       128370  15<    85486  16     10921  12   1602091   6   1005108  10    107865  14     2.8
c  6 30       114256  13     77438  15<    10787  12<  1078872   4    804409   8    114149  15     5.1
c  7 41        79953   9     52227  10      9139  10    668326   2    492470   5     60332   8     2.2
c  8 54        66086   8     44253   8      8779   9    403258   1    279229   3     45468   6     2.7
c  9 69        56926   6     37767   7      8212   9    207978   1    124607   1     17430   2     3.0
c 10 86        63342   7     38363   7     12547  13    192352   1     96385   1     14294   2     5.0
c 11 126       10982   1      4731   1      2735   3     36730   0     14510   0      1664   0     1.6
c 12 230         572   0       273   0       144   0      1376   0       762   0       180   0     0.3
c 13 534           1   0         0   0         1   0         1   0         0   0         0   0     0.0
c 
c avg                  5.3           5.7           6.2           2.1           2.9           4.4
c std                  2.7           2.4           2.7           2.4           2.5           2.4
c 
c   98.267  15% elim
c   83.902  13% block
c   28.474   4% bump
c   19.416   3% probe
c   17.605   3% decide
c   14.874   2% sweep
c   11.544   2% bca
c   11.469   2% unhide
c    5.779   1% quatres
c 
c    9.583 < 1% rest (below)
c 
c    4.189   1% cce
c    3.608   1% gauss
c    0.857   0% transred
c    0.729   0% ternres
c    0.200   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    9.330   1% preprocessing     3%
c  274.358  42% inprocessing     97%
c ==================================
c  283.688  43% simplifying
c  373.184  57% search
c ==================================
c  656.875 100% all
c 
c        949300 conflicts,        1445.2 confs/sec
c         20196 ternaries,          47.0 confs/ternary
c         10345 binaries,           91.8 confs/binary
c           147 iterations,       6457.8 confs/iteration
c 
c            18 reductions,          0.0 redus/sec,  52738.9 confs/reduction
c         16854 restarts,           25.7 rests/sec,     56.3 confs/restart
c      26272401 decisions,       39996.1 decis/sec,     27.7 decis/conflict
c    2324585223 propagations,  3538856.3 props/sec,     88.5 props/decision
c 
c 656.9 seconds, 329.6 MB
c launch: done
