c launch: /data/cnf/sc2014/app/gss-19-s100.cnf.bz2
c host: atom08
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/gss-19-s100.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/gss-19-s100.cnf.bz2
c no embedded options
c found 'p cnf 31435 94548' header
c read 31435 variables, 94548 clauses, 222806 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 31340 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   31340    94348         0       0      0     0    0     0    5   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 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 2000000 for elimination
c [card-1] 2 out of 2 constraints (100%) meet size limits
c [card-1] found 1 units
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 1110 variables
c [simpleprobe-1] all 30325 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 2814 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 2814 variables, found 313 hbrs, 67 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
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 27511 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 18286 variables 66% in round 1 in 5506681 steps
c [elim-1-1] backward subsumption/strengthening limit 5506600
c [elim-1-1-1] backward checking 21962 touched variables 80%
c [elim-1-1-1] incomplete backward checking 18286 remain 83%
c [elim-1-1] subsumed 128 and strengthened 2235 clauses in 5506624 steps
c [elim-1-1] rescheduled 3498 variables 13% by backward subsumption
c [elim-1-2] eliminated 9 variables 0% in round 2 in 1200728 steps
c [elim-1-2] backward subsumption/strengthening limit 1200700
c [elim-1-2-1] backward checking 18500 touched variables 67%
c [elim-1-2-1] incomplete backward checking 17266 remain 93%
c [elim-1-2] subsumed 22 and strengthened 397 clauses in 1200717 steps
c [elim-1-2] rescheduled 880 variables 3% by backward subsumption
c [elim-1-3] eliminated 3 variables 0% in round 3 in 333108 steps
c [elim-1-3] backward subsumption/strengthening limit 333100
c [elim-1-3-1] backward checking 17306 touched variables 63%
c [elim-1-3-1] incomplete backward checking 17060 remain 99%
c [elim-1-3] subsumed 3 and strengthened 131 clauses in 333214 steps
c [elim-1] incomplete 190 not tried 1% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 18331 = 67% variables out of 27511 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 50768 negative 99.2% of 51176 except 408 0.8%
c [phase-count-1] 42159 positive 82.4% of 51176 except 9017 17.6%
c [phase-count-1] less non-negative clauses 408 than limit 5100 (10.0%)
c [phase-count-1] non-pos/non-neg = 9017/408 = 22.10 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 9180 negative 100%
c [sort-queue-1] sorted 9180 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 9180 (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 22107 variables 70.7% (9180 remain 29%)
c [simplification-1] removed 43172 irredundant clauses 45.8% (51176 remain 54%)
c [simplification-1] maximum reduction of 71% = max (71%, 46%)
c [simplification-1] large reduction 71% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 9 variables
c [simpleprobe-2] all 9171 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 14 variables
c [simpleprobe-2] 884 variables remain 10% (8273 retained 90%)
c [simpleprobe-2] removed 14 variables, found 658 hbrs, 11 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 18314 literals 100%
c [treelook-1] scheduling used 153217 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 309040 steps
c [treelook-1] 18201 literals remain 99%
c [treelook-1] 9157 variables remain to probed next time 100%
c [treelook-1] removed 0 variables, found 672 hbrs
c [basicprobe-1] limit 1478743 penalty 0 = 0 + 0
c [basicprobe-1-0] 3975 probes remain 43% after last round
c [basicprobe-1-0] 1 units = 1 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 17 variables, found 440 hbrs
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 9140 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 80 variables 1% in round 1 in 7249027 steps
c [elim-2-1] backward subsumption/strengthening limit 7249000
c [elim-2-1-1] backward checking 1261 touched variables 14%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 2 and strengthened 1 clauses in 920471 steps
c [elim-2-1] rescheduled 11 variables 0% by backward subsumption
c [elim-2-2] no variable eliminated in round 2 in 66060 steps
c [elim-2] fully completed in 2 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 80 = 1% variables out of 9140 scheduled
c [elim-2] 80 < 1/100 * 9140 = 91 considered unsuccessful
c [sort-queue-2] sorted 56 enqueued variables after 1001 conflicts
c [score-dist-2] active 9004 (99%), one 0 (0%), zero 56 (1%)
c [score-dist-2] max exp 511, different 8 (2%)
c [score-dist-2] median active exp 511, avg 511.0
c [simplification-2] removed 120 variables 1.3% (9060 remain 29%)
c [simplification-2] removed 576 irredundant clauses 1.1% (50600 remain 54%)
c [simplification-2] maximum reduction of 1% = max (1%, 1%)
c [simplification-2] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-2] new conflict interval 10000
c [simplification-2] penalized conflict interval 10000 = 1 * 10000
c [simplification-2] hard conflict limit 21001 (soft 11001 + delta 10000)
c [simplification-2] new conflict limit 11001 (hard 21001)
c 
c [simplification-3] limit 11001 conflicts (hard 21001) hit after 11001 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 87 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 87 out of 87 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 14 at-most-one constraints, 12 used 86%
c [card-2] exported 15 binary clauses, 1.2 per/constraint
c [decomp-6] removed 5 variables
c [unhide-2] limit 335043 with penalty 1 = 1 + 0
c [unhide-2-3] 0 units, 0 failed, 253 tauts, 0 hbrs, 1651 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 9055 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 10 blocked clauses
c [block-1] 10 < 1/100 * 50527 = 505 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 25
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 24
c [cce-1-1] eliminated 6 clauses out of 7 (86%) of length 23
c [cce-1-1] eliminated 8 clauses out of 15 (53%) of length 21
c [cce-1-1] eliminated 12 clauses out of 14 (86%) of length 20
c [cce-1-1] eliminated 19 clauses out of 27 (70%) of length 19
c [cce-1-1] eliminated 26 clauses out of 31 (84%) of length 18
c [cce-1-1] eliminated 39 clauses out of 47 (83%) of length 17
c [cce-1-1] eliminated 41 clauses out of 64 (64%) of length 16
c [cce-1-1] eliminated 31 clauses out of 66 (47%) of length 15
c [cce-1-1] eliminated 46 clauses out of 125 (37%) of length 14
c [cce-1-1] eliminated 48 clauses out of 156 (31%) of length 13
c [cce-1-1] eliminated 59 clauses out of 220 (27%) of length 12
c [cce-1-1] eliminated 93 clauses out of 321 (29%) of length 11
c [cce-1-1] eliminated 79 clauses out of 356 (22%) of length 10
c [cce-1-1] eliminated 98 clauses out of 420 (23%) of length 9
c [cce-1-1] eliminated 92 clauses out of 429 (21%) of length 8
c [cce-1-1] eliminated 102 clauses out of 430 (24%) of length 7
c [cce-1-1] eliminated 119 clauses out of 423 (28%) of length 6
c [cce-1-1] eliminated 95 clauses out of 2587 (4%) of length 5
c [cce-1-1] eliminated 107 clauses out of 4724 (2%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 1125 large clauses in 9596302 steps
c [cce-1-1] allowing another 4798151 steps for small clauses
c [cce-1-1] scheduling 37446 clauses = 34555 binary + 2891 ternary
c [cce-1-1] tried to eliminate 27975 small clauses 75%
c [cce-1-1] eliminated 2893 binary clauses 8%
c [cce-1-1] eliminated 23 ternary clauses 1%
c [cce-1-1] eliminated 2916 small clauses 8%
c [cce-1-1] eliminated 2916 small clauses in 30000004 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 4041 covered clauses in round 1
c [cce-1] eliminated 4041 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 93452 added (scaled 2)
c [bca-1] 16422 out of 18110 literals actually usable 91%
c [bca-1] added 0 blocked clauses in 46926 steps
c [sweep-1] limit 1005131 penalty 0 = 0 + 0
c [sweep-1-1] 905 pos 10.0% + 8149 neg 90.0% = 9054 sched 100.0% ret 0
c [sweep-1-1] 2974631 steps 87 queries 929.89 avg class size
c [sweep-1-1] 783 decisions 85 SAT calls 29.62 avg env size
c [sweep-1-1] 8053 variables remain 89% (1001 retained 11%)
c [decomp-7] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 1 eqs, 1 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 86 queries)
c [score-dist-3] active 9053 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-3] max exp 515, different 3 (1%)
c [score-dist-3] median active exp 515, avg 515.0
c [simplification-3] removed 7 variables 0.1% (9053 remain 29%)
c [simplification-3] removed 4126 irredundant clauses 8.2% (46474 remain 49%)
c [simplification-3] maximum reduction of 8% = max (0%, 8%)
c [simplification-3] large reduction 8% >= 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 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 13002 conflicts
c [quatres-1] found 4677 quaternary clauses 49% in total
c [quatres-1-2] added 12 single-self-subsuming ternary resolvents
c [quatres-1-2] added 1927 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 9053 free variables schedulable
c [ternres-1] 1603 ternary resolvents (10 bin, 1593 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 5880 xors of average arity 3.0
c [gauss-1] connected 17616 occurrences of 895 variables (average 19.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 2 ternary equations
c [decomp-8] removed 6 variables
c [treelook-2] limit 195697 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 18094 literals 100%
c [treelook-2] scheduling used 166487 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 195697 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 203639 steps
c [treelook-2] 17959 literals remain 99%
c [treelook-2] 9047 variables remain to probed next time 100%
c [treelook-2] removed 0 variables, found 574 hbrs
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 466 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 2492 (0%) of length 5
c [cce-2-1] eliminated 2 clauses out of 4615 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 3 large clauses in 8410740 steps
c [cce-2-1] allowing another 4205370 steps for small clauses
c [cce-2-1] scheduling 34213 clauses = 31656 binary + 2557 ternary
c [cce-2-1] tried to eliminate 30210 small clauses 88%
c [cce-2-1] eliminated 755 binary clauses 2%
c [cce-2-1] eliminated 14 ternary clauses 1%
c [cce-2-1] eliminated 769 small clauses 2%
c [cce-2-1] eliminated 769 small clauses in 30000002 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 772 covered clauses in round 1
c [cce-2] eliminated 772 covered clauses in TOTAL during 1 rounds
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 9047 variables 100%
c [elim-3] limit of 39139507 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 443 variables 5% in round 1 in 6287371 steps
c [elim-3-1] backward subsumption/strengthening limit 6287300
c [elim-3-1-1] backward checking 4649 touched variables 51%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 47 and strengthened 370 clauses in 2074921 steps
c [elim-3-1] rescheduled 1402 variables 15% by backward subsumption
c [elim-3-2] eliminated 5 variables 0% in round 2 in 1988317 steps
c [elim-3-2] backward subsumption/strengthening limit 1988300
c [elim-3-2-1] backward checking 85 touched variables 1%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 1 and strengthened 10 clauses in 100715 steps
c [elim-3-2] rescheduled 53 variables 1% by backward subsumption
c [elim-3-3] eliminated 2 variables 0% in round 3 in 59405 steps
c [elim-3-3] backward subsumption/strengthening limit 59400
c [elim-3-3-1] backward checking 10 touched variables 0%
c [elim-3-3-1] incomplete backward checking 0 remain 0%
c [elim-3-3] subsumed 0 and strengthened 4 clauses in 59401 steps
c [elim-3] incomplete 8 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 450 = 5% variables out of 9047 scheduled
c [sweep-2] limit 1174185 penalty 0 = 0 + 0
c [sweep-2-1] 784 pos 10.2% + 6875 neg 89.8% = 7659 sched 89.1% ret 938
c [sweep-2-1] 2652343 steps 6 queries 1406.17 avg class size
c [sweep-2-1] 306 decisions 5 SAT calls 95.80 avg env size
c [sweep-2-1] 7642 variables remain 89% (955 retained 11%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 5 queries)
c [score-dist-4] active 8597 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-4] max exp 515, different 3 (1%)
c [score-dist-4] median active exp 515, avg 515.0
c [simplification-4] removed 456 variables 5.0% (8597 remain 27%)
c [simplification-4] removed 1245 irredundant clauses 2.7% (45229 remain 48%)
c [simplification-4] maximum reduction of 5% = max (5%, 3%)
c [simplification-4] large reduction 5% >= 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 25002 (soft 15002 + delta 10000)
c [simplification-4] new conflict limit 15002 (hard 25002)
c 
c [simplification-5] limit 15002 conflicts (hard 25002) hit after 15004 conflicts
c [quatres-2] found 6779 quaternary clauses 54% in total
c [quatres-2-2] added 10 single-self-subsuming ternary resolvents
c [quatres-2-2] added 1453 quaternary resolvents
c [ternres-2] limit 4390111 with penalty 0 = 0 + 0
c [ternres-2] all 8597 free variables schedulable
c [ternres-2] 441 ternary resolvents (1 bin, 440 trn)
c [ternres-2] fully completed ternary resolution
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 5813 xors of average arity 3.0
c [gauss-2] connected 17451 occurrences of 888 variables (average 19.7)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-11] removed 1 variables
c [basicprobe-2] limit 21950558 penalty 0 = 0 + 0
c [basicprobe-2-0] 3855 sched 45%, 0 failed, 0 lifted, 1112 hbrs
c [basicprobe-2-1] 5104 sched 59%, 0 failed, 0 lifted, 103 hbrs
c [basicprobe-2-2] 5103 sched 59%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-2-3] 262 probes remain 3% after last round
c [basicprobe-2-3] removed 0 variables, found 1217 hbrs
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 266 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 8596 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 [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 1 clauses out of 8 (12%) of length 21
c [cce-3-1] eliminated 2 clauses out of 13 (15%) of length 18
c [cce-3-1] eliminated 1 clauses out of 18 (6%) of length 17
c [cce-3-1] eliminated 7 clauses out of 41 (17%) of length 16
c [cce-3-1] eliminated 4 clauses out of 47 (9%) of length 15
c [cce-3-1] eliminated 3 clauses out of 92 (3%) of length 14
c [cce-3-1] eliminated 7 clauses out of 107 (7%) of length 13
c [cce-3-1] eliminated 12 clauses out of 176 (7%) of length 12
c [cce-3-1] eliminated 30 clauses out of 264 (11%) of length 11
c [cce-3-1] eliminated 33 clauses out of 320 (10%) of length 10
c [cce-3-1] eliminated 53 clauses out of 398 (13%) of length 9
c [cce-3-1] eliminated 64 clauses out of 438 (15%) of length 8
c [cce-3-1] eliminated 60 clauses out of 430 (14%) of length 7
c [cce-3-1] eliminated 59 clauses out of 413 (14%) of length 6
c [cce-3-1] eliminated 31 clauses out of 2675 (1%) of length 5
c [cce-3-1] eliminated 33 clauses out of 4891 (1%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 400 large clauses in 10295018 steps
c [cce-3-1] allowing another 5147509 steps for small clauses
c [cce-3-1] scheduling 32678 clauses = 29854 binary + 2824 ternary
c [cce-3-1] tried to eliminate 28456 small clauses 87%
c [cce-3-1] eliminated 918 binary clauses 3%
c [cce-3-1] eliminated 55 ternary clauses 2%
c [cce-3-1] eliminated 973 small clauses 3%
c [cce-3-1] eliminated 973 small clauses in 30000063 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1373 covered clauses in round 1
c [cce-3] eliminated 1373 covered clauses in TOTAL during 1 rounds
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 8596 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1756044640 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 144 variables 2% in round 1 in 5922786 steps
c [elim-4-1] backward subsumption/strengthening limit 5922700
c [elim-4-1-1] backward checking 2207 touched variables 26%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 2 and strengthened 40 clauses in 946975 steps
c [elim-4-1] rescheduled 253 variables 3% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 554728 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 144 = 2% variables out of 8596 scheduled
c [bca-2] limit of 10000000 steps and 88066 added (scaled 2)
c [bca-2] 10467 out of 16906 literals actually usable 62%
c [bca-2] added 33 blocked clauses in 35229 steps
c [sweep-3] limit 1317033 penalty 0 = 0 + 0
c [sweep-3-1] 805 pos 10.7% + 6705 neg 89.3% = 7510 sched 88.9% ret 942
c [sweep-3-1] 3340142 steps 117 queries 788.70 avg class size
c [sweep-3-1] 807 decisions 116 SAT calls 31.67 avg env size
c [sweep-3-1] 6770 variables remain 80% (1682 retained 20%)
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 0 vars in TOTAL (1 rounds, 116 queries)
c [score-dist-5] active 8452 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-5] max exp 515, different 1 (0%)
c [score-dist-5] median active exp 515, avg 515.0
c [simplification-5] removed 145 variables 1.7% (8452 remain 27%)
c [simplification-5] removed 1446 irredundant clauses 3.2% (43783 remain 46%)
c [simplification-5] maximum reduction of 3% = max (2%, 3%)
c [simplification-5] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-5] new conflict interval 15000
c [simplification-5] penalized conflict interval 15000 = 1 * 15000
c [simplification-5] hard conflict limit 40004 (soft 30004 + delta 10000)
c [simplification-5] new conflict limit 30004 (hard 40004)
c 
c [simplification-6] limit 30004 conflicts (hard 40004) hit after 30004 conflicts
c [quatres-3] found 8114 quaternary clauses 57% in total
c [quatres-3-2] added 11 single-self-subsuming ternary resolvents
c [quatres-3-2] added 750 quaternary resolvents
c [ternres-3] limit 9094388 with penalty 0 = 0 + 0
c [ternres-3] all 8452 free variables schedulable
c [ternres-3] 58 ternary resolvents (0 bin, 58 trn)
c [ternres-3] fully completed ternary resolution
c [card-3] limit 1136798 penalty 2 = 2 + 0
c [card-3] found 106 at-most-one constraints of average size 3.0
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 1136798 for elimination
c [card-3] 106 out of 106 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 4 at-most-one constraints, 3 used 75%
c [card-3] exported 8 binary clauses, 2.7 per/constraint
c [simpleprobe-3] 819 schedulable variables 10%
c [simpleprobe-3] limit 36377553 penalty 0 = 0 + 0
c [decomp-17] removed 1 variables
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 1 variables, found 733 hbrs, 0 units
c [unhide-3] limit 454719 with penalty 2 = 2 + 0
c [unhide-3-4] 0 units, 0 failed, 72 tauts, 0 hbrs, 21493 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 522 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 454719410 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 24
c [cce-4-1] eliminated 1 clauses out of 8 (12%) of length 21
c [cce-4-1] eliminated 1 clauses out of 9 (11%) of length 20
c [cce-4-1] eliminated 1 clauses out of 19 (5%) of length 18
c [cce-4-1] eliminated 2 clauses out of 20 (10%) of length 17
c [cce-4-1] eliminated 2 clauses out of 46 (4%) of length 15
c [cce-4-1] eliminated 3 clauses out of 95 (3%) of length 13
c [cce-4-1] eliminated 4 clauses out of 165 (2%) of length 12
c [cce-4-1] eliminated 8 clauses out of 242 (3%) of length 11
c [cce-4-1] eliminated 18 clauses out of 313 (6%) of length 10
c [cce-4-1] eliminated 34 clauses out of 398 (9%) of length 9
c [cce-4-1] eliminated 33 clauses out of 424 (8%) of length 8
c [cce-4-1] eliminated 42 clauses out of 443 (9%) of length 7
c [cce-4-1] eliminated 18 clauses out of 401 (4%) of length 6
c [cce-4-1] eliminated 15 clauses out of 2724 (1%) of length 5
c [cce-4-1] eliminated 32 clauses out of 4921 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 215 large clauses in 9488486 steps
c [cce-4-1] allowing another 4744243 steps for small clauses
c [cce-4-1] scheduling 30687 clauses = 28551 binary + 2136 ternary
c [cce-4-1] tried to eliminate 30687 small clauses 100%
c [cce-4-1] eliminated 137 binary clauses 0%
c [cce-4-1] eliminated 17 ternary clauses 1%
c [cce-4-1] eliminated 154 small clauses 1%
c [cce-4-1] eliminated 154 small clauses in 30174145 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 369 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 4632639 steps for small clauses
c [cce-4-2] scheduling 30533 clauses = 28414 binary + 2119 ternary
c [cce-4-2] tried to eliminate 30533 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 369 covered clauses in TOTAL during 2 rounds
c [cce-4] 369 < 1/100 * 43780 = 437 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 8451 variables 100%
c [elim-5] limit of 181887766 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 45 variables 1% in round 1 in 5762412 steps
c [elim-5-1] backward subsumption/strengthening limit 5762400
c [elim-5-1-1] backward checking 696 touched variables 8%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 13 clauses in 342782 steps
c [elim-5-1] rescheduled 43 variables 1% by backward subsumption
c [elim-5-2] eliminated 1 variables 0% in round 2 in 68196 steps
c [elim-5-2] backward subsumption/strengthening limit 68100
c [elim-5-2-1] backward checking 9 touched variables 0%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 0 clauses in 21408 steps
c [elim-5] fully completed in 2 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 46 = 1% variables out of 8451 scheduled
c [elim-5] 46 < 1/100 * 8451 = 84 considered unsuccessful
c [bca-3] limit of 10000000 steps and 87300 added (scaled 2)
c [bca-3] 9685 out of 16812 literals actually usable 58%
c [bca-3] added 0 blocked clauses in 39585 steps
c [sweep-4] limit 2728316 penalty 0 = 0 + 0
c [sweep-4-1] 656 pos 9.7% + 6075 neg 90.3% = 6731 sched 80.1% ret 1674
c [sweep-4-1] 2913762 steps 243 queries 328.88 avg class size
c [sweep-4-1] 1718 decisions 242 SAT calls 32.73 avg env size
c [sweep-4-1] 5141 variables remain 61% (3264 retained 39%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 242 queries)
c [score-dist-6] active 8405 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-6] max exp 516, different 2 (0%)
c [score-dist-6] median active exp 516, avg 516.0
c [simplification-6] removed 47 variables 0.6% (8405 remain 27%)
c [simplification-6] removed 391 irredundant clauses 0.9% (43392 remain 46%)
c [simplification-6] maximum reduction of 1% = max (1%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 25000
c [simplification-6] penalized conflict interval 25000 = 1 * 25000
c [simplification-6] hard conflict limit 67504 (soft 55004 + delta 12500)
c [simplification-6] new conflict limit 55004 (hard 67504)
c 
c [simplification-7] limit 55004 conflicts (hard 67504) hit after 55004 conflicts
c [quatres-4] found 8715 quaternary clauses 58% in total
c [quatres-4-2] added 41 single-self-subsuming ternary resolvents
c [quatres-4-2] added 230 quaternary resolvents
c [ternres-4] limit 18220706 with penalty 0 = 0 + 0
c [ternres-4] all 8405 free variables schedulable
c [ternres-4] 78 ternary resolvents (0 bin, 78 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-3] limit 1822070 penalty 1 = 1 + 0
c [gauss-3] extracted 5797 xors of average arity 3.0
c [gauss-3] connected 17407 occurrences of 885 variables (average 19.7)
c [gauss-3] limit 1822070 penalty 1 = 1 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 202 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 54662110 penalty 0 = 0 + 0
c [sweep-5-1] 492 pos 9.6% + 4649 neg 90.4% = 5141 sched 61.2% ret 3264
c [sweep-5-1] 16166115 steps 2125 queries 32.75 avg class size
c [sweep-5-1] 3952 decisions 2124 SAT calls 26.05 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5-2] 947 pos 11.3% + 7458 neg 88.7% = 8405 sched 100.0% ret 0
c [sweep-5-2] 38497117 steps 655 queries 101.18 avg class size
c [sweep-5-2] 4619 decisions 654 SAT calls 31.91 avg env size
c [sweep-5-2] 2732 variables remain 33% (5673 retained 67%)
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5] removed 0 vars in TOTAL (2 rounds, 2778 queries)
c [score-dist-7] active 8405 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-7] max exp 517, different 1 (0%)
c [score-dist-7] median active exp 517, avg 517.0
c [simplification-7] removed 0 variables 0.0% (8405 remain 27%)
c [simplification-7] removed 1 irredundant clauses 0.0% (43391 remain 46%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 25000
c [simplification-7] new conflict interval 50000
c [simplification-7] penalized conflict interval 50000 = 1 * 50000
c [simplification-7] hard conflict limit 130004 (soft 105004 + delta 25000)
c [simplification-7] new conflict limit 105004 (hard 130004)
c 
c [simplification-8] limit 105004 conflicts (hard 130004) hit after 105006 conflicts
c [quatres-5] found 8949 quaternary clauses 57% in total
c [quatres-5-2] added 12 single-self-subsuming ternary resolvents
c [quatres-5-2] added 41 quaternary resolvents
c [ternres-5] limit 38126593 with penalty 0 = 0 + 0
c [ternres-5] all 8405 free variables schedulable
c [ternres-5] 27 ternary resolvents (1 bin, 26 trn)
c [ternres-5] fully completed ternary resolution
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 92 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 8405 variables 100%
c [block-3] limit of 95316484 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 [cce-5] limit of 95316484 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 1 clauses out of 11 (9%) of length 19
c [cce-5-1] eliminated 1 clauses out of 35 (3%) of length 16
c [cce-5-1] eliminated 1 clauses out of 88 (1%) of length 14
c [cce-5-1] eliminated 4 clauses out of 94 (4%) of length 13
c [cce-5-1] eliminated 2 clauses out of 163 (1%) of length 12
c [cce-5-1] eliminated 3 clauses out of 235 (1%) of length 11
c [cce-5-1] eliminated 11 clauses out of 307 (4%) of length 10
c [cce-5-1] eliminated 9 clauses out of 375 (2%) of length 9
c [cce-5-1] eliminated 5 clauses out of 403 (1%) of length 8
c [cce-5-1] eliminated 8 clauses out of 412 (2%) of length 7
c [cce-5-1] eliminated 8 clauses out of 400 (2%) of length 6
c [cce-5-1] eliminated 8 clauses out of 2727 (0%) of length 5
c [cce-5-1] eliminated 13 clauses out of 4891 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 74 large clauses in 9989064 steps
c [cce-5-1] allowing another 4994532 steps for small clauses
c [cce-5-1] scheduling 31023 clauses = 28278 binary + 2745 ternary
c [cce-5-1] tried to eliminate 31023 small clauses 100%
c [cce-5-1] eliminated 161 binary clauses 1%
c [cce-5-1] eliminated 16 ternary clauses 1%
c [cce-5-1] eliminated 177 small clauses 1%
c [cce-5-1] eliminated 177 small clauses in 31269306 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 251 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 4942634 steps for small clauses
c [cce-5-2] scheduling 30846 clauses = 28117 binary + 2729 ternary
c [cce-5-2] tried to eliminate 30846 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 251 covered clauses in TOTAL during 2 rounds
c [cce-5] 251 < 1/100 * 43391 = 433 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 8405 variables 100%
c [elim-6] limit of 381265938 steps penalty 1 = 1 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 33 variables 0% in round 1 in 5712108 steps
c [elim-6-1] backward subsumption/strengthening limit 5712100
c [elim-6-1-1] backward checking 559 touched variables 7%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 7 clauses in 291265 steps
c [elim-6-1] rescheduled 41 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 84448 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 33 = 0% variables out of 8405 scheduled
c [elim-6] 33 < 1/100 * 8405 = 84 considered unsuccessful
c [bca-4] limit of 10000000 steps and 86758 added (scaled 2)
c [bca-4] 7967 out of 16746 literals actually usable 48%
c [bca-4] added 4 blocked clauses in 46915 steps
c [score-dist-8] active 8372 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-8] max exp 518, different 2 (0%)
c [score-dist-8] median active exp 518, avg 518.0
c [simplification-8] removed 33 variables 0.4% (8372 remain 27%)
c [simplification-8] removed 270 irredundant clauses 0.6% (43121 remain 46%)
c [simplification-8] maximum reduction of 1% = max (0%, 1%)
c [simplification-8] geometric conflict interval increment 25000 = 50000 / 2
c [simplification-8] new conflict interval 75000
c [simplification-8] penalized conflict interval 75000 = 1 * 75000
c [simplification-8] hard conflict limit 217506 (soft 180006 + delta 37500)
c [simplification-8] new conflict limit 180006 (hard 217506)
c 
c [simplification-9] limit 180006 conflicts (hard 217506) hit after 217506 conflicts
c [quatres-6] found 8993 quaternary clauses 55% in total
c [quatres-6-1] added 1 double-self-subsuming ternary resolvents
c [quatres-6-2] added 15 single-self-subsuming ternary resolvents
c [quatres-6-2] added 99 quaternary resolvents
c [ternres-6] limit 89070365 with penalty 0 = 0 + 0
c [ternres-6] all 8372 free variables schedulable
c [ternres-6] 85 ternary resolvents (2 bin, 83 trn)
c [ternres-6] fully completed ternary resolution
c [treelook-3] limit 2226759 penalty 2 = 2 + 0 boost 1
c [treelook-3] scheduled 16744 literals 100%
c [treelook-3] scheduling used 255033 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 2226759 penalty 2 = 2 + 0 boost 1
c [treelook-3] used 2232936 steps
c [treelook-3] 16302 literals remain 97%
c [treelook-3] 8368 variables remain to probed next time 100%
c [treelook-3] removed 4 variables, found 2420 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 370 transitive binary clauses
c [bca-5] limit of 10000000 steps and 86722 added (scaled 2)
c [bca-5] 7799 out of 16738 literals actually usable 47%
c [bca-5] added 3 blocked clauses in 67242 steps
c [sweep-6] limit 13360554 penalty 1 = 1 + 0
c [sweep-6-1] 159 pos 5.8% + 2559 neg 94.2% = 2718 sched 32.5% ret 5650
c [sweep-6-1] 13459280 steps 469 queries 60.50 avg class size
c [sweep-6-1] 1961 decisions 468 SAT calls 28.66 avg env size
c [sweep-6-1] 1511 variables remain 18% (6857 retained 82%)
c [sweep-6-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-6] removed 0 vars in TOTAL (1 rounds, 468 queries)
c [score-dist-9] active 8368 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-9] max exp 519, different 1 (0%)
c [score-dist-9] median active exp 519, avg 519.0
c [simplification-9] removed 4 variables 0.0% (8368 remain 27%)
c [simplification-9] removed 19 irredundant clauses 0.0% (43102 remain 46%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 75000
c [simplification-9] new conflict interval 150000
c [simplification-9] penalized conflict interval 150000 = 1 * 150000
c [simplification-9] hard conflict limit 442506 (soft 367506 + delta 75000)
c [simplification-9] new conflict limit 367506 (hard 442506)
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 1  717.1    8368    43102    337953   55578   1731  8786    8     8   28 100%   1018   -2    6    9   71%
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 SATISFIABLE
c
c bate: 0 basic ate = 0 trn 0% + 0 lrg 0% in 0 updates
c bcas: 5 count, 40 added (0 skipped), 235897 steps
c bkwd: tried 147364 clauses, 294459 lits, 2.00 lits/clause
c bkwd: checked 7577675 occs, 51.42 occs/clause, 25.73 occs/lit
c bkwd: subsumed 0 binary, 12 ternary, 193 large
c bkwd: strengthened 1 binary, 15 ternary (100% self), 3192 large (0% self)
c blkd: 3 bces, 10 removed, 557673 resolutions, 1442845 steps
c blkd: 704 blocking literals 1%, 1 pure
c bump: 341327 bumped seen, 1075669021 lits 3151.4 on average
c card: 3 count, 1 units, 23 am1, 5867639 steps
c card: 46 rescheduled, 395 eliminated, 68054 resolved, 593 subsumed
c card: 195 at-most-one constraints found, average size 3.00
c card: 195 at-most-one constraints used 100%, average size 3.00
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, 6806 eliminated, 6280 ate 92%, 526 abce 8%
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: 317354 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 42 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 25 decompositions, 1974 equivalent 6%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 354810 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 19052 eliminated 61%, 0 pure 0%
c elms: 17 rounds, 2.8 rounds/bve
c elms: 15736 small 83%, 3315 large 17%
c elms: 20675 tried small, 15736 succeeded 76%, 4939 failed 24%
c elms: 620 subsumed, 12526 strengthened, 93 blocked
c elms: 1256844 copies, 1596545 resolutions, 410849 ipos
c elms: 544645 subchks, 719355 strchks
c gaus: 3 extractions, 17490 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 0 binary and 2 ternary equations
c gaus: 0 gc, 4872294 steps, 2436147 extr 50%, 765824 elim 16%
c glue: 10.0 orig avg, 10.0 real avg, 2.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 7161 = 1704 simple 24% + 2205 trn 31% + 3252 lrg 45%, 378 sub 5%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 341327 clauses, 18.2 length
c lrnd: 6225706 lits = 189948015 orig - 183722309 removed 97%
c lrnd: 4924 uips 1%, 335592 flips 98%
c mins: 340810 mins 100%, 13 bin 0%, 504 size 0%
c mins: 205478435 poisoned searches, 1066416 hits, 1% hit rate
c mins: 394016617 used twice searches, 296331 hits, 0% hit rate
c move: moved 4999, 4873 bin 97%, 126 trn 3%
c otfs: 70 driving 27%, 191 restarting 73%
c otfs: str 261, 215 red 82%, 46 irr 18%
c otfs: str 261, 0 bin 0%, 9 trn 3%, 252 lrg 97%
c otfs: sub 5, 5 red 100%, 0 irr 0%
c otfs: sub 5, 0 bin 0%, 0 trn 0%, 5 lrg 100%
c phas: 1 computed, 9180 set, 0 pos (0%), 9180 neg (100%)
c prbs: 2 basic, 40435 probed, 1 failed, 0 lifted
c prbs: 3 simple, 85197 probed, 78 failed, 4991 eqs
c prbs: 3 treelook, 686 probed, 4 failed, 0 lifted
c prom: 0 locked 0% out of 1486317 tried
c prps: 1942221496 props, 5448 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 6 count, 4500 quat, 101 self1, 1 self2, 1 dup
c queu: 2 sorted, 354810 next (1015 steps 0.00)
c queu: 1075709692 enq (2420458715 steps 2.25), 1075669021 deq 100%
c redc: 1436 clauses 6%, 24175 tried 7%, 1 sat 0%
c redc: 4500 lits 2%, 192750 tried 0%, 1 sat 0%
c redc: 46 times jump level reduced, 1.9 levels on average
c reds: 0 count, 0.0 conflicts per reduce
c reds: 0 memlim 0%, 0 arith 0%
c reds: 0 collected 0%, 0 retired 0%
c rmbd: 67 removed, 63 red 94%
c rsts: 979 restarts 9%, 9950 skipped 91%
c rsts: 9950 saturating 100%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 9 count, 9 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 341327 count (489674 tried 1.4), 288261 sub out of 341069 (84.5%)
c swps: 6 count, 7 rounds, 3695 queries (527.9/round)
c swps: 3694 sat calls, 0 unsat (0.9% success rate)
c swps: 14146 decisions 3.8, 3444 conflicts 0.9
c swps; 115.2 avg class size, 28.2 avg environment size
c swps: 0 failed, 5 impls, 1 equivs
c swp0: 1229 type 0 queries, 54 unsat (4.4%), 1229 sat (100.0%)
c swp1: 2466 type 1 queries, 330 unsat (13.4%), 2465 sat (100.0%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 1392430 calls to obtain time
c tops: 2041 fixed 6%, 0 its, 0.00 confs/it
c trds: 6 transitive reductions, 1918 removed, 0 failed
c trds: 80554 nodes, 198744 edges, 12000275 steps
c trim: 3284172 words, 12.5 MB
c trnr: 6 count, 14 bin, 2278 trn, 9153396 steps
c unhd: 3 count, 4 rounds, 1713811 steps
c unhd: 2 non-trivial sccs of average size 2.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 325 tauts, 75 bin 23%, 16 trn 5%, 17 lrg 5%
c unhd: 325 tauts, 217 stamp 67%, 264 red 81%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 23144 str, 0 bin 0%, 8 trn 0%, 23136 lrg 100%, 22719 red 98%
c vars: 8368 remaining 27% and 23067 removed 73% out of 31435
c vars: 2041 fixed 6%, 19052 eliminated 61%, 1974 equivalent 6%
c vsts: 15080722919 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 7.8 search visits per propagation, 44390.7 per conflict
c wchs: 3152256426 pushed, 248103673 enlarged, 78 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         345569             0             0      32253090      21786348         33875
c 
c  0 0          9138   3         0   0<        0   0< 29207304  91< 19253625  88<    30322  90<    0.2
c  1 5          6400   2         0   0         0   0   1941589   6   1578151   7      1567   5     0.1
c  2 6         82740  24         0   0         0   0    682918   2    584829   3       962   3     1.5
c  3 9        215654  62<        0   0         0   0    372899   1    323621   1       712   2     5.7
c  4 14        31502   9         0   0         0   0     48189   0     45980   0       304   1     1.3
c  5 21          127   0         0   0         0   0       181   0       134   0         7   0     0.0
c  6 30            8   0         0   0         0   0        10   0         8   0         1   0     0.0
c 
c avg                  2.7           0.0           0.0           0.1           0.2           0.2
c std                  0.8           0.0           0.0           0.5           0.6           0.7
c 
c  241.774  34% bump
c    3.966   1% cce
c    3.230   0% sweep
c 
c    2.642 < 1% rest (below)
c 
c    1.593   0% elim
c    1.138   0% probe
c    0.473   0% transred
c    0.172   0% unhide
c    0.171   0% decide
c    0.138   0% gauss
c    0.135   0% card
c    0.122   0% block
c    0.122   0% bca
c    0.117   0% quatres
c    0.054   0% ternres
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.842   0% preprocessing     7%
c   10.803   2% inprocessing     93%
c ==================================
c   11.645   2% simplifying
c  705.463  98% search
c ==================================
c  717.110 100% all
c 
c        337953 conflicts,         471.3 confs/sec
c           188 ternaries,        1797.6 confs/ternary
c            21 binaries,        16093.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c           979 restarts,            1.4 rests/sec,    345.2 confs/restart
c        354810 decisions,         494.8 decis/sec,      1.0 decis/conflict
c    1942221496 propagations,  2708401.9 props/sec,   5474.0 props/decision
c 
c 717.1 seconds, 29.5 MB
c launch: done
