c launch: /data/cnf/sc2014/app/AProVE09-06.cnf.bz2
c host: atom21
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/AProVE09-06.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/AProVE09-06.cnf.bz2
c no embedded options
c found 'p cnf 77262 263137' header
c read 77262 variables, 263137 clauses, 679549 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=5
c --scoreshift=0
c --scoreresetint=2147483647
c --seed=0
c --simpbintinc=100
c --simpbintinclim=10000
c --simpcintdelay=2000
c --simpcintinc=20000
c --simpcintincdiv=1
c --simpcintmaxhard=10000000
c --simpcintmaxsoft=1000000
c --simpincdelmaxfact=50
c --simpincdelmaxmin=10000
c --simpinitdelay=0
c --simpintsizepen=0
c --simpen=0
c --simpidiv=3
c --simpiscale=100
c --simpitdelay=10
c --simpitintinc=10
c --simpitintinclim=1000
c --simplify=2
c --simprtc=5
c --simptintinc=1000
c --simptintinclim=10000
c --simpvarchg=100
c --simpvarlim=100
c --sizemaxpen=5
c --sizepen=1000000
c --sleeponabort=0
c --smallirr=90
c --smallve=1
c --smallvevars=10
c --smallvewait=0
c --sortlits=0
c --subl=9
c --sweep=1
c --sweepboost=10
c --sweepboostdel=4
c --sweepboostint=7
c --sweepboostvlim=1000000
c --sweepfacdec=10
c --sweepforgive=2
c --sweepirr=3
c --sweepmaxeff=200000000
c --sweepmaxdec=10000
c --sweepmaxround=3
c --sweepmindec=100
c --sweepmineff=1000000
c --sweepred=3
c --sweepreleff=3
c --sweeprtc=0
c --sweeprtcint=14
c --sweeprtcintvlim=100000
c --sweepsuccessmaxwortc=6
c --sweepsuccessrat=1000
c --sweepwait=2
c --synclsall=1
c --synclsglue=8
c --synclsint=100
c --synclslen=40
c --syncunint=111111
c --termint=122222
c --ternres=1
c --ternresboost=5
c --ternresrtc=0
c --ternreswait=2
c --transred=1
c --transredwait=2
c --trapiflush=0
c --trdmaxeff=2000000
c --trdmineff=100000
c --trdreleff=10
c --treelook=1
c --treelookboost=10
c --treelookfull=0
c --treelookmaxeff=50000000
c --treelookmineff=300000
c --treelookreleff=2
c --treelookrtc=0
c --trep=1
c --trepint=55555
c --trnreleff=10
c --trnrmaxeff=200000000
c --trnrmineff=4000000
c --unhdatrn=2
c --unhdextstamp=1
c --unhdhbr=0
c --unhdlnpr=3
c --unhdmaxeff=20000000
c --unhdmineff=100000
c --unhdreleff=2
c --unhdroundlim=20
c --unhide=1
c --unhidewait=0
c --usedtwice=1
c --vsidsdint=256
c --wait=1
c --waitmax=4
c --witness=0
c --check=0
c --log=-1
c --profile=1
c --profilelong=1
c --verbose=1
c [freezer] frozen 0 variables out of 77185 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] EVSIDS (--score=5)
c [set-score-increment-1] factor 1.200000d+00 (200/1000) after 0 conflicts
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c *    0.0   77185   262886         0       0      0     0    0     0   16   0%      0    0    0    0    0%
c 
c [simplification-1] limit 0 conflicts (hard 0) hit after 0 conflicts
c [card-1] limit 2000000 penalty 0 = 0 + 0
c [card-1] no at-most-one constraint found
c [card-1] no at-most-two constraint found
c [decomp-1] removed 1104 variables
c [simpleprobe-1] all 76158 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 297 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 297 variables, found 12929 hbrs, 102 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 0 units, 0 failed, 120 tauts, 0 hbrs, 13 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 75861 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 893 not tried 1% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 41942 = 55% variables out of 75861 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 189358 negative 99.1% of 191030 except 1672 0.9%
c [phase-count-1] 184954 positive 96.8% of 191030 except 6076 3.2%
c [phase-count-1] less non-negative clauses 1672 than limit 19100 (10.0%)
c [phase-count-1] non-pos/non-neg = 6076/1672 = 3.63 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 33919 negative 100%
c [sort-queue-1] sorted 33919 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 33919 (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 43266 variables 56.1% (33919 remain 44%)
c [simplification-1] removed 71856 irredundant clauses 27.3% (191030 remain 73%)
c [simplification-1] maximum reduction of 56% = max (56%, 27%)
c [simplification-1] large reduction 56% >= 5% limit
c [simplification-1] next conflict interval 1000 = 2000/2
c [simplification-1] penalized conflict interval 1000 = 1 * 1000
c [simplification-1] hard conflict limit 11000 (soft 1000 + delta 10000)
c [simplification-1] new conflict limit 1000 (hard 11000)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    3.4   33918   191030       121      90     19  2820    0     4   21   3%      0    4    2    0 20313%
c i    3.5   33827   191030       486     353     96  2834    1     8   21   6%      1    8    4    0 12799%
c i    3.5   33825   191030       490     356     96  2834    1     8   21   6%      1    8    4    0 12726%
c i    3.5   33822   191030       493     358     96  2834    1     8   21   6%      1    8    4    0 12646%
c i    3.5   33821   191030       494     358     96  2834    1     8   21   6%      1    8    4    0 12596%
c i    3.5   33820   191030       495     358     96  2834    1     8   21   6%      1    8    4    0 12547%
c i    3.5   33818   191030       534     379    106  2839    1     8   21   6%      1    8    4    0 11347%
c i    3.5   33815   191030       556     385    115  2841    1     8   21   7%      1    8    4    0 10910%
c i    3.5   33812   191030       602     417    123  2843    1     9   21   7%      1    9    4    0 10155%
c i    3.5   33810   191030       631     436    128  2843    1     9   21   7%      1    9    4    0 10065%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 147 variables
c [simpleprobe-2] all 33772 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 2 variables
c [simpleprobe-2] 29865 variables remain 88% (3905 retained 12%)
c [simpleprobe-2] removed 2 variables, found 639 hbrs, 2 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 26096 literals 39%
c [treelook-1] scheduling used 300012 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 300021 steps
c [treelook-1] 25835 literals remain 38%
c [treelook-1] 22419 variables remain to probed next time 66%
c [treelook-1] removed 0 variables, found 2102 hbrs
c [basicprobe-1] limit 1522072 based on 190259 irredundant clauses
c [basicprobe-1-0] 10322 probes remain 31% after last round
c [basicprobe-1-0] 29 units = 29 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 39 variables, found 2349 hbrs
c [elim-2] 891 variables 3% will be scheduled this time
c [elim-2] scheduled 891 variables 3%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] no variable eliminated in round 1 in 2960745 steps
c [elim-2] fully completed in 1 rounds
c [elim-2] transition to [ all 0 rem 0 ] state
c [elim-2] eliminated 2 = 0% variables out of 891 scheduled
c [elim-2] 2 < 1/100 * 891 = 8 considered unsuccessful
c [sort-queue-2] sorted 28888 enqueued variables after 631 conflicts
c [score-dist-2] active 4841 (14%), one 0 (0%), zero 28888 (86%)
c [score-dist-2] max exp 662, different 155 (23%)
c [score-dist-2] median active exp 595, avg 581.0
c [simplification-2] removed 78 variables 0.2% (33729 remain 44%)
c [simplification-2] removed 1085 irredundant clauses 0.6% (189945 remain 72%)
c [simplification-2] maximum reduction of 1% = max (0%, 1%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1025 (hard 11000)
c [simplification-2] new iteration interval 100
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    4.2   33728   189945       632     427    123  7672    1     9   20   7%      1    9    4    0 10026%
c i    4.2   33727   189945       659     446    129  7672    1     9   20   7%      1    9    4    0 9515%
c i    4.2   33725   189945       662     447    130  7672    1     9   20   7%      1    9    4    0 9427%
c i    4.2   33724   189945       699     471    138  7673    1     9   20   7%      1    9    4    0 8799%
c i    4.2   33721   189945       776     534    145  7677    1    10   21   8%      1   10    4    0 8558%
c i    4.3   33720   189945       872     597    166  7683    1    10   21   8%      1   10    4    0 7573%
c i    4.3   33718   189945      1031     713    200  7688    1    11   21   9%      1   11    4    0 6456%
c 
c [simplification-3] limit 1038 conflicts (hard 11000) hit after 1039 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 272 at-most-one constraints of average size 3.0
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 272 out of 272 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 53 variables
c [unhide-2] limit 50000 with penalty 1 = 1 + 0
c [unhide-2-2] 14 units, 8 failed, 148 tauts, 0 hbrs, 1226 literals
c [block-1] scheduling all variables this time
c [block-1] scheduled 33653 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 3485 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 125 (1%) of length 10
c [cce-1-1] eliminated 2 clauses out of 143 (1%) of length 7
c [cce-1-1] eliminated 1 clauses out of 205 (0%) of length 6
c [cce-1-1] eliminated 24 clauses out of 1453 (2%) of length 5
c [cce-1-1] eliminated 2456 clauses out of 79339 (3%) of length 4
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 2484 large clauses in 30000034 steps
c [cce-1-1] allowing another 15000017 steps for small clauses
c [cce-1-1] scheduling 83159 clauses = 26338 binary + 56821 ternary
c [cce-1-1] tried to eliminate 18231 small clauses 22%
c [cce-1-1] eliminated 128 binary clauses 0%
c [cce-1-1] eliminated 412 ternary clauses 1%
c [cce-1-1] eliminated 540 small clauses 1%
c [cce-1-1] eliminated 540 small clauses in 30000004 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 3024 covered clauses in round 1
c [cce-1] eliminated 3024 covered clauses in TOTAL during 1 rounds
c [bca-1] limit of 10000000 steps and 366634 added (scaled 2)
c [bca-1] 64639 out of 67308 literals actually usable 96%
c [bca-1] added 497 blocked clauses in 175044 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 2878 pos 8.6% + 30775 neg 91.4% = 33653 sched 100.0% ret 0
c [sweep-1-1] 1005515 steps 108 queries 4853.31 avg class size
c [sweep-1-1] 831 decisions 106 SAT calls 20.08 avg env size
c [sweep-1-1] 32725 variables remain 97% (928 retained 3%)
c [decomp-7] removed 40 variables
c [sweep-1-1] removed 40 vars (0 failed, 1 eqs, 4 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 40 vars in TOTAL (1 rounds, 107 queries)
c [sort-queue-3] sorted 28494 enqueued variables after 1039 conflicts
c [score-dist-3] active 5119 (15%), one 0 (0%), zero 28494 (85%)
c [score-dist-3] max exp 770, different 203 (26%)
c [score-dist-3] median active exp 599, avg 600.9
c [simplification-3] removed 101 variables 0.3% (33613 remain 44%)
c [simplification-3] removed 6988 irredundant clauses 3.7% (182957 remain 70%)
c [simplification-3] maximum reduction of 4% = max (0%, 4%)
c [simplification-3] geometric conflict interval increment 4000 = 20000 / 5
c [simplification-3] new conflict interval 4000
c [simplification-3] penalized conflict interval 4000 = 1 * 4000
c [simplification-3] hard conflict limit 15039 (soft 5039 + delta 10000)
c [simplification-3] new conflict limit 5039 (hard 15039)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    5.8   33612   182957      1077     733   2918  7725    1    11   20   9%      1   11    4    0 6076%
c i    5.8   33611   182957      1078     733   2918  7725    1    11   20   9%      1   11    4    0 6052%
c i    5.8   33610   182957      1080     732   2919  7725    1    11   20   9%      1   11    4    0 6028%
c i    5.8   33609   182957      1120     757   2928  7727    1    11   20   9%      1   11    4    0 5729%
c i    5.8   33607   182957      1121     757   2928  7727    1    11   20   9%      1   11    4    0 5707%
c i    5.8   33601   182957      1122     757   2928  7727    1    11   20   9%      1   11    4    0 5685%
c i    5.8   33598   182957      1123     757   2928  7727    1    11   20   9%      1   11    4    0 5663%
c i    5.8   33596   182957      1124     757   2928  7727    1    11   20   9%      1   11    4    0 5641%
c i    5.8   33595   182957      1129     759   2928  7727    1    11   20   9%      1   11    4    0 5592%
c i    5.8   33592   182957      1132     760   2929  7727    1    11   20   9%      1   11    4    0 5548%
c i    5.8   33590   182957      1140     761   2933  7729    1    11   20   9%      1   11    4    0 5418%
c i    5.8   33589   182957      1155     767   2936  7732    1    11   20   9%      1   11    4    0 5249%
c i    5.9   33588   182957      1232     818   2950  7737    1    11   20  10%      1   11    4    0 4858%
c i    5.9   33586   182957      1236     819   2951  7738    1    11   20  10%      1   11    4    0 4795%
c i    6.0   33581   182957      2322    1581   3174  7785    2    16   21  12%      7   15    5    0 3190%
c i    6.1   33580   182957      2656    1844   3228  7792    2    17   21  13%      6   17    5    0 3071%
c i    6.4   33578   182957      4212    3139   3415  7815    4    21   21  17%     13   20    7    0 2088%
c i    6.4   33573   182957      4213    3139   3415  7815    4    21   21  17%     13   20    7    0 2080%
c i    6.4   33570   182957      4218    3142   3415  7815    4    21   21  17%     13   20    7    0 2058%
c i    6.4   33567   182957      4222    3140   3416  7817    4    21   21  17%     13   20    7    0 2030%
c i    6.5   33556   182957      4630    3477   3458  7828    4    22   21  17%      9   21    6    0 1709%
c i    6.5   33555   182957      4631    3477   3458  7828    4    22   21  17%      9   21    6    0 1702%
c 
c [simplification-4] limit of 138 binary hit after 138 binaries
c [quatres-1] found 77291 quaternary clauses 96% in total
c [quatres-1-2] added 356 single-self-subsuming ternary resolvents
c [quatres-1-2] added 408 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 33555 free variables schedulable
c [ternres-1] 3697 ternary resolvents (91 bin, 3606 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 11191 xors of average arity 3.0
c [gauss-1] connected 33525 occurrences of 3853 variables (average 8.7)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-8] removed 35 variables
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] scheduled 12215 literals 18%
c [treelook-2] scheduling used 150002 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 150000 penalty 1 = 1 + 0 boost 1
c [treelook-2] used 150001 steps
c [treelook-2] 11891 literals remain 18%
c [treelook-2] 9048 variables remain to probed next time 27%
c [decomp-9] removed 10 variables
c [treelook-2] removed 13 variables, found 189 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 11 units, 10 failed, 196 tauts, 0 hbrs, 1259 literals
c [transred-1] limit 274433 with penalty 0 = 0 + 0
c [transred-1] removed 13 transitive binary clauses
c [transred-1] found 1 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 33452 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 30 blocked clauses
c [block-2] 30 < 1/100 * 182225 = 1822 considered unsuccessful
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 4 clauses out of 1419 (0%) of length 5
c [cce-2-1] eliminated 184 clauses out of 76172 (0%) of length 4
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] eliminated 188 large clauses in 30000003 steps
c [cce-2-1] allowing another 15000001 steps for small clauses
c [cce-2-1] scheduling 47515 clauses = 26354 binary + 21161 ternary
c [cce-2-1] tried to eliminate 13762 small clauses 29%
c [cce-2-1] eliminated 132 binary clauses 1%
c [cce-2-1] eliminated 136 ternary clauses 1%
c [cce-2-1] eliminated 268 small clauses 1%
c [cce-2-1] eliminated 268 small clauses in 30000003 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 456 covered clauses in round 1
c [cce-2] eliminated 456 covered clauses in TOTAL during 1 rounds
c [cce-2] 456 < 1/100 * 181991 = 1819 considered unsuccessful
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 33452 variables 100%
c [elim-3] limit of 10000000 steps penalty 1 = 1 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 9527 not tried 28% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 2790 = 8% variables out of 33452 scheduled
c [bca-2] limit of 10000000 steps and 356092 added (scaled 2)
c [bca-2] 57139 out of 61326 literals actually usable 93%
c [bca-2] added 138 blocked clauses in 163205 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1056 pos 3.5% + 28798 neg 96.5% = 29854 sched 97.4% ret 808
c [sweep-2-1] 1005542 steps 72 queries 2956.94 avg class size
c [sweep-2-1] 857 decisions 71 SAT calls 27.54 avg env size
c [sweep-2-1] 28920 variables remain 94% (1742 retained 6%)
c [sweep-2-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 0 vars in TOTAL (1 rounds, 71 queries)
c [sort-queue-4] sorted 28603 enqueued variables after 5003 conflicts
c [score-dist-4] active 2059 (7%), one 4285 (14%), zero 24318 (79%)
c [score-dist-4] max exp 799, different 145 (18%)
c [score-dist-4] median active exp 761, avg 728.3
c [simplification-4] removed 2893 variables 8.6% (30662 remain 40%)
c [simplification-4] removed 5285 irredundant clauses 2.9% (177672 remain 68%)
c [simplification-4] maximum reduction of 9% = max (9%, 3%)
c [simplification-4] forced so keeping old conflict interval 4000
c [simplification-4] conflict limit remains at 5126 (hard 15039)
c [simplification-4] new binary interval 1000
c 
c [simplification-5] limit 5126 conflicts (hard 15039) hit after 5129 conflicts
c [quatres-2] found 75552 quaternary clauses 93% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 364 single-self-subsuming ternary resolvents
c [quatres-2-2] added 367 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 30662 free variables schedulable
c [ternres-2] 594 ternary resolvents (12 bin, 582 trn)
c [ternres-2] 378 variables remain 1% (30284 retained 99%)
c [basicprobe-2] limit 1427800 penalty 0 = 0 + 0
c [basicprobe-2-0] 5481 probes remain 18% after last round
c [basicprobe-2-0] removed 0 variables, found 3803 hbrs
c [bate-1] eliminated 366 asymmetric tautologies during probing
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 0 units, 1 failed, 538 tauts, 0 hbrs, 1705 literals
c [transred-2] limit 285560 with penalty 0 = 0 + 0
c [transred-2] removed 13 transitive binary clauses
c [elim-4] 9527 variables 31% will be scheduled this time
c [elim-4] scheduled 9527 variables 31%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 18 variables 0% in round 1 in 43176510 steps
c [elim-4-1] backward subsumption/strengthening limit 43176500
c [elim-4-1-1] backward checking 1900 touched variables 6%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 10 and strengthened 130 clauses in 16484437 steps
c [elim-4-1] rescheduled 292 variables 1% by backward subsumption
c [elim-4-2] eliminated 61 variables 0% in round 2 in 24483109 steps
c [elim-4-2] backward subsumption/strengthening limit 24483100
c [elim-4-2-1] backward checking 329 touched variables 1%
c [elim-4-2-1] fully completed backward checking in 1 rounds
c [elim-4-2] subsumed 1 and strengthened 4 clauses in 4534054 steps
c [elim-4-2] rescheduled 13 variables 0% by backward subsumption
c [elim-4-3] no variable eliminated in round 3 in 1146828 steps
c [elim-4] fully completed in 3 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 79 = 1% variables out of 9527 scheduled
c [elim-4] 79 < 1/100 * 9527 = 95 considered unsuccessful
c [bca-3] limit of 10000000 steps and 352679 added (scaled 2)
c [bca-3] 56458 out of 61166 literals actually usable 92%
c [bca-3] added 21 blocked clauses in 160065 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 776 pos 2.7% + 28070 neg 97.3% = 28846 sched 94.3% ret 1736
c [sweep-3-1] 1008169 steps 125 queries 2843.81 avg class size
c [sweep-3-1] 730 decisions 124 SAT calls 15.34 avg env size
c [sweep-3-1] 27780 variables remain 91% (2802 retained 9%)
c [decomp-12] removed 1 variables
c [sweep-3-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 1 vars in TOTAL (1 rounds, 124 queries)
c [sort-queue-5] sorted 28372 enqueued variables after 5129 conflicts
c [score-dist-5] active 2209 (7%), one 4240 (14%), zero 24132 (79%)
c [score-dist-5] max exp 832, different 160 (19%)
c [score-dist-5] median active exp 785, avg 758.5
c [simplification-5] removed 81 variables 0.3% (30581 remain 40%)
c [simplification-5] removed 1745 irredundant clauses 1.0% (175927 remain 67%)
c [simplification-5] maximum reduction of 1% = max (0%, 1%)
c [simplification-5] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-5] new conflict interval 14000
c [simplification-5] penalized conflict interval 14000 = 1 * 14000
c [simplification-5] hard conflict limit 29129 (soft 19129 + delta 10000)
c [simplification-5] new conflict limit 19129 (hard 29129)
c 
c [simplification-6] limit 19129 conflicts (hard 29129) hit after 19129 conflicts
c [quatres-3] found 76301 quaternary clauses 91% in total
c [quatres-3-1] added 2 double-self-subsuming ternary resolvents
c [quatres-3-2] added 324 single-self-subsuming ternary resolvents
c [quatres-3-2] added 290 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] 372 schedulable variables 1%
c [ternres-3] 3239 ternary resolvents (48 bin, 3191 trn)
c [ternres-3] 55 variables remain 0% (30526 retained 100%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 151 at-most-one constraints of average size 3.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 151 out of 151 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 2297 xors of average arity 3.0
c [gauss-2] connected 6891 occurrences of 1730 variables (average 4.0)
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 [simpleprobe-3] 27051 schedulable variables 88%
c [simpleprobe-3] limit 5872308 penalty 0 = 0 + 0
c [simpleprobe-3] 9519 variables remain 31% (21062 retained 69%)
c [simpleprobe-3] removed 0 variables, found 972 hbrs, 0 units
c [unhide-5] limit 293615 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 0 failed, 133 tauts, 0 hbrs, 4474 literals
c [transred-3] limit 1468077 with penalty 0 = 0 + 0
c [transred-3] removed 139 transitive binary clauses
c [block-3] scheduling all variables this time
c [block-3] scheduled 30581 variables 100%
c [block-3] limit of 25000000 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 628 blocked clauses
c [block-3] 628 < 1/100 * 175863 = 1758 considered unsuccessful
c [cce-3] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-3-1] eliminated 2 clauses out of 33 (6%) of length 13
c [cce-3-1] eliminated 6 clauses out of 88 (7%) of length 12
c [cce-3-1] eliminated 2 clauses out of 102 (2%) of length 11
c [cce-3-1] eliminated 2 clauses out of 101 (2%) of length 10
c [cce-3-1] eliminated 4 clauses out of 64 (6%) of length 9
c [cce-3-1] eliminated 4 clauses out of 100 (4%) of length 8
c [cce-3-1] eliminated 7 clauses out of 169 (4%) of length 7
c [cce-3-1] eliminated 84 clauses out of 348 (24%) of length 6
c [cce-3-1] eliminated 287 clauses out of 2692 (11%) of length 5
c [cce-3-1] eliminated 115 clauses out of 74103 (0%) of length 4
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 513 large clauses in 15000222 steps
c [cce-3-1] allowing another 7500111 steps for small clauses
c [cce-3-1] scheduling 74549 clauses = 22444 binary + 52105 ternary
c [cce-3-1] tried to eliminate 6776 small clauses 9%
c [cce-3-1] eliminated 42 binary clauses 0%
c [cce-3-1] eliminated 92 ternary clauses 0%
c [cce-3-1] eliminated 134 small clauses 0%
c [cce-3-1] eliminated 134 small clauses in 15000000 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 647 covered clauses in round 1
c [cce-3] eliminated 647 covered clauses in TOTAL during 1 rounds
c [cce-3] 647 < 1/100 * 175235 = 1752 considered unsuccessful
c [bca-4] limit of 10000000 steps and 350004 added (scaled 2)
c [bca-4] 53535 out of 61164 literals actually usable 88%
c [bca-4] added 35 blocked clauses in 163177 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 923 pos 3.3% + 26856 neg 96.7% = 27779 sched 90.8% ret 2802
c [sweep-4-1] 1014078 steps 53 queries 3975.68 avg class size
c [sweep-4-1] 549 decisions 52 SAT calls 23.25 avg env size
c [sweep-4-1] 27446 variables remain 90% (3135 retained 10%)
c [sweep-4-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 0 vars in TOTAL (1 rounds, 52 queries)
c [sort-queue-6] sorted 27898 enqueued variables after 19129 conflicts
c [score-dist-6] active 2683 (9%), one 9197 (30%), zero 18701 (61%)
c [score-dist-6] max exp 502, different 141 (28%)
c [score-dist-6] median active exp 452, avg 326.5
c [simplification-6] removed 0 variables 0.0% (30581 remain 40%)
c [simplification-6] removed 1339 irredundant clauses 0.8% (174588 remain 66%)
c [simplification-6] maximum reduction of 1% = max (0%, 1%)
c [simplification-6] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-6] new conflict interval 24000
c [simplification-6] penalized conflict interval 24000 = 1 * 24000
c [simplification-6] hard conflict limit 55129 (soft 43129 + delta 12000)
c [simplification-6] new conflict limit 43129 (hard 55129)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   23.2   30580   174588     32869   28895   8982 12189   11    22   25  49%    348   13   12    4  335%
c 
c [simplification-7] limit 43129 conflicts (hard 55129) hit after 43129 conflicts
c [quatres-4] found 76100 quaternary clauses 89% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [quatres-4-1] added 3 double-self-subsuming ternary resolvents
c [quatres-4-2] added 195 single-self-subsuming ternary resolvents
c [quatres-4-2] added 171 quaternary resolvents
c [ternres-4] limit 4616222 with penalty 0 = 0 + 0
c [ternres-4] 55 schedulable variables 0%
c [ternres-4] 3653 ternary resolvents (13 bin, 3640 trn)
c [ternres-4] 5 variables remain 0% (30573 retained 100%)
c [decomp-16] removed 3 variables
c [treelook-3] limit 461622 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 21278 literals 35%
c [treelook-3] scheduling used 461627 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 461622 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 639956 steps
c [treelook-3] 21269 literals remain 35%
c [treelook-3] 7534 variables remain to probed next time 25%
c [treelook-3] removed 0 variables, found 5300 hbrs
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 148 transitive binary clauses
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 30578 variables 100%
c [elim-5] limit of 46162221 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 4 not tried 0% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 214 = 1% variables out of 30578 scheduled
c [elim-5] 214 < 1/100 * 30578 = 305 considered unsuccessful
c [bca-5] limit of 10000000 steps and 349043 added (scaled 2)
c [bca-5] 50789 out of 60730 literals actually usable 84%
c [bca-5] added 161 blocked clauses in 172386 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 13848660 penalty 0 = 0 + 0
c [sweep-5-1] 812 pos 3.0% + 26460 neg 97.0% = 27272 sched 89.8% ret 3092
c [sweep-5-1] 13850291 steps 326 queries 780.80 avg class size
c [sweep-5-1] 4595 decisions 325 SAT calls 39.11 avg env size
c [sweep-5-1] 20423 variables remain 67% (9941 retained 33%)
c [sweep-5-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 0 vars in TOTAL (1 rounds, 325 queries)
c [sort-queue-7] sorted 22634 enqueued variables after 43129 conflicts
c [score-dist-7] active 7730 (25%), one 7696 (25%), zero 14938 (49%)
c [score-dist-7] max exp 970, different 216 (22%)
c [score-dist-7] median active exp 551, avg 476.9
c [simplification-7] removed 214 variables 0.7% (30364 remain 39%)
c [simplification-7] removed 489 irredundant clauses 0.3% (174099 remain 66%)
c [simplification-7] maximum reduction of 1% = max (1%, 0%)
c [simplification-7] geometric conflict interval increment 12000 = 24000 / 2
c [simplification-7] new conflict interval 36000
c [simplification-7] penalized conflict interval 36000 = 1 * 36000
c [simplification-7] hard conflict limit 97129 (soft 79129 + delta 18000)
c [simplification-7] new conflict limit 79129 (hard 97129)
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 -   47.2   30364   174099     69239   22508  12524 17584   12    22   24  55%    378    8   11    7  160%
c 
c [simplification-8] limit 79129 conflicts (hard 97129) hit after 79130 conflicts
c [quatres-5] found 76864 quaternary clauses 87% in total
c [quatres-5-1] added 1 double-self-subsuming ternary resolvents
c [quatres-5-2] added 339 single-self-subsuming ternary resolvents
c [quatres-5-2] added 388 quaternary resolvents
c [ternres-5] limit 10403642 with penalty 0 = 0 + 0
c [ternres-5] 5 schedulable variables 0%
c [ternres-5] 11838 ternary resolvents (12 bin, 11826 trn)
c [ternres-5] fully completed ternary resolution
c [unhide-6] limit 1040364 with penalty 1 = 1 + 0
c [unhide-6-6] 1 units, 1 failed, 1340 tauts, 0 hbrs, 15020 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 101 transitive binary clauses
c [transred-5] found 1 units
c [bca-6] limit of 10000000 steps and 349076 added (scaled 2)
c [bca-6] 50441 out of 60724 literals actually usable 83%
c [bca-6] added 46 blocked clauses in 168552 steps
c [sweep-6] limit 3121092 penalty 0 = 0 + 0
c [sweep-6-1] 717 pos 3.5% + 19706 neg 96.5% = 20423 sched 67.3% ret 9938
c [sweep-6-1] 3157880 steps 257 queries 676.21 avg class size
c [sweep-6-1] 1911 decisions 256 SAT calls 17.13 avg env size
c [sweep-6-1] 18466 variables remain 61% (11895 retained 39%)
c [decomp-20] removed 1 variables
c [sweep-6-1] removed 1 vars (0 failed, 0 eqs, 1 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 1 vars in TOTAL (1 rounds, 256 queries)
c [sort-queue-8] sorted 23703 enqueued variables after 79130 conflicts
c [score-dist-8] active 6657 (22%), one 10879 (36%), zero 12824 (42%)
c [score-dist-8] max exp 913, different 305 (33%)
c [score-dist-8] median active exp 711, avg 632.1
c [simplification-8] removed 4 variables 0.0% (30360 remain 39%)
c [simplification-8] removed 30 irredundant clauses 0.0% (174069 remain 66%)
c [simplification-8] maximum reduction of 0% = max (0%, 0%)
c [simplification-8] full geometric conflict interval increment 36000
c [simplification-8] new conflict interval 72000
c [simplification-8] penalized conflict interval 72000 = 1 * 72000
c [simplification-8] hard conflict limit 187130 (soft 151130 + delta 36000)
c [simplification-8] new conflict limit 151130 (hard 187130)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i   72.2   30359   174069    109829   60152  23940 18055   11    19   32  61%    676    1    5   10   51%
c -   73.9   30359   174069    113617   30240  23973 18065   10    24   25  42%   -427    6    9   10   89%
c 
c [simplification-9] limit 151130 conflicts (hard 187130) hit after 152819 conflicts
c [quatres-6] found 77659 quaternary clauses 84% in total
c [quatres-6-1] removed 2 duplicate quaternary clauses
c [quatres-6-1] added 2 double-self-subsuming ternary resolvents
c [quatres-6-2] added 570 single-self-subsuming ternary resolvents
c [quatres-6-2] added 409 quaternary resolvents
c [ternres-6] limit 22771581 with penalty 0 = 0 + 0
c [ternres-6] all 30359 free variables schedulable
c [ternres-6] 5055 ternary resolvents (28 bin, 5027 trn)
c [ternres-6] 240 variables remain 1% (30119 retained 99%)
c [gauss-3] limit 1138579 penalty 2 = 2 + 0
c [gauss-3] extracted 1366 xors of average arity 3.0
c [gauss-3] connected 4098 occurrences of 1330 variables (average 3.1)
c [gauss-3] limit 1138579 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-3] limit 56928954 penalty 1 = 1 + 0
c [basicprobe-3-0] 7624 sched 25%, 8 failed, 0 lifted, 7194 hbrs
c [decomp-22] removed 9 variables
c [basicprobe-3-1] 18953 sched 62%, 13 failed, 0 lifted, 5983 hbrs
c [decomp-23] removed 21 variables
c [basicprobe-3-2] 19000 sched 63%, 4 failed, 0 lifted, 2431 hbrs
c [decomp-24] removed 7 variables
c [basicprobe-3-3] 19235 sched 63%, 1 failed, 0 lifted, 856 hbrs
c [decomp-25] removed 2 variables
c [basicprobe-3-4] 19228 sched 63%, 0 failed, 0 lifted, 60 hbrs
c [basicprobe-3-5] 19226 sched 63%, 0 failed, 0 lifted, 25 hbrs
c [basicprobe-3-6] 4336 probes remain 14% after last round
c [basicprobe-3-6] 26 units = 26 failed (100%) + 0 lifted (0%)
c [basicprobe-3-6] removed 39 variables, found 16573 hbrs
c [bate-2] eliminated 130 asymmetric tautologies during probing
c [unhide-7] limit 4554316 with penalty 0 = 0 + 0
c [unhide-7-9] 0 units, 0 failed, 2974 tauts, 0 hbrs, 63009 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 120 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 30320 variables 100%
c [block-4] limit of 56928954 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 34 blocked clauses
c [block-4] 34 < 1/100 * 173604 = 1736 considered unsuccessful
c [cce-4] boosting limit by 10
c [cce-4] limit of 284644772 steps penalty 2 = 2 + 0
c [cce-4-1] eliminated 2 clauses out of 288 (1%) of length 6
c [cce-4-1] eliminated 38 clauses out of 2484 (2%) of length 5
c [cce-4-1] eliminated 580 clauses out of 73461 (1%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 620 large clauses in 40164675 steps
c [cce-4-1] allowing another 20082337 steps for small clauses
c [cce-4-1] scheduling 45177 clauses = 22491 binary + 22686 ternary
c [cce-4-1] tried to eliminate 45177 small clauses 100%
c [cce-4-1] eliminated 289 binary clauses 1%
c [cce-4-1] eliminated 561 ternary clauses 2%
c [cce-4-1] eliminated 850 small clauses 2%
c [cce-4-1] eliminated 850 small clauses in 72542799 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 1470 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 19085685 steps for small clauses
c [cce-4-2] scheduling 44327 clauses = 22202 binary + 22125 ternary
c [cce-4-2] tried to eliminate 44327 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 1470 covered clauses in TOTAL during 2 rounds
c [cce-4] 1470 < 1/100 * 173570 = 1735 considered unsuccessful
c [bca-7] limit of 10000000 steps and 345149 added (scaled 2)
c [bca-7] 46960 out of 60642 literals actually usable 77%
c [bca-7] added 50 blocked clauses in 191568 steps
c [sweep-7] limit 6831474 penalty 0 = 0 + 0
c [sweep-7-1] 820 pos 4.4% + 17646 neg 95.6% = 18466 sched 60.9% ret 11854
c [sweep-7-1] 6903755 steps 504 queries 700.54 avg class size
c [sweep-7-1] 4603 decisions 503 SAT calls 23.11 avg env size
c [sweep-7-1] 14179 variables remain 47% (16141 retained 53%)
c [decomp-28] removed 1 variables
c [sweep-7-1] removed 1 vars (0 failed, 0 eqs, 3 impls)
c [sweep-7] 1 < 1/1000 * 30320 = 30 considered unsuccessful
c [sweep-7] removed 1 vars in TOTAL (1 rounds, 503 queries)
c [sort-queue-9] sorted 24332 enqueued variables after 152819 conflicts
c [score-dist-9] active 5987 (20%), one 13255 (44%), zero 11077 (37%)
c [score-dist-9] max exp 773, different 245 (32%)
c [score-dist-9] median active exp 676, avg 673.9
c [simplification-9] removed 40 variables 0.1% (30319 remain 39%)
c [simplification-9] removed 1971 irredundant clauses 1.1% (172098 remain 65%)
c [simplification-9] maximum reduction of 1% = max (0%, 1%)
c [simplification-9] geometric conflict interval increment 36000 = 72000 / 2
c [simplification-9] new conflict interval 108000
c [simplification-9] penalized conflict interval 108000 = 1 * 108000
c [simplification-9] hard conflict limit 314819 (soft 260819 + delta 54000)
c [simplification-9] new conflict limit 260819 (hard 314819)
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 -  102.7   30319   172098    154151   35637  28436 31664   12    19   27  64%    226   -0   12   10  113%
c i  103.5   30318   172098    155185   36512  28454 31670   11    17   28  65%    239   -2    6   10   55%
c -  123.2   30318   172098    192736   40313  29066 31746   11    21   27  54%    175    1   13   10  126%
c 
c [simplification-10] limit of 4057 ternary hit after 4057 ternaries
c [quatres-7] found 77500 quaternary clauses 80% in total
c [quatres-7-1] removed 14 duplicate quaternary clauses
c [quatres-7-1] added 5 double-self-subsuming ternary resolvents
c [quatres-7-2] added 711 single-self-subsuming ternary resolvents
c [quatres-7-2] added 487 quaternary resolvents
c [ternres-7] limit 34991665 with penalty 0 = 0 + 0
c [ternres-7] 236 schedulable variables 1%
c [ternres-7] 8637 ternary resolvents (126 bin, 8511 trn)
c [ternres-7] 2 variables remain 0% (30316 retained 100%)
c [card-4] limit 2186979 penalty 3 = 3 + 0
c [card-4] found 112 at-most-one constraints of average size 3.5
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 2186979 for elimination
c [card-4] 112 out of 112 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-29] removed 1 variables
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 144 transitive binary clauses
c [elim-6] 4 variables 0% will be scheduled this time
c [elim-6] scheduled 4 variables 0%
c [elim-6] limit of 174958326 steps penalty 2 = 2 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 3589535 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 4 scheduled
c [bca-8] limit of 10000000 steps and 345152 added (scaled 2)
c [bca-8] 43055 out of 60638 literals actually usable 71%
c [bca-8] added 15 blocked clauses in 188093 steps
c [sort-queue-10] sorted 26471 enqueued variables after 227937 conflicts
c [score-dist-10] active 3847 (13%), one 16218 (53%), zero 10253 (34%)
c [score-dist-10] max exp 964, different 300 (31%)
c [score-dist-10] median active exp 918, avg 866.9
c [simplification-10] removed 0 variables 0.0% (30318 remain 39%)
c [simplification-10] removed 9 irredundant clauses 0.0% (172089 remain 65%)
c [simplification-10] maximum reduction of 0% = max (0%, 0%)
c [simplification-10] forced so keeping old conflict interval 108000
c [simplification-10] conflict limit remains at 260819 (hard 314819)
c [simplification-10] new ternary interval 10000
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c -  143.9   30318   172089    229909   43457  38678 31773   11    19   28  55%    543   -1   11   11  100%
c i  149.0   30317   172089    239699   52268  38802 31789   10    20   32  51%    609   -0   12   11  111%
c -  164.6   30311   172089    266950   45773  39011 31825   12    16   29  71%   -135   -3   13   11  118%
c 
c [simplification-11] limit 260819 conflicts (hard 314819) hit after 301755 conflicts
c [quatres-8] found 77841 quaternary clauses 78% in total
c [quatres-8-1] added 4 double-self-subsuming ternary resolvents
c [quatres-8-2] added 320 single-self-subsuming ternary resolvents
c [quatres-8-2] added 199 quaternary resolvents
c [ternres-8] limit 47920765 with penalty 0 = 0 + 0
c [ternres-8] 2 schedulable variables 0%
c [ternres-8] 10296 ternary resolvents (51 bin, 10245 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-30] removed 11 variables
c [simpleprobe-4] 9418 schedulable variables 31%
c [simpleprobe-4] limit 95841531 penalty 1 = 1 + 0
c [decomp-31] removed 4 variables
c [simpleprobe-4] 569 variables remain 2% (29734 retained 98%)
c [simpleprobe-4] removed 4 variables, found 11326 hbrs, 2 units
c [unhide-8] limit 4792076 with penalty 1 = 1 + 0
c [unhide-8-12] 1 units, 0 failed, 14471 tauts, 0 hbrs, 55465 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 275 transitive binary clauses
c [bca-9] limit of 10000000 steps and 344819 added (scaled 2)
c [bca-9] 43684 out of 60606 literals actually usable 72%
c [bca-9] added 54 blocked clauses in 194587 steps
c [sweep-8] limit 7188114 penalty 1 = 1 + 0
c [sweep-8-1] 538 pos 3.8% + 13639 neg 96.2% = 14177 sched 46.8% ret 16125
c [sweep-8-1] 7188452 steps 419 queries 501.26 avg class size
c [sweep-8-1] 5560 decisions 418 SAT calls 33.89 avg env size
c [sweep-8-1] 10022 variables remain 33% (20280 retained 67%)
c [decomp-32] removed 2 variables
c [sweep-8-1] removed 2 vars (0 failed, 1 eqs, 2 impls)
c [sweep-8] 2 < 1/1000 * 30302 = 30 considered unsuccessful
c [sweep-8] removed 2 vars in TOTAL (1 rounds, 418 queries)
c [sort-queue-11] sorted 19092 enqueued variables after 301755 conflicts
c [score-dist-11] active 11208 (37%), one 9267 (31%), zero 9825 (32%)
c [score-dist-11] max exp 884, different 329 (37%)
c [score-dist-11] median active exp 733, avg 712.2
c [simplification-11] removed 11 variables 0.0% (30300 remain 39%)
c [simplification-11] removed 174 irredundant clauses 0.1% (171915 remain 65%)
c [simplification-11] maximum reduction of 0% = max (0%, 0%)
c [simplification-11] full geometric conflict interval increment 108000
c [simplification-11] new conflict interval 216000
c [simplification-11] penalized conflict interval 216000 = 1 * 216000
c [simplification-11] hard conflict limit 625755 (soft 517755 + delta 108000)
c [simplification-11] new conflict limit 517755 (hard 625755)
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 -  188.6   30300   171915    304690   48594  35475 41430   12    20   29  59%    373    2   13   11  120%
c i  190.5   30299   171915    306959   50747  35481 41431   11    20   31  56%    395    1   11   11  102%
c -  212.7   30299   171915    341445   50190  35624 41441   11    19   29  61%     21    0   10   11   88%
c i  234.9   30298   171915    375991   81380  35825 41469   10    16   38  64%    432   -2    8   11   72%
c -  238.2   30298   171915    380574   52954  35837 41472   11    17   29  67%   -537   -0   13   11  122%
c -  260.6   30298   171915    420145   56206  35975 41483    8    11   30  76%    164   -6    8   10   81%
c i  265.0   30297   171915    429024   63672  36005 41494    8     9   32  86%    273   -7    6   10   57%
c i  277.3   30296   171915    445186   78599  36088 41502   11    19   35  61%   -221    2   10   10  101%
c i  287.0   30295   171915    457977   90289  36148 41509   12    21   38  56%   -211    4   14   11  129%
c -  287.8   30295   171915    459066   56619  36150 41509   12    20   30  58%   -321    3   11   11  104%
c i  305.3   30294   171915    482450   77749  36274 41529   11    17   38  64%     34   -1    7   11   62%
c -  318.8   30269   171915    499993   59054  36345 41540   11    16   30  69%    -31   -3   13   11  123%
c 
c [simplification-12] limit 517755 conflicts (hard 625755) hit after 517756 conflicts
c [quatres-9] found 78217 quaternary clauses 73% in total
c [quatres-9-1] removed 7 duplicate quaternary clauses
c [quatres-9-1] added 1 double-self-subsuming ternary resolvents
c [quatres-9-2] added 568 single-self-subsuming ternary resolvents
c [quatres-9-2] added 400 quaternary resolvents
c [ternres-9] limit 93016781 with penalty 0 = 0 + 0
c [ternres-9] all 30269 free variables schedulable
c [ternres-9] 7976 ternary resolvents (85 bin, 7891 trn)
c [ternres-9] 3 variables remain 0% (30266 retained 100%)
c [decomp-33] removed 43 variables
c [unhide-9] limit 18603356 with penalty 0 = 0 + 0
c [unhide-9-23] 1 units, 6 failed, 6345 tauts, 0 hbrs, 45041 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 98 transitive binary clauses
c [bca-10] limit of 10000000 steps and 343818 added (scaled 2)
c [bca-10] 41775 out of 60506 literals actually usable 69%
c [bca-10] added 51 blocked clauses in 185876 steps
c [sort-queue-12] sorted 17051 enqueued variables after 517756 conflicts
c [score-dist-12] active 13201 (44%), one 8125 (27%), zero 8926 (30%)
c [score-dist-12] max exp 579, different 298 (51%)
c [score-dist-12] median active exp 557, avg 503.4
c [simplification-12] removed 17 variables 0.1% (30252 remain 39%)
c [simplification-12] removed 510 irredundant clauses 0.3% (171405 remain 65%)
c [simplification-12] maximum reduction of 0% = max (0%, 0%)
c [simplification-12] full geometric conflict interval increment 216000
c [simplification-12] new conflict interval 432000
c [simplification-12] penalized conflict interval 432000 = 1 * 432000
c [simplification-12] hard conflict limit 1165756 (soft 949756 + delta 216000)
c [simplification-12] new conflict limit 949756 (hard 1165756)
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 -  356.4   30252   171405    541210   59512  39322 40071   11    21   30  53%    462    2   11   11   97%
c i  368.4   30251   171405    558778   75363  39379 40082   10    15   35  62%    594   -3    5   11   45%
c -  390.0   30251   171405    583107   62313  39464 40089   11    20   30  56%   -109    1   11   11   96%
c -  415.2   30251   171405    623343   64532  39543 40095    9    26   31  37%    411    4    9   11   82%
c -  447.4   30251   171405    665101   65680  39684 40114   12    18   31  64%    700   -4    9   11   84%
c -  484.0   30251   171405    707809   66714  39833 40135   12    19   31  65%    855   -2   10   11   90%
c -  522.4   30251   171405    752486   69318  39942 40144   11    17   31  64%    939   -2   12   11  104%
c -  566.4   30251   171405    797615   69463  40154 40170   14    24   31  58%    981    3   11   12   90%
c i  592.7   30250   171405    827768   95507  40258 40181    8    11   44  76%    997   -8    8   12   71%
c -  613.5   30250   171405    846675   73486  40339 40186   15    29   31  50%  -2196   10   17   12  138%
c i  628.7   30249   171405    865555   90799  40385 40189   11    15   39  72%  -1390   -5   11   12   90%
c -  653.0   30249   171405    891829   75712  40470 40199   13    23   46  55%   -994    2   13   12  109%
c i  664.7   30248   171405    904333   86813  40545 40208   12    24   52  49%   -644    3    7   12   61%
c 1  674.0   30248   171405    913704   95563  40594 40211   13    25   56  55%   -955    3   14   12  111%
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: 496 basic ate = 399 trn 80% + 97 lrg 20% in 2 updates
c bcas: 10 count, 1068 added (1018 skipped), 1762553 steps
c bkwd: tried 81291 clauses, 162558 lits, 2.00 lits/clause
c bkwd: checked 17550547 occs, 215.90 occs/clause, 107.96 occs/lit
c bkwd: subsumed 0 binary, 4 ternary, 7 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 134 large (0% self)
c blkd: 4 bces, 4177 removed, 3761079 resolutions, 9361965 steps
c blkd: 2183 blocking literals 1%, 0 pure
c bump: 912506 bumped seen, 140366148 lits 153.8 on average
c card: 4 count, 0 units, 0 am1, 14775207 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 2856 subsumed
c card: 535 at-most-one constraints found, average size 3.14
c card: 535 at-most-one constraints used 100%, average size 3.14
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 4 cces, 5597 eliminated, 5480 ate 98%, 117 abce 2%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 942686 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 73 gcs, 0 rescored clauses, 480 rescored vars
c dcps: 33 decompositions, 1200 equivalent 2%
c deco: 429 decision-only clauses 0%, 66% reduction
c decs: 2047353 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 6 elims, 44971 eliminated 58%, 0 pure 0%
c elms: 8 rounds, 1.3 rounds/bve
c elms: 44348 small 99%, 623 large 1%
c elms: 128376 tried small, 44348 succeeded 35%, 84028 failed 65%
c elms: 2694 subsumed, 3544 strengthened, 850 blocked
c elms: 3646011 copies, 4585873 resolutions, 6898596 ipos
c elms: 1743160 subchks, 1883039 strchks
c gaus: 3 extractions, 14854 extracted, 3.0 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 8277224 steps, 4138612 extr 50%, 2849980 elim 34%
c glue: 11.1 orig avg, 11.1 real avg, 2.8 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 60305 = 25866 simple 43% + 31998 trn 53% + 2441 lrg 4%, 1256 sub 2%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 912506 clauses, 39.1 length
c lrnd: 35694292 lits = 81398478 orig - 45704186 removed 56%
c lrnd: 260609 uips 29%, 574984 flips 63%
c mins: 900497 mins 99%, 443 bin 0%, 11121 size 1%
c mins: 191862615 poisoned searches, 12992043 hits, 7% hit rate
c mins: 258506707 used twice searches, 3496294 hits, 1% hit rate
c move: moved 5189, 866 bin 17%, 4323 trn 83%
c otfs: 2454 driving 28%, 6161 restarting 72%
c otfs: str 8615, 8418 red 98%, 197 irr 2%
c otfs: str 8615, 0 bin 0%, 267 trn 3%, 8348 lrg 97%
c otfs: sub 56, 56 red 100%, 0 irr 0%
c otfs: sub 56, 0 bin 0%, 20 trn 36%, 36 lrg 64%
c phas: 1 computed, 33919 set, 0 pos (0%), 33919 neg (100%)
c prbs: 3 basic, 262386 probed, 55 failed, 0 lifted
c prbs: 4 simple, 274677 probed, 106 failed, 144 eqs
c prbs: 3 treelook, 594 probed, 3 failed, 0 lifted
c prom: 298286 locked 10% out of 3066305 tried
c prps: 1875836818 props, 913 props/dec
c prps: 100% srch, 0% simp, 0% lkhd
c quat: 9 count, 3119 quat, 3747 self1, 18 self2, 27 dup
c queu: 12 sorted, 2047353 next (536494 steps 0.26)
c queu: 145816645 enq (157366965 steps 1.08), 140366148 deq 96%
c redc: 12607 clauses 10%, 131522 tried 14%, 22 sat 0%
c redc: 16434 lits 1%, 1562025 tried 2%, 22 sat 0%
c redc: 458 times jump level reduced, 3.2 levels on average
c reds: 21 count, 43509.7 conflicts per reduce
c reds: 0 memlim 0%, 21 arith 100%
c reds: 630071 collected 87%, 96250 retired 13%
c rmbd: 5630 removed, 5561 red 99%
c rsts: 27299 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 1 count, 1.200 min (200/1000), 1.200 max (200/1000)
c simp: 12 count, 9 confs 75%, 0 vars 0%
c simp: 1 its 8%, 1 bin 8%, 1 trns 8%
c subl: 912506 count (580934 tried 0.6), 73583 sub out of 904668 (8.1%)
c swps: 8 count, 8 rounds, 1856 queries (232.0/round)
c swps: 1855 sat calls, 1 unsat (0.7% success rate)
c swps: 19636 decisions 10.6, 1256 conflicts 0.7
c swps; 1236.4 avg class size, 27.0 avg environment size
c swps: 0 failed, 13 impls, 2 equivs
c swp0: 615 type 0 queries, 4 unsat (0.7%), 615 sat (100.0%)
c swp1: 1241 type 1 queries, 56 unsat (4.5%), 1239 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: 5920970 calls to obtain time
c tops: 843 fixed 1%, 53 its, 17239.70 confs/it
c trds: 9 transitive reductions, 1051 removed, 2 failed
c trds: 174413 nodes, 117975 edges, 14030917 steps
c trim: 633425 words, 2.4 MB
c trnr: 9 count, 466 bin, 54519 trn, 233006457 steps
c unhd: 9 count, 23 rounds, 35463557 steps
c unhd: 28 non-trivial sccs of average size 2.0
c unhd: 28 units, 7 bin, 21 trn, 0 lrg
c unhd: 26 failed, 14 stamp, 0 lits, 0 bin, 11 trn, 0 lrg
c unhd: 26265 tauts, 580 bin 2%, 17667 trn 67%, 871 lrg 3%
c unhd: 26265 tauts, 7147 stamp 27%, 25680 red 98%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 187212 str, 7 bin 0%, 5469 trn 3%, 181736 lrg 97%, 182968 red 98%
c vars: 30248 remaining 39% and 47014 removed 61% out of 77262
c vars: 843 fixed 1%, 44971 eliminated 58%, 1200 equivalent 2%
c vsts: 18996389220 visits, 100% srch, 0% simp, 0% lkhd
c vsts: 10.1 search visits per propagation, 20697.8 per conflict
c wchs: 2602389807 pushed, 13867663 enlarged, 118 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         907787        630071         96250      80786360      14215625        446478
c 
c  0 0         59964   7      6320   1         0   0  57782967  72<  8081853  57    169446  38     1.7
c  1 5         40245   4     21085   3      6890   7   9594994  12   1953072  14<    60059  13<    0.6
c  2 6        202526  22    145909  23     17426  18  10481753  13   2809772  20    120608  27     2.4
c  3 9        378863  42<   291868  46<    34032  35<  2482256   3   1079923   8     70874  16     4.8
c  4 14       183826  20    137350  22     27430  28    370635   0    242675   2     18950   4     3.3
c  5 21        32246   4     21635   3      7655   8     53836   0     34283   0      3463   1     1.1
c  6 30         5432   1      3356   1      1537   2     10048   0      6533   0      1095   0     0.4
c  7 41         1915   0      1147   0       526   1      3792   0      2725   0       656   0     0.2
c  8 54         1035   0       633   0       259   0      2158   0      1685   0       424   0     0.1
c  9 69          744   0       418   0       205   0      1838   0      1510   0       465   0     0.1
c 10 86          621   0       282   0       164   0      1595   0      1325   0       393   0     0.1
c 11 126         326   0        56   0       113   0       433   0       239   0        37   0     0.0
c 12 230          44   0        12   0        13   0        55   0        30   0         8   0     0.0
c 
c avg                  2.8           3.0           3.2           0.5           0.8           1.4
c std                  1.2           1.0           1.2           0.9           1.1           1.4
c 
c   24.866   4% bump
c    7.619   1% elim
c    5.366   1% probe
c    5.295   1% unhide
c    4.281   1% cce
c    3.073   0% sweep
c    1.731   0% ternres
c 
c    6.838 < 1% rest (below)
c 
c    1.717   0% quatres
c    1.134   0% decide
c    1.030   0% bca
c    0.797   0% block
c    0.771   0% rescore
c    0.631   0% transred
c    0.567   0% gauss
c    0.190   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    3.336   0% preprocessing    10%
c   31.547   5% inprocessing     90%
c ==================================
c   34.883   5% simplifying
c  639.101  95% search
c ==================================
c  673.991 100% all
c 
c        913704 conflicts,        1355.7 confs/sec
c          6783 ternaries,         134.7 confs/ternary
c           826 binaries,         1106.2 confs/binary
c            53 iterations,      17239.7 confs/iteration
c 
c            21 reductions,          0.0 redus/sec,  43509.7 confs/reduction
c         27299 restarts,           40.5 rests/sec,     33.5 confs/restart
c       2047353 decisions,        3037.7 decis/sec,      2.2 decis/conflict
c    1875836818 propagations,  2783178.7 props/sec,    916.2 props/decision
c 
c 674.0 seconds, 64.8 MB
c launch: done
