c launch: /data/cnf/sc2014/app/010-23-80.cnf.bz2
c host: atom09
c Lingeling SAT Solver
c 
c Version b7ztzvv 37b745a123cb37a24a48e992b1e2073d5d4068bb
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sat May  2 12:17:55 CEST 2015
c compiled Sat May  2 12:17:55 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 fmvx1 3.13.0-51-generic x86_64
c 
c piping '/data/cnf/sc2014/app/010-23-80.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/010-23-80.cnf.bz2
c no embedded options
c found 'p cnf 4288 132592' header
c read 4288 variables, 132592 clauses, 873647 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 --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 3829 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 
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    3829    76353         0       0      0     0    0     0    4   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] found 3 at-most-one constraints of average size 3.0
c [card-1] found 7 at-most-two constraints of average size 4.0
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9 out of 10 constraints (90%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 598 variables
c [simpleprobe-1] all 3690 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 136 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 136 variables, found 5 hbrs, 51 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 647 tauts, 0 hbrs, 22 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 3554 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 128 variables 4% in round 1 in 2087460 steps
c [elim-1-1] backward subsumption/strengthening limit 2087400
c [elim-1-1-1] backward checking 1165 touched variables 33%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 18 and strengthened 68 clauses in 745292 steps
c [elim-1-1] rescheduled 146 variables 4% by backward subsumption
c [elim-1-2] eliminated 2 variables 0% in round 2 in 98870 steps
c [elim-1-2] backward subsumption/strengthening limit 98800
c [elim-1-2-1] backward checking 26 touched variables 1%
c [elim-1-2-1] incomplete backward checking 0 remain 0%
c [elim-1-2] subsumed 0 and strengthened 0 clauses in 98801 steps
c [elim-1-2] fully rescheduled 3423 variables 96%
c [elim-1-3] no variable eliminated in round 3 in 1787323 steps
c [elim-1] fully completed in 3 rounds
c [elim-1] transition to [ all 0 rem 0 ] state
c [elim-1] eliminated 131 = 4% variables out of 3554 scheduled
c [phase-count-1] 67965 negative 99.3% of 68467 except 502 0.7%
c [phase-count-1] 67647 positive 98.8% of 68467 except 820 1.2%
c [phase-1] phase bias: 1476 positive 43%, 1947 negative 57%
c [sort-queue-1] sorted 3423 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 3423 (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 402 variables 10.5% (3423 remain 89%)
c [simplification-1] removed 7886 irredundant clauses 10.3% (68467 remain 90%)
c [simplification-1] maximum reduction of 11% = max (11%, 10%)
c [simplification-1] large reduction 11% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c [simplification-2] limit 1000 conflicts (hard 11000) hit after 1001 conflicts
c [decomp-3] removed 1 variables
c [simpleprobe-2] all 3422 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 1934 variables remain 57% (1488 retained 43%)
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 6844 literals 100%
c [treelook-1] scheduling used 294351 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300233 steps
c [treelook-1] 5641 literals remain 82%
c [treelook-1] 2880 variables remain to probed next time 84%
c [treelook-1] removed 0 variables, found 4 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 352 sched 10%, 0 failed, 0 lifted, 17 hbrs
c [basicprobe-1-1] 357 sched 10%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-1-1] fully completed probing
c [basicprobe-1-1] removed 0 variables, found 17 hbrs
c [block-1] scheduling all variables this time
c [block-1] scheduled 3422 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 235 blocked clauses
c [block-1] 235 < 1/100 * 68464 = 684 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 3530 clauses out of 21480 (16%) of length 7
c [cce-1-1] eliminated 558 clauses out of 20954 (3%) of length 6
c [cce-1-1] eliminated 2644 clauses out of 13740 (19%) of length 5
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 6732 large clauses in 30000027 steps
c [cce-1-1] allowing another 15000013 steps for small clauses
c [cce-1-1] scheduling 785 clauses = 237 binary + 548 ternary
c [cce-1-1] tried to eliminate 785 small clauses 100%
c [cce-1-1] eliminated 4 binary clauses 2%
c [cce-1-1] eliminated 43 ternary clauses 8%
c [cce-1-1] eliminated 47 small clauses 6%
c [cce-1-1] eliminated 47 small clauses in 15166225 steps
c [cce-1-1] completed small round (ATE)
c [cce-1-1] eliminated 6779 covered clauses in round 1
c [cce-1-2] incomplete large round (ATE)
c [cce-1-2] allowing another 7416905 steps for small clauses
c [cce-1-2] scheduling 738 clauses = 233 binary + 505 ternary
c [cce-1-2] tried to eliminate 738 small clauses 100%
c [cce-1-2] completed small round (ATE)
c [cce-1-2] eliminated 0 covered clauses in round 2
c [cce-1] eliminated 6779 covered clauses in TOTAL during 2 rounds
c [elim-2] scheduling all variables this time
c [elim-2] scheduled 3422 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 739 not tried 22% in round 1
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 25 = 1% variables out of 3422 scheduled
c [elim-2] 25 < 1/100 * 3422 = 34 considered unsuccessful
c [bca-1] limit of 10000000 steps and 121786 added (scaled 2)
c [bca-1] 5025 out of 6796 literals actually usable 74%
c [bca-1] added 0 blocked clauses in 34547 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1567 pos 46.1% + 1830 neg 53.9% = 3397 sched 100.0% ret 0
c [sweep-1-1] 500843 steps 570 queries 189.16 avg class size
c [sweep-1-1] 8935 decisions 569 SAT calls 21.61 avg env size
c [sweep-1-1] fully completed sweeping round
c [decomp-7] removed 4 variables
c [sweep-1-1] removed 4 vars (0 failed, 2 eqs, 1 impls)
c [sweep-1-2] 1563 pos 46.1% + 1830 neg 53.9% = 3393 sched 100.0% ret 0
c [sweep-1-2] 461092 steps 550 queries 185.80 avg class size
c [sweep-1-2] 8614 decisions 547 SAT calls 22.19 avg env size
c [sweep-1-2] fully completed sweeping round
c [decomp-8] removed 4 variables
c [sweep-1-2] removed 4 vars (0 failed, 4 eqs, 5 impls)
c [sweep-1-3] 1561 pos 46.1% + 1828 neg 53.9% = 3389 sched 100.0% ret 0
c [sweep-1-3] 38782 steps 40 queries 974.88 avg class size
c [sweep-1-3] 705 decisions 39 SAT calls 25.15 avg env size
c [sweep-1-3] 3243 variables remain 96% (146 retained 4%)
c [sweep-1-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-1] removed 8 vars in TOTAL (3 rounds, 1157 queries)
c [sort-queue-2] sorted 3389 enqueued variables after 1001 conflicts
c [score-dist-2] active 0 (0%), one 3001 (89%), zero 388 (11%)
c [score-dist-2] max exp 1, different 2 (100%)
c [score-dist-2] median active exp 0, avg 0.0
c [simplification-2] removed 34 variables 1.0% (3389 remain 89%)
c [simplification-2] removed 7844 irredundant clauses 11.5% (60623 remain 79%)
c [simplification-2] maximum reduction of 11% = max (1%, 11%)
c [simplification-2] large reduction 11% >= 5% limit
c [simplification-2] next conflict interval 2000 = 2000/1
c [simplification-2] penalized conflict interval 2000 = 1 * 2000
c [simplification-2] hard conflict limit 13001 (soft 3001 + delta 10000)
c [simplification-2] new conflict limit 3001 (hard 13001)
c 
c [simplification-3] limit 3001 conflicts (hard 13001) hit after 3002 conflicts
c [quatres-1] found 7395 quaternary clauses 13% in total
c [quatres-1-1] added 31 double-self-subsuming ternary resolvents
c [quatres-1-2] added 125 single-self-subsuming ternary resolvents
c [quatres-1-2] added 270 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 3389 free variables schedulable
c [ternres-1] 159 ternary resolvents (12 bin, 147 trn)
c [ternres-1] fully completed ternary resolution
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 2 at-most-one constraints of average size 3.0
c [card-2] found 12 at-most-two constraints of average size 4.1
c [card-2] using previous limit 1000000 for elimination
c [card-2] 14 out of 14 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 4084 xors of average arity 4.8
c [gauss-1] connected 19614 occurrences of 864 variables (average 22.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] connected 1505 occurrences of 864 variables (average 1.7)
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 0 units, 0 failed, 62 tauts, 0 hbrs, 124 literals
c [transred-1] limit 100000 with penalty 0 = 0 + 0
c [transred-1] removed 10 transitive binary clauses
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 16841 (0%) of length 7
c [cce-2-1] eliminated 151 clauses out of 20688 (1%) of length 6
c [cce-2-1] eliminated 69 clauses out of 11337 (1%) of length 5
c [cce-2-1] eliminated 300 clauses out of 6760 (4%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 521 large clauses in 29667791 steps
c [cce-2-1] allowing another 14833895 steps for small clauses
c [cce-2-1] scheduling 791 clauses = 253 binary + 538 ternary
c [cce-2-1] tried to eliminate 791 small clauses 100%
c [cce-2-1] eliminated 2 binary clauses 1%
c [cce-2-1] eliminated 15 ternary clauses 3%
c [cce-2-1] eliminated 17 small clauses 2%
c [cce-2-1] eliminated 17 small clauses in 14996236 steps
c [cce-2-1] completed small round (ATE)
c [cce-2-1] completed small and large (ATE)
c [cce-2-1] eliminated 538 covered clauses in round 1
c [cce-2-2] incomplete large round (ATE)
c [cce-2-2] allowing another 7501920 steps for small clauses
c [cce-2-2] scheduling 774 clauses = 251 binary + 523 ternary
c [cce-2-2] tried to eliminate 774 small clauses 100%
c [cce-2-2] completed small round (ATE)
c [cce-2-2] eliminated 0 covered clauses in round 2
c [cce-2] eliminated 538 covered clauses in TOTAL during 2 rounds
c [cce-2] 538 < 1/100 * 60619 = 606 considered unsuccessful
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1584 pos 48.8% + 1659 neg 51.2% = 3243 sched 95.7% ret 146
c [sweep-2-1] 521639 steps 545 queries 174.24 avg class size
c [sweep-2-1] 9337 decisions 543 SAT calls 23.92 avg env size
c [sweep-2-1] fully completed sweeping round
c [decomp-11] removed 3 variables
c [sweep-2-1] removed 3 vars (0 failed, 1 eqs, 2 impls)
c [sweep-2-2] 1649 pos 48.7% + 1737 neg 51.3% = 3386 sched 100.0% ret 0
c [sweep-2-2] 478612 steps 517 queries 189.63 avg class size
c [sweep-2-2] 9062 decisions 518 SAT calls 24.54 avg env size
c [sweep-2-2] 12 variables remain 0% (3374 retained 100%)
c [sweep-2-2] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] removed 3 vars in TOTAL (2 rounds, 1060 queries)
c [sort-queue-3] sorted 3386 enqueued variables after 3002 conflicts
c [score-dist-3] active 0 (0%), one 3262 (96%), zero 124 (4%)
c [score-dist-3] max exp 1, different 2 (100%)
c [score-dist-3] median active exp 0, avg 0.0
c [simplification-3] removed 3 variables 0.1% (3386 remain 88%)
c [simplification-3] removed 554 irredundant clauses 0.9% (60067 remain 79%)
c [simplification-3] maximum reduction of 1% = max (0%, 1%)
c [simplification-3] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-3] new conflict interval 10000
c [simplification-3] penalized conflict interval 10000 = 1 * 10000
c [simplification-3] hard conflict limit 23002 (soft 13002 + delta 10000)
c [simplification-3] new conflict limit 13002 (hard 23002)
c 
c [simplification-4] limit 13002 conflicts (hard 23002) hit after 13002 conflicts
c [quatres-2] found 8031 quaternary clauses 13% in total
c [quatres-2-1] added 39 double-self-subsuming ternary resolvents
c [quatres-2-2] added 203 single-self-subsuming ternary resolvents
c [quatres-2-2] added 267 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 3386 free variables schedulable
c [ternres-2] 77 ternary resolvents (11 bin, 66 trn)
c [ternres-2] fully completed ternary resolution
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 3036 literals 45%
c [treelook-2] scheduling used 150032 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150058 steps
c [treelook-2] 2404 literals remain 36%
c [treelook-2] 1852 variables remain to probed next time 55%
c [treelook-2] removed 1 variables, found 11 hbrs
c [transred-2] limit 282176 with penalty 0 = 0 + 0
c [transred-2] removed 5 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 3385 variables 100%
c [block-2] limit of 25000000 steps penalty 1 = 1 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 0 blocked clauses
c [elim-3] 739 variables 22% will be scheduled this time
c [elim-3] scheduled 739 variables 22%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 324 not tried 10% in round 1
c [elim-3] transition to [ all 0 rem 1 ] state
c [elim-3] eliminated 0 = 0% variables out of 739 scheduled
c [bca-2] limit of 10000000 steps and 120582 added (scaled 2)
c [bca-2] 780 out of 6772 literals actually usable 12%
c [bca-2] added 0 blocked clauses in 18854 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 7 pos 58.3% + 5 neg 41.7% = 12 sched 0.4% ret 3373
c [sweep-3-1] 7908 steps 9 queries 3.78 avg class size
c [sweep-3-1] 164 decisions 8 SAT calls 31.50 avg env size
c [sweep-3-1] fully completed sweeping round
c [sweep-3-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3-2] 1697 pos 50.1% + 1688 neg 49.9% = 3385 sched 100.0% ret 0
c [sweep-3-2] 528823 steps 460 queries 156.18 avg class size
c [sweep-3-2] 11198 decisions 459 SAT calls 32.32 avg env size
c [sweep-3-2] fully completed sweeping round
c [sweep-3-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-3-3] 1697 pos 50.1% + 1688 neg 49.9% = 3385 sched 100.0% ret 0
c [sweep-3-3] 463699 steps 353 queries 191.18 avg class size
c [sweep-3-3] 9503 decisions 353 SAT calls 35.82 avg env size
c [sweep-3-3] 366 variables remain 11% (3019 retained 89%)
c [sweep-3-3] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3] removed 0 vars in TOTAL (3 rounds, 819 queries)
c [sort-queue-4] sorted 3385 enqueued variables after 13002 conflicts
c [score-dist-4] active 0 (0%), one 3317 (98%), zero 68 (2%)
c [score-dist-4] max exp 1, different 2 (100%)
c [score-dist-4] median active exp 0, avg 0.0
c [simplification-4] removed 1 variables 0.0% (3385 remain 88%)
c [simplification-4] removed 26 irredundant clauses 0.0% (60041 remain 79%)
c [simplification-4] maximum reduction of 0% = max (0%, 0%)
c [simplification-4] full geometric conflict interval increment 20000
c [simplification-4] new conflict interval 30000
c [simplification-4] penalized conflict interval 30000 = 1 * 30000
c [simplification-4] hard conflict limit 58002 (soft 43002 + delta 15000)
c [simplification-4] new conflict limit 43002 (hard 58002)
c 
c [simplification-5] limit 43002 conflicts (hard 58002) hit after 43002 conflicts
c [quatres-3] found 10169 quaternary clauses 15% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-1] added 50 double-self-subsuming ternary resolvents
c [quatres-3-2] added 411 single-self-subsuming ternary resolvents
c [quatres-3-2] added 421 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 3385 free variables schedulable
c [ternres-3] 65 ternary resolvents (5 bin, 60 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 1182 xors of average arity 4.2
c [gauss-2] connected 4974 occurrences of 334 variables (average 14.9)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [transred-3] limit 1366707 with penalty 0 = 0 + 0
c [transred-3] removed 0 transitive binary clauses
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 16399 (0%) of length 7
c [cce-3-1] eliminated 19 clauses out of 20805 (0%) of length 6
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 21 large clauses in 15000029 steps
c [cce-3-1] allowing another 7500014 steps for small clauses
c [cce-3-1] scheduling 866 clauses = 270 binary + 596 ternary
c [cce-3-1] tried to eliminate 866 small clauses 100%
c [cce-3-1] eliminated 1 binary clauses 0%
c [cce-3-1] eliminated 14 ternary clauses 2%
c [cce-3-1] eliminated 15 small clauses 2%
c [cce-3-1] eliminated 15 small clauses in 7717900 steps
c [cce-3-1] completed small round (ACCE)
c [cce-3-1] eliminated 36 covered clauses in round 1
c [cce-3-2] incomplete large round (ACCE)
c [cce-3-2] allowing another 3641073 steps for small clauses
c [cce-3-2] scheduling 851 clauses = 269 binary + 582 ternary
c [cce-3-2] tried to eliminate 851 small clauses 100%
c [cce-3-2] completed small round (ACCE)
c [cce-3-2] eliminated 0 covered clauses in round 2
c [cce-3] eliminated 36 covered clauses in TOTAL during 2 rounds
c [cce-3] 36 < 1/100 * 60041 = 600 considered unsuccessful
c [sort-queue-5] sorted 3385 enqueued variables after 43002 conflicts
c [score-dist-5] active 0 (0%), one 3343 (99%), zero 42 (1%)
c [score-dist-5] max exp 1, different 2 (100%)
c [score-dist-5] median active exp 0, avg 0.0
c [simplification-5] removed 0 variables 0.0% (3385 remain 88%)
c [simplification-5] removed 36 irredundant clauses 0.1% (60005 remain 79%)
c [simplification-5] maximum reduction of 0% = max (0%, 0%)
c [simplification-5] full geometric conflict interval increment 30000
c [simplification-5] new conflict interval 60000
c [simplification-5] penalized conflict interval 60000 = 1 * 60000
c [simplification-5] hard conflict limit 133002 (soft 103002 + delta 30000)
c [simplification-5] new conflict limit 103002 (hard 133002)
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.4    3385    60005     75560   28681   2615   146   12   339   14   3%    696  126   11    7  166%
c 
c [simplification-6] limit 103002 conflicts (hard 133002) hit after 103003 conflicts
c [quatres-4] found 13306 quaternary clauses 17% in total
c [quatres-4-1] removed 5 duplicate quaternary clauses
c [quatres-4-1] added 41 double-self-subsuming ternary resolvents
c [quatres-4-2] added 492 single-self-subsuming ternary resolvents
c [quatres-4-2] added 388 quaternary resolvents
c [ternres-4] limit 4370984 with penalty 0 = 0 + 0
c [ternres-4] all 3385 free variables schedulable
c [ternres-4] 39 ternary resolvents (4 bin, 35 trn)
c [ternres-4] fully completed ternary resolution
c [card-3] limit 546373 penalty 2 = 2 + 0
c [card-3] found 3 at-most-one constraints of average size 3.0
c [card-3] found 10 at-most-two constraints of average size 4.2
c [card-3] using previous limit 546373 for elimination
c [card-3] 13 out of 13 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [basicprobe-2] limit 10927462 penalty 1 = 1 + 0
c [basicprobe-2-0] 487 sched 14%, 0 failed, 0 lifted, 8 hbrs
c [basicprobe-2-1] 488 sched 14%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-2-1] fully completed probing
c [basicprobe-2-1] removed 0 variables, found 8 hbrs
c [bate-1] eliminated 33 asymmetric tautologies during probing
c [unhide-3] limit 218549 with penalty 2 = 2 + 0
c [unhide-3-3] 0 units, 0 failed, 76 tauts, 0 hbrs, 1458 literals
c [sweep-4] limit 655647 penalty 1 = 1 + 0
c [sweep-4-1] 179 pos 48.9% + 187 neg 51.1% = 366 sched 10.8% ret 3019
c [sweep-4-1] 342506 steps 148 queries 24.87 avg class size
c [sweep-4-1] 5930 decisions 148 SAT calls 63.14 avg env size
c [sweep-4-1] fully completed sweeping round
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4-2] 1757 pos 51.9% + 1628 neg 48.1% = 3385 sched 100.0% ret 0
c [sweep-4-2] 318163 steps 51 queries 332.61 avg class size
c [sweep-4-2] 3956 decisions 50 SAT calls 174.72 avg env size
c [sweep-4-2] 2138 variables remain 63% (1247 retained 37%)
c [sweep-4-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] removed 0 vars in TOTAL (2 rounds, 197 queries)
c [sort-queue-6] sorted 3385 enqueued variables after 103003 conflicts
c [score-dist-6] active 0 (0%), one 3380 (100%), zero 5 (0%)
c [score-dist-6] max exp 1, different 2 (100%)
c [score-dist-6] median active exp 0, avg 0.0
c [simplification-6] removed 0 variables 0.0% (3385 remain 88%)
c [simplification-6] removed 44 irredundant clauses 0.1% (59961 remain 79%)
c [simplification-6] maximum reduction of 0% = max (0%, 0%)
c [simplification-6] full geometric conflict interval increment 60000
c [simplification-6] new conflict interval 120000
c [simplification-6] penalized conflict interval 120000 = 1 * 120000
c [simplification-6] hard conflict limit 283003 (soft 223003 + delta 60000)
c [simplification-6] new conflict limit 223003 (hard 283003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   26.6    3385    59961    131049   37187   3635   174   13   329   16   4%    883   49   15   10  152%
c -   37.9    3385    59961    184698   45408   3918   176   15   328   17   5%    962   18   14   12  117%
c 
c [simplification-7] limit 223003 conflicts (hard 283003) hit after 223003 conflicts
c [quatres-5] found 17458 quaternary clauses 18% in total
c [quatres-5-1] removed 7 duplicate quaternary clauses
c [quatres-5-1] added 38 double-self-subsuming ternary resolvents
c [quatres-5-2] added 486 single-self-subsuming ternary resolvents
c [quatres-5-2] added 227 quaternary resolvents
c [ternres-5] limit 10991969 with penalty 0 = 0 + 0
c [ternres-5] all 3385 free variables schedulable
c [ternres-5] 20 ternary resolvents (3 bin, 17 trn)
c [ternres-5] fully completed ternary resolution
c [transred-4] limit 1000000 with penalty 1 = 1 + 0
c [transred-4] removed 10 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 3385 variables 100%
c [block-3] limit of 27479923 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 0 blocked clauses
c [elim-4] scheduling all variables this time
c [elim-4] scheduled 3385 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 1099196945 steps penalty 2 = 2 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 2 variables 0% in round 1 in 45098828 steps
c [elim-4-1] backward subsumption/strengthening limit 45098800
c [elim-4-1-1] backward checking 1268 touched variables 37%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 1 and strengthened 2 clauses in 798535 steps
c [elim-4-1] rescheduled 8 variables 0% by backward subsumption
c [elim-4-2] no variable eliminated in round 2 in 32410 steps
c [elim-4] fully completed in 2 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 2 = 0% variables out of 3385 scheduled
c [elim-4] 2 < 1/100 * 3385 = 33 considered unsuccessful
c [bca-3] limit of 10000000 steps and 120144 added (scaled 2)
c [bca-3] 21 out of 6768 literals actually usable 0%
c [bca-3] not enough literals usable
c [bca-3] added 0 blocked clauses in 81410 steps
c [sort-queue-7] sorted 3383 enqueued variables after 223003 conflicts
c [score-dist-7] active 0 (0%), one 3383 (100%), zero 0 (0%)
c [score-dist-7] max exp 1, different 1 (50%)
c [score-dist-7] median active exp 0, avg 0.0
c [simplification-7] removed 2 variables 0.1% (3383 remain 88%)
c [simplification-7] removed 139 irredundant clauses 0.2% (59822 remain 78%)
c [simplification-7] maximum reduction of 0% = max (0%, 0%)
c [simplification-7] full geometric conflict interval increment 120000
c [simplification-7] new conflict interval 240000
c [simplification-7] penalized conflict interval 240000 = 1 * 240000
c [simplification-7] hard conflict limit 583003 (soft 463003 + delta 120000)
c [simplification-7] new conflict limit 463003 (hard 583003)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -   48.7    3383    59822    237391   47222   4601   168   16   349   17   5%    996   16   16   14  117%
c -   57.8    3383    59822    295561   56200   4750   169   17   369   11   5%   1013   16   18   15  120%
c -   66.3    3383    59822    351131   62389   4853   169   18   347   19   5%   1019  -13   20   17  119%
c -   74.4    3383    59822    406283   67609   4963   170   19   371   20   5%   1022    6   16   18   91%
c -   82.2    3383    59822    461600   71983   5036   170   20   378   21   5%   1023    5   20   19  108%
c 
c [simplification-8] limit 463003 conflicts (hard 583003) hit after 463005 conflicts
c [quatres-6] found 22041 quaternary clauses 19% in total
c [quatres-6-1] removed 32 duplicate quaternary clauses
c [quatres-6-1] added 18 double-self-subsuming ternary resolvents
c [quatres-6-2] added 309 single-self-subsuming ternary resolvents
c [quatres-6-2] added 158 quaternary resolvents
c [ternres-6] limit 21280703 with penalty 0 = 0 + 0
c [ternres-6] all 3383 free variables schedulable
c [ternres-6] 13 ternary resolvents (1 bin, 12 trn)
c [ternres-6] fully completed ternary resolution
c [gauss-3] limit 1064035 penalty 2 = 2 + 0
c [gauss-3] extracted 388 xors of average arity 3.0
c [gauss-3] connected 1164 occurrences of 116 variables (average 10.0)
c [gauss-3] limit 1064035 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [simpleprobe-3] 1919 schedulable variables 57%
c [simpleprobe-3] limit 42561407 penalty 1 = 1 + 0
c [simpleprobe-3] fully completed simple probing
c [simpleprobe-3] removed 0 variables, found 14 hbrs, 0 units
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 11 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 266008792 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 75 clauses out of 21331 (0%) of length 6
c [cce-4-1] eliminated 56 clauses out of 11435 (0%) of length 5
c [cce-4-1] eliminated 72 clauses out of 6211 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 203 large clauses in 29030775 steps
c [cce-4-1] allowing another 14515387 steps for small clauses
c [cce-4-1] scheduling 4565 clauses = 279 binary + 4286 ternary
c [cce-4-1] tried to eliminate 4565 small clauses 100%
c [cce-4-1] eliminated 1041 ternary clauses 24%
c [cce-4-1] eliminated 1041 small clauses 23%
c [cce-4-1] eliminated 1041 small clauses in 15748487 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] eliminated 1244 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 14331283 steps for small clauses
c [cce-4-2] scheduling 3524 clauses = 279 binary + 3245 ternary
c [cce-4-2] tried to eliminate 3524 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 1244 covered clauses in TOTAL during 2 rounds
c [sort-queue-8] sorted 3383 enqueued variables after 463005 conflicts
c [score-dist-8] active 0 (0%), one 3383 (100%), zero 0 (0%)
c [score-dist-8] max exp 1, different 1 (50%)
c [score-dist-8] median active exp 0, avg 0.0
c [simplification-8] removed 0 variables 0.0% (3383 remain 88%)
c [simplification-8] removed 1244 irredundant clauses 2.1% (58578 remain 77%)
c [simplification-8] maximum reduction of 2% = max (0%, 2%)
c [simplification-8] geometric conflict interval increment 80000 = 240000 / 3
c [simplification-8] new conflict interval 320000
c [simplification-8] penalized conflict interval 320000 = 1 * 320000
c [simplification-8] hard conflict limit 943005 (soft 783005 + delta 160000)
c [simplification-8] new conflict limit 783005 (hard 943005)
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 -   91.2    3383    58578    517769   75842   6426   174   21   387   21   5%   1024    9   25   20  126%
c -   99.3    3383    58578    574772   79779   6448   174   22   365   22   6%   1024  -20   25   21  117%
c -  107.3    3383    58578    632313   83290   6471   174   24   395   14   6%   1024    4   26   22  115%
c -  115.6    3383    58578    691032   87287   6497   174   23   411   14   6%   1024   13   19   23   83%
c -  124.1    3383    58578    750150   91324   6510   174   25   405   23   6%   1024    2   24   24  101%
c 
c [simplification-9] limit 783005 conflicts (hard 943005) hit after 783005 conflicts
c [quatres-7] found 24761 quaternary clauses 18% in total
c [quatres-7-1] removed 59 duplicate quaternary clauses
c [quatres-7-1] added 9 double-self-subsuming ternary resolvents
c [quatres-7-2] added 140 single-self-subsuming ternary resolvents
c [quatres-7-2] added 112 quaternary resolvents
c [ternres-7] limit 34981309 with penalty 0 = 0 + 0
c [ternres-7] all 3383 free variables schedulable
c [ternres-7] 9 ternary resolvents (1 bin, 8 trn)
c [ternres-7] fully completed ternary resolution
c [treelook-3] limit 3498130 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 3780 literals 56%
c [treelook-3] scheduling used 583382 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 3498130 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 872515 steps
c [treelook-3] fully completed tree based probing
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 1 transitive binary clauses
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 26235980 penalty 2 = 2 + 0
c [sweep-5-1] 1128 pos 52.8% + 1008 neg 47.2% = 2136 sched 63.1% ret 1247
c [sweep-5-1] 1173364 steps 172 queries 51.20 avg class size
c [sweep-5-1] 15856 decisions 171 SAT calls 410.78 avg env size
c [sweep-5-1] fully completed sweeping round
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-2] 1818 pos 53.7% + 1565 neg 46.3% = 3383 sched 100.0% ret 0
c [sweep-5-2] 1402336 steps 201 queries 73.98 avg class size
c [sweep-5-2] 18243 decisions 200 SAT calls 400.25 avg env size
c [sweep-5-2] fully completed sweeping round
c [sweep-5-2] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5-3] 1818 pos 53.7% + 1565 neg 46.3% = 3383 sched 100.0% ret 0
c [sweep-5-3] 1328805 steps 193 queries 92.28 avg class size
c [sweep-5-3] 18029 decisions 192 SAT calls 435.71 avg env size
c [sweep-5-3] fully completed sweeping round
c [sweep-5-3] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-5] removed 0 vars in TOTAL (3 rounds, 563 queries)
c [sort-queue-9] sorted 3383 enqueued variables after 783005 conflicts
c [score-dist-9] active 0 (0%), one 3383 (100%), zero 0 (0%)
c [score-dist-9] max exp 1, different 1 (50%)
c [score-dist-9] median active exp 0, avg 0.0
c [simplification-9] removed 0 variables 0.0% (3383 remain 88%)
c [simplification-9] removed 0 irredundant clauses 0.0% (58578 remain 77%)
c [simplification-9] maximum reduction of 0% = max (0%, 0%)
c [simplification-9] full geometric conflict interval increment 320000
c [simplification-9] new conflict interval 640000
c [simplification-9] penalized conflict interval 640000 = 1 * 640000
c [simplification-9] hard conflict limit 1743005 (soft 1423005 + delta 320000)
c [simplification-9] new conflict limit 1423005 (hard 1743005)
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 -  133.7    3383    58578    809328   94884   6671   174   25   405   14   6%   1024   -1   25   24  102%
c -  142.7    3383    58578    869247   98951   6678   174   26   413   25   6%   1024    3   25   25  100%
c -  151.8    3383    58578    928965  102194   6686   174   27   410   15   7%   1024    1   32   26  123%
c -  161.0    3383    58578    989319  105892   6697   174   27   424   25   6%   1024    9   31   26  117%
c -  170.4    3383    58578   1049993  109163   6710   174   27   414   26   6%   1024   -4   30   26  115%
c -  179.9    3383    58578   1111230  112430   6715   174   27   422   26   6%   1024    5   30   26  115%
c -  189.7    3383    58578   1173064  116366   6720   174   27   418   16   6%   1024    6   22   27   80%
c -  199.6    3383    58578   1234712  119866   6730   174   27   419   27   6%   1024    4   29   27  107%
c -  209.6    3383    58578   1296331  122733   6734   174   28   427   17   7%   1024   11   29   27  107%
c -  220.1    3383    58578   1358734  125413   6741   174   28   418   28   7%   1024    3   26   28   92%
c -  230.6    3383    58578   1422073  128613   6747   174   28   417   28   7%   1024    1   33   28  118%
c 
c [simplification-10] limit 1423005 conflicts (hard 1743005) hit after 1426694 conflicts
c [quatres-8] found 27570 quaternary clauses 16% in total
c [quatres-8-1] removed 107 duplicate quaternary clauses
c [quatres-8-1] added 9 double-self-subsuming ternary resolvents
c [quatres-8-2] added 79 single-self-subsuming ternary resolvents
c [quatres-8-2] added 50 quaternary resolvents
c [ternres-8] limit 68127738 with penalty 0 = 0 + 0
c [ternres-8] all 3383 free variables schedulable
c [ternres-8] 6 ternary resolvents (1 bin, 5 trn)
c [ternres-8] fully completed ternary resolution
c [card-4] limit 4257983 penalty 3 = 3 + 0
c [card-4] found 2 at-most-one constraints of average size 3.0
c [card-4] found 14 at-most-two constraints of average size 4.1
c [card-4] using previous limit 4257983 for elimination
c [card-4] 16 out of 16 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [unhide-4] limit 1703193 with penalty 3 = 3 + 0
c [unhide-4-6] 0 units, 0 failed, 200 tauts, 0 hbrs, 2634 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 0 transitive binary clauses
c [cce-5] limit of 170319347 steps penalty 1 = 1 + 0
c [cce-5-1] eliminated 2 clauses out of 21350 (0%) of length 6
c [cce-5-1] eliminated 3 clauses out of 11375 (0%) of length 5
c [cce-5-1] eliminated 13 clauses out of 6138 (0%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 18 large clauses in 31646113 steps
c [cce-5-1] allowing another 15823056 steps for small clauses
c [cce-5-1] scheduling 961 clauses = 284 binary + 677 ternary
c [cce-5-1] tried to eliminate 961 small clauses 100%
c [cce-5-1] eliminated 1 binary clauses 0%
c [cce-5-1] eliminated 6 ternary clauses 1%
c [cce-5-1] eliminated 7 small clauses 1%
c [cce-5-1] eliminated 7 small clauses in 16061944 steps
c [cce-5-1] completed small round (ACCE)
c [cce-5-1] completed small and large (ACCE)
c [cce-5-1] eliminated 25 covered clauses in round 1
c [cce-5-2] completed large round (ACCE)
c [cce-5-2] allowing another 15800214 steps for small clauses
c [cce-5-2] scheduling 954 clauses = 283 binary + 671 ternary
c [cce-5-2] tried to eliminate 954 small clauses 100%
c [cce-5-2] completed small round (ACCE)
c [cce-5-2] eliminated 0 covered clauses in round 2
c [cce-5] eliminated 25 covered clauses in TOTAL during 2 rounds
c [cce-5] 25 < 1/100 * 58576 = 585 considered unsuccessful
c [sort-queue-10] sorted 3383 enqueued variables after 1426694 conflicts
c [score-dist-10] active 0 (0%), one 3383 (100%), zero 0 (0%)
c [score-dist-10] max exp 1, different 1 (50%)
c [score-dist-10] median active exp 0, avg 0.0
c [simplification-10] removed 0 variables 0.0% (3383 remain 88%)
c [simplification-10] removed 27 irredundant clauses 0.0% (58551 remain 77%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] full geometric conflict interval increment 640000
c [simplification-10] conflict interval soft limit 1000000 reached
c [simplification-10] new conflict interval 1000000
c [simplification-10] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-10] hard conflict limit 2926694 (soft 2426694 + delta 500000)
c [simplification-10] new conflict limit 2426694 (hard 2926694)
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 -  243.2    3383    58551   1485854  131035   6694   170   29   418   29   7%   1024    7   24   29   85%
c -  254.3    3383    58551   1550372  134392   6697   170   30   426   29   7%   1024   10   38   29  130%
c -  265.4    3383    58551   1615101  137970   6700   170   29   417   18   7%   1024   -2   31   29  105%
c -  276.6    3383    58551   1679716  141056   6705   170   32   422   18   8%   1024    4   37   30  124%
c -  287.9    3383    58551   1744497  143799   6706   170   30   443   19   7%   1024   18   36   31  119%
c -  299.5    3383    58551   1809795  146535   6708   170   34   424   31   8%   1024   -1   42   31  133%
c -  310.8    3383    58551   1875570  149280   6710   170   32   434   19   7%   1024    8   32   31  103%
c -  323.0    3383    58551   1941721  151706   6713   170   33   427   19   8%   1024   -2   35   32  108%
c -  334.9    3383    58551   2008660  154621   6715   170   32   425   20   8%   1024   -4   33   32  104%
c -  346.8    3383    58551   2075796  157212   6718   170   30   436   20   7%   1024    6   32   32  101%
c -  359.2    3383    58551   2143583  159543   6719   170   33   410   20   8%   1024  -17   27   32   84%
c -  371.6    3383    58551   2212247  162774   6720   170   31   426   33   7%   1024   -0   38   32  119%
c -  384.3    3383    58551   2280889  164972   6721   170   33   423   21   8%   1024   -3   38   32  117%
c -  397.5    3383    58551   2350341  167981   6722   170   34   432   21   8%   1024    9   38   33  115%
c -  410.8    3383    58551   2419871  169587   6724   170   33   431   21   8%   1024    7   29   33   87%
c 
c [simplification-11] limit 2426694 conflicts (hard 2926694) hit after 2426696 conflicts
c [quatres-9] found 29405 quaternary clauses 14% in total
c [quatres-9-1] removed 130 duplicate quaternary clauses
c [quatres-9-1] added 2 double-self-subsuming ternary resolvents
c [quatres-9-2] added 46 single-self-subsuming ternary resolvents
c [quatres-9-2] added 64 quaternary resolvents
c [ternres-9] limit 130261487 with penalty 0 = 0 + 0
c [ternres-9] all 3383 free variables schedulable
c [ternres-9] 18 ternary resolvents (1 bin, 17 trn)
c [ternres-9] fully completed ternary resolution
c [block-4] scheduling all variables this time
c [block-4] scheduled 3383 variables 100%
c [block-4] limit of 100000000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 0 blocked clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 3383 variables 100%
c [elim-5] limit of 100000000 steps penalty 3 = 3 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 2 variables 0% in round 1 in 43614772 steps
c [elim-5-1] backward subsumption/strengthening limit 43614700
c [elim-5-1-1] backward checking 275 touched variables 8%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 0 and strengthened 0 clauses in 187400 steps
c [elim-5] fully completed in 1 rounds
c [elim-5] transition to [ all 0 rem 0 ] state
c [elim-5] eliminated 2 = 0% variables out of 3383 scheduled
c [elim-5] 2 < 1/100 * 3383 = 33 considered unsuccessful
c [bca-4] limit of 10000000 steps and 117594 added (scaled 2)
c [bca-4] 2 out of 6764 literals actually usable 0%
c [bca-4] not enough literals usable
c [bca-4] added 0 blocked clauses in 176201 steps
c [sort-queue-11] sorted 3381 enqueued variables after 2426696 conflicts
c [score-dist-11] active 0 (0%), one 3381 (100%), zero 0 (0%)
c [score-dist-11] max exp 1, different 1 (50%)
c [score-dist-11] median active exp 0, avg 0.0
c [simplification-11] removed 2 variables 0.1% (3381 remain 88%)
c [simplification-11] removed 4 irredundant clauses 0.0% (58547 remain 77%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 1000000
c [simplification-11] conflict interval soft limit 1000000 reached
c [simplification-11] new conflict interval 1000000
c [simplification-11] penalized conflict interval 1000000 = 1 * 1000000
c [simplification-11] hard conflict limit 3926696 (soft 3426696 + delta 500000)
c [simplification-11] new conflict limit 3426696 (hard 3926696)
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 -  425.7    3381    58547   2490892  171704   6757   169   33   433   21   8%   1024   10   37   33  109%
c -  439.1    3381    58547   2562640  175127   6757   169   34   446   21   8%   1024   18   39   33  116%
c -  453.3    3381    58547   2633877  176341   6761   169   34   423   22   8%   1024   -6   38   33  115%
c -  467.9    3381    58547   2707058  178543   6761   169   33   427   22   8%   1024   -3   34   33  104%
c -  482.7    3381    58547   2780988  180989   6763   169   34   442   22   8%   1024    6   39   33  118%
c -  497.5    3381    58547   2855664  183407   6765   169   33   430   22   8%   1024   -2   38   33  115%
c -  512.7    3381    58547   2930656  185854   6767   169   34   427   37   8%   1024   -2   40   34  117%
c -  527.7    3381    58547   3006283  188216   6769   169   37   434   37   8%   1024    4   32   34   94%
c -  543.2    3381    58547   3082702  191328   6770   169   33   439   23   7%   1024   10   35   34  103%
c -  558.8    3381    58547   3158840  193433   6770   169   34   423   23   8%   1024  -10   22   35   62%
c -  574.6    3381    58547   3235896  195598   6770   169   35   424   23   8%   1024   -9   44   34  128%
c -  590.4    3381    58547   3313804  197785   6772   169   35   448   23   8%   1024   16   41   34  118%
c -  606.8    3381    58547   3392822  200693   6772   169   33   416   24   8%   1024  -13   27   34   79%
c 
c [simplification-12] limit 3426696 conflicts (hard 3926696) hit after 3436955 conflicts
c [quatres-10] found 30546 quaternary clauses 13% in total
c [quatres-10-1] removed 107 duplicate quaternary clauses
c [quatres-10-2] added 30 single-self-subsuming ternary resolvents
c [quatres-10-2] added 54 quaternary resolvents
c [ternres-10] limit 200000000 with penalty 0 = 0 + 0
c [ternres-10] all 3381 free variables schedulable
c [ternres-10] 5 ternary resolvents (0 bin, 5 trn)
c [ternres-10] fully completed ternary resolution
c [gauss-4] limit 5078076 penalty 3 = 3 + 0
c [gauss-4] extracted 4453 xors of average arity 4.9
c [gauss-4] connected 22005 occurrences of 947 variables (average 23.2)
c [gauss-4] limit 5078076 penalty 3 = 3 + 0
c [gauss-4] connected 2601 occurrences of 947 variables (average 2.7)
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 100000000 penalty 2 = 2 + 0
c [basicprobe-3-0] 509 sched 15%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-3-0] fully completed probing
c [transred-8] limit 1000000 with penalty 1 = 1 + 0
c [transred-8] removed 0 transitive binary clauses
c [sort-queue-12] sorted 3381 enqueued variables after 3436955 conflicts
c [score-dist-12] active 0 (0%), one 3381 (100%), zero 0 (0%)
c [score-dist-12] max exp 1, different 1 (50%)
c [score-dist-12] median active exp 0, avg 0.0
c [simplification-12] removed 0 variables 0.0% (3381 remain 88%)
c [simplification-12] removed 0 irredundant clauses 0.0% (58547 remain 77%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 1000000
c [simplification-12] new conflict interval 2000000
c [simplification-12] penalized conflict interval 2000000 = 1 * 2000000
c [simplification-12] hard conflict limit 6436955 (soft 5436955 + delta 1000000)
c [simplification-12] new conflict limit 5436955 (hard 6436955)
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 -  624.4    3381    58547   3471726  202852   6808   169   35   429   24   8%   1024    2   35   35  100%
c -  641.6    3381    58547   3551494  204239   6808   169   35   436   24   8%   1024    9   32   35   93%
c -  659.5    3381    58547   3633010  206466   6810   169   35   436   25   8%   1024    8   39   34  114%
c -  677.3    3381    58547   3715220  208904   6811   169   35   426   25   8%   1024   -0   35   35  101%
c -  695.3    3381    58547   3798106  211854   6812   169   36   440   25   8%   1024    9   27   35   78%
c -  713.1    3381    58547   3880831  214581   6814   169   37   423   25   9%   1024   -4   40   35  116%
c -  731.2    3381    58547   3963970  216773   6816   169   34   410   26   8%   1024  -19   40   35  115%
c -  749.6    3381    58547   4047876  218710   6816   169   35   425   26   8%   1024   -6   30   35   85%
c -  768.8    3381    58547   4132906  221070   6819   169   34   421   26   8%   1024   -8   34   35   98%
c -  788.2    3381    58547   4218613  223836   6819   169   35   438   26   8%   1024   10   38   35  108%
c -  807.6    3381    58547   4304527  226135   6819   169   36   426   26   8%   1024   -2   41   35  115%
c -  827.1    3381    58547   4391043  228034   6821   169   35   425   27   8%   1024   -8   34   35   98%
c -  847.5    3381    58547   4478727  230520   6821   169   35   448   27   8%   1024   18   35   35  100%
c -  867.9    3381    58547   4566896  232916   6822   169   36   423   27   9%   1024  -10   32   36   88%
c -  888.4    3381    58547   4655758  236709   6825   169   36   429   27   8%   1024   -5   29   36   80%
c -  908.5    3381    58547   4743619  238397   6826   169   36   432   27   8%   1024   -0   41   36  114%
c -  929.7    3381    58547   4832734  240556   6827   169   35   437   28   8%   1024    5   37   36  103%
c -  950.5    3381    58547   4922531  241974   6829   169   35   450   28   8%   1024   15   43   36  120%
c -  972.1    3381    58547   5013747  243490   6830   169   36   429   28   8%   1024   -7   42   35  118%
c -  994.4    3381    58547   5106427  246650   6831   169   37   443   28   8%   1024    8   36   36  100%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 33 basic ate = 31 trn 94% + 2 lrg 6% in 1 updates
c bcas: 4 count, 0 added (0 skipped), 311012 steps
c bkwd: tried 6156 clauses, 12253 lits, 1.99 lits/clause
c bkwd: checked 632958 occs, 102.82 occs/clause, 51.66 occs/lit
c bkwd: subsumed 0 binary, 2 ternary, 17 large
c bkwd: strengthened 0 binary, 3 ternary (100% self), 67 large (0% self)
c blkd: 4 bces, 235 removed, 3114275 resolutions, 6373068 steps
c blkd: 29 blocking literals 0%, 0 pure
c bump: 5093800 bumped seen, 418380581 lits 82.1 on average
c card: 4 count, 0 units, 0 am1, 8009721 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 1443 subsumed
c card: 10 at-most-one constraints found, average size 3.00
c card: 10 at-most-one constraints used 100%, average size 3.00
c card: 43 at-most-two constraints found, average size 4.09
c card: 42 at-most-two constraints used 98%, average size 4.10
c cces: 5 cces, 8622 eliminated, 8620 ate 100%, 2 abce 0%
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: 1006239 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 45 gcs, 0 rescored clauses, 0 rescored vars
c dcps: 32 decompositions, 220 equivalent 5%
c deco: 916 decision-only clauses 0%, 42% reduction
c decs: 40629775 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 5 elims, 159 eliminated 4%, 0 pure 0%
c elms: 9 rounds, 1.8 rounds/bve
c elms: 159 small 100%, 0 large 0%
c elms: 1588 tried small, 160 succeeded 10%, 1428 failed 90%
c elms: 2120 subsumed, 3167 strengthened, 0 blocked
c elms: 1182072 copies, 2933397 resolutions, 441092 ipos
c elms: 233933 subchks, 165179 strchks
c gaus: 4 extractions, 10107 extracted, 4.7 size, 7 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 2 gc, 18284590 steps, 9142295 extr 50%, 382797 elim 2%
c glue: 30.7 orig avg, 30.7 real avg, 4.6 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 96 = 19 simple 20% + 71 trn 74% + 6 lrg 6%, 35 sub 36%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 5093799 clauses, 60.5 length
c lrnd: 308409284 lits = 324125562 orig - 15716278 removed 5%
c lrnd: 2450115 uips 48%, 2076190 flips 41%
c mins: 4685195 mins 92%, 31 bin 0%, 398930 size 8%
c mins: 235580834 poisoned searches, 19232243 hits, 8% hit rate
c mins: 491134107 used twice searches, 101518129 hits, 21% hit rate
c move: moved 1363, 8 bin 1%, 1355 trn 99%
c otfs: 42136 driving 51%, 40789 restarting 49%
c otfs: str 82925, 81209 red 98%, 1716 irr 2%
c otfs: str 82925, 0 bin 0%, 92 trn 0%, 82833 lrg 100%
c otfs: sub 511, 507 red 99%, 4 irr 1%
c otfs: sub 511, 0 bin 0%, 14 trn 3%, 497 lrg 97%
c phas: 1 computed, 3423 set, 1476 pos (43%), 1947 neg (57%)
c prbs: 3 basic, 4386 probed, 0 failed, 0 lifted
c prbs: 3 simple, 16223 probed, 51 failed, 143 eqs
c prbs: 3 treelook, 5615 probed, 1 failed, 0 lifted
c prom: 675149 locked 18% out of 3778590 tried
c prps: 569691364 props, 14 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 10 count, 2011 quat, 2321 self1, 237 self2, 454 dup
c queu: 12 sorted, 40629775 next (161 steps 0.00)
c queu: 418425516 enq (0 steps 0.00), 418380581 deq 100%
c redc: 837 clauses 0%, 613034 tried 12%, 1 sat 0%
c redc: 860 lits 0%, 5063429 tried 2%, 1 sat 0%
c redc: 41 times jump level reduced, 19.3 levels on average
c reds: 72 count, 71280.2 conflicts per reduce
c reds: 0 memlim 0%, 72 arith 100%
c reds: 3027611 collected 63%, 1763790 retired 37%
c rmbd: 25 removed, 11 red 44%
c rsts: 36742 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c simp: 12 count, 12 confs 100%, 0 vars 0%
c simp: 0 its 0%, 0 bin 0%, 0 trns 0%
c subl: 5093799 count (8148034 tried 1.6), 25012 sub out of 5091787 (0.5%)
c swps: 5 count, 13 rounds, 3796 queries (292.0/round)
c swps: 3797 sat calls, 8 unsat (1.0% success rate)
c swps: 119532 decisions 31.5, 3759 conflicts 1.0
c swps; 169.5 avg class size, 87.1 avg environment size
c swps: 0 failed, 10 impls, 7 equivs
c swp0: 1262 type 0 queries, 27 unsat (2.1%), 1260 sat (99.8%)
c swp1: 2534 type 1 queries, 136 unsat (5.4%), 2529 sat (99.8%)
c sync: 0 produced units, 0 successful consumptions 0%
c sync: 0 consume units calls, 0 tried 0%, 0 success 0%
c sync: 0 produced clauses, 0 successful consumptions 0%
c sync: 0 consume clause calls, 0 tried 0%, 0 success 0%
c time: 91447409 calls to obtain time
c tops: 528 fixed 12%, 0 its, 0.00 confs/it
c trds: 8 transitive reductions, 37 removed, 0 failed
c trds: 53811 nodes, 3346 edges, 4793 steps
c trim: 206166 words, 0.8 MB
c trnr: 10 count, 39 bin, 372 trn, 15574026 steps
c unhd: 4 count, 6 rounds, 2723195 steps
c unhd: 0 non-trivial sccs of average size 0.0
c unhd: 0 units, 0 bin, 0 trn, 0 lrg
c unhd: 0 failed, 0 stamp, 0 lits, 0 bin, 0 trn, 0 lrg
c unhd: 985 tauts, 0 bin 0%, 683 trn 69%, 295 lrg 30%
c unhd: 985 tauts, 7 stamp 1%, 529 red 54%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 4238 str, 0 bin 0%, 65 trn 2%, 4173 lrg 98%, 4163 red 98%
c vars: 3381 remaining 79% and 907 removed 21% out of 4288
c vars: 528 fixed 12%, 159 eliminated 4%, 220 equivalent 5%
c vsts: 34572505412 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 60.7 search visits per propagation, 6735.0 per conflict
c wchs: 11237623446 pushed, 16221434 enlarged, 1198 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all        5093798       3027611       1763790     226409864      43717629       2570407
c 
c  0 0        221250   4       349   0         0   0 188588189  83< 33293257  76   1971224  77     7.0
c  1 5        260832   5    124880   4    117916   7  20538876   9   3969136   9<   257717  10<    0.7
c  2 6        858698  17    454969  15    384419  22   9100741   4   2333799   5    139890   5     1.1
c  3 9        857094  17    492195  16    354198  20   2898670   1   1157055   3     54637   2     1.1
c  4 14       673562  13    427722  14    238751  14<  1658308   1    819884   2     36284   1     1.3
c  5 21       545039  11<   361436  12<   177823  10   1106975   0    604963   1     26672   1     1.7
c  6 30       425071   8    289128  10    131396   7    733638   0    426614   1     19832   1     2.0
c  7 41       339951   7    236269   8     99979   6    525724   0    319569   1     15468   1     2.5
c  8 54       272549   5    193199   6     76463   4    393633   0    246459   1     12864   1     2.9
c  9 69       217283   4    155753   5     58866   3    299925   0    191600   0     10925   0     3.2
c 10 86       286795   6    204440   7     78223   4    385662   0    247609   1     16075   1     6.6
c 11 126      130300   3     84222   3     43735   2    172451   0    103119   0      8227   0     4.8
c 12 230        5368   0      3047   0      2019   0      7063   0      4561   0       592   0     0.3
c 13 534           6   0         2   0         2   0         9   0         4   0         0   0     0.0
c 
c avg                  4.6           5.1           4.4           0.4           0.7           0.6
c std                  2.8           2.7           2.6           1.1           1.7           1.7
c 
c   27.979   3% decide
c   27.750   3% bump
c    2.901   0% cce
c 
c    3.901 < 1% rest (below)
c 
c    2.107   0% elim
c    1.093   0% sweep
c    0.824   0% quatres
c    0.620   0% probe
c    0.501   0% block
c    0.346   0% gauss
c    0.221   0% unhide
c    0.129   0% card
c    0.088   0% ternres
c    0.067   0% bca
c    0.011   0% transred
c    0.000   0% locs
c    0.000   0% queuesort
c    0.000   0% rescore
c ==================================
c    0.487   0% preprocessing     5%
c    9.485   1% inprocessing     95%
c ==================================
c    9.972   1% simplifying
c  989.931  99% search
c ==================================
c  999.902 100% all
c 
c       5132177 conflicts,        5132.7 confs/sec
c          1675 ternaries,        3064.0 confs/ternary
c            43 binaries,       119353.0 confs/binary
c             0 iterations,          0.0 confs/iteration
c 
c            72 reductions,          0.1 redus/sec,  71280.2 confs/reduction
c         36742 restarts,           36.7 rests/sec,    139.7 confs/restart
c      40629775 decisions,       40633.7 decis/sec,      7.9 decis/conflict
c     569691364 propagations,   569747.0 props/sec,     14.0 props/decision
c 
c 999.9 seconds, 109.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
