c launch: /data/cnf/sc2014/app/countbitssrl032.cnf.bz2
c host: atom14
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/countbitssrl032.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/countbitssrl032.cnf.bz2
c no embedded options
c found 'p cnf 18607 55724' header
c read 18607 variables, 55724 clauses, 130020 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=5
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 18605 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   18605    55722         0       0      0     0    0     0    3   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] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 2 variables
c [simpleprobe-1] all 18605 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 192 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 192 variables, found 105 hbrs, 37 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 192 units, 823 failed, 2136 tauts, 0 hbrs, 936 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 17679 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 11632 variables 66% in round 1 in 2845415 steps
c [elim-1-1] backward subsumption/strengthening limit 2845400
c [elim-1-1-1] backward checking 12570 touched variables 71%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 192 and strengthened 288 clauses in 940181 steps
c [elim-1-1] rescheduled 575 variables 3% by backward subsumption
c [elim-1-2] eliminated 24 variables 0% in round 2 in 222559 steps
c [elim-1-2] backward subsumption/strengthening limit 222500
c [elim-1-2-1] backward checking 247 touched variables 1%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 10 and strengthened 39 clauses in 160764 steps
c [elim-1-2] rescheduled 116 variables 1% by backward subsumption
c [elim-1-3] eliminated 18 variables 0% in round 3 in 51417 steps
c [elim-1-3] backward subsumption/strengthening limit 51400
c [elim-1-3-1] backward checking 119 touched variables 1%
c [elim-1-3-1] incomplete backward checking 0 remain 0%
c [elim-1-3] subsumed 2 and strengthened 23 clauses in 51401 steps
c [elim-1] incomplete 25 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 11706 = 66% variables out of 17679 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 27681 negative 92.5% of 29923 except 2242 7.5%
c [phase-count-1] 25737 positive 86.0% of 29923 except 4186 14.0%
c [phase-1] phase bias: 1103 positive 18%, 4870 negative 82%
c [sort-queue-1] sorted 5973 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 5973 (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 12632 variables 67.9% (5973 remain 32%)
c [simplification-1] removed 25799 irredundant clauses 46.3% (29923 remain 54%)
c [simplification-1] maximum reduction of 68% = max (68%, 46%)
c [simplification-1] large reduction 68% >= 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  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    0.5    5972    29923         6       4      0    30    0     0    4  81%      0    0    1    0 25253%
c i    0.5    5966    29923         7       4      0    30    0     0    4  81%      0    0    1    0 25155%
c i    0.5    5965    29923        13       4      0    35    0     0    4  81%      0    0    1    0 24589%
c i    0.5    5964    29923        14       4      0    35    0     0    4  81%      0    0    1    0 24493%
c i    0.5    5961    29923        15       4      0    35    0     0    4  81%      0    0    1    0 24398%
c i    0.5    5960    29923        16       4      0    35    0     0    4  81%      0    0    1    0 24303%
c i    0.5    5959    29923        19       4      0    36    0     0    4  80%      0    0    1    0 24120%
c i    0.5    5948    29923        34      11      4    38    0     0    5  71%      0    0    1    0 23134%
c i    0.5    5933    29923        37      11      4    40    0     0    5  71%      0    0    1    0 22884%
c i    0.5    5919    29923        41      13      5    40    0     0    5  69%      0    0    1    0 22622%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 297 variables
c [simpleprobe-2] all 5676 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 474 variables
c [simpleprobe-2] 265 variables remain 5% (4937 retained 95%)
c [simpleprobe-2] removed 474 variables, found 1801 hbrs, 101 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 10404 literals 100%
c [treelook-1] scheduling used 109931 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 320585 steps
c [treelook-1] 10364 literals remain 100%
c [treelook-1] 5202 variables remain to probed next time 100%
c [decomp-5] removed 29 variables
c [treelook-1] removed 29 variables, found 550 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 876 probes remain 17% after last round
c [basicprobe-1-0] 55 units = 42 failed (76%) + 13 lifted (24%)
c [basicprobe-1-0] removed 148 variables, found 2009 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 34 failed, 1169 tauts, 0 hbrs, 2029 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 4996 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 518 variables 10% in round 1 in 2837454 steps
c [elim-2-1] backward subsumption/strengthening limit 2837400
c [elim-2-1-1] backward checking 1965 touched variables 39%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 46 and strengthened 149 clauses in 444807 steps
c [elim-2-1] rescheduled 382 variables 8% by backward subsumption
c [elim-2-2] eliminated 43 variables 1% in round 2 in 695139 steps
c [elim-2-2] backward subsumption/strengthening limit 695100
c [elim-2-2-1] backward checking 266 touched variables 5%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 14 and strengthened 37 clauses in 138103 steps
c [elim-2-2] rescheduled 107 variables 2% by backward subsumption
c [elim-2-3] eliminated 11 variables 0% in round 3 in 266272 steps
c [elim-2-3] backward subsumption/strengthening limit 266200
c [elim-2-3-1] backward checking 60 touched variables 1%
c [elim-2-3-1] fully completed backward checking in 1 rounds
c [elim-2-3] subsumed 1 and strengthened 7 clauses in 42777 steps
c [elim-2] incomplete 18 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 584 = 12% variables out of 4996 scheduled
c [elim-2] considered successful since not run to completion yet
c [sort-queue-2] sorted 337 enqueued variables after 41 conflicts
c [score-dist-2] active 4075 (92%), one 0 (0%), zero 337 (8%)
c [score-dist-2] max exp 513, different 13 (3%)
c [score-dist-2] median active exp 504, avg 504.2
c [simplification-2] removed 1506 variables 25.4% (4412 remain 24%)
c [simplification-2] removed 6364 irredundant clauses 21.3% (23559 remain 42%)
c [simplification-2] maximum reduction of 25% = max (25%, 21%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1050 (hard 11000)
c [simplification-2] new iteration interval 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    0.9    4411    23558       223     164      6   899    0     2    5  16%      0    2    4    0 16206%
c i    0.9    4410    23558       228     164      7   900    0     2    5  16%      0    2    4    0 16036%
c i    0.9    4404    23558       230     165      7   900    0     2    5  16%      0    2    4    0 15924%
c i    0.9    4403    23558       231     165      7   900    0     2    5  16%      0    2    4    0 15862%
c i    0.9    4400    23558       235     165      8   902    0     2    5  16%      0    2    4    0 15641%
c i    0.9    4399    23558       240     165     10   904    0     2    5  16%      0    2    4    0 15378%
c i    0.9    4398    23558       241     165     10   904    0     2    5  16%      0    2    4    0 15318%
c i    0.9    4397    23558       242     165     10   904    0     2    5  16%      0    2    4    0 15258%
c i    0.9    4395    23558       247     166     11   905    0     2    5  16%      0    2    4    0 15042%
c i    0.9    4394    23558       279     188     16   908    0     3    5  15%      0    3    4    0 14661%
c i    0.9    4371    23558       280     188     16   908    0     3    5  15%      0    3    4    0 14604%
c i    0.9    4368    23558       281     188     16   908    0     3    5  15%      0    3    4    0 14547%
c i    0.9    4367    23558       283     188     16   909    0     3    5  15%      0    3    4    0 14440%
c i    0.9    4365    23558       284     188     16   909    0     3    5  15%      0    3    4    0 14384%
c i    0.9    4363    23558       285     188     16   909    0     3    5  15%      0    3    4    0 14328%
c i    0.9    4357    23558       289     188     18   910    0     3    5  15%      0    3    4    0 14137%
c 
c [simplification-3] limit 1140 conflicts (hard 11000) hit after 1141 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 82 at-most-one constraints of average size 3.0
c [card-2] found 5 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 87 out of 87 constraints (100%) meet size limits
c [card-2] found 1 units
c [card-2] no units found
c [card-2] generated 35 at-most-one constraints, 24 used 69%
c [card-2] exported 34 binary clauses, 1.4 per/constraint
c [decomp-6] removed 334 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 8156 literals 100%
c [treelook-2] scheduling used 98038 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 348917 steps
c [treelook-2] 8087 literals remain 99%
c [treelook-2] 4078 variables remain to probed next time 100%
c [decomp-7] removed 1 variables
c [treelook-2] removed 1 variables, found 3345 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 12 failed, 62 tauts, 0 hbrs, 1151 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 4062 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 157 variables 4% in round 1 in 4559460 steps
c [elim-3-1] backward subsumption/strengthening limit 4559400
c [elim-3-1-1] backward checking 809 touched variables 20%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 8 and strengthened 30 clauses in 345556 steps
c [elim-3-1] rescheduled 90 variables 2% by backward subsumption
c [elim-3-2] eliminated 7 variables 0% in round 2 in 374437 steps
c [elim-3-2] backward subsumption/strengthening limit 374400
c [elim-3-2-1] backward checking 68 touched variables 2%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 2 and strengthened 3 clauses in 49882 steps
c [elim-3-2] rescheduled 8 variables 0% by backward subsumption
c [elim-3-3] eliminated 1 variables 0% in round 3 in 5659 steps
c [elim-3-3] backward subsumption/strengthening limit 5600
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 1 and strengthened 7 clauses in 5601 steps
c [elim-3] incomplete 9 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 172 = 4% variables out of 4062 scheduled
c [elim-3] considered successful since not run to completion yet
c [score-dist-3] active 3890 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-3] max exp 800, different 64 (8%)
c [score-dist-3] median active exp 797, avg 792.0
c [simplification-3] removed 454 variables 10.5% (3890 remain 21%)
c [simplification-3] removed 1530 irredundant clauses 6.5% (22028 remain 40%)
c [simplification-3] maximum reduction of 10% = max (10%, 6%)
c [simplification-3] large reduction 10% >= 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 13141 (soft 3141 + delta 10000)
c [simplification-3] new conflict limit 3141 (hard 13141)
c 
c [simplification-4] limit 3141 conflicts (hard 13141) hit after 3141 conflicts
c [decomp-8] removed 47 variables
c [basicprobe-2] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-2-0] 748 sched 20%, 12 failed, 0 lifted, 359 hbrs
c [decomp-9] removed 60 variables
c [basicprobe-2-1] 1955 sched 52%, 6 failed, 0 lifted, 106 hbrs
c [decomp-10] removed 15 variables
c [basicprobe-2-2] 655 probes remain 17% after last round
c [basicprobe-2-2] 23 units = 22 failed (96%) + 1 lifted (4%)
c [basicprobe-2-2] removed 79 variables, found 486 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 0 failed, 611 tauts, 0 hbrs, 4010 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 3764 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 60 variables 2% in round 1 in 4672841 steps
c [elim-4-1] backward subsumption/strengthening limit 4672800
c [elim-4-1-1] backward checking 432 touched variables 11%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 6 and strengthened 24 clauses in 284940 steps
c [elim-4-1] rescheduled 67 variables 2% by backward subsumption
c [elim-4-2] eliminated 2 variables 0% in round 2 in 465339 steps
c [elim-4-2] backward subsumption/strengthening limit 465300
c [elim-4-2-1] backward checking 21 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 0 and strengthened 0 clauses in 67397 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 62 = 2% variables out of 3764 scheduled
c [score-dist-4] active 3702 (100%), one 0 (0%), zero 0 (0%)
c [score-dist-4] max exp 820, different 111 (14%)
c [score-dist-4] median active exp 802, avg 790.6
c [simplification-4] removed 188 variables 4.8% (3702 remain 20%)
c [simplification-4] removed 584 irredundant clauses 2.7% (21444 remain 38%)
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 15141 (soft 5141 + delta 10000)
c [simplification-4] new conflict limit 5141 (hard 15141)
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    2.0    3701    21444      4794    3884    166  1474    5    25    5  20%     53   24    7    0 1319%
c i    2.0    3700    21444      4797    3884    166  1476    5    25    5  20%     53   24    6    0 1305%
c 
c [simplification-5] limit 5144 conflicts (hard 15141) hit after 5145 conflicts
c [quatres-1] found 6506 quaternary clauses 62% in total
c [quatres-1-2] added 10 single-self-subsuming ternary resolvents
c [quatres-1-2] added 166 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 3700 free variables schedulable
c [ternres-1] 2526 ternary resolvents (17 bin, 2509 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4840 xors of average arity 3.0
c [gauss-1] connected 14396 occurrences of 845 variables (average 17.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-11] removed 30 variables
c [gauss-1] exported 0 unary, 6 binary and 60 ternary equations
c [simpleprobe-3] 87 schedulable variables 2%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [decomp-13] removed 9 variables
c [simpleprobe-3] 77 variables remain 2% (3584 retained 98%)
c [simpleprobe-3] removed 9 variables, found 2067 hbrs, 0 units
c [transred-1] limit 140172 with penalty 0 = 0 + 0
c [transred-1] removed 120 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 3661 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 111 blocked clauses
c [block-1] 111 < 1/100 * 21152 = 211 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 32
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 31
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 30
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 28
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 21
c [cce-1-1] eliminated 1 clauses out of 3 (33%) of length 20
c [cce-1-1] eliminated 3 clauses out of 4 (75%) of length 19
c [cce-1-1] eliminated 3 clauses out of 5 (60%) of length 14
c [cce-1-1] eliminated 2 clauses out of 3 (67%) of length 13
c [cce-1-1] eliminated 2 clauses out of 5 (40%) of length 12
c [cce-1-1] eliminated 1 clauses out of 1 (100%) of length 11
c [cce-1-1] eliminated 4 clauses out of 13 (31%) of length 7
c [cce-1-1] eliminated 6 clauses out of 156 (4%) of length 6
c [cce-1-1] eliminated 74 clauses out of 2391 (3%) of length 5
c [cce-1-1] eliminated 122 clauses out of 6258 (2%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 224 large clauses in 16308481 steps
c [cce-1-1] allowing another 8154240 steps for small clauses
c [cce-1-1] scheduling 8065 clauses = 3922 binary + 4143 ternary
c [cce-1-1] tried to eliminate 8065 small clauses 100%
c [cce-1-1] eliminated 31 binary clauses 1%
c [cce-1-1] eliminated 71 ternary clauses 2%
c [cce-1-1] eliminated 102 small clauses 1%
c [cce-1-1] eliminated 102 small clauses in 24362687 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] completed small and large (ATE)
c [cce-1-1] eliminated 326 covered clauses in round 1
c [cce-1-2] eliminated 7 clauses out of 2317 (0%) of length 5
c [cce-1-2] eliminated 3 clauses out of 6136 (0%) of length 4
c [cce-1-2] incomplete large round (ABCE)
c [cce-1-2] eliminated 10 large clauses in 5637348 steps
c [cce-1-2] allowing another 2818674 steps for small clauses
c [cce-1-2] scheduling 7963 clauses = 3891 binary + 4072 ternary
c [cce-1-2] tried to eliminate 1158 small clauses 15%
c [cce-1-2] eliminated 1 ternary clauses 0%
c [cce-1-2] eliminated 1 small clauses 0%
c [cce-1-2] eliminated 1 small clauses in 5637354 steps
c [cce-1-2] incomplete small round (ABCE)
c [cce-1-2] eliminated 11 covered clauses in round 2
c [cce-1] eliminated 337 covered clauses in TOTAL during 2 rounds
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 3661 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 51 variables 1% in round 1 in 4670447 steps
c [elim-5-1] backward subsumption/strengthening limit 4670400
c [elim-5-1-1] backward checking 339 touched variables 9%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 2 and strengthened 12 clauses in 287812 steps
c [elim-5-1] rescheduled 45 variables 1% by backward subsumption
c [elim-5-2] eliminated 3 variables 0% in round 2 in 583348 steps
c [elim-5-2] backward subsumption/strengthening limit 583300
c [elim-5-2-1] backward checking 42 touched variables 1%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 0 and strengthened 6 clauses in 77341 steps
c [elim-5-2] rescheduled 14 variables 0% by backward subsumption
c [elim-5-3] no variable eliminated in round 3 in 230052 steps
c [elim-5] fully completed in 3 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 54 = 1% variables out of 3661 scheduled
c [bca-1] limit of 10000000 steps and 41560 added (scaled 2)
c [bca-1] 1682 out of 7216 literals actually usable 23%
c [bca-1] added 0 blocked clauses in 7792 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1584 pos 43.9% + 2023 neg 56.1% = 3607 sched 100.0% ret 0
c [sweep-1-1] 1017354 steps 60 queries 157.80 avg class size
c [sweep-1-1] 1087 decisions 60 SAT calls 42.53 avg env size
c [sweep-1-1] 1990 variables remain 55% (1617 retained 45%)
c [decomp-14] removed 1 variables
c [sweep-1-1] removed 1 vars (0 failed, 0 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 1 vars in TOTAL (1 rounds, 59 queries)
c [sort-queue-3] sorted 1 enqueued variables after 5145 conflicts
c [score-dist-5] active 3605 (100%), one 1 (0%), zero 0 (0%)
c [score-dist-5] max exp 892, different 101 (11%)
c [score-dist-5] median active exp 838, avg 847.4
c [simplification-5] removed 94 variables 2.5% (3606 remain 19%)
c [simplification-5] removed 914 irredundant clauses 4.3% (20530 remain 37%)
c [simplification-5] maximum reduction of 4% = max (3%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 4000
c [simplification-5] penalized conflict interval 4000 = 1 * 4000
c [simplification-5] hard conflict limit 19145 (soft 9145 + delta 10000)
c [simplification-5] new conflict limit 9145 (hard 19145)
c 
c [simplification-6] limit 9145 conflicts (hard 19145) hit after 9145 conflicts
c [quatres-2] found 6945 quaternary clauses 58% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-1] added 3 double-self-subsuming ternary resolvents
c [quatres-2-2] added 38 single-self-subsuming ternary resolvents
c [quatres-2-2] added 203 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3606 free variables schedulable
c [ternres-2] 808 ternary resolvents (5 bin, 803 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 40 at-most-one constraints of average size 3.0
c [card-3] found 16 at-most-two constraints of average size 4.0
c [card-3] using previous limit 500000 for elimination
c [card-3] 56 out of 56 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 19 at-most-one constraints, 4 used 21%
c [card-3] exported 4 binary clauses, 1.0 per/constraint
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 5086 xors of average arity 3.0
c [gauss-2] connected 15240 occurrences of 785 variables (average 19.4)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-15] removed 6 variables
c [gauss-2] exported 0 unary, 2 binary and 7 ternary equations
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 7200 literals 100%
c [treelook-3] scheduling used 128927 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 326498 steps
c [treelook-3] 7183 literals remain 100%
c [treelook-3] 3600 variables remain to probed next time 100%
c [treelook-3] removed 0 variables, found 2166 hbrs
c [unhide-5] limit 50000 with penalty 1 = 1 + 0
c [unhide-5-5] 0 units, 0 failed, 44 tauts, 0 hbrs, 7071 literals
c [transred-2] limit 300133 with penalty 0 = 0 + 0
c [transred-2] removed 187 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 16
c [cce-2-1] eliminated 1 clauses out of 3 (33%) of length 15
c [cce-2-1] eliminated 1 clauses out of 2 (50%) of length 14
c [cce-2-1] eliminated 1 clauses out of 4 (25%) of length 13
c [cce-2-1] eliminated 1 clauses out of 7 (14%) of length 9
c [cce-2-1] eliminated 1 clauses out of 163 (1%) of length 6
c [cce-2-1] eliminated 12 clauses out of 2291 (1%) of length 5
c [cce-2-1] eliminated 19 clauses out of 6223 (0%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 37 large clauses in 15237076 steps
c [cce-2-1] allowing another 7618538 steps for small clauses
c [cce-2-1] scheduling 7724 clauses = 3788 binary + 3936 ternary
c [cce-2-1] tried to eliminate 7724 small clauses 100%
c [cce-2-1] eliminated 5 binary clauses 0%
c [cce-2-1] eliminated 7 ternary clauses 0%
c [cce-2-1] eliminated 12 small clauses 0%
c [cce-2-1] eliminated 12 small clauses in 22852751 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] eliminated 49 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 3573646 steps for small clauses
c [cce-2-2] scheduling 7712 clauses = 3783 binary + 3929 ternary
c [cce-2-2] tried to eliminate 1670 small clauses 22%
c [cce-2-2] incomplete small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 49 covered clauses in TOTAL during 2 rounds
c [cce-2] 49 < 1/100 * 20507 = 205 considered unsuccessful
c [elim-6] scheduling all variables this time
c [elim-6] scheduled 3600 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 14 variables 0% in round 1 in 4640192 steps
c [elim-6-1] backward subsumption/strengthening limit 4640100
c [elim-6-1-1] backward checking 158 touched variables 4%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 0 and strengthened 2 clauses in 119051 steps
c [elim-6-1] rescheduled 10 variables 0% by backward subsumption
c [elim-6-2] no variable eliminated in round 2 in 291232 steps
c [elim-6] fully completed in 2 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 14 = 0% variables out of 3600 scheduled
c [elim-6] 14 < 1/100 * 3600 = 36 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1390 pos 70.3% + 586 neg 29.7% = 1976 sched 55.1% ret 1610
c [sweep-2-1] 1011009 steps 50 queries 133.88 avg class size
c [sweep-2-1] 1425 decisions 48 SAT calls 58.69 avg env size
c [sweep-2-1] 1299 variables remain 36% (2287 retained 64%)
c [decomp-18] removed 7 variables
c [sweep-2-1] removed 7 vars (0 failed, 2 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 7 vars in TOTAL (1 rounds, 49 queries)
c [sort-queue-4] sorted 20 enqueued variables after 9145 conflicts
c [score-dist-6] active 3559 (99%), one 20 (1%), zero 0 (0%)
c [score-dist-6] max exp 521, different 96 (18%)
c [score-dist-6] median active exp 436, avg 447.9
c [simplification-6] removed 27 variables 0.7% (3579 remain 19%)
c [simplification-6] removed 139 irredundant clauses 0.7% (20391 remain 37%)
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 14000
c [simplification-6] penalized conflict interval 14000 = 1 * 14000
c [simplification-6] hard conflict limit 33145 (soft 23145 + delta 10000)
c [simplification-6] new conflict limit 23145 (hard 33145)
c 
c [simplification-7] limit 23145 conflicts (hard 33145) hit after 23145 conflicts
c [quatres-3] found 7621 quaternary clauses 48% in total
c [quatres-3-1] added 4 double-self-subsuming ternary resolvents
c [quatres-3-2] added 48 single-self-subsuming ternary resolvents
c [quatres-3-2] added 155 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3579 free variables schedulable
c [ternres-3] 615 ternary resolvents (3 bin, 612 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 5095 xors of average arity 3.0
c [gauss-3] connected 15281 occurrences of 767 variables (average 19.9)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 3 ternary equations
c [decomp-19] removed 1 variables
c [basicprobe-3] limit 5200194 penalty 0 = 0 + 0
c [basicprobe-3-0] 683 sched 19%, 3 failed, 0 lifted, 179 hbrs
c [decomp-20] removed 3 variables
c [basicprobe-3-1] 1861 sched 52%, 1 failed, 0 lifted, 238 hbrs
c [decomp-21] removed 1 variables
c [basicprobe-3-2] 1850 sched 52%, 0 failed, 0 lifted, 13 hbrs
c [basicprobe-3-3] 1850 sched 52%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-3-4] 1556 probes remain 44% after last round
c [basicprobe-3-4] 4 units = 4 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 4 variables, found 431 hbrs
c [bate-1] eliminated 5 asymmetric tautologies during probing
c [transred-3] limit 1040038 with penalty 0 = 0 + 0
c [transred-3] removed 275 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3574 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 1 blocked clauses
c [block-2] 1 < 1/100 * 20358 = 203 considered unsuccessful
c [bca-2] limit of 10000000 steps and 41214 added (scaled 2)
c [bca-2] 703 out of 7150 literals actually usable 10%
c [bca-2] added 0 blocked clauses in 22654 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 906 pos 70.0% + 388 neg 30.0% = 1294 sched 36.2% ret 2280
c [sweep-3-1] 1475819 steps 20 queries 156.80 avg class size
c [sweep-3-1] 716 decisions 19 SAT calls 145.74 avg env size
c [sweep-3-1] 1146 variables remain 32% (2428 retained 68%)
c [decomp-24] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 19 queries)
c [sort-queue-5] sorted 39 enqueued variables after 23145 conflicts
c [score-dist-7] active 3534 (99%), one 39 (1%), zero 0 (0%)
c [score-dist-7] max exp 732, different 119 (16%)
c [score-dist-7] median active exp 698, avg 693.6
c [simplification-7] removed 6 variables 0.2% (3573 remain 19%)
c [simplification-7] removed 34 irredundant clauses 0.2% (20357 remain 37%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 20000
c [simplification-7] new conflict interval 34000
c [simplification-7] penalized conflict interval 34000 = 1 * 34000
c [simplification-7] hard conflict limit 74145 (soft 57145 + delta 17000)
c [simplification-7] new conflict limit 57145 (hard 74145)
c 
c [simplification-8] limit 57145 conflicts (hard 74145) hit after 57145 conflicts
c [quatres-4] found 8289 quaternary clauses 38% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 2 double-self-subsuming ternary resolvents
c [quatres-4-2] added 35 single-self-subsuming ternary resolvents
c [quatres-4-2] added 104 quaternary resolvents
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 3573 free variables schedulable
c [ternres-4] 407 ternary resolvents (7 bin, 400 trn)
c [ternres-4] fully completed ternary resolution
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] extracted 5128 xors of average arity 3.0
c [gauss-4] connected 15385 occurrences of 769 variables (average 20.0)
c [gauss-4] limit 2000000 penalty 0 = 0 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-4] 77 schedulable variables 2%
c [simpleprobe-4] limit 15353736 penalty 0 = 0 + 0
c [decomp-26] removed 10 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 10 variables, found 2043 hbrs, 1 units
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 242 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 19
c [cce-3-1] eliminated 1 clauses out of 4 (25%) of length 17
c [cce-3-1] eliminated 1 clauses out of 3 (33%) of length 14
c [cce-3-1] eliminated 2 clauses out of 3 (67%) of length 13
c [cce-3-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-3-1] eliminated 1 clauses out of 9 (11%) of length 7
c [cce-3-1] eliminated 2 clauses out of 167 (1%) of length 6
c [cce-3-1] eliminated 11 clauses out of 2255 (0%) of length 5
c [cce-3-1] eliminated 18 clauses out of 6181 (0%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 38 large clauses in 15000007 steps
c [cce-3-1] allowing another 7500003 steps for small clauses
c [cce-3-1] scheduling 7893 clauses = 3892 binary + 4001 ternary
c [cce-3-1] tried to eliminate 4656 small clauses 59%
c [cce-3-1] eliminated 12 binary clauses 0%
c [cce-3-1] eliminated 183 ternary clauses 5%
c [cce-3-1] eliminated 195 small clauses 2%
c [cce-3-1] eliminated 195 small clauses in 15000101 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 233 covered clauses in round 1
c [cce-3] eliminated 233 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 3563 variables 100%
c [elim-7] limit of 38384341 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 37 variables 1% in round 1 in 4691408 steps
c [elim-7-1] backward subsumption/strengthening limit 4691400
c [elim-7-1-1] backward checking 247 touched variables 7%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 9 clauses in 114293 steps
c [elim-7-1] rescheduled 53 variables 1% by backward subsumption
c [elim-7-2] eliminated 2 variables 0% in round 2 in 392154 steps
c [elim-7-2] backward subsumption/strengthening limit 392100
c [elim-7-2-1] backward checking 25 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 1 clauses in 52476 steps
c [elim-7-2] rescheduled 5 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 193616 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 39 = 1% variables out of 3563 scheduled
c [sweep-4] limit 1151530 penalty 0 = 0 + 0
c [sweep-4-1] 681 pos 61.0% + 435 neg 39.0% = 1116 sched 31.7% ret 2408
c [sweep-4-1] 1353173 steps 8 queries 241.62 avg class size
c [sweep-4-1] 499 decisions 7 SAT calls 323.00 avg env size
c [sweep-4-1] 1090 variables remain 31% (2434 retained 69%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 7 queries)
c [sort-queue-6] sorted 97 enqueued variables after 57145 conflicts
c [score-dist-8] active 3427 (97%), one 97 (3%), zero 0 (0%)
c [score-dist-8] max exp 694, different 110 (16%)
c [score-dist-8] median active exp 643, avg 638.5
c [simplification-8] removed 49 variables 1.4% (3524 remain 19%)
c [simplification-8] removed 400 irredundant clauses 2.0% (19957 remain 36%)
c [simplification-8] maximum reduction of 2% = max (1%, 2%)
c [simplification-8] geometric conflict interval increment 11333 = 34000 / 3
c [simplification-8] new conflict interval 45333
c [simplification-8] penalized conflict interval 45333 = 1 * 45333
c [simplification-8] hard conflict limit 125144 (soft 102478 + delta 22666)
c [simplification-8] new conflict limit 102478 (hard 125144)
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 -   27.5    3524    19957     76146   29275   5111  7927   11    32   14  34%    673   10   10    7  146%
c 
c [simplification-9] limit 102478 conflicts (hard 125144) hit after 102479 conflicts
c [quatres-5] found 8602 quaternary clauses 33% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-1] added 2 double-self-subsuming ternary resolvents
c [quatres-5-2] added 25 single-self-subsuming ternary resolvents
c [quatres-5-2] added 98 quaternary resolvents
c [ternres-5] limit 8364422 with penalty 0 = 0 + 0
c [ternres-5] all 3524 free variables schedulable
c [ternres-5] 311 ternary resolvents (4 bin, 307 trn)
c [ternres-5] fully completed ternary resolution
c [unhide-6] limit 418221 with penalty 2 = 2 + 0
c [unhide-6-6] 0 units, 0 failed, 3981 tauts, 0 hbrs, 181413 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 146 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 418221100 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 3 (33%) of length 25
c [cce-4-1] eliminated 4 clauses out of 136 (3%) of length 6
c [cce-4-1] eliminated 5 clauses out of 2061 (0%) of length 5
c [cce-4-1] eliminated 18 clauses out of 6225 (0%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 28 large clauses in 14905114 steps
c [cce-4-1] allowing another 7452557 steps for small clauses
c [cce-4-1] scheduling 7674 clauses = 3889 binary + 3785 ternary
c [cce-4-1] tried to eliminate 7674 small clauses 100%
c [cce-4-1] eliminated 26 binary clauses 1%
c [cce-4-1] eliminated 111 ternary clauses 3%
c [cce-4-1] eliminated 137 small clauses 2%
c [cce-4-1] eliminated 137 small clauses in 31356808 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 165 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 7309874 steps for small clauses
c [cce-4-2] scheduling 7537 clauses = 3863 binary + 3674 ternary
c [cce-4-2] tried to eliminate 7537 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 165 covered clauses in TOTAL during 2 rounds
c [cce-4] 165 < 1/100 * 19957 = 199 considered unsuccessful
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 3524 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 3345768840 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 18 variables 1% in round 1 in 4377235 steps
c [elim-8-1] backward subsumption/strengthening limit 4377200
c [elim-8-1-1] backward checking 201 touched variables 6%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 0 and strengthened 3 clauses in 89347 steps
c [elim-8-1] rescheduled 10 variables 0% by backward subsumption
c [elim-8-2] no variable eliminated in round 2 in 172816 steps
c [elim-8] fully completed in 2 rounds
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 18 = 1% variables out of 3524 scheduled
c [elim-8] 18 < 1/100 * 3524 = 35 considered unsuccessful
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 25093260 penalty 0 = 0 + 0
c [sweep-5-1] 717 pos 66.3% + 365 neg 33.7% = 1082 sched 30.9% ret 2424
c [sweep-5-1] 8909654 steps 115 queries 21.21 avg class size
c [sweep-5-1] 3994 decisions 110 SAT calls 111.64 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-29] removed 12 variables
c [sweep-5-1] removed 12 vars (0 failed, 5 eqs, 11 impls)
c [sweep-5-2] 1636 pos 46.8% + 1858 neg 53.2% = 3494 sched 100.0% ret 0
c [sweep-5-2] 13117244 steps 180 queries 38.32 avg class size
c [sweep-5-2] 5209 decisions 167 SAT calls 120.90 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-30] removed 16 variables
c [sweep-5-2] removed 16 vars (0 failed, 20 eqs, 20 impls)
c [sweep-5-3] 1631 pos 46.9% + 1847 neg 53.1% = 3478 sched 100.0% ret 0
c [sweep-5-3] 3095606 steps 16 queries 356.38 avg class size
c [sweep-5-3] 1163 decisions 15 SAT calls 252.20 avg env size
c [sweep-5-3] 2857 variables remain 82% (621 retained 18%)
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 28 vars in TOTAL (3 rounds, 308 queries)
c [sort-queue-7] sorted 99 enqueued variables after 102479 conflicts
c [score-dist-9] active 3379 (97%), one 99 (3%), zero 0 (0%)
c [score-dist-9] max exp 769, different 224 (29%)
c [score-dist-9] median active exp 690, avg 657.8
c [simplification-9] removed 46 variables 1.3% (3478 remain 19%)
c [simplification-9] removed 197 irredundant clauses 1.0% (19760 remain 35%)
c [simplification-9] maximum reduction of 1% = max (1%, 1%)
c [simplification-9] geometric conflict interval increment 22666 = 45333 / 2
c [simplification-9] new conflict interval 67999
c [simplification-9] penalized conflict interval 67999 = 1 * 67999
c [simplification-9] hard conflict limit 204477 (soft 170478 + delta 33999)
c [simplification-9] new conflict limit 170478 (hard 204477)
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 -   46.2    3478    19760    119765   37952   5335  4788   11    28   15  37%    844    2   12    9  134%
c i   49.9    3477    19760    134179   51321   5353  4789   10    29   13  35%    879    3   10    9  109%
c -   59.7    3477    19760    158443   43875   5384  4790   12    27   17  43%   -494    0   13    9  133%
c 
c [simplification-10] limit 170478 conflicts (hard 204477) hit after 185010 conflicts
c [quatres-6] found 9134 quaternary clauses 28% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 59 single-self-subsuming ternary resolvents
c [quatres-6-2] added 165 quaternary resolvents
c [ternres-6] limit 16727071 with penalty 0 = 0 + 0
c [ternres-6] all 3477 free variables schedulable
c [ternres-6] 676 ternary resolvents (10 bin, 666 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 1045441 penalty 3 = 3 + 0
c [card-4] found 102 at-most-one constraints of average size 3.0
c [card-4] found 37 at-most-two constraints of average size 4.0
c [card-4] using previous limit 1045441 for elimination
c [card-4] 139 out of 139 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-5] limit 1672707 penalty 1 = 1 + 0
c [gauss-5] extracted 4996 xors of average arity 3.0
c [gauss-5] connected 14968 occurrences of 750 variables (average 20.0)
c [gauss-5] limit 1672707 penalty 1 = 1 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 4 ternary equations
c [decomp-32] removed 2 variables
c [treelook-4] limit 836353 penalty 1 = 1 + 0 boost 1
c [treelook-4] scheduled 6950 literals 100%
c [treelook-4] scheduling used 262902 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 836353 penalty 1 = 1 + 0 boost 1
c [treelook-4] used 842571 steps
c [treelook-4] 6868 literals remain 99%
c [treelook-4] 3475 variables remain to probed next time 100%
c [decomp-33] removed 1 variables
c [treelook-4] removed 1 variables, found 3205 hbrs
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 434 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3474 variables 100%
c [block-3] limit of 41817678 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 7 blocked clauses
c [block-3] 7 < 1/100 * 19715 = 197 considered unsuccessful
c [bca-3] limit of 10000000 steps and 39916 added (scaled 2)
c [bca-3] 844 out of 6950 literals actually usable 12%
c [bca-3] added 2 blocked clauses in 71319 steps
c [sweep-6] limit 5018121 penalty 0 = 0 + 0
c [sweep-6-1] 1546 pos 54.2% + 1308 neg 45.8% = 2854 sched 82.2% ret 620
c [sweep-6-1] 5465541 steps 33 queries 153.21 avg class size
c [sweep-6-1] 1397 decisions 32 SAT calls 211.44 avg env size
c [sweep-6-1] 2189 variables remain 63% (1285 retained 37%)
c [decomp-34] removed 1 variables
c [sweep-6-1] removed 1 vars (0 failed, 2 eqs, 0 impls)
c [sweep-6] 1 < 1/1000 * 3474 = 3 considered unsuccessful
c [sweep-6] removed 1 vars in TOTAL (1 rounds, 32 queries)
c [sort-queue-8] sorted 293 enqueued variables after 185010 conflicts
c [score-dist-10] active 3180 (92%), one 293 (8%), zero 0 (0%)
c [score-dist-10] max exp 572, different 138 (24%)
c [score-dist-10] median active exp 518, avg 497.5
c [simplification-10] removed 4 variables 0.1% (3473 remain 19%)
c [simplification-10] removed 52 irredundant clauses 0.3% (19708 remain 35%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 67999
c [simplification-10] new conflict interval 135998
c [simplification-10] penalized conflict interval 135998 = 1 * 135998
c [simplification-10] hard conflict limit 389007 (soft 321008 + delta 67999)
c [simplification-10] new conflict limit 321008 (hard 389007)
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 -   74.1    3473    19708    192818   47387   6137  7652   11    23   16  50%    125   -2   13   10  133%
c -   88.1    3473    19708    229644   50701   6153  7653   11    24   18  47%    512    2   12   10  119%
c -  103.0    3473    19708    263642   50879   6165  7653   13    21   18  59%    719    0   14   10  132%
c -  118.6    3473    19708    300165   53144   6173  7653    9    12   19  77%    849   -7    8   10   78%
c i  132.0    3472    19708    334214   78033   6274  7669    7     8   28  85%    920   -7    5    9   49%
c -  136.5    3469    19708    344151   56044   6296  7671    8    10   17  82%  -1793   -5    7    9   80%
c i  142.2    3468    19708    356899   67035   6351  7682    8    10   27  75%  -1296   -4    5    9   56%
c i  143.0    3458    19708    358738   68386   6382  7690    7    10   27  73%  -1522   -4    5    9   58%
c i  145.6    3453    19708    365429   73746   6406  7700    8    10   29  75%  -1355   -4    5    9   58%
c i  145.8    3279    19708    365863   74152   6406  7700    8    11   29  73%  -1375   -3    7    9   78%
c i  146.1    3275    19708    366552   74624   6422  7710    7    10   29  74%  -1387   -4    5    9   59%
c i  146.4    3273    19708    367100   74874   6452  7718    7     9   29  74%  -1387   -4    4    9   49%
c i  146.5    3261    19708    367295   74955   6466  7722    7     9   29  75%  -1386   -5    4    9   50%
c i  146.5    3258    19708    367305   74955   6469  7726    7     9   29  75%  -1386   -5    4    9   49%
c i  146.6    3228    19708    367801   75353   6485  7737    7     9   29  75%  -1381   -5    5    9   52%
c 0  146.6    2867    19708    367801   75353   6485  7737    7     9   29  75%  -1381   -5    5    9   52%
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: 5 basic ate = 5 trn 100% + 0 lrg 0% in 1 updates
c bcas: 3 count, 2 added (0 skipped), 101765 steps
c bkwd: tried 74844 clauses, 148976 lits, 1.99 lits/clause
c bkwd: checked 1884807 occs, 25.18 occs/clause, 12.65 occs/lit
c bkwd: subsumed 103 binary, 103 ternary, 80 large
c bkwd: strengthened 4 binary, 4 ternary (100% self), 632 large (0% self)
c blkd: 3 bces, 119 removed, 318115 resolutions, 793573 steps
c blkd: 77 blocking literals 0%, 0 pure
c bump: 370981 bumped seen, 86750090 lits 233.8 on average
c card: 4 count, 1 units, 38 am1, 6422808 steps
c card: 15 rescheduled, 130 eliminated, 41089 resolved, 2132 subsumed
c card: 224 at-most-one constraints found, average size 3.00
c card: 224 at-most-one constraints used 100%, average size 3.00
c card: 58 at-most-two constraints found, average size 4.02
c card: 58 at-most-two constraints used 100%, average size 4.02
c cces: 4 cces, 784 eliminated, 740 ate 94%, 44 abce 6%
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: 185744 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 58 gcs, 0 rescored clauses, 195 rescored vars
c dcps: 34 decompositions, 1101 equivalent 6%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1105135 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 8 elims, 12598 eliminated 68%, 0 pure 0%
c elms: 25 rounds, 3.1 rounds/bve
c elms: 12298 small 98%, 300 large 2%
c elms: 25816 tried small, 12299 succeeded 48%, 13517 failed 52%
c elms: 937 subsumed, 1594 strengthened, 68 blocked
c elms: 1017715 copies, 1178385 resolutions, 958854 ipos
c elms: 276488 subchks, 255819 strchks
c gaus: 5 extractions, 25145 extracted, 3.0 size, 4 max
c gaus: exported 0 units, 8 binary and 74 ternary equations
c gaus: 0 gc, 9354100 steps, 4677050 extr 50%, 877184 elim 9%
c glue: 9.8 orig avg, 9.8 real avg, 2.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 19968 = 6016 simple 30% + 11834 trn 59% + 2118 lrg 11%, 883 sub 4%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 370981 clauses, 38.5 length
c lrnd: 14265227 lits = 39942357 orig - 25677130 removed 64%
c lrnd: 82616 uips 22%, 258643 flips 70%
c mins: 366938 mins 99%, 334 bin 0%, 3709 size 1%
c mins: 61242934 poisoned searches, 5320481 hits, 9% hit rate
c mins: 95476804 used twice searches, 1165459 hits, 1% hit rate
c move: moved 1230, 91 bin 7%, 1139 trn 93%
c otfs: 905 driving 23%, 2959 restarting 77%
c otfs: str 3864, 3801 red 98%, 63 irr 2%
c otfs: str 3864, 0 bin 0%, 59 trn 2%, 3805 lrg 98%
c otfs: sub 28, 27 red 96%, 1 irr 4%
c otfs: sub 28, 0 bin 0%, 3 trn 11%, 25 lrg 89%
c phas: 1 computed, 5973 set, 1103 pos (18%), 4870 neg (82%)
c prbs: 3 basic, 25126 probed, 68 failed, 14 lifted
c prbs: 4 simple, 52749 probed, 139 failed, 1030 eqs
c prbs: 4 treelook, 192 probed, 0 failed, 0 lifted
c prom: 151245 locked 4% out of 3839059 tried
c prps: 154791080 props, 138 props/dec
c prps: 99% srch, 1% simp, 0% lkhd
c quat: 6 count, 891 quat, 215 self1, 11 self2, 5 dup
c queu: 8 sorted, 1105135 next (236047 steps 0.21)
c queu: 87414913 enq (97746222 steps 1.12), 86750090 deq 99%
c redc: 22962 clauses 28%, 80824 tried 22%, 3 sat 0%
c redc: 49760 lits 5%, 967971 tried 2%, 3 sat 0%
c redc: 285 times jump level reduced, 2.2 levels on average
c reds: 8 count, 45975.1 conflicts per reduce
c reds: 0 memlim 0%, 8 arith 100%
c reds: 214011 collected 86%, 34582 retired 14%
c rmbd: 678 removed, 569 red 84%
c rsts: 16873 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 10 count, 9 confs 90%, 0 vars 0%
c simp: 1 its 10%, 0 bin 0%, 0 trns 0%
c subl: 370981 count (298277 tried 0.8), 33993 sub out of 368998 (9.2%)
c swps: 6 count, 8 rounds, 474 queries (59.2/round)
c swps: 458 sat calls, 13 unsat (8.9% success rate)
c swps: 15490 decisions 33.8, 4085 conflicts 8.9
c swps; 87.2 avg class size, 116.6 avg environment size
c swps: 0 failed, 36 impls, 29 equivs
c swp0: 155 type 0 queries, 38 unsat (24.5%), 145 sat (93.5%)
c swp1: 319 type 1 queries, 68 unsat (21.3%), 300 sat (94.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: 2952844 calls to obtain time
c tops: 2041 fixed 11%, 39 its, 9430.79 confs/it
c trds: 6 transitive reductions, 1404 removed, 0 failed
c trds: 41275 nodes, 27746 edges, 1980220 steps
c trim: 226382 words, 0.9 MB
c trnr: 6 count, 46 bin, 5297 trn, 20222561 steps
c unhd: 6 count, 6 rounds, 2051993 steps
c unhd: 205 non-trivial sccs of average size 4.8
c unhd: 193 units, 193 bin, 0 trn, 0 lrg
c unhd: 869 failed, 868 stamp, 0 lits, 1 bin, 0 trn, 0 lrg
c unhd: 8003 tauts, 40 bin 0%, 1827 trn 23%, 87 lrg 1%
c unhd: 8003 tauts, 6049 stamp 76%, 6549 red 82%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 196610 str, 193 bin 0%, 936 trn 0%, 195481 lrg 99%, 194630 red 99%
c vars: 2867 remaining 15% and 15740 removed 85% out of 18607
c vars: 2041 fixed 11%, 12598 eliminated 68%, 1101 equivalent 6%
c vsts: 4126442724 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 26.7 search visits per propagation, 11113.6 per conflict
c wchs: 1601514430 pushed, 2375764 enlarged, 140 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         369889        214011         34582      30126906      11651041        198781
c 
c  0 0         39951  11      6421   3         0   0  18307381  61   6273085  54     58571  29     1.3
c  1 5         27874   8     14382   7      1819   5   4777185  16<  1914410  16<    23217  12     0.7
c  2 6        107320  29<    67901  32      7103  21   5592686  19   2567126  22     51087  26<    3.6
c  3 9        130169  35     85228  40<    12829  37<  1290179   4    759820   7     38795  20     4.1
c  4 14        47063  13     30425  14      8536  25    108328   0     88716   1     12984   7     1.5
c  5 21        12633   3      7253   3      3211   9     36460   0     32198   0      8824   4     0.7
c  6 30         3920   1      2056   1       913   3     12415   0     13613   0      4719   2     0.3
c  7 41          832   0       320   0       157   0      1984   0      1876   0       547   0     0.1
c  8 54          122   0        25   0        14   0       280   0       192   0        37   0     0.0
c  9 69            5   0         0   0         0   0         8   0         5   0         0   0     0.0
c 
c avg                  2.5           2.7           3.2           0.7           0.9           1.9
c std                  1.3           1.1           1.1           1.0           1.1           1.6
c 
c   14.537  10% bump
c    1.951   1% cce
c    1.564   1% sweep
c    1.496   1% elim
c    0.832   1% probe
c 
c    2.112 < 1% rest (below)
c 
c    0.667   0% decide
c    0.371   0% unhide
c    0.278   0% gauss
c    0.185   0% transred
c    0.141   0% quatres
c    0.140   0% ternres
c    0.092   0% block
c    0.090   0% card
c    0.083   0% rescore
c    0.067   0% bca
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    0.502   0% preprocessing     7%
c    7.086   5% inprocessing     93%
c ==================================
c    7.588   5% simplifying
c  139.052  95% search
c ==================================
c  146.641 100% all
c 
c        367801 conflicts,        2508.2 confs/sec
c          1334 ternaries,         275.7 confs/ternary
c           436 binaries,          843.6 confs/binary
c            39 iterations,       9430.8 confs/iteration
c 
c             8 reductions,          0.1 redus/sec,  45975.1 confs/reduction
c         16873 restarts,          115.1 rests/sec,     21.8 confs/restart
c       1105135 decisions,        7536.4 decis/sec,      3.0 decis/conflict
c     154791080 propagations,  1055581.5 props/sec,    140.1 props/decision
c 
c 146.6 seconds, 34.4 MB
c launch: done
