c launch: /data/cnf/sc2014/app/atco_enc2_opt1_10_21.cnf.bz2
c host: atom17
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/atco_enc2_opt1_10_21.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/atco_enc2_opt1_10_21.cnf.bz2
c no embedded options
c found 'p cnf 44854 239768' header
c read 44854 variables, 239768 clauses, 860746 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=3
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 44508 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] SUM (--score=3)
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   44508   229782         0       0      0     0    0     0   15   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 9346 at-most-one constraints of average size 3.0
c [card-1] found 24 at-most-two constraints of average size 7.4
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9370 out of 9370 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 9320 variables
c [simpleprobe-1] all 35534 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 3286 variables
c [simpleprobe-1] 24790 variables remain 77% (7458 retained 23%)
c [simpleprobe-1] removed 3286 variables, found 4561 hbrs, 334 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 1248 failed, 1040 tauts, 0 hbrs, 2303 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 30978 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 16669 variables 54% in round 1 in 12418442 steps
c [elim-1-1] backward subsumption/strengthening limit 7581558
c [elim-1-1-1] backward checking 24375 touched variables 79%
c [elim-1-1-1] incomplete backward checking 21249 remain 87%
c [elim-1-1] subsumed 127 and strengthened 713 clauses in 7581565 steps
c [elim-1] incomplete 403 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 16669 = 54% variables out of 30978 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 153280 negative 90.4% of 169615 except 16335 9.6%
c [phase-count-1] 154684 positive 91.2% of 169615 except 14931 8.8%
c [phase-1] phase bias: 6744 positive 47%, 7565 negative 53%
c [sort-queue-1] sorted 14309 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 14309 (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 30010 variables 67.7% (14309 remain 32%)
c [simplification-1] removed 60167 irredundant clauses 26.2% (169615 remain 74%)
c [simplification-1] maximum reduction of 68% = max (68%, 26%)
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 [simplification-2] limit 1000 conflicts (hard 11000) hit after 1000 conflicts
c [decomp-3] removed 364 variables
c [simpleprobe-2] 11109 schedulable variables 80%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 6 variables
c [simpleprobe-2] 11271 variables remain 81% (2668 retained 19%)
c [simpleprobe-2] removed 6 variables, found 697 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 19041 literals 68%
c [treelook-1] scheduling used 300377 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 316438 steps
c [treelook-1] 18938 literals remain 68%
c [treelook-1] 12821 variables remain to probed next time 92%
c [decomp-5] removed 5 variables
c [treelook-1] removed 5 variables, found 97 hbrs
c [basicprobe-1] limit 1350904 based on 168863 irredundant clauses
c [basicprobe-1-0] 5477 probes remain 39% after last round
c [basicprobe-1-0] 2 units = 2 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 2 variables, found 3838 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 1 units, 2 failed, 988 tauts, 0 hbrs, 435 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 13930 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 907 not tried 7% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 98 = 1% variables out of 13930 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 151712 negative 90.6% of 167491 except 15779 9.4%
c [phase-count-2] 152310 positive 90.9% of 167491 except 15181 9.1%
c [phase-2] phase bias: 32 positive 71%, 13 negative 29%
c [sort-queue-2] sorted 13309 enqueued variables after 1000 conflicts
c [score-dist-2] active 523 (4%), one 0 (0%), zero 13309 (96%)
c [score-dist-2] max exp 520, different 20 (4%)
c [score-dist-2] median active exp 515, avg 512.9
c [simplification-2] removed 477 variables 3.3% (13832 remain 31%)
c [simplification-2] removed 2124 irredundant clauses 1.3% (167491 remain 73%)
c [simplification-2] maximum reduction of 3% = max (3%, 1%)
c [simplification-2] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-2] new conflict interval 5000
c [simplification-2] penalized conflict interval 5000 = 1 * 5000
c [simplification-2] hard conflict limit 16000 (soft 6000 + delta 10000)
c [simplification-2] new conflict limit 6000 (hard 16000)
c 
c [simplification-3] limit 6000 conflicts (hard 16000) hit after 6002 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 4778 at-most-one constraints of average size 3.2
c [card-2] found 37 at-most-two constraints of average size 4.0
c [card-2] using previous limit 1000000 for elimination
c [card-2] 4815 out of 4815 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 274 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 18989 literals 70%
c [treelook-2] scheduling used 300994 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 309746 steps
c [treelook-2] 18942 literals remain 70%
c [treelook-2] 11977 variables remain to probed next time 88%
c [decomp-7] removed 3 variables
c [treelook-2] removed 3 variables, found 105 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 0 failed, 1010 tauts, 0 hbrs, 1632 literals
c [elim-3] 795 variables 6% will be scheduled this time
c [elim-3] scheduled 795 variables 6%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 559 not tried 4% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 795 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 149883 negative 90.5% of 165663 except 15780 9.5%
c [phase-count-3] 150962 positive 91.1% of 165663 except 14701 8.9%
c [phase-3] phase bias: 11 positive 58%, 8 negative 42%
c [sort-queue-3] sorted 13008 enqueued variables after 6002 conflicts
c [score-dist-3] active 547 (4%), one 0 (0%), zero 13008 (96%)
c [score-dist-3] max exp 525, different 24 (5%)
c [score-dist-3] median active exp 519, avg 516.7
c [simplification-3] removed 277 variables 2.0% (13555 remain 30%)
c [simplification-3] removed 1828 irredundant clauses 1.1% (165663 remain 72%)
c [simplification-3] maximum reduction of 2% = max (2%, 1%)
c [simplification-3] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-3] new conflict interval 11666
c [simplification-3] penalized conflict interval 11666 = 1 * 11666
c [simplification-3] hard conflict limit 27668 (soft 17668 + delta 10000)
c [simplification-3] new conflict limit 17668 (hard 27668)
c 
c [simplification-4] limit 17668 conflicts (hard 27668) hit after 17668 conflicts
c [decomp-8] removed 38 variables
c [basicprobe-2] limit 5008924 penalty 0 = 0 + 0
c [basicprobe-2-0] 5246 sched 39%, 10 failed, 0 lifted, 4194 hbrs
c [decomp-9] removed 305 variables
c [basicprobe-2-1] 4009 probes remain 30% after last round
c [basicprobe-2-1] 11 units = 11 failed (100%) + 0 lifted (0%)
c [basicprobe-2-1] removed 306 variables, found 4697 hbrs
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 13211 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400713980 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 80 variables 1% in round 1 in 120633676 steps
c [elim-4-1] backward subsumption/strengthening limit 120633600
c [elim-4-1-1] backward checking 804 touched variables 6%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 15 and strengthened 81 clauses in 7081907 steps
c [elim-4-1] rescheduled 91 variables 1% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 2891808 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 80 = 1% variables out of 13211 scheduled
c [elim-4] 80 < 1/100 * 13211 = 132 considered unsuccessful
c [phase-count-4] 145149 negative 88.9% of 163297 except 18148 11.1%
c [phase-count-4] 147585 positive 90.4% of 163297 except 15712 9.6%
c [phase-4] phase bias: 9 positive 43%, 12 negative 57%
c [sort-queue-4] sorted 12541 enqueued variables after 17668 conflicts
c [score-dist-4] active 590 (4%), one 0 (0%), zero 12541 (96%)
c [score-dist-4] max exp 528, different 25 (5%)
c [score-dist-4] median active exp 523, avg 519.9
c [simplification-4] removed 424 variables 3.1% (13131 remain 30%)
c [simplification-4] removed 2366 irredundant clauses 1.4% (163297 remain 71%)
c [simplification-4] maximum reduction of 3% = max (3%, 1%)
c [simplification-4] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-4] new conflict interval 16666
c [simplification-4] penalized conflict interval 16666 = 1 * 16666
c [simplification-4] hard conflict limit 44334 (soft 34334 + delta 10000)
c [simplification-4] new conflict limit 34334 (hard 44334)
c 
c [simplification-5] limit 34334 conflicts (hard 44334) hit after 34335 conflicts
c [quatres-1] found 29504 quaternary clauses 30% in total
c [quatres-1-1] removed 1 duplicate quaternary clauses
c [quatres-1-2] added 10 single-self-subsuming ternary resolvents
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 13131 free variables schedulable
c [ternres-1] 416 ternary resolvents (0 bin, 416 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 1136 xors of average arity 3.0
c [gauss-1] connected 3402 occurrences of 1718 variables (average 2.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-10] removed 3 variables
c [simpleprobe-3] 10613 schedulable variables 81%
c [simpleprobe-3] limit 9595744 penalty 0 = 0 + 0
c [decomp-11] removed 34 variables
c [simpleprobe-3] 9618 variables remain 73% (3476 retained 27%)
c [simpleprobe-3] removed 34 variables, found 1289 hbrs, 0 units
c [unhide-4] limit 239893 with penalty 1 = 1 + 0
c [unhide-4-4] 0 units, 0 failed, 1183 tauts, 0 hbrs, 8745 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 1371 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 13094 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 4846 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 2 clauses out of 2 (100%) of length 22
c [cce-1-1] eliminated 6 clauses out of 6 (100%) of length 21
c [cce-1-1] eliminated 3 clauses out of 3 (100%) of length 20
c [cce-1-1] eliminated 230 clauses out of 525 (44%) of length 13
c [cce-1-1] eliminated 60 clauses out of 827 (7%) of length 12
c [cce-1-1] eliminated 62 clauses out of 318 (19%) of length 11
c [cce-1-1] eliminated 8 clauses out of 389 (2%) of length 10
c [cce-1-1] eliminated 11 clauses out of 4024 (0%) of length 9
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 382 large clauses in 30000061 steps
c [cce-1-1] allowing another 15000030 steps for small clauses
c [cce-1-1] scheduling 26890 clauses = 23986 binary + 2904 ternary
c [cce-1-1] tried to eliminate 4691 small clauses 17%
c [cce-1-1] eliminated 156 binary clauses 1%
c [cce-1-1] eliminated 23 ternary clauses 1%
c [cce-1-1] eliminated 179 small clauses 1%
c [cce-1-1] eliminated 179 small clauses in 30000024 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 561 covered clauses in round 1
c [cce-1] eliminated 561 covered clauses in TOTAL during 1 rounds
c [cce-1] 561 < 1/100 * 157838 = 1578 considered unsuccessful
c [bca-1] limit of 10000000 steps and 315054 added (scaled 2)
c [bca-1] 25380 out of 26190 literals actually usable 97%
c [bca-1] added 5035 blocked clauses in 124462 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 3250 pos 24.8% + 9844 neg 75.2% = 13094 sched 100.0% ret 0
c [sweep-1-1] 1172782 steps 77 queries 2194.32 avg class size
c [sweep-1-1] 1312 decisions 73 SAT calls 43.95 avg env size
c [sweep-1-1] 12599 variables remain 96% (495 retained 4%)
c [decomp-12] removed 21 variables
c [sweep-1-1] removed 21 vars (0 failed, 5 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 21 vars in TOTAL (1 rounds, 76 queries)
c [phase-count-5] 139780 negative 88.9% of 157268 except 17488 11.1%
c [phase-count-5] 141891 positive 90.2% of 157268 except 15377 9.8%
c [phase-5] phase bias: 19 positive 63%, 11 negative 37%
c [sort-queue-5] sorted 12311 enqueued variables after 34335 conflicts
c [score-dist-5] active 762 (6%), one 0 (0%), zero 12311 (94%)
c [score-dist-5] max exp 530, different 26 (5%)
c [score-dist-5] median active exp 523, avg 520.9
c [simplification-5] removed 58 variables 0.4% (13073 remain 29%)
c [simplification-5] removed 6029 irredundant clauses 3.7% (157268 remain 68%)
c [simplification-5] maximum reduction of 4% = max (0%, 4%)
c [simplification-5] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-5] new conflict interval 20666
c [simplification-5] penalized conflict interval 20666 = 1 * 20666
c [simplification-5] hard conflict limit 65334 (soft 55001 + delta 10333)
c [simplification-5] new conflict limit 55001 (hard 65334)
c 
c [simplification-6] limit 55001 conflicts (hard 65334) hit after 55002 conflicts
c [quatres-2] found 28572 quaternary clauses 29% in total
c [ternres-2] limit 4604839 with penalty 0 = 0 + 0
c [ternres-2] all 13073 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 4589 variables remain 35% (8484 retained 65%)
c [card-3] limit 575604 penalty 2 = 2 + 0
c [card-3] found 2795 at-most-one constraints of average size 3.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 575604 for elimination
c [card-3] 2795 out of 2795 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [treelook-3] limit 460483 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 22662 literals 87%
c [treelook-3] scheduling used 461118 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 460483 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 461939 steps
c [treelook-3] 22605 literals remain 86%
c [treelook-3] 11498 variables remain to probed next time 88%
c [decomp-14] removed 3 variables
c [treelook-3] removed 3 variables, found 73 hbrs
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 579 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 13070 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 28 blocked clauses
c [block-2] 28 < 1/100 * 157174 = 1571 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 13070 variables 100%
c [elim-5] limit of 46048397 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 401 not tried 3% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 81 = 1% variables out of 13070 scheduled
c [elim-5] 81 < 1/100 * 13070 = 130 considered unsuccessful
c [bca-2] limit of 10000000 steps and 316647 added (scaled 2)
c [bca-2] 25049 out of 25980 literals actually usable 96%
c [bca-2] added 16 blocked clauses in 142280 steps
c [sweep-2] limit 1381451 penalty 0 = 0 + 0
c [sweep-2-1] 3259 pos 26.1% + 9246 neg 73.9% = 12505 sched 96.3% ret 484
c [sweep-2-1] 1402056 steps 38 queries 3197.37 avg class size
c [sweep-2-1] 722 decisions 37 SAT calls 46.68 avg env size
c [sweep-2-1] 12289 variables remain 95% (700 retained 5%)
c [decomp-15] 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, 37 queries)
c [phase-count-6] 139254 negative 88.8% of 156811 except 17557 11.2%
c [phase-count-6] 141480 positive 90.2% of 156811 except 15331 9.8%
c [phase-6] phase bias: 6 positive 60%, 4 negative 40%
c [sort-queue-6] sorted 12012 enqueued variables after 55002 conflicts
c [score-dist-6] active 970 (7%), one 0 (0%), zero 12012 (93%)
c [score-dist-6] max exp 532, different 28 (5%)
c [score-dist-6] median active exp 521, avg 521.2
c [simplification-6] removed 91 variables 0.7% (12982 remain 29%)
c [simplification-6] removed 457 irredundant clauses 0.3% (156811 remain 68%)
c [simplification-6] maximum reduction of 1% = max (1%, 0%)
c [simplification-6] geometric conflict interval increment 10333 = 20666 / 2
c [simplification-6] new conflict interval 30999
c [simplification-6] penalized conflict interval 30999 = 1 * 30999
c [simplification-6] hard conflict limit 101500 (soft 86001 + delta 15499)
c [simplification-6] new conflict limit 86001 (hard 101500)
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 -   15.0   12982   156811     55986   25222   3620  9222   11    13   19  84%    581    4   11    7  151%
c 
c [simplification-7] limit 86001 conflicts (hard 101500) hit after 86002 conflicts
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 527 xors of average arity 3.0
c [gauss-2] connected 1581 occurrences of 1053 variables (average 1.5)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 38646180 penalty 0 = 0 + 0
c [basicprobe-3-0] 3907 sched 30%, 1 failed, 0 lifted, 759 hbrs
c [decomp-17] removed 89 variables
c [basicprobe-3-1] 7590 sched 59%, 2 failed, 0 lifted, 449 hbrs
c [decomp-18] removed 51 variables
c [basicprobe-3-2] 7593 sched 59%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-3-3] 7593 sched 59%, 0 failed, 0 lifted, 7 hbrs
c [basicprobe-3-4] 7593 sched 59%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-4] fully completed probing
c [basicprobe-3-4] 3 units = 3 failed (100%) + 0 lifted (0%)
c [basicprobe-3-4] removed 140 variables, found 1252 hbrs
c [bate-1] eliminated 19 asymmetric tautologies during probing
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 519 transitive binary clauses
c [cce-2] limit of 19323090 steps penalty 1 = 1 + 0
c [cce-2-1] eliminated 2 clauses out of 260 (1%) of length 11
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 2 large clauses in 19323622 steps
c [cce-2-1] allowing another 9661811 steps for small clauses
c [cce-2-1] scheduling 56721 clauses = 23003 binary + 33718 ternary
c [cce-2-1] tried to eliminate 2676 small clauses 5%
c [cce-2-1] eliminated 37 binary clauses 0%
c [cce-2-1] eliminated 98 ternary clauses 0%
c [cce-2-1] eliminated 135 small clauses 0%
c [cce-2-1] eliminated 135 small clauses in 19323181 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 137 covered clauses in round 1
c [cce-2] eliminated 137 covered clauses in TOTAL during 1 rounds
c [cce-2] 137 < 1/100 * 156615 = 1566 considered unsuccessful
c [bca-3] limit of 10000000 steps and 315981 added (scaled 2)
c [bca-3] 24697 out of 25686 literals actually usable 96%
c [bca-3] added 155 blocked clauses in 143854 steps
c [sweep-3] limit 2318770 penalty 0 = 0 + 0
c [sweep-3-1] 3220 pos 26.5% + 8928 neg 73.5% = 12148 sched 94.6% ret 694
c [sweep-3-1] 2324941 steps 87 queries 1919.40 avg class size
c [sweep-3-1] 1853 decisions 85 SAT calls 48.11 avg env size
c [sweep-3-1] 11661 variables remain 91% (1181 retained 9%)
c [decomp-21] removed 4 variables
c [sweep-3-1] removed 4 vars (0 failed, 3 eqs, 2 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 4 vars in TOTAL (1 rounds, 86 queries)
c [phase-count-7] 138888 negative 88.8% of 156478 except 17590 11.2%
c [phase-count-7] 141129 positive 90.2% of 156478 except 15349 9.8%
c [phase-7] phase bias: 2 positive 100%, 0 negative 0%
c [sort-queue-7] sorted 11786 enqueued variables after 86002 conflicts
c [score-dist-7] active 1052 (8%), one 0 (0%), zero 11786 (92%)
c [score-dist-7] max exp 533, different 29 (5%)
c [score-dist-7] median active exp 522, avg 521.8
c [simplification-7] removed 144 variables 1.1% (12838 remain 29%)
c [simplification-7] removed 333 irredundant clauses 0.2% (156478 remain 68%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 15499 = 30999 / 2
c [simplification-7] new conflict interval 46498
c [simplification-7] penalized conflict interval 46498 = 1 * 46498
c [simplification-7] hard conflict limit 155749 (soft 132500 + delta 23249)
c [simplification-7] new conflict limit 132500 (hard 155749)
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 -   21.2   12838   156478     87759   26538   3507  9758   11    13   19  87%    751    2   12    9  132%
c -   25.0   12838   156478    119935   27533   3520  9758   10    11   19  87%    857   -0   10   10  102%
c 
c [simplification-8] limit 132500 conflicts (hard 155749) hit after 132502 conflicts
c [quatres-3] found 28712 quaternary clauses 29% in total
c [quatres-3-2] added 9 single-self-subsuming ternary resolvents
c [quatres-3-2] added 4 quaternary resolvents
c [ternres-3] limit 5914658 with penalty 1 = 1 + 0
c [ternres-3] 4511 schedulable variables 35%
c [ternres-3] 1 ternary resolvents (0 bin, 1 trn)
c [ternres-3] fully completed ternary resolution
c [simpleprobe-4] 9419 schedulable variables 73%
c [simpleprobe-4] limit 47317271 penalty 0 = 0 + 0
c [decomp-23] removed 57 variables
c [simpleprobe-4] 3903 variables remain 31% (8878 retained 69%)
c [simpleprobe-4] removed 57 variables, found 3182 hbrs, 0 units
c [unhide-5] limit 591465 with penalty 2 = 2 + 0
c [unhide-5-5] 0 units, 0 failed, 354 tauts, 0 hbrs, 7137 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 1305 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 12781 variables 100%
c [block-3] limit of 59146589 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 120 blocked clauses
c [block-3] 120 < 1/100 * 156185 = 1561 considered unsuccessful
c [bca-4] limit of 10000000 steps and 315233 added (scaled 2)
c [bca-4] 24489 out of 25564 literals actually usable 96%
c [bca-4] added 0 blocked clauses in 130600 steps
c [sweep-4] limit 3548795 penalty 0 = 0 + 0
c [sweep-4-1] 3065 pos 26.4% + 8545 neg 73.6% = 11610 sched 90.8% ret 1171
c [sweep-4-1] 3555718 steps 179 queries 1159.64 avg class size
c [sweep-4-1] 3672 decisions 175 SAT calls 41.54 avg env size
c [sweep-4-1] 10196 variables remain 80% (2585 retained 20%)
c [decomp-24] removed 9 variables
c [sweep-4-1] removed 9 vars (0 failed, 9 eqs, 10 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 9 vars in TOTAL (1 rounds, 178 queries)
c [phase-count-8] 138778 negative 88.9% of 156064 except 17286 11.1%
c [phase-count-8] 140922 positive 90.3% of 156064 except 15142 9.7%
c [phase-8] phase bias: 1 positive 12%, 7 negative 88%
c [sort-queue-8] sorted 11539 enqueued variables after 132502 conflicts
c [score-dist-8] active 1233 (10%), one 0 (0%), zero 11539 (90%)
c [score-dist-8] max exp 534, different 30 (6%)
c [score-dist-8] median active exp 521, avg 522.4
c [simplification-8] removed 66 variables 0.5% (12772 remain 29%)
c [simplification-8] removed 414 irredundant clauses 0.3% (156064 remain 68%)
c [simplification-8] maximum reduction of 1% = max (1%, 0%)
c [simplification-8] geometric conflict interval increment 23249 = 46498 / 2
c [simplification-8] new conflict interval 69747
c [simplification-8] penalized conflict interval 69747 = 1 * 69747
c [simplification-8] hard conflict limit 237122 (soft 202249 + delta 34873)
c [simplification-8] new conflict limit 202249 (hard 237122)
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 -   30.0   12772   156064    152781   26218   3633 10813   11    14   18  81%    923    2   11   10  110%
c -   34.0   12772   156064    189327   28072   3643 10814   11    14   18  81%    966    1   12   11  111%
c 
c [simplification-9] limit 202249 conflicts (hard 237122) hit after 218843 conflicts
c [quatres-4] found 28806 quaternary clauses 29% in total
c [quatres-4-2] added 1 single-self-subsuming ternary resolvents
c [quatres-4-2] added 6 quaternary resolvents
c [ternres-4] limit 19245962 with penalty 0 = 0 + 0
c [ternres-4] all 12772 free variables schedulable
c [ternres-4] 2 ternary resolvents (0 bin, 2 trn)
c [ternres-4] fully completed ternary resolution
c [treelook-4] limit 1924596 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 24729 literals 97%
c [treelook-4] scheduling used 545576 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 1924596 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 2021223 steps
c [treelook-4] 24496 literals remain 96%
c [treelook-4] 11218 variables remain to probed next time 88%
c [decomp-26] removed 4 variables
c [treelook-4] removed 4 variables, found 247 hbrs
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 901 transitive binary clauses
c [elim-6] 398 variables 3% will be scheduled this time
c [elim-6] scheduled 398 variables 3%
c [elim-6] limit of 96229814 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6] incomplete 183 not tried 1% in round 1
c [elim-6] transition to [ all 0 rem 1 ] state
c [elim-6] eliminated 0 = 0% variables out of 398 scheduled
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 57737880 penalty 0 = 0 + 0
c [sweep-5-1] 2754 pos 27.0% + 7441 neg 73.0% = 10195 sched 79.8% ret 2573
c [sweep-5-1] 21181920 steps 2165 queries 98.43 avg class size
c [sweep-5-1] 30240 decisions 2005 SAT calls 29.06 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-27] removed 176 variables
c [sweep-5-1] removed 176 vars (0 failed, 180 eqs, 227 impls)
c [sweep-5-2] 5128 pos 40.7% + 7464 neg 59.3% = 12592 sched 100.0% ret 0
c [sweep-5-2] 26168710 steps 2301 queries 76.96 avg class size
c [sweep-5-2] 33261 decisions 2208 SAT calls 30.70 avg env size
c [sweep-5-2] fully completed sweeping round
c [decomp-28] removed 115 variables
c [sweep-5-2] removed 115 vars (0 failed, 121 eqs, 134 impls)
c [sweep-5-3] 5277 pos 42.3% + 7200 neg 57.7% = 12477 sched 100.0% ret 0
c [sweep-5-3] 10392934 steps 399 queries 427.71 avg class size
c [sweep-5-3] 8006 decisions 384 SAT calls 45.19 avg env size
c [sweep-5-3] 8432 variables remain 68% (4045 retained 32%)
c [decomp-29] removed 16 variables
c [sweep-5-3] removed 16 vars (0 failed, 17 eqs, 22 impls)
c [sweep-5] removed 307 vars in TOTAL (3 rounds, 4862 queries)
c [phase-count-9] 138528 negative 89.0% of 155725 except 17197 11.0%
c [phase-count-9] 140587 positive 90.3% of 155725 except 15138 9.7%
c [phase-9] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-9] sorted 9766 enqueued variables after 218843 conflicts
c [score-dist-9] active 2695 (22%), one 0 (0%), zero 9766 (78%)
c [score-dist-9] max exp 536, different 30 (6%)
c [score-dist-9] median active exp 523, avg 523.7
c [simplification-9] removed 311 variables 2.4% (12461 remain 28%)
c [simplification-9] removed 339 irredundant clauses 0.2% (155725 remain 68%)
c [simplification-9] maximum reduction of 2% = max (2%, 0%)
c [simplification-9] geometric conflict interval increment 23249 = 69747 / 3
c [simplification-9] new conflict interval 92996
c [simplification-9] penalized conflict interval 92996 = 1 * 92996
c [simplification-9] hard conflict limit 358337 (soft 311839 + delta 46498)
c [simplification-9] new conflict limit 311839 (hard 358337)
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 -   41.5   12461   155725    220087   29489   3392 10486   11    13   19  80%    988    1   11   10  110%
c -   45.4   12461   155725    256145   30169   3403 10487   10    13   19  79%   1003    0   10   10   94%
c -   49.1   12461   155725    291474   31934   3406 10488   12    19   19  64%   1012    5   12   11  114%
c 
c [simplification-10] limit 311839 conflicts (hard 358337) hit after 311841 conflicts
c [quatres-5] found 29025 quaternary clauses 28% in total
c [quatres-5-2] added 14 single-self-subsuming ternary resolvents
c [quatres-5-2] added 11 quaternary resolvents
c [ternres-5] limit 26339236 with penalty 0 = 0 + 0
c [ternres-5] all 12461 free variables schedulable
c [ternres-5] 47 ternary resolvents (1 bin, 46 trn)
c [ternres-5] fully completed ternary resolution
c [card-4] limit 1646202 penalty 3 = 3 + 0
c [card-4] found 3451 at-most-one constraints of average size 3.2
c [card-4] found 38 at-most-two constraints of average size 4.0
c [card-4] using previous limit 1646202 for elimination
c [card-4] 3489 out of 3489 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 1316961 penalty 2 = 2 + 0
c [gauss-3] extracted 728 xors of average arity 3.0
c [gauss-3] connected 2172 occurrences of 1320 variables (average 1.6)
c [gauss-3] limit 1316961 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-30] removed 1 variables
c [basicprobe-4] limit 131696181 penalty 0 = 0 + 0
c [basicprobe-4-0] 7535 sched 61%, 8 failed, 0 lifted, 220 hbrs
c [decomp-31] removed 8 variables
c [basicprobe-4-1] 7538 sched 61%, 2 failed, 0 lifted, 20 hbrs
c [decomp-32] removed 2 variables
c [basicprobe-4-2] 7539 sched 61%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-3] 7539 sched 61%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-4] 7539 sched 61%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-5] 7539 sched 61%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-4-6] 7539 sched 61%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-4-6] fully completed probing
c [basicprobe-4-6] 10 units = 10 failed (100%) + 0 lifted (0%)
c [basicprobe-4-6] removed 10 variables, found 244 hbrs
c [bate-2] eliminated 156 asymmetric tautologies during probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1029 transitive binary clauses
c [cce-3] limit of 32924045 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 44 clauses out of 295 (15%) of length 13
c [cce-3-1] eliminated 64 clauses out of 764 (8%) of length 12
c [cce-3-1] eliminated 46 clauses out of 259 (18%) of length 11
c [cce-3-1] eliminated 55 clauses out of 381 (14%) of length 10
c [cce-3-1] eliminated 225 clauses out of 4003 (6%) of length 9
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 434 large clauses in 32924575 steps
c [cce-3-1] allowing another 16462287 steps for small clauses
c [cce-3-1] scheduling 55508 clauses = 22280 binary + 33228 ternary
c [cce-3-1] tried to eliminate 4241 small clauses 8%
c [cce-3-1] eliminated 133 binary clauses 1%
c [cce-3-1] eliminated 537 ternary clauses 2%
c [cce-3-1] eliminated 670 small clauses 1%
c [cce-3-1] eliminated 670 small clauses in 32924046 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1104 covered clauses in round 1
c [cce-3] eliminated 1104 covered clauses in TOTAL during 1 rounds
c [cce-3] 1104 < 1/100 * 154864 = 1548 considered unsuccessful
c [bca-5] limit of 10000000 steps and 310623 added (scaled 2)
c [bca-5] 22328 out of 24902 literals actually usable 90%
c [bca-5] added 275 blocked clauses in 141444 steps
c [sweep-6] limit 7901770 penalty 0 = 0 + 0
c [sweep-6-1] 3240 pos 38.4% + 5189 neg 61.6% = 8429 sched 67.7% ret 4021
c [sweep-6-1] 7936782 steps 569 queries 335.66 avg class size
c [sweep-6-1] 9918 decisions 567 SAT calls 34.64 avg env size
c [sweep-6-1] 5372 variables remain 43% (7075 retained 57%)
c [decomp-37] removed 19 variables
c [sweep-6-1] removed 19 vars (0 failed, 16 eqs, 12 impls)
c [sweep-6] removed 19 vars in TOTAL (1 rounds, 568 queries)
c [phase-count-10] 136789 negative 89.0% of 153712 except 16923 11.0%
c [phase-count-10] 138842 positive 90.3% of 153712 except 14870 9.7%
c [phase-10] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-10] sorted 9655 enqueued variables after 311841 conflicts
c [score-dist-10] active 2776 (22%), one 0 (0%), zero 9655 (78%)
c [score-dist-10] max exp 537, different 31 (6%)
c [score-dist-10] median active exp 523, avg 524.1
c [simplification-10] removed 30 variables 0.2% (12431 remain 28%)
c [simplification-10] removed 2013 irredundant clauses 1.3% (153712 remain 67%)
c [simplification-10] maximum reduction of 1% = max (0%, 1%)
c [simplification-10] geometric conflict interval increment 46498 = 92996 / 2
c [simplification-10] new conflict interval 139494
c [simplification-10] penalized conflict interval 139494 = 1 * 139494
c [simplification-10] hard conflict limit 521082 (soft 451335 + delta 69747)
c [simplification-10] new conflict limit 451335 (hard 521082)
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 -   55.7   12431   153712    324341   31631   3999 10368   12    18   19  66%   1017    2   11   11  102%
c -   59.9   12431   153712    361341   34099   4003 10368   12    16   19  78%   1020   -0   13   12  113%
c -   63.2   12431   153712    397099   34371   4009 10368   13    15   19  83%   1022   -1   11   12   96%
c -   67.0   12431   153712    435726   35247   4013 10368   13    15   19  81%   1023   -0   12   12   97%
c 
c [simplification-11] limit 451335 conflicts (hard 521082) hit after 451586 conflicts
c [quatres-6] found 28992 quaternary clauses 28% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 6 single-self-subsuming ternary resolvents
c [quatres-6-2] added 9 quaternary resolvents
c [ternres-6] limit 37488881 with penalty 0 = 0 + 0
c [ternres-6] all 12431 free variables schedulable
c [ternres-6] 24 ternary resolvents (1 bin, 23 trn)
c [ternres-6] fully completed ternary resolution
c [simpleprobe-5] 3722 schedulable variables 30%
c [simpleprobe-5] limit 149955526 penalty 0 = 0 + 0
c [decomp-39] removed 17 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 17 variables, found 4228 hbrs, 0 units
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 2177 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 12414 variables 100%
c [block-4] limit of 93722203 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 513 blocked clauses
c [block-4] 513 < 1/100 * 153396 = 1533 considered unsuccessful
c [bca-6] limit of 10000000 steps and 309006 added (scaled 2)
c [bca-6] 22614 out of 24798 literals actually usable 91%
c [bca-6] added 3 blocked clauses in 139681 steps
c [sweep-7] limit 11246664 penalty 0 = 0 + 0
c [sweep-7-1] 2086 pos 38.9% + 3282 neg 61.1% = 5368 sched 43.3% ret 7030
c [sweep-7-1] 11266552 steps 1188 queries 132.81 avg class size
c [sweep-7-1] 15899 decisions 1178 SAT calls 25.80 avg env size
c [sweep-7-1] 625 variables remain 5% (11773 retained 95%)
c [decomp-40] removed 14 variables
c [sweep-7-1] removed 14 vars (0 failed, 15 eqs, 18 impls)
c [sweep-7] removed 14 vars in TOTAL (1 rounds, 1187 queries)
c [phase-count-11] 136075 negative 89.0% of 152881 except 16806 11.0%
c [phase-count-11] 138065 positive 90.3% of 152881 except 14816 9.7%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-11] sorted 9541 enqueued variables after 451586 conflicts
c [score-dist-11] active 2843 (23%), one 0 (0%), zero 9541 (77%)
c [score-dist-11] max exp 538, different 32 (6%)
c [score-dist-11] median active exp 523, avg 524.4
c [simplification-11] removed 47 variables 0.4% (12384 remain 28%)
c [simplification-11] removed 831 irredundant clauses 0.5% (152881 remain 67%)
c [simplification-11] maximum reduction of 1% = max (0%, 1%)
c [simplification-11] geometric conflict interval increment 69747 = 139494 / 2
c [simplification-11] new conflict interval 209241
c [simplification-11] penalized conflict interval 209241 = 1 * 209241
c [simplification-11] hard conflict limit 765447 (soft 660827 + delta 104620)
c [simplification-11] new conflict limit 660827 (hard 765447)
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 -   72.7   12384   152881    474505   36095   4044 12651   12    15   19  78%   1023   -1   11   12   89%
c -   76.6   12384   152881    516105   37505   4053 12652   11    13   19  84%   1024   -2   11   12   89%
c -   80.7   12384   152881    556636   38895   4058 12652   12    15   19  78%   1024    0   13   12  106%
c -   85.0   12384   152881    597675   38154   4058 12652   11    13   19  86%   1024   -2   10   12   84%
c -   89.6   12384   152881    642043   40004   4072 12653   11    13   19  85%   1024   -1   12   12  100%
c 
c [simplification-12] limit 660827 conflicts (hard 765447) hit after 660829 conflicts
c [quatres-7] found 29115 quaternary clauses 28% in total
c [quatres-7-1] added 1 double-self-subsuming ternary resolvents
c [quatres-7-2] added 2 single-self-subsuming ternary resolvents
c [quatres-7-2] added 17 quaternary resolvents
c [ternres-7] limit 55789996 with penalty 0 = 0 + 0
c [ternres-7] all 12384 free variables schedulable
c [ternres-7] 18 ternary resolvents (1 bin, 17 trn)
c [ternres-7] fully completed ternary resolution
c [treelook-5] limit 5578999 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 24065 literals 97%
c [treelook-5] scheduling used 550576 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 5578999 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 5620162 steps
c [treelook-5] 23374 literals remain 94%
c [treelook-5] 10860 variables remain to probed next time 88%
c [treelook-5] removed 0 variables, found 662 hbrs
c [unhide-6] limit 1394749 with penalty 3 = 3 + 0
c [unhide-6-6] 0 units, 0 failed, 2169 tauts, 0 hbrs, 14081 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 854 transitive binary clauses
c [bca-7] limit of 10000000 steps and 308694 added (scaled 2)
c [bca-7] 22554 out of 24770 literals actually usable 91%
c [bca-7] added 1 blocked clauses in 145771 steps
c [sweep-8] limit 16736999 penalty 0 = 0 + 0
c [sweep-8-1] 305 pos 48.8% + 320 neg 51.2% = 625 sched 5.0% ret 11759
c [sweep-8-1] 3230379 steps 339 queries 25.94 avg class size
c [sweep-8-1] 5510 decisions 337 SAT calls 37.08 avg env size
c [sweep-8-1] fully completed sweeping round
c [decomp-43] removed 3 variables
c [sweep-8-1] removed 3 vars (0 failed, 3 eqs, 4 impls)
c [sweep-8-2] 5298 pos 42.8% + 7083 neg 57.2% = 12381 sched 100.0% ret 0
c [sweep-8-2] 13526771 steps 550 queries 276.26 avg class size
c [sweep-8-2] 9922 decisions 548 SAT calls 39.92 avg env size
c [sweep-8-2] 7375 variables remain 60% (5006 retained 40%)
c [decomp-44] removed 17 variables
c [sweep-8-2] removed 17 vars (0 failed, 16 eqs, 15 impls)
c [sweep-8] removed 20 vars in TOTAL (2 rounds, 887 queries)
c [phase-count-12] 135986 negative 89.0% of 152725 except 16739 11.0%
c [phase-count-12] 137924 positive 90.3% of 152725 except 14801 9.7%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 9434 enqueued variables after 660829 conflicts
c [score-dist-12] active 2930 (24%), one 0 (0%), zero 9434 (76%)
c [score-dist-12] max exp 539, different 32 (6%)
c [score-dist-12] median active exp 524, avg 524.7
c [simplification-12] removed 20 variables 0.2% (12364 remain 28%)
c [simplification-12] removed 156 irredundant clauses 0.1% (152725 remain 66%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 209241
c [simplification-12] new conflict interval 418482
c [simplification-12] penalized conflict interval 418482 = 1 * 418482
c [simplification-12] hard conflict limit 1288552 (soft 1079311 + delta 209241)
c [simplification-12] new conflict limit 1079311 (hard 1288552)
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 -   95.6   12364   152725    683944   40706   3943 10494   11    14   19  82%   1024   -0   10   12   87%
c -  100.2   12364   152725    727799   41897   3948 10494   10    13   20  84%   1024   -1    9   11   79%
c -  104.6   12364   152725    771113   42703   3950 10494   12    14   20  82%   1024    1   12   11  103%
c -  108.9   12364   152725    816272   43461   3954 10494   12    14   20  85%   1024    1   13   11  114%
c -  114.1   12364   152725    863678   44625   3967 10495   11    14   20  82%   1024    1   10   11   92%
c -  119.3   12364   152725    910507   45178   3974 10495   10    13   20  80%   1024   -0   11   11   98%
c -  123.6   12364   152725    956600   46917   3980 10495   11    14   20  79%   1024   -0   10   11   93%
c -  130.6   12364   152725   1003128   48071   4007 10497   29    61   30  48%   1024   36   27   15  189%
c -  145.0   12364   152725   1048078   47874   4009 10497   44    76   31  58%   1024   30   52   26  200%
c 
c [simplification-13] limit 1079311 conflicts (hard 1288552) hit after 1079314 conflicts
c [quatres-8] found 29570 quaternary clauses 26% in total
c [quatres-8-1] removed 3 duplicate quaternary clauses
c [quatres-8-1] added 1 double-self-subsuming ternary resolvents
c [quatres-8-2] added 12 single-self-subsuming ternary resolvents
c [quatres-8-2] added 45 quaternary resolvents
c [ternres-8] limit 95503659 with penalty 0 = 0 + 0
c [ternres-8] all 12364 free variables schedulable
c [ternres-8] 24 ternary resolvents (0 bin, 24 trn)
c [ternres-8] fully completed ternary resolution
c [basicprobe-5] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-5-0] 7453 sched 60%, 4 failed, 0 lifted, 209 hbrs
c [decomp-46] removed 4 variables
c [basicprobe-5-1] 7459 sched 60%, 1 failed, 0 lifted, 53 hbrs
c [decomp-47] removed 1 variables
c [basicprobe-5-2] 7458 sched 60%, 0 failed, 0 lifted, 4 hbrs
c [basicprobe-5-3] 7458 sched 60%, 0 failed, 0 lifted, 1 hbrs
c [basicprobe-5-4] 7458 sched 60%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-5-5] 7458 sched 60%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-5-5] fully completed probing
c [basicprobe-5-5] 5 units = 5 failed (100%) + 0 lifted (0%)
c [basicprobe-5-5] removed 5 variables, found 272 hbrs
c [bate-3] eliminated 44 asymmetric tautologies during probing
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 555 transitive binary clauses
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 12359 variables 100%
c [elim-7] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7] incomplete 232 not tried 2% in round 1
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 51 = 0% variables out of 12359 scheduled
c [elim-7] 51 < 1/100 * 12359 = 123 considered unsuccessful
c [bca-8] limit of 10000000 steps and 304270 added (scaled 2)
c [bca-8] 17885 out of 24618 literals actually usable 73%
c [bca-8] added 6 blocked clauses in 142229 steps
c [sweep-9] limit 28651097 penalty 0 = 0 + 0
c [sweep-9-1] 2946 pos 40.1% + 4407 neg 59.9% = 7353 sched 59.7% ret 4955
c [sweep-9-1] 13557078 steps 1700 queries 46.19 avg class size
c [sweep-9-1] 34829 decisions 1687 SAT calls 42.78 avg env size
c [sweep-9-1] fully completed sweeping round
c [decomp-51] removed 30 variables
c [sweep-9-1] removed 30 vars (0 failed, 29 eqs, 36 impls)
c [sweep-9-2] 5284 pos 43.0% + 6994 neg 57.0% = 12278 sched 100.0% ret 0
c [sweep-9-2] 15096511 steps 1292 queries 62.22 avg class size
c [sweep-9-2] 30423 decisions 1306 SAT calls 51.48 avg env size
c [sweep-9-2] 2556 variables remain 21% (9722 retained 79%)
c [decomp-52] removed 38 variables
c [sweep-9-2] removed 38 vars (0 failed, 42 eqs, 20 impls)
c [sweep-9] removed 68 vars in TOTAL (2 rounds, 2990 queries)
c [sort-queue-13] sorted 5016 enqueued variables after 1079314 conflicts
c [score-dist-13] active 7224 (59%), one 0 (0%), zero 5016 (41%)
c [score-dist-13] max exp 540, different 32 (6%)
c [score-dist-13] median active exp 528, avg 528.1
c [simplification-13] removed 124 variables 1.0% (12240 remain 28%)
c [simplification-13] removed 2214 irredundant clauses 1.4% (150511 remain 66%)
c [simplification-13] maximum reduction of 1% = max (1%, 1%)
c [simplification-13] geometric conflict interval increment 209241 = 418482 / 2
c [simplification-13] new conflict interval 627723
c [simplification-13] penalized conflict interval 627723 = 1 * 627723
c [simplification-13] hard conflict limit 2020898 (soft 1707037 + delta 313861)
c [simplification-13] new conflict limit 1707037 (hard 2020898)
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 -  165.2   12240   150511   1093332   48677   3907 10164   46    69   24  67%   1024    9   49   36  136%
c -  180.1   12240   150511   1140906   47931   3907 10164   41    61   24  68%   1024   -1   43   39  110%
c 1  189.6   12240   150511   1169896   75192   3908 10164   43    65   42  67%   1024    3   35   41   86%
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: 219 basic ate = 54 trn 25% + 165 lrg 75% in 3 updates
c bcas: 8 count, 5491 added (281 skipped), 1110321 steps
c bkwd: tried 44416 clauses, 88192 lits, 1.99 lits/clause
c bkwd: checked 7541607 occs, 169.79 occs/clause, 85.51 occs/lit
c bkwd: subsumed 0 binary, 7 ternary, 135 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 794 large (0% self)
c blkd: 4 bces, 5507 removed, 2927296 resolutions, 9537408 steps
c blkd: 4952 blocking literals 6%, 16 pure
c bump: 1182592 bumped seen, 81725949 lits 69.1 on average
c card: 4 count, 0 units, 0 am1, 12857236 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 46688 subsumed
c card: 20370 at-most-one constraints found, average size 3.11
c card: 20370 at-most-one constraints used 100%, average size 3.11
c card: 99 at-most-two constraints found, average size 4.82
c card: 99 at-most-two constraints used 100%, average size 4.82
c cces: 3 cces, 1802 eliminated, 1010 ate 56%, 792 abce 44%
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: 1100514 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 62 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 52 decompositions, 13113 equivalent 29%
c deco: 0 decision-only clauses 0%, 0% reduction
c decs: 1760544 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 7 elims, 16995 eliminated 38%, 431 pure 3%
c elms: 9 rounds, 1.3 rounds/bve
c elms: 10763 small 63%, 5785 large 34%
c elms: 12600 tried small, 10763 succeeded 85%, 1837 failed 15%
c elms: 9090 subsumed, 5772 strengthened, 160 blocked
c elms: 2554557 copies, 3484464 resolutions, 180810 ipos
c elms: 4214000 subchks, 1026479 strchks
c gaus: 3 extractions, 2391 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8635162 steps, 4317581 extr 50%, 251133 elim 3%
c glue: 15.9 orig avg, 15.9 real avg, 3.5 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 26362 = 13957 simple 53% + 11722 trn 44% + 683 lrg 3%, 397 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 1182592 clauses, 31.2 length
c lrnd: 36870702 lits = 52929123 orig - 16058421 removed 30%
c lrnd: 401747 uips 34%, 701584 flips 59%
c mins: 1178219 mins 100%, 152 bin 0%, 4221 size 0%
c mins: 33375927 poisoned searches, 8180228 hits, 25% hit rate
c mins: 76918487 used twice searches, 10304592 hits, 13% hit rate
c move: moved 4688, 526 bin 11%, 4162 trn 89%
c otfs: 1297 driving 32%, 2767 restarting 68%
c otfs: str 4064, 3860 red 95%, 204 irr 5%
c otfs: str 4064, 0 bin 0%, 89 trn 2%, 3975 lrg 98%
c otfs: sub 88, 88 red 100%, 0 irr 0%
c otfs: sub 88, 0 bin 0%, 6 trn 7%, 82 lrg 93%
c phas: 12 computed, 14444 set, 6824 pos (47%), 7620 neg (53%)
c prbs: 5 basic, 287279 probed, 31 failed, 0 lifted
c prbs: 5 simple, 87180 probed, 334 failed, 2766 eqs
c prbs: 5 treelook, 1130 probed, 0 failed, 0 lifted
c prom: 78917 locked 11% out of 729712 tried
c prps: 339083825 props, 187 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 8 count, 92 quat, 54 self1, 2 self2, 334 dup
c queu: 13 sorted, 1760544 next (117614 steps 0.07)
c queu: 81915030 enq (110566681 steps 1.35), 81725949 deq 100%
c redc: 2885 clauses 4%, 65138 tried 6%, 1 sat 0%
c redc: 3383 lits 0%, 735752 tried 1%, 1 sat 0%
c redc: 84 times jump level reduced, 3.2 levels on average
c reds: 28 count, 41782.0 conflicts per reduce
c reds: 0 memlim 0%, 28 arith 100%
c reds: 889080 collected 91%, 86832 retired 9%
c rmbd: 7995 removed, 2226 red 28%
c rsts: 10389 restarts 91%, 1024 skipped 9%
c rsts: 1024 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: 13 count, 13 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 1182592 count (728926 tried 0.6), 129256 sub out of 1181348 (10.9%)
c swps: 9 count, 13 rounds, 10871 queries (836.2/round)
c swps: 10590 sat calls, 186 unsat (1.3% success rate)
c swps: 185567 decisions 17.5, 13993 conflicts 1.3
c swps; 174.3 avg class size, 36.2 avg environment size
c swps: 0 failed, 504 impls, 458 equivs
c swp0: 3618 type 0 queries, 577 unsat (15.9%), 3528 sat (97.5%)
c swp1: 7253 type 1 queries, 2229 unsat (30.7%), 6885 sat (94.9%)
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: 5886524 calls to obtain time
c tops: 2506 fixed 6%, 0 its, 0.00 confs/it
c trds: 9 transitive reductions, 9290 removed, 0 failed
c trds: 211109 nodes, 279446 edges, 8078047 steps
c trim: 601976 words, 2.3 MB
c trnr: 8 count, 3 bin, 529 trn, 48940624 steps
c unhd: 6 count, 6 rounds, 9709041 steps
c unhd: 380 non-trivial sccs of average size 2.1
c unhd: 2 units, 2 bin, 0 trn, 0 lrg
c unhd: 1250 failed, 1250 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 6744 tauts, 761 bin 11%, 312 trn 5%, 1061 lrg 16%
c unhd: 6744 tauts, 4610 stamp 68%, 5118 red 76%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 34333 str, 2 bin 0%, 2520 trn 7%, 31811 lrg 93%, 31618 red 92%
c vars: 12240 remaining 27% and 32614 removed 73% out of 44854
c vars: 2506 fixed 6%, 16995 eliminated 38%, 13113 equivalent 29%
c vsts: 10791980177 visits, 98% srch, 2% simp, 0% lkhd
c vsts: 32.1 search visits per propagation, 9060.5 per conflict
c wchs: 1382261043 pushed, 16276507 enlarged, 127 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        1181440        889080         86832      15475178       6524742        351048
c 
c  0 0         18615   2       657   0         0   0   6096596  39   2247419  34    105397  30     0.6
c  1 5         18497   2      6644   1      8036   9   1986402  13    721944  11     39364  11     0.3
c  2 6        149434  13     97846  11     35621  41   3392696  22<  1247660  19<    79943  23<    1.3
c  3 9        574845  49    464454  52     31232  36<  2136140  14   1163363  18     56790  16     3.4
c  4 14       260057  22<   212077  24<     5710   7    937163   6    547476   8     22841   7     2.3
c  5 21        21794   2     13109   1       974   1    426836   3    241057   4     17523   5     2.7
c  6 30        35420   3     24060   3      1633   2    279673   2    187016   3     16146   5     4.6
c  7 41        60413   5     38691   4      2097   2    151779   1    116442   2      8559   2     8.8
c  8 54        37433   3     27385   3      1331   2     60653   0     46807   1      4137   1     6.5
c  9 69         4914   0      4147   0       197   0      7215   0      5541   0       347   0     1.6
c 10 86           18   0        10   0         1   0        25   0        17   0         1   0     0.0
c 
c avg                  3.5           3.6           2.7           1.6           1.9           2.1
c std                  1.5           1.4           1.4           1.7           1.9           2.0
c 
c    8.031   4% bump
c    7.812   4% probe
c    6.791   4% sweep
c    5.517   3% elim
c    1.241   1% cce
c    1.040   1% decide
c    0.887   0% unhide
c    0.883   0% quatres
c    0.691   0% block
c 
c    1.968 < 1% rest (below)
c 
c    0.655   0% bca
c    0.563   0% transred
c    0.285   0% ternres
c    0.267   0% gauss
c    0.198   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    1.339   1% preprocessing     5%
c   26.538  14% inprocessing     95%
c ==================================
c   27.877  15% simplifying
c  161.671  85% search
c ==================================
c  189.555 100% all
c 
c       1169896 conflicts,        6171.8 confs/sec
c           263 ternaries,        4448.3 confs/ternary
c            32 binaries,        36559.2 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            28 reductions,          0.1 redus/sec,  41782.0 confs/reduction
c         10389 restarts,           54.8 rests/sec,    112.6 confs/restart
c       1760544 decisions,        9287.8 decis/sec,      1.5 decis/conflict
c     339083825 propagations,  1788844.6 props/sec,    192.6 props/decision
c 
c 189.6 seconds, 59.3 MB
c launch: done
