c launch: /data/cnf/sc2014/app/dated-10-11-u.cnf.bz2
c host: atom03
c Lingeling SAT Solver
c 
c Version b7ztzud 55d9a3e9649fc56eacf3e72d8e2e2d5c615d5f18
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Fri May  1 11:44:04 CEST 2015
c compiled Fri May  1 11:44:04 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-49-generic x86_64
c 
c piping '/data/cnf/sc2014/app/dated-10-11-u.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/dated-10-11-u.cnf.bz2
c no embedded options
c found 'p cnf 141860 629461' header
c read 141860 variables, 629461 clauses, 1429872 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 --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 135830 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 [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  135830   617431         0       0      0     0    0     0   31   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 9985 at-most-one constraints of average size 5.1
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 9985 out of 9985 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 73366 variables
c [simpleprobe-1] all 68494 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 45584 variables
c [simpleprobe-1] fully completed simple probing
c [simpleprobe-1] removed 45584 variables, found 5600 hbrs, 920 units
c [unhide-1] limit 100000 with penalty 0 = 0 + 0
c [unhide-1-1] 1 units, 625 failed, 4664 tauts, 0 hbrs, 352 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 22330 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 7935 variables 36% in round 1 in 8218579 steps
c [elim-1-1] backward subsumption/strengthening limit 8218500
c [elim-1-1-1] backward checking 14493 touched variables 65%
c [elim-1-1-1] fully completed backward checking in 1 rounds
c [elim-1-1] subsumed 73 and strengthened 236 clauses in 1854079 steps
c [elim-1-1] rescheduled 580 variables 3% by backward subsumption
c [elim-1-2] eliminated 167 variables 1% in round 2 in 305123 steps
c [elim-1-2] backward subsumption/strengthening limit 305100
c [elim-1-2-1] backward checking 563 touched variables 3%
c [elim-1-2-1] fully completed backward checking in 1 rounds
c [elim-1-2] subsumed 51 and strengthened 44 clauses in 220620 steps
c [elim-1-2] rescheduled 160 variables 1% by backward subsumption
c [elim-1-3] eliminated 44 variables 0% in round 3 in 91627 steps
c [elim-1-3] backward subsumption/strengthening limit 91600
c [elim-1-3-1] backward checking 183 touched variables 1%
c [elim-1-3-1] incomplete backward checking 0 remain 0%
c [elim-1-3] subsumed 36 and strengthened 16 clauses in 91601 steps
c [elim-1] incomplete 101 not tried 0% in round 3
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 8230 = 37% variables out of 22330 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 98493 negative 99.1% of 99405 except 912 0.9%
c [phase-count-1] 81651 positive 82.1% of 99405 except 17754 17.9%
c [phase-count-1] less non-negative clauses 912 than limit 9900 (10.0%)
c [phase-count-1] non-pos/non-neg = 17754/912 = 19.47 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 14100 negative 100%
c [score-distribution-1] 0 pos 0.00%, 0 min 0.00%, 14100 zero 100.00%
c [score-distribution-1] 1 different 0.01% out of total 14100 variables
c [simplification-1] removed 90208 variables 86.5% (14100 remain 10%)
c [simplification-1] removed 518026 irredundant clauses 83.9% (99405 remain 16%)
c [simplification-1] maximum reduction of 86% = max (86%, 84%)
c [simplification-1] large reduction 86% >= 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    1.3   14099    99405        18      13      0  3305    0     1   10   3%      0    1    1    0 24653%
c i    1.3   14098    99405        24      17      0  3306    0     1   10   4%      0    1    1    0 24258%
c i    1.3   14095    99405        26      18      0  3306    0     1   10   4%      0    1    1    0 24306%
c i    1.3   14092    99405        41      27      2  3308    0     1   10   6%      0    1    1    0 23502%
c i    1.3   14089    99405       158     121     12  3318    0     2   10  11%      0    2    3    0 19409%
c i    1.3   14086    99405       266     211     16  3331    0     3   10  13%      0    3    4    0 15969%
c i    1.3   14082    99405       267     211     16  3331    0     3   10  13%      0    3    4    0 15907%
c i    1.3   14079    99405       272     213     16  3332    0     3   10  14%      0    3    4    0 15705%
c i    1.4   14075    99405       426     342     24  3343    1     5   10  22%      0    5   12    0 16452%
c i    1.4   14072    99405       453     362     29  3344    1     6   10  21%      0    6   12    0 15320%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 53 variables
c [simpleprobe-2] all 14047 free variables schedulable
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [decomp-4] removed 618 variables
c [simpleprobe-2] 3774 variables remain 28% (9655 retained 72%)
c [simpleprobe-2] removed 618 variables, found 2401 hbrs, 240 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 26858 literals 100%
c [treelook-1] scheduling used 291985 steps
c [treelook-1] scheduled completely
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 392070 steps
c [treelook-1] 26821 literals remain 100%
c [treelook-1] 13419 variables remain to probed next time 100%
c [decomp-5] removed 4 variables
c [treelook-1] removed 14 variables, found 4107 hbrs
c [basicprobe-1] limit 1000000 penalty 0 = 0 + 0
c [basicprobe-1-0] 1751 probes remain 13% after last round
c [basicprobe-1-0] 16 units = 16 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 52 variables, found 5122 hbrs
c [unhide-2] limit 100000 with penalty 0 = 0 + 0
c [unhide-2-2] 3 units, 193 failed, 2346 tauts, 0 hbrs, 1619 literals
c [elim-2] no untried remaining variables left
c [elim-2] scheduled 13194 variables 100%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2-1] eliminated 595 variables 5% in round 1 in 6614306 steps
c [elim-2-1] backward subsumption/strengthening limit 6614300
c [elim-2-1-1] backward checking 2583 touched variables 20%
c [elim-2-1-1] fully completed backward checking in 1 rounds
c [elim-2-1] subsumed 49 and strengthened 57 clauses in 563026 steps
c [elim-2-1] rescheduled 197 variables 1% by backward subsumption
c [elim-2-2] eliminated 40 variables 0% in round 2 in 154854 steps
c [elim-2-2] backward subsumption/strengthening limit 154800
c [elim-2-2-1] backward checking 194 touched variables 1%
c [elim-2-2-1] fully completed backward checking in 1 rounds
c [elim-2-2] subsumed 41 and strengthened 7 clauses in 77859 steps
c [elim-2-2] rescheduled 75 variables 1% by backward subsumption
c [elim-2-3] eliminated 20 variables 0% in round 3 in 61383 steps
c [elim-2-3] backward subsumption/strengthening limit 61300
c [elim-2-3-1] backward checking 88 touched variables 1%
c [elim-2-3-1] fully completed backward checking in 1 rounds
c [elim-2-3] subsumed 16 and strengthened 1 clauses in 39112 steps
c [elim-2] incomplete 31 not tried 0% in round 3
c [elim-2] transition to [ all 1 rem 1 ] state
c [elim-2] eliminated 701 = 5% variables out of 13194 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 87668 negative 99.1% of 88444 except 776 0.9%
c [phase-count-2] 71274 positive 80.6% of 88444 except 17170 19.4%
c [phase-count-2] less non-negative clauses 776 than limit 8800 (10.0%)
c [phase-count-2] non-pos/non-neg = 17170/776 = 22.13 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 49 negative 100%
c [score-distribution-2] 4945 pos 39.58%, 0 min 0.00%, 7548 zero 60.42%
c [score-distribution-2] 1136 different 9.09% out of total 12493 variables
c [simplification-2] removed 1579 variables 11.2% (12493 remain 9%)
c [simplification-2] removed 10961 irredundant clauses 11.0% (88444 remain 14%)
c [simplification-2] maximum reduction of 11% = max (11%, 11%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1018 (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    2.0   12492    88444       470     335     19  8197    1     6   10  21%      0    6   11    0 14441%
c i    2.0   12490    88444       473     336     20  8197    1     6   10  21%      0    6   11    0 14281%
c i    2.0   12448    88444       484     345     20  8197    1     6   10  21%      0    6   11    0 13929%
c i    2.0   12444    88444       529     386     21  8199    1     6   10  21%      0    6   10    0 12160%
c i    2.0   11793    88444       542     396     22  8200    1     6   10  21%      0    6   10    0 11704%
c i    2.0   11790    88444       584     433     22  8202    1     6   10  21%      0    6    9    0 10658%
c i    2.0   11789    88444       591     437     23  8203    1     6   10  21%      0    6    9    0 10427%
c i    2.0   11788    88444       622     467     23  8203    1     7   10  22%      0    7   10    0 10122%
c i    2.0   11786    88444       623     467     23  8203    1     7   10  22%      0    7   10    0 10083%
c i    2.0   11784    88444       624     467     23  8203    1     7   10  22%      0    7   10    0 10044%
c i    2.0   11780    88444       643     482     23  8204    1     7   10  22%      0    7    9    0 9482%
c i    2.0   11777    88444       690     521     25  8208    2     7   10  22%      0    7   11    0 9721%
c i    2.1   10842    88444       759     586     25  8208    2     8   10  24%      0    8   12    0 9772%
c i    2.1   10837    88444       768     592     25  8208    2     8   10  24%      0    8   13    0 9860%
c i    2.1   10836    88444       772     594     26  8208    2     8   10  24%      0    8   13    0 9761%
c i    2.1   10825    88444       974     776     31  8215    3    12   10  27%      1   12   22    0 10098%
c i    2.1   10824    88444      1029     824     34  8217    3    12   10  28%      1   12   21    0 9137%
c 
c [simplification-3] limit 1045 conflicts (hard 11000) hit after 1050 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 5251 at-most-one constraints of average size 3.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 5251 out of 5251 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] generated 76 at-most-one constraints, 56 used 74%
c [card-2] exported 1646 binary clauses, 29.4 per/constraint
c [decomp-6] removed 1936 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 21114 literals 100%
c [treelook-2] scheduling used 234902 steps
c [treelook-2] scheduled completely
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 306909 steps
c [treelook-2] 21085 literals remain 100%
c [treelook-2] 10552 variables remain to probed next time 100%
c [decomp-7] removed 2 variables
c [treelook-2] removed 7 variables, found 86 hbrs
c [unhide-3] limit 100000 with penalty 0 = 0 + 0
c [unhide-3-3] 0 units, 377 failed, 3743 tauts, 0 hbrs, 1192 literals
c [elim-3] no untried remaining variables left
c [elim-3] scheduled 10268 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3-1] eliminated 938 variables 9% in round 1 in 4526986 steps
c [elim-3-1] backward subsumption/strengthening limit 4526900
c [elim-3-1-1] backward checking 2908 touched variables 28%
c [elim-3-1-1] fully completed backward checking in 1 rounds
c [elim-3-1] subsumed 27 and strengthened 21 clauses in 458832 steps
c [elim-3-1] rescheduled 119 variables 1% by backward subsumption
c [elim-3-2] eliminated 14 variables 0% in round 2 in 61757 steps
c [elim-3-2] backward subsumption/strengthening limit 61700
c [elim-3-2-1] backward checking 82 touched variables 1%
c [elim-3-2-1] fully completed backward checking in 1 rounds
c [elim-3-2] subsumed 6 and strengthened 3 clauses in 28125 steps
c [elim-3-2] rescheduled 16 variables 0% by backward subsumption
c [elim-3-3] eliminated 8 variables 0% in round 3 in 5999 steps
c [elim-3-3] backward subsumption/strengthening limit 5900
c [elim-3-3-1] backward checking 15 touched variables 0%
c [elim-3-3-1] incomplete backward checking 0 remain 0%
c [elim-3-3] subsumed 2 and strengthened 0 clauses in 5901 steps
c [elim-3] incomplete 4 not tried 0% in round 3
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 969 = 9% variables out of 10268 scheduled
c [elim-3] considered successful since not run to completion yet
c [score-distribution-3] 4353 pos 46.81%, 0 min 0.00%, 4946 zero 53.19%
c [score-distribution-3] 1312 different 14.11% out of total 9299 variables
c [simplification-3] removed 1522 variables 14.1% (9299 remain 7%)
c [simplification-3] removed 25469 irredundant clauses 28.8% (62975 remain 10%)
c [simplification-3] maximum reduction of 29% = max (14%, 29%)
c [simplification-3] large reduction 29% >= 5% limit
c [simplification-3] next conflict interval 2000 = 2000/1
c [simplification-3] penalized conflict interval 2000 = 1 * 2000
c [simplification-3] hard conflict limit 13050 (soft 3050 + delta 10000)
c [simplification-3] new conflict limit 3050 (hard 13050)
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
c i    2.5    9298    62975      1086     615     27  6894    4    12    9  29%      1   12   21    0 8463%
c i    2.6    9297    62975      1429     916     35  6899    5    17    9  31%      1   17   23    0 6263%
c i    2.6    9296    62975      1489     969     35  6900    6    19    9  32%      1   18   29    0 6940%
c i    2.7    9295    62975      1648    1103     36  6909    7    20    9  33%      1   20   29    0 6022%
c i    2.7    9292    62975      1997    1401     40  6911    8    24    9  36%      2   23   26    1 4089%
c i    2.7    9291    62975      2017    1417     41  6911    8    24    9  36%      2   23   25    1 3919%
c i    2.8    9290    62975      2050    1442     42  6912    9    24    9  36%      2   23   25    1 3876%
c i    2.8    9289    62975      2055    1444     43  6912    9    24    9  36%      2   23   25    1 3912%
c i    2.8    9286    62975      2275    1641     46  6915   10    27    9  36%      2   26   30    1 3979%
c i    2.9    9284    62975      2422    1779     46  6917   11    29    9  36%      2   29   33    1 4020%
c i    2.9    9281    62975      2475    1822     47  6918   11    30    9  36%      1   29   30    1 3603%
c i    2.9    9280    62975      2511    1856     47  6919   11    30    9  35%      1   30   28    1 3352%
c i    2.9    9279    62975      2536    1876     48  6921   11    31   10  35%      1   30   28    1 3267%
c i    2.9    9277    62975      2548    1886     48  6922   11    31   10  35%      1   30   27    1 3152%
c i    2.9    9276    62975      2556    1892     48  6922   11    31   10  35%      1   30   27    1 3115%
c i    2.9    9275    62975      2652    1969     48  6922   12    33   10  37%      1   32   41    1 4278%
c i    3.0    9273    62975      3008    2285     50  6924   14    37   10  38%      2   36   38    1 3368%
c 
c [simplification-4] limit 3053 conflicts (hard 13050) hit after 3057 conflicts
c [decomp-8] removed 49 variables
c [basicprobe-2] limit 1359460 penalty 0 = 0 + 0
c [basicprobe-2-0] 1282 probes remain 14% after last round
c [basicprobe-2-0] 29 units = 29 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 86 variables, found 6137 hbrs
c [unhide-4] limit 100000 with penalty 0 = 0 + 0
c [unhide-4-4] 2 units, 120 failed, 1761 tauts, 0 hbrs, 6179 literals
c [elim-4] no untried remaining variables left
c [elim-4] scheduled 9061 variables 100%
c [elim-4] boosting limit by 20
c [elim-4] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] eliminated 200 variables 2% in round 1 in 4147283 steps
c [elim-4-1] backward subsumption/strengthening limit 4147200
c [elim-4-1-1] backward checking 1099 touched variables 12%
c [elim-4-1-1] fully completed backward checking in 1 rounds
c [elim-4-1] subsumed 7 and strengthened 6 clauses in 205584 steps
c [elim-4-1] rescheduled 44 variables 0% by backward subsumption
c [elim-4-2] eliminated 10 variables 0% in round 2 in 22926 steps
c [elim-4-2] backward subsumption/strengthening limit 22900
c [elim-4-2-1] backward checking 63 touched variables 1%
c [elim-4-2-1] incomplete backward checking 0 remain 0%
c [elim-4-2] subsumed 17 and strengthened 5 clauses in 22901 steps
c [elim-4-2] rescheduled 21 variables 0% by backward subsumption
c [elim-4-3] eliminated 7 variables 0% in round 3 in 16931 steps
c [elim-4-3] backward subsumption/strengthening limit 16900
c [elim-4-3-1] backward checking 32 touched variables 0%
c [elim-4-3-1] fully completed backward checking in 1 rounds
c [elim-4-3] subsumed 6 and strengthened 1 clauses in 15586 steps
c [elim-4] incomplete 12 not tried 0% in round 3
c [elim-4] transition to [ all 1 rem 1 ] state
c [elim-4] eliminated 229 = 3% variables out of 9061 scheduled
c [elim-4] considered successful since not run to completion yet
c [score-distribution-4] 5153 pos 58.34%, 0 min 0.00%, 3679 zero 41.66%
c [score-distribution-4] 2098 different 23.75% out of total 8832 variables
c [simplification-4] removed 441 variables 4.8% (8832 remain 7%)
c [simplification-4] removed 3378 irredundant clauses 5.4% (59597 remain 10%)
c [simplification-4] maximum reduction of 5% = max (5%, 5%)
c [simplification-4] large reduction 5% >= 5% limit
c [simplification-4] next conflict interval 2000 = 2000/1
c [simplification-4] penalized conflict interval 2000 = 1 * 2000
c [simplification-4] hard conflict limit 15057 (soft 5057 + delta 10000)
c [simplification-4] new conflict limit 5057 (hard 15057)
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.5    8831    59597      3339    2269     47  9556   15    40   10  38%      2   39   28    1 2234%
c i    3.5    8830    59597      3532    2442     50  9558   16    43   10  37%      2   42   33    1 2374%
c i    3.6    8829    59597      3829    2708     52  9561   18    49   10  37%      2   47   44    2 2778%
c i    3.7    8828    59597      4177    3023     56  9564   19    53   10  37%      2   51   34    2 1955%
c i    3.7    8329    59597      4261    3102     57  9566   20    54   10  36%      2   52   34    2 1896%
c i    3.9    8328    59597      4833    3634     60  9571   22    60   10  36%      3   58   39    2 1877%
c 
c [simplification-5] limit 5057 conflicts (hard 15057) hit after 5057 conflicts
c [quatres-1] found 2990 quaternary clauses 67% in total
c [quatres-1-2] added 1 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 8326 free variables schedulable
c [ternres-1] 139 ternary resolvents (1 bin, 138 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 614 xors of average arity 2.3
c [gauss-1] connected 1386 occurrences of 458 variables (average 3.0)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [decomp-9] removed 121 variables
c [gauss-1] exported 2 unary, 0 binary and 3 ternary equations
c [simpleprobe-3] 1966 schedulable variables 24%
c [simpleprobe-3] limit 2000000 penalty 0 = 0 + 0
c [decomp-11] removed 262 variables
c [simpleprobe-3] 89 variables remain 1% (7854 retained 99%)
c [simpleprobe-3] removed 262 variables, found 3715 hbrs, 64 units
c [unhide-5] limit 100000 with penalty 0 = 0 + 0
c [unhide-5-5] 1 units, 96 failed, 2455 tauts, 0 hbrs, 4253 literals
c [transred-1] limit 441881 with penalty 0 = 0 + 0
c [transred-1] removed 230 transitive binary clauses
c [transred-1] found 9 units
c [block-1] scheduling all variables this time
c [block-1] scheduled 7654 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 405 blocked clauses
c [block-1] 405 < 1/100 * 50222 = 502 considered unsuccessful
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 1 clauses out of 2 (50%) of length 9
c [cce-1-1] eliminated 3 clauses out of 16 (19%) of length 7
c [cce-1-1] eliminated 12 clauses out of 189 (6%) of length 6
c [cce-1-1] eliminated 68 clauses out of 642 (11%) of length 5
c [cce-1-1] eliminated 729 clauses out of 2515 (29%) of length 4
c [cce-1-1] completed large round (ATE)
c [cce-1-1] eliminated 813 large clauses in 8868197 steps
c [cce-1-1] allowing another 4434098 steps for small clauses
c [cce-1-1] scheduling 36131 clauses = 27909 binary + 8222 ternary
c [cce-1-1] tried to eliminate 3639 small clauses 10%
c [cce-1-1] eliminated 1118 binary clauses 4%
c [cce-1-1] eliminated 140 ternary clauses 2%
c [cce-1-1] eliminated 1258 small clauses 3%
c [cce-1-1] eliminated 1258 small clauses in 30000006 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 2071 covered clauses in round 1
c [cce-1] eliminated 2071 covered clauses in TOTAL during 1 rounds
c [elim-5] no untried remaining variables left
c [elim-5] scheduled 7639 variables 100%
c [elim-5] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5-1] eliminated 887 variables 12% in round 1 in 2991233 steps
c [elim-5-1] backward subsumption/strengthening limit 2991200
c [elim-5-1-1] backward checking 2917 touched variables 38%
c [elim-5-1-1] fully completed backward checking in 1 rounds
c [elim-5-1] subsumed 11 and strengthened 16 clauses in 423302 steps
c [elim-5-1] rescheduled 74 variables 1% by backward subsumption
c [elim-5-2] eliminated 6 variables 0% in round 2 in 36698 steps
c [elim-5-2] backward subsumption/strengthening limit 36600
c [elim-5-2-1] backward checking 51 touched variables 1%
c [elim-5-2-1] fully completed backward checking in 1 rounds
c [elim-5-2] subsumed 3 and strengthened 2 clauses in 20649 steps
c [elim-5-2] rescheduled 21 variables 0% by backward subsumption
c [elim-5-3] eliminated 4 variables 0% in round 3 in 10945 steps
c [elim-5-3] backward subsumption/strengthening limit 10900
c [elim-5-3-1] backward checking 22 touched variables 0%
c [elim-5-3-1] incomplete backward checking 0 remain 0%
c [elim-5-3] subsumed 0 and strengthened 3 clauses in 10901 steps
c [elim-5] incomplete 14 not tried 0% in round 3
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 900 = 12% variables out of 7639 scheduled
c [bca-1] limit of 10000000 steps and 88380 added (scaled 2)
c [bca-1] 10637 out of 13480 literals actually usable 79%
c [bca-1] added 5 blocked clauses in 24307 steps
c [sweep-1] limit 1000000 penalty 0 = 0 + 0
c [sweep-1-1] 1151 pos 17.1% + 5588 neg 82.9% = 6739 sched 100.0% ret 0
c [sweep-1-1] 1005264 steps 28 queries 404.14 avg class size
c [sweep-1-1] 497 decisions 26 SAT calls 78.15 avg env size
c [sweep-1-1] 5648 variables remain 84% (1082 retained 16%)
c [decomp-12] removed 19 variables
c [sweep-1-1] removed 19 vars (0 failed, 1 eqs, 2 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 19 vars in TOTAL (1 rounds, 27 queries)
c [score-distribution-5] 4113 pos 61.21%, 46 min 0.68%, 2561 zero 38.11%
c [score-distribution-5] 1963 different 29.21% out of total 6720 variables
c [simplification-5] removed 1606 variables 19.3% (6720 remain 5%)
c [simplification-5] removed 15775 irredundant clauses 26.5% (43822 remain 7%)
c [simplification-5] maximum reduction of 26% = max (19%, 26%)
c [simplification-5] large reduction 26% >= 5% limit
c [simplification-5] next conflict interval 2000 = 2000/1
c [simplification-5] penalized conflict interval 2000 = 1 * 2000
c [simplification-5] hard conflict limit 17057 (soft 7057 + delta 10000)
c [simplification-5] new conflict limit 7057 (hard 17057)
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.4    6719    43822      5299    2664    246 11145   25    66    9  37%      3   64   48    2 2021%
c i    5.4    6718    43822      5306    2669    246 11145   25    67    9  37%      3   64   49    2 2031%
c i    5.4    6717    43822      5407    2764    247 11145   25    67    9  37%      3   65   43    2 1771%
c i    5.4    6714    43822      5410    2766    247 11145   25    67    9  37%      3   65   43    2 1753%
c i    5.4    6713    43822      5416    2770    248 11145   25    68    9  37%      3   65   42    2 1728%
c i    5.5    6712    43822      5774    3087    251 11148   27    72    9  38%      3   69   49    3 1773%
c i    5.5    6689    43822      5775    3087    251 11148   27    72    9  38%      3   69   48    3 1766%
c i    5.5    6688    43822      5781    3089    251 11148   27    72    9  38%      3   69   47    3 1732%
c i    5.5    6687    43822      5787    3094    251 11148   27    72    9  38%      3   69   47    3 1705%
c i    5.5    6685    43822      5792    3098    251 11148   27    72    9  38%      3   69   46    3 1682%
c i    5.5    6684    43822      5793    3098    251 11148   27    72    9  38%      3   69   46    3 1676%
c i    5.5    6683    43822      5802    3102    251 11148   27    72    9  38%      3   69   45    3 1641%
c i    5.5    6642    43822      5804    3102    251 11149   27    72    9  38%      3   69   45    3 1629%
c i    5.5    6623    43822      5828    3124    251 11149   27    72    9  38%      3   69   44    3 1601%
c i    5.6    6622    43822      6037    3317    254 11152   28    73    9  38%      3   70   38    3 1336%
c i    5.6    6619    43822      6057    3336    254 11152   28    73    9  38%      3   70   38    3 1338%
c i    5.6    6532    43822      6210    3479    254 11152   29    76    9  39%      2   73   57    3 1888%
c i    5.6    6531    43822      6211    3479    254 11152   29    76    9  39%      2   73   57    3 1880%
c i    5.6    6530    43822      6252    3512    254 11152   30    77    9  39%      2   73   57    3 1864%
c i    5.6    6529    43822      6332    3586    254 11155   30    77   10  39%      2   74   52    3 1689%
c i    5.6    6527    43822      6345    3597    255 11155   30    77   10  39%      2   73   50    3 1623%
c i    5.7    6526    43822      6455    3703    255 11156   31    78   10  39%      2   74   53    3 1654%
c i    5.7    6524    43822      6456    3703    255 11156   31    78   10  39%      2   74   53    3 1647%
c 
c [simplification-6] limit 7112 conflicts (hard 17057) hit after 7114 conflicts
c [quatres-2] found 1870 quaternary clauses 59% in total
c [quatres-2-1] removed 1 duplicate quaternary clauses
c [quatres-2-2] added 1 quaternary resolvents
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 6524 free variables schedulable
c [ternres-2] 59 ternary resolvents (0 bin, 59 trn)
c [ternres-2] fully completed ternary resolution
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2314 at-most-one constraints of average size 3.6
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2314 out of 2314 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] generated 48 at-most-one constraints, 34 used 71%
c [card-3] exported 527 binary clauses, 15.5 per/constraint
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] extracted 302 xors of average arity 2.1
c [gauss-2] connected 648 occurrences of 178 variables (average 3.6)
c [gauss-2] limit 2000000 penalty 0 = 0 + 0
c [gauss-2] fully completed
c [decomp-13] removed 63 variables
c [gauss-2] exported 0 unary, 5 binary and 0 ternary equations
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] scheduled 12922 literals 100%
c [treelook-3] scheduling used 161566 steps
c [treelook-3] scheduled completely
c [treelook-3] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-3] used 319441 steps
c [treelook-3] 12889 literals remain 100%
c [treelook-3] 6453 variables remain to probed next time 100%
c [treelook-3] removed 8 variables, found 2706 hbrs
c [unhide-6] limit 119142 with penalty 0 = 0 + 0
c [unhide-6-6] 4 units, 201 failed, 2675 tauts, 0 hbrs, 6277 literals
c [transred-2] limit 595712 with penalty 0 = 0 + 0
c [transred-2] removed 337 transitive binary clauses
c [transred-2] found 10 units
c [cce-2] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-2-1] eliminated 1 clauses out of 6 (17%) of length 9
c [cce-2-1] eliminated 2 clauses out of 189 (1%) of length 6
c [cce-2-1] eliminated 27 clauses out of 636 (4%) of length 5
c [cce-2-1] eliminated 224 clauses out of 1834 (12%) of length 4
c [cce-2-1] completed large round (ATE)
c [cce-2-1] eliminated 254 large clauses in 7873235 steps
c [cce-2-1] allowing another 3936617 steps for small clauses
c [cce-2-1] scheduling 30562 clauses = 23797 binary + 6765 ternary
c [cce-2-1] tried to eliminate 4002 small clauses 13%
c [cce-2-1] eliminated 1095 binary clauses 5%
c [cce-2-1] eliminated 191 ternary clauses 3%
c [cce-2-1] eliminated 1286 small clauses 4%
c [cce-2-1] eliminated 2667 small clauses in 30000007 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 2921 covered clauses in round 1
c [cce-2] eliminated 2921 covered clauses in TOTAL during 1 rounds
c [elim-6] no untried remaining variables left
c [elim-6] scheduled 6309 variables 100%
c [elim-6] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] eliminated 346 variables 5% in round 1 in 2471667 steps
c [elim-6-1] backward subsumption/strengthening limit 2471600
c [elim-6-1-1] backward checking 1518 touched variables 24%
c [elim-6-1-1] fully completed backward checking in 1 rounds
c [elim-6-1] subsumed 5 and strengthened 4 clauses in 221962 steps
c [elim-6-1] rescheduled 36 variables 1% by backward subsumption
c [elim-6-2] eliminated 1 variables 0% in round 2 in 15219 steps
c [elim-6-2] backward subsumption/strengthening limit 15200
c [elim-6-2-1] backward checking 9 touched variables 0%
c [elim-6-2-1] fully completed backward checking in 1 rounds
c [elim-6-2] subsumed 1 and strengthened 0 clauses in 8271 steps
c [elim-6-2] rescheduled 3 variables 0% by backward subsumption
c [elim-6-3] no variable eliminated in round 3 in 2760 steps
c [elim-6] fully completed in 3 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 349 = 6% variables out of 6309 scheduled
c [bca-2] limit of 10000000 steps and 76084 added (scaled 2)
c [bca-2] 8937 out of 11922 literals actually usable 75%
c [bca-2] added 5 blocked clauses in 22121 steps
c [sweep-2] limit 1000000 penalty 0 = 0 + 0
c [sweep-2-1] 1021 pos 20.3% + 4005 neg 79.7% = 5026 sched 84.3% ret 934
c [sweep-2-1] 1018546 steps 26 queries 276.04 avg class size
c [sweep-2-1] 447 decisions 23 SAT calls 110.61 avg env size
c [sweep-2-1] 4441 variables remain 75% (1513 retained 25%)
c [decomp-16] removed 14 variables
c [sweep-2-1] removed 14 vars (0 failed, 2 eqs, 5 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 14 vars in TOTAL (1 rounds, 25 queries)
c [score-distribution-6] 3827 pos 64.36%, 85 min 1.43%, 2034 zero 34.21%
c [score-distribution-6] 1895 different 31.87% out of total 5946 variables
c [simplification-6] removed 578 variables 8.9% (5946 remain 4%)
c [simplification-6] removed 6151 irredundant clauses 14.0% (37671 remain 6%)
c [simplification-6] maximum reduction of 14% = max (9%, 14%)
c [simplification-6] large reduction 14% >= 5% limit
c [simplification-6] next conflict interval 2000 = 2000/1
c [simplification-6] penalized conflict interval 2000 = 1 * 2000
c [simplification-6] hard conflict limit 19114 (soft 9114 + delta 10000)
c [simplification-6] new conflict limit 9114 (hard 19114)
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    7.1    5945    37671      7140    3681    369 11768   34    82    9  42%      4   78   48    4 1290%
c i    7.2    5943    37671      7532    4023    375 11773   35    84   10  42%      4   79   48    4 1203%
c i    7.2    5900    37671      7535    4023    375 11775   35    84   10  42%      4   79   47    4 1189%
c i    7.5    5866    37671      8538    4910    379 11781   40    89   10  45%      7   82   54    5 1125%
c i    7.5    5862    37671      8560    4926    379 11781   40    88   10  45%      7   82   53    5 1104%
c i    7.5    5861    37671      8561    4926    379 11781   40    88   10  45%      7   82   53    5 1100%
c 
c [simplification-7] limit 9127 conflicts (hard 19114) hit after 9127 conflicts
c [quatres-3] found 1689 quaternary clauses 55% in total
c [quatres-3-1] removed 1 duplicate quaternary clauses
c [quatres-3-2] added 2 single-self-subsuming ternary resolvents
c [quatres-3-2] added 1 quaternary resolvents
c [ternres-3] limit 4000000 with penalty 0 = 0 + 0
c [ternres-3] all 5857 free variables schedulable
c [ternres-3] 60 ternary resolvents (0 bin, 60 trn)
c [ternres-3] fully completed ternary resolution
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] extracted 136 xors of average arity 2.4
c [gauss-3] connected 320 occurrences of 105 variables (average 3.0)
c [gauss-3] limit 2000000 penalty 0 = 0 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-17] removed 22 variables
c [basicprobe-3] limit 3663176 penalty 0 = 0 + 0
c [basicprobe-3-0] 691 probes remain 12% after last round
c [basicprobe-3-0] 132 units = 117 failed (89%) + 15 lifted (11%)
c [basicprobe-3-0] removed 280 variables, found 10739 hbrs
c [bate-1] eliminated 74 asymmetric tautologies during probing
c [unhide-7] limit 146527 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 46 failed, 1183 tauts, 0 hbrs, 5166 literals
c [transred-3] limit 732635 with penalty 0 = 0 + 0
c [transred-3] removed 379 transitive binary clauses
c [transred-3] found 10 units
c [block-2] scheduling all variables this time
c [block-2] scheduled 5498 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 206 blocked clauses
c [block-2] 206 < 1/100 * 32842 = 328 considered unsuccessful
c [cce-3] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-3-1] eliminated 2 clauses out of 5 (40%) of length 9
c [cce-3-1] eliminated 3 clauses out of 14 (21%) of length 8
c [cce-3-1] eliminated 1 clauses out of 30 (3%) of length 7
c [cce-3-1] eliminated 9 clauses out of 141 (6%) of length 6
c [cce-3-1] eliminated 22 clauses out of 507 (4%) of length 5
c [cce-3-1] eliminated 128 clauses out of 1441 (9%) of length 4
c [cce-3-1] completed large round (ACCE)
c [cce-3-1] eliminated 165 large clauses in 5119290 steps
c [cce-3-1] allowing another 2559645 steps for small clauses
c [cce-3-1] scheduling 24642 clauses = 19594 binary + 5048 ternary
c [cce-3-1] tried to eliminate 5192 small clauses 21%
c [cce-3-1] eliminated 1271 binary clauses 6%
c [cce-3-1] eliminated 189 ternary clauses 4%
c [cce-3-1] eliminated 1460 small clauses 6%
c [cce-3-1] eliminated 1460 small clauses in 30000002 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 1625 covered clauses in round 1
c [cce-3] eliminated 1625 covered clauses in TOTAL during 1 rounds
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 5493 variables 100%
c [elim-7] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 533 variables 10% in round 1 in 1905451 steps
c [elim-7-1] backward subsumption/strengthening limit 1905400
c [elim-7-1-1] backward checking 1947 touched variables 35%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 4 and strengthened 10 clauses in 248169 steps
c [elim-7-1] rescheduled 66 variables 1% by backward subsumption
c [elim-7-2] eliminated 6 variables 0% in round 2 in 24519 steps
c [elim-7-2] backward subsumption/strengthening limit 24500
c [elim-7-2-1] backward checking 54 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 7 and strengthened 2 clauses in 16108 steps
c [elim-7-2] rescheduled 22 variables 0% by backward subsumption
c [elim-7-3] no variable eliminated in round 3 in 7735 steps
c [elim-7] fully completed in 3 rounds
c [elim-7] transition to [ all 0 rem 0 ] state
c [elim-7] eliminated 540 = 10% variables out of 5493 scheduled
c [bca-3] limit of 10000000 steps and 60283 added (scaled 2)
c [bca-3] 7263 out of 9908 literals actually usable 73%
c [bca-3] added 11 blocked clauses in 18723 steps
c [sweep-3] limit 1000000 penalty 0 = 0 + 0
c [sweep-3-1] 713 pos 19.3% + 2976 neg 80.7% = 3689 sched 74.5% ret 1264
c [sweep-3-1] 1000582 steps 60 queries 123.55 avg class size
c [sweep-3-1] 632 decisions 54 SAT calls 74.26 avg env size
c [sweep-3-1] 2325 variables remain 47% (2620 retained 53%)
c [decomp-18] removed 19 variables
c [sweep-3-1] removed 19 vars (0 failed, 6 eqs, 8 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 19 vars in TOTAL (1 rounds, 59 queries)
c [score-distribution-7] 3196 pos 64.78%, 160 min 3.24%, 1578 zero 31.98%
c [score-distribution-7] 1757 different 35.61% out of total 4934 variables
c [simplification-7] removed 923 variables 15.8% (4934 remain 4%)
c [simplification-7] removed 7875 irredundant clauses 20.9% (29796 remain 5%)
c [simplification-7] maximum reduction of 21% = max (16%, 21%)
c [simplification-7] large reduction 21% >= 5% limit
c [simplification-7] next conflict interval 2000 = 2000/1
c [simplification-7] penalized conflict interval 2000 = 1 * 2000
c [simplification-7] hard conflict limit 21127 (soft 11127 + delta 10000)
c [simplification-7] new conflict limit 11127 (hard 21127)
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    8.9    4933    29796      9152    3652    427 18063   42    92    9  46%      6   85   63    5 1194%
c i    8.9    4930    29796      9163    3658    427 18064   42    92    9  46%      6   85   62    5 1170%
c i    8.9    4929    29796      9172    3665    427 18064   42    92    9  46%      6   85   61    5 1150%
c i    9.0    4928    29796      9690    4152    431 18065   42    91   10  46%      5   84   36    6  657%
c i    9.0    4927    29796      9756    4213    432 18067   41    91   10  45%      5   83   32    6  578%
c i    9.1    4926    29796     10023    4463    435 18068   42    92   10  46%      4   84   49    6  845%
c i    9.1    4925    29796     10040    4477    434 18069   42    92   10  46%      4   84   47    6  814%
c i    9.1    4924    29796     10041    4477    434 18069   42    92   10  46%      4   84   47    6  811%
c i    9.1    4922    29796     10043    4477    434 18070   42    92   10  46%      4   84   46    6  805%
c i    9.1    4919    29796     10112    4538    436 18072   42    91   10  46%      4   83   39    6  682%
c i    9.2    4916    29796     10416    4818    441 18075   42    92   10  46%      3   83   43    6  731%
c 
c [simplification-8] limit 11143 conflicts (hard 21127) hit after 11145 conflicts
c [quatres-4] found 1416 quaternary clauses 55% in total
c [quatres-4-1] removed 1 duplicate quaternary clauses
c [ternres-4] limit 4000000 with penalty 0 = 0 + 0
c [ternres-4] all 4915 free variables schedulable
c [ternres-4] 114 ternary resolvents (0 bin, 114 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 26 variables
c [simpleprobe-4] 74 schedulable variables 2%
c [simpleprobe-4] limit 3423118 penalty 0 = 0 + 0
c [decomp-20] removed 11 variables
c [simpleprobe-4] fully completed simple probing
c [simpleprobe-4] removed 11 variables, found 1148 hbrs, 8 units
c [unhide-8] limit 171155 with penalty 0 = 0 + 0
c [unhide-8-8] 2 units, 53 failed, 2450 tauts, 0 hbrs, 5395 literals
c [transred-4] limit 855779 with penalty 0 = 0 + 0
c [transred-4] removed 365 transitive binary clauses
c [transred-4] found 8 units
c [cce-4] boosting limit by 10
c [cce-4] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-4-1] eliminated 1 clauses out of 1 (100%) of length 12
c [cce-4-1] eliminated 1 clauses out of 5 (20%) of length 11
c [cce-4-1] eliminated 1 clauses out of 9 (11%) of length 9
c [cce-4-1] eliminated 6 clauses out of 156 (4%) of length 6
c [cce-4-1] eliminated 25 clauses out of 515 (5%) of length 5
c [cce-4-1] eliminated 90 clauses out of 1326 (7%) of length 4
c [cce-4-1] completed large round (ATE)
c [cce-4-1] eliminated 124 large clauses in 4899192 steps
c [cce-4-1] allowing another 2449596 steps for small clauses
c [cce-4-1] scheduling 22357 clauses = 17215 binary + 5142 ternary
c [cce-4-1] tried to eliminate 22357 small clauses 100%
c [cce-4-1] eliminated 3279 binary clauses 19%
c [cce-4-1] eliminated 844 ternary clauses 16%
c [cce-4-1] eliminated 4123 small clauses 18%
c [cce-4-1] eliminated 4406 small clauses in 101650023 steps
c [cce-4-1] completed small round (ATE)
c [cce-4-1] completed small and large (ATE)
c [cce-4-1] eliminated 4530 covered clauses in round 1
c [cce-4-2] completed large round (ATE)
c [cce-4-2] allowing another 1823244 steps for small clauses
c [cce-4-2] scheduling 18234 clauses = 13936 binary + 4298 ternary
c [cce-4-2] tried to eliminate 18234 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 4530 covered clauses in TOTAL during 2 rounds
c [elim-8] scheduling all variables this time
c [elim-8] scheduled 4860 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 400000000 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 431 variables 9% in round 1 in 1515116 steps
c [elim-8-1] backward subsumption/strengthening limit 1515100
c [elim-8-1-1] backward checking 2000 touched variables 41%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 1 and strengthened 5 clauses in 207570 steps
c [elim-8-1] rescheduled 19 variables 0% by backward subsumption
c [elim-8-2] eliminated 1 variables 0% in round 2 in 7240 steps
c [elim-8-2] backward subsumption/strengthening limit 7200
c [elim-8-2-1] backward checking 4 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 0 clauses in 6666 steps
c [elim-8] fully completed in 2 rounds
c [gc-59] reconnected 18961 binary clauses (produced 0 empty 1 units)
c [elim-8] transition to [ all 0 rem 0 ] state
c [elim-8] eliminated 435 = 9% variables out of 4860 scheduled
c [bca-4] limit of 10000000 steps and 49012 added (scaled 2)
c [bca-4] 6184 out of 8852 literals actually usable 70%
c [bca-4] added 5 blocked clauses in 17115 steps
c [sweep-4] limit 1000000 penalty 0 = 0 + 0
c [sweep-4-1] 490 pos 23.4% + 1606 neg 76.6% = 2096 sched 47.4% ret 2329
c [sweep-4-1] 1032159 steps 66 queries 88.15 avg class size
c [sweep-4-1] 1315 decisions 63 SAT calls 73.48 avg env size
c [sweep-4-1] 1527 variables remain 35% (2893 retained 65%)
c [decomp-21] removed 12 variables
c [sweep-4-1] removed 12 vars (0 failed, 4 eqs, 8 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 12 vars in TOTAL (1 rounds, 65 queries)
c [score-distribution-8] 2878 pos 65.22%, 246 min 5.57%, 1289 zero 29.21%
c [score-distribution-8] 1764 different 39.97% out of total 4413 variables
c [simplification-8] removed 502 variables 10.2% (4413 remain 3%)
c [simplification-8] removed 5574 irredundant clauses 18.7% (24222 remain 4%)
c [simplification-8] maximum reduction of 19% = max (10%, 19%)
c [simplification-8] large reduction 19% >= 5% limit
c [simplification-8] next conflict interval 2000 = 2000/1
c [simplification-8] penalized conflict interval 2000 = 1 * 2000
c [simplification-8] hard conflict limit 23145 (soft 13145 + delta 10000)
c [simplification-8] new conflict limit 13145 (hard 23145)
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   13.6    4412    24222     11334    4423    846 16712   43    93   10  46%      6   83   49    7  751%
c i   13.6    4408    24222     11546    4619    847 16712   42    92   10  46%      5   82   34    7  514%
c i   13.6    4406    24222     11553    4625    847 16712   42    92   10  46%      5   82   35    7  529%
c 
c [simplification-9] limit 13146 conflicts (hard 23145) hit after 13146 conflicts
c [ternres-5] limit 4000000 with penalty 0 = 0 + 0
c [ternres-5] all 4406 free variables schedulable
c [ternres-5] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-5] fully completed ternary resolution
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] extracted 24 xors of average arity 2.8
c [gauss-4] connected 68 occurrences of 26 variables (average 2.6)
c [gauss-4] limit 1000000 penalty 1 = 1 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 8812 literals 100%
c [treelook-4] scheduling used 130135 steps
c [treelook-4] scheduled completely
c [treelook-4] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 313318 steps
c [treelook-4] 8732 literals remain 100%
c [treelook-4] 4380 variables remain to probed next time 100%
c [decomp-23] removed 1 variables
c [treelook-4] removed 27 variables, found 1762 hbrs
c [unhide-9] limit 193380 with penalty 0 = 0 + 0
c [unhide-9-9] 2 units, 3 failed, 179 tauts, 0 hbrs, 7882 literals
c [transred-5] limit 966901 with penalty 0 = 0 + 0
c [transred-5] removed 465 transitive binary clauses
c [transred-5] found 16 units
c [cce-5] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-5-1] eliminated 1 clauses out of 1 (100%) of length 20
c [cce-5-1] eliminated 1 clauses out of 3 (33%) of length 15
c [cce-5-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-5-1] eliminated 2 clauses out of 6 (33%) of length 11
c [cce-5-1] eliminated 3 clauses out of 6 (50%) of length 10
c [cce-5-1] eliminated 2 clauses out of 14 (14%) of length 9
c [cce-5-1] eliminated 2 clauses out of 58 (3%) of length 7
c [cce-5-1] eliminated 8 clauses out of 161 (5%) of length 6
c [cce-5-1] eliminated 15 clauses out of 506 (3%) of length 5
c [cce-5-1] eliminated 122 clauses out of 1250 (10%) of length 4
c [cce-5-1] completed large round (ACCE)
c [cce-5-1] eliminated 157 large clauses in 4583987 steps
c [cce-5-1] allowing another 2291993 steps for small clauses
c [cce-5-1] scheduling 17737 clauses = 13607 binary + 4130 ternary
c [cce-5-1] tried to eliminate 7008 small clauses 40%
c [cce-5-1] eliminated 332 binary clauses 2%
c [cce-5-1] eliminated 313 ternary clauses 8%
c [cce-5-1] eliminated 645 small clauses 4%
c [cce-5-1] eliminated 834 small clauses in 30000002 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 991 covered clauses in round 1
c [cce-5] eliminated 991 covered clauses in TOTAL during 1 rounds
c [elim-9] scheduling all variables this time
c [elim-9] scheduled 4349 variables 100%
c [elim-9] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 155 variables 4% in round 1 in 1358964 steps
c [elim-9-1] backward subsumption/strengthening limit 1358900
c [elim-9-1-1] backward checking 900 touched variables 21%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 1 and strengthened 0 clauses in 96825 steps
c [elim-9-1] rescheduled 3 variables 0% by backward subsumption
c [elim-9-2] no variable eliminated in round 2 in 925 steps
c [elim-9] fully completed in 2 rounds
c [elim-9] transition to [ all 0 rem 0 ] state
c [elim-9] eliminated 155 = 4% variables out of 4349 scheduled
c [bca-5] limit of 10000000 steps and 46011 added (scaled 2)
c [bca-5] 5510 out of 8390 literals actually usable 66%
c [bca-5] added 10 blocked clauses in 17389 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 10000000 penalty 0 = 0 + 0
c [sweep-5-1] 468 pos 31.8% + 1003 neg 68.2% = 1471 sched 35.1% ret 2723
c [sweep-5-1] 5403850 steps 484 queries 9.63 avg class size
c [sweep-5-1] 4329 decisions 441 SAT calls 46.24 avg env size
c [sweep-5-1] fully completed sweeping round
c [decomp-24] removed 103 variables
c [sweep-5-1] removed 103 vars (0 failed, 58 eqs, 50 impls)
c [sweep-5-2] 647 pos 15.8% + 3444 neg 84.2% = 4091 sched 100.0% ret 0
c [sweep-5-2] 4603490 steps 277 queries 31.04 avg class size
c [sweep-5-2] 4251 decisions 264 SAT calls 72.74 avg env size
c [sweep-5-2] 524 variables remain 13% (3529 retained 87%)
c [decomp-25] removed 58 variables
c [sweep-5-2] removed 58 vars (0 failed, 15 eqs, 25 impls)
c [sweep-5] removed 161 vars in TOTAL (2 rounds, 759 queries)
c [score-distribution-9] 2704 pos 67.05%, 292 min 7.24%, 1037 zero 25.71%
c [score-distribution-9] 1627 different 40.34% out of total 4033 variables
c [simplification-9] removed 373 variables 8.5% (4033 remain 3%)
c [simplification-9] removed 2378 irredundant clauses 9.8% (21844 remain 4%)
c [simplification-9] maximum reduction of 10% = max (8%, 10%)
c [simplification-9] large reduction 10% >= 5% limit
c [simplification-9] next conflict interval 2000 = 2000/1
c [simplification-9] penalized conflict interval 2000 = 1 * 2000
c [simplification-9] hard conflict limit 25146 (soft 15146 + delta 10000)
c [simplification-9] new conflict limit 15146 (hard 25146)
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   15.4    4032    21844     13276    6106    817 20959   42    92   10  45%     14   80   38    7  503%
c i   15.5    4030    21844     13434    6248    820 20963   41    92   10  45%     12   80   33    8  440%
c i   15.5    4028    21844     13442    6255    820 20963   41    92   10  45%     12   80   33    8  433%
c i   15.5    4027    21844     13465    6276    820 20964   41    92   10  45%     12   80   32    8  430%
c i   15.5    4023    21844     13501    6310    821 20964   41    93   10  44%     11   80   33    8  443%
c i   15.5    4022    21844     13517    6325    821 20964   41    92   10  44%     11   80   32    8  426%
c i   15.5    4021    21844     13547    6350    821 20964   41    92   10  44%     11   80   34    8  447%
c i   15.5    4020    21844     13656    6458    821 20964   41    92   10  44%     10   79   32    8  419%
c i   15.5    4019    21844     13685    6486    821 20964   41    92   10  44%      9   79   31    8  413%
c i   15.5    4018    21844     13707    6507    821 20964   41    92   10  44%      9   79   31    8  406%
c i   15.5    4017    21844     13756    6554    821 20964   41    92   10  44%      9   79   31    8  410%
c i   15.6    4015    21844     13880    6665    821 20964   41    92   10  45%      8   79   42    8  539%
c i   15.6    4014    21844     14194    6970    821 20964   40    91   12  44%      6   78   36    8  453%
c i   15.7    4013    21844     14299    7071    821 20964   41    91   12  45%      6   78   42    8  531%
c i   15.7    4012    21844     14334    7104    821 20964   41    91   12  45%      5   78   40    8  506%
c i   15.7    4008    21844     14397    7163    821 20965   41    91   12  45%      5   78   40    8  496%
c i   15.7    4007    21844     14507    7269    821 20965   40    91   12  45%      5   77   37    8  458%
c i   15.7    4006    21844     14561    7317    821 20966   40    90   12  45%      4   77   37    8  461%
c i   15.7    4004    21844     14640    7388    821 20966   40    90   12  45%      4   76   38    8  473%
c i   15.7    4003    21844     14691    7437    821 20966   40    90   12  45%      4   76   35    8  436%
c i   15.8    4002    21844     15029    7763    822 20967   40    88   12  45%      3   74   32    8  393%
c i   15.8    4001    21844     15073    7800    823 20969   39    88   12  45%      3   73   30    8  367%
c i   15.8    4000    21844     15076    7802    823 20969   39    88   12  45%      3   73   30    8  364%
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   15.8    3997    21844     15080    7805    823 20969   39    88   12  45%      3   73   30    8  366%
c 
c [simplification-10] limit 15152 conflicts (hard 25146) hit after 15153 conflicts
c [quatres-5] found 1152 quaternary clauses 52% in total
c [quatres-5-2] added 1 quaternary resolvents
c [ternres-6] limit 4000000 with penalty 0 = 0 + 0
c [ternres-6] all 3997 free variables schedulable
c [ternres-6] 56 ternary resolvents (0 bin, 56 trn)
c [ternres-6] fully completed ternary resolution
c [card-4] limit 250000 penalty 3 = 3 + 0
c [card-4] found 809 at-most-one constraints of average size 3.6
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 250000 for elimination
c [card-4] 809 out of 809 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [decomp-26] removed 46 variables
c [basicprobe-4] limit 5424566 penalty 0 = 0 + 0
c [basicprobe-4-0] 87 probes remain 2% after last round
c [basicprobe-4-0] 286 units = 255 failed (89%) + 31 lifted (11%)
c [basicprobe-4-0] removed 370 variables, found 9003 hbrs
c [bate-2] eliminated 57 asymmetric tautologies during probing
c [unhide-10] limit 216982 with penalty 0 = 0 + 0
c [unhide-10-10] 5 units, 20 failed, 2488 tauts, 0 hbrs, 11487 literals
c [transred-6] limit 1084913 with penalty 0 = 0 + 0
c [transred-6] removed 620 transitive binary clauses
c [transred-6] found 6 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 3574 variables 100%
c [block-3] limit of 12500000 steps penalty 2 = 2 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 118 blocked clauses
c [block-3] 118 < 1/100 * 18547 = 185 considered unsuccessful
c [cce-6] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-6-1] eliminated 1 clauses out of 7 (14%) of length 8
c [cce-6-1] eliminated 2 clauses out of 30 (7%) of length 7
c [cce-6-1] eliminated 6 clauses out of 263 (2%) of length 5
c [cce-6-1] eliminated 35 clauses out of 863 (4%) of length 4
c [cce-6-1] completed large round (ATE)
c [cce-6-1] eliminated 44 large clauses in 1594320 steps
c [cce-6-1] allowing another 797160 steps for small clauses
c [cce-6-1] scheduling 14271 clauses = 11340 binary + 2931 ternary
c [cce-6-1] tried to eliminate 12078 small clauses 85%
c [cce-6-1] eliminated 696 binary clauses 6%
c [cce-6-1] eliminated 165 ternary clauses 6%
c [cce-6-1] eliminated 861 small clauses 6%
c [cce-6-1] eliminated 861 small clauses in 30000005 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 905 covered clauses in round 1
c [cce-6] eliminated 905 covered clauses in TOTAL during 1 rounds
c [elim-10] scheduling all variables this time
c [elim-10] scheduled 3574 variables 100%
c [elim-10] limit of 21698265 steps penalty 0 = 0 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 508 variables 14% in round 1 in 1012190 steps
c [elim-10-1] backward subsumption/strengthening limit 1012100
c [elim-10-1-1] backward checking 1598 touched variables 45%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 3 and strengthened 7 clauses in 157857 steps
c [elim-10-1] rescheduled 51 variables 1% by backward subsumption
c [elim-10-2] no variable eliminated in round 2 in 21454 steps
c [elim-10] fully completed in 2 rounds
c [elim-10] transition to [ all 0 rem 0 ] state
c [elim-10] eliminated 508 = 14% variables out of 3574 scheduled
c [bca-6] limit of 10000000 steps and 33794 added (scaled 2)
c [bca-6] 3909 out of 6134 literals actually usable 64%
c [bca-6] added 12 blocked clauses in 14025 steps
c [sweep-6] limit 1000000 penalty 0 = 0 + 0
c [sweep-6-1] 109 pos 27.0% + 294 neg 73.0% = 403 sched 13.1% ret 2663
c [sweep-6-1] 1001351 steps 133 queries 14.77 avg class size
c [sweep-6-1] 1244 decisions 131 SAT calls 32.61 avg env size
c [sweep-6-1] 152 variables remain 5% (2912 retained 95%)
c [decomp-27] removed 6 variables
c [sweep-6-1] removed 6 vars (0 failed, 2 eqs, 4 impls)
c [sweep-6] removed 6 vars in TOTAL (1 rounds, 132 queries)
c [score-distribution-10] 2110 pos 68.95%, 317 min 10.36%, 633 zero 20.69%
c [score-distribution-10] 1378 different 45.03% out of total 3060 variables
c [simplification-10] removed 937 variables 23.4% (3060 remain 2%)
c [simplification-10] removed 5238 irredundant clauses 24.0% (16606 remain 3%)
c [simplification-10] maximum reduction of 24% = max (23%, 24%)
c [simplification-10] large reduction 24% >= 5% limit
c [simplification-10] next conflict interval 2000 = 2000/1
c [simplification-10] penalized conflict interval 2000 = 1 * 2000
c [simplification-10] hard conflict limit 27153 (soft 17153 + delta 10000)
c [simplification-10] new conflict limit 17153 (hard 27153)
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   17.1    3059    16606     15213    5596    396 11388   39    87    9  45%      3   73   30    8  363%
c i   17.2    3057    16606     15510    5883    397 11388   39    86    9  45%      2   71   32    8  388%
c i   17.3    3056    16606     15999    6356    398 11389   38    85   10  45%      3   70   34    9  395%
c 
c [simplification-11] limit 17153 conflicts (hard 27153) hit after 17153 conflicts
c [quatres-6] found 1067 quaternary clauses 48% in total
c [quatres-6-1] removed 1 duplicate quaternary clauses
c [quatres-6-2] added 12 quaternary resolvents
c [ternres-7] limit 4000000 with penalty 0 = 0 + 0
c [ternres-7] all 3056 free variables schedulable
c [ternres-7] 38 ternary resolvents (0 bin, 38 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-28] removed 9 variables
c [simpleprobe-5] all 3051 free variables schedulable
c [simpleprobe-5] limit 4689461 penalty 0 = 0 + 0
c [decomp-29] removed 16 variables
c [simpleprobe-5] fully completed simple probing
c [simpleprobe-5] removed 16 variables, found 1134 hbrs, 13 units
c [unhide-11] limit 234473 with penalty 0 = 0 + 0
c [unhide-11-12] 0 units, 1 failed, 1117 tauts, 0 hbrs, 7014 literals
c [transred-7] limit 1172365 with penalty 0 = 0 + 0
c [transred-7] removed 622 transitive binary clauses
c [transred-7] found 4 units
c [cce-7] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 12
c [cce-7-1] eliminated 1 clauses out of 3 (33%) of length 11
c [cce-7-1] eliminated 4 clauses out of 16 (25%) of length 8
c [cce-7-1] eliminated 2 clauses out of 36 (6%) of length 7
c [cce-7-1] eliminated 7 clauses out of 94 (7%) of length 6
c [cce-7-1] eliminated 12 clauses out of 360 (3%) of length 5
c [cce-7-1] eliminated 88 clauses out of 953 (9%) of length 4
c [cce-7-1] completed large round (ACCE)
c [cce-7-1] eliminated 115 large clauses in 2553959 steps
c [cce-7-1] allowing another 1276979 steps for small clauses
c [cce-7-1] scheduling 12296 clauses = 9792 binary + 2504 ternary
c [cce-7-1] tried to eliminate 11334 small clauses 92%
c [cce-7-1] eliminated 572 binary clauses 6%
c [cce-7-1] eliminated 250 ternary clauses 10%
c [cce-7-1] eliminated 822 small clauses 7%
c [cce-7-1] eliminated 844 small clauses in 30000003 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 959 covered clauses in round 1
c [cce-7] eliminated 959 covered clauses in TOTAL during 1 rounds
c [elim-11] scheduling all variables this time
c [elim-11] scheduled 3030 variables 100%
c [elim-11] limit of 23447305 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 155 variables 5% in round 1 in 901904 steps
c [elim-11-1] backward subsumption/strengthening limit 901900
c [elim-11-1-1] backward checking 800 touched variables 26%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 1 clauses in 84865 steps
c [elim-11-1] rescheduled 10 variables 0% by backward subsumption
c [elim-11-2] eliminated 1 variables 0% in round 2 in 3251 steps
c [elim-11-2] backward subsumption/strengthening limit 3200
c [elim-11-2-1] backward checking 7 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 0 and strengthened 1 clauses in 3201 steps
c [elim-11-2] rescheduled 6 variables 0% by backward subsumption
c [elim-11-3] no variable eliminated in round 3 in 2238 steps
c [elim-11] fully completed in 3 rounds
c [elim-11] transition to [ all 0 rem 0 ] state
c [elim-11] eliminated 156 = 5% variables out of 3030 scheduled
c [bca-7] limit of 10000000 steps and 31038 added (scaled 2)
c [bca-7] 3518 out of 5750 literals actually usable 61%
c [bca-7] added 4 blocked clauses in 14868 steps
c [sweep-7] limit 1000000 penalty 0 = 0 + 0
c [sweep-7-1] 21 pos 14.5% + 124 neg 85.5% = 145 sched 5.0% ret 2729
c [sweep-7-1] 606206 steps 98 queries 6.08 avg class size
c [sweep-7-1] 602 decisions 95 SAT calls 22.27 avg env size
c [sweep-7-1] fully completed sweeping round
c [decomp-30] removed 4 variables
c [sweep-7-1] removed 4 vars (0 failed, 4 eqs, 3 impls)
c [sweep-7-2] 445 pos 15.5% + 2425 neg 84.5% = 2870 sched 100.0% ret 0
c [sweep-7-2] 399247 steps 23 queries 228.70 avg class size
c [sweep-7-2] 552 decisions 22 SAT calls 96.05 avg env size
c [sweep-7-2] 2476 variables remain 86% (390 retained 14%)
c [decomp-31] removed 4 variables
c [sweep-7-2] removed 4 vars (0 failed, 0 eqs, 1 impls)
c [sweep-7] removed 8 vars in TOTAL (2 rounds, 119 queries)
c [score-distribution-11] 1912 pos 66.71%, 394 min 13.75%, 560 zero 19.54%
c [score-distribution-11] 1168 different 40.75% out of total 2866 variables
c [simplification-11] removed 190 variables 6.2% (2866 remain 2%)
c [simplification-11] removed 1372 irredundant clauses 8.3% (15234 remain 2%)
c [simplification-11] maximum reduction of 8% = max (6%, 8%)
c [simplification-11] large reduction 8% >= 5% limit
c [simplification-11] next conflict interval 2000 = 2000/1
c [simplification-11] penalized conflict interval 2000 = 1 * 2000
c [simplification-11] hard conflict limit 29153 (soft 19153 + delta 10000)
c [simplification-11] new conflict limit 19153 (hard 29153)
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   18.6    2865    15234     17233    7206    505  9687   36    81    9  45%      8   64   33    9  370%
c i   18.7    2864    15234     17792    7735    506  9689   36    79   11  45%      6   61   33    9  365%
c i   18.7    2863    15234     17798    7738    507  9689   36    78   11  45%      6   61   33    9  359%
c i   18.7    2862    15234     17817    7753    507  9690   36    78   11  46%      6   61   32    9  350%
c i   18.7    2860    15234     17892    7824    507  9691   35    78   11  45%      6   60   29    9  313%
c i   18.8    2859    15234     18405    8319    507  9691   35    77   11  46%      5   59   31    9  333%
c i   18.9    2858    15234     18896    8789    512  9692   35    77   11  46%      4   59   36   10  380%
c 
c [simplification-12] limit 19154 conflicts (hard 29153) hit after 19154 conflicts
c [quatres-7] found 1000 quaternary clauses 46% in total
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [ternres-8] limit 4000000 with penalty 0 = 0 + 0
c [ternres-8] all 2858 free variables schedulable
c [ternres-8] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-8] fully completed ternary resolution
c [gauss-5] limit 500000 penalty 2 = 2 + 0
c [gauss-5] extracted 34 xors of average arity 2.6
c [gauss-5] connected 90 occurrences of 30 variables (average 3.0)
c [gauss-5] limit 500000 penalty 2 = 2 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 3 variables
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 5710 literals 100%
c [treelook-5] scheduling used 90707 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 309743 steps
c [treelook-5] 5657 literals remain 99%
c [treelook-5] 2852 variables remain to probed next time 100%
c [treelook-5] removed 3 variables, found 2949 hbrs
c [unhide-12] limit 253451 with penalty 0 = 0 + 0
c [unhide-12-14] 3 units, 4 failed, 1134 tauts, 0 hbrs, 10141 literals
c [transred-8] limit 1267257 with penalty 0 = 0 + 0
c [transred-8] removed 404 transitive binary clauses
c [transred-8] found 2 units
c [cce-8] boosting limit by 10
c [cce-8] limit of 300000000 steps penalty 0 = 0 + 0
c [cce-8-1] eliminated 1 clauses out of 15 (7%) of length 8
c [cce-8-1] eliminated 1 clauses out of 90 (1%) of length 6
c [cce-8-1] eliminated 1 clauses out of 343 (0%) of length 5
c [cce-8-1] eliminated 20 clauses out of 885 (2%) of length 4
c [cce-8-1] completed large round (ATE)
c [cce-8-1] eliminated 23 large clauses in 2318152 steps
c [cce-8-1] allowing another 1159076 steps for small clauses
c [cce-8-1] scheduling 11118 clauses = 8963 binary + 2155 ternary
c [cce-8-1] tried to eliminate 11118 small clauses 100%
c [cce-8-1] eliminated 131 binary clauses 1%
c [cce-8-1] eliminated 14 ternary clauses 1%
c [cce-8-1] eliminated 145 small clauses 1%
c [cce-8-1] eliminated 173 small clauses in 26996937 steps
c [cce-8-1] completed small round (ATE)
c [cce-8-1] eliminated 196 covered clauses in round 1
c [cce-8-2] completed large round (ATE)
c [cce-8-2] allowing another 1117364 steps for small clauses
c [cce-8-2] scheduling 10973 clauses = 8832 binary + 2141 ternary
c [cce-8-2] tried to eliminate 10973 small clauses 100%
c [cce-8-2] completed small round (ATE)
c [cce-8-2] eliminated 0 covered clauses in round 2
c [cce-8] eliminated 196 covered clauses in TOTAL during 2 rounds
c [elim-12] scheduling all variables this time
c [elim-12] scheduled 2843 variables 100%
c [elim-12] limit of 25345145 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 47 variables 2% in round 1 in 865453 steps
c [elim-12-1] backward subsumption/strengthening limit 865400
c [elim-12-1-1] backward checking 287 touched variables 10%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 1 and strengthened 1 clauses in 32228 steps
c [elim-12-1] rescheduled 11 variables 0% by backward subsumption
c [elim-12-2] eliminated 1 variables 0% in round 2 in 4424 steps
c [elim-12-2] backward subsumption/strengthening limit 4400
c [elim-12-2-1] backward checking 7 touched variables 0%
c [elim-12-2-1] fully completed backward checking in 1 rounds
c [elim-12-2] subsumed 0 and strengthened 1 clauses in 3579 steps
c [elim-12-2] rescheduled 6 variables 0% by backward subsumption
c [elim-12-3] no variable eliminated in round 3 in 1971 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 48 = 2% variables out of 2843 scheduled
c [bca-8] limit of 10000000 steps and 30134 added (scaled 2)
c [bca-8] 3304 out of 5592 literals actually usable 59%
c [bca-8] added 12 blocked clauses in 16081 steps
c [sweep-8] limit 1000000 penalty 0 = 0 + 0
c [sweep-8-1] 334 pos 13.9% + 2077 neg 86.1% = 2411 sched 86.3% ret 384
c [sweep-8-1] 1060603 steps 27 queries 186.67 avg class size
c [sweep-8-1] 799 decisions 27 SAT calls 109.30 avg env size
c [sweep-8-1] 1734 variables remain 62% (1056 retained 38%)
c [decomp-34] removed 5 variables
c [sweep-8-1] removed 5 vars (0 failed, 0 eqs, 0 impls)
c [sweep-8] removed 5 vars in TOTAL (1 rounds, 26 queries)
c [score-distribution-12] 1916 pos 68.67%, 358 min 12.83%, 516 zero 18.49%
c [score-distribution-12] 1164 different 41.72% out of total 2790 variables
c [simplification-12] removed 68 variables 2.4% (2790 remain 2%)
c [simplification-12] removed 478 irredundant clauses 3.1% (14756 remain 2%)
c [simplification-12] maximum reduction of 3% = max (2%, 3%)
c [simplification-12] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-12] new conflict interval 5000
c [simplification-12] penalized conflict interval 5000 = 1 * 5000
c [simplification-12] hard conflict limit 34154 (soft 24154 + delta 10000)
c [simplification-12] new conflict limit 24154 (hard 34154)
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   20.8    2789    14756     20213    9880    489 10446   35    76   12  47%      9   56   34   10  341%
c i   20.9    2788    14756     20274    9937    489 10446   35    75   12  47%      9   56   35   10  344%
c 
c [simplification-13] limit 24154 conflicts (hard 34154) hit after 24154 conflicts
c [quatres-8] found 1029 quaternary clauses 43% in total
c [ternres-9] limit 4000000 with penalty 0 = 0 + 0
c [ternres-9] all 2788 free variables schedulable
c [ternres-9] 6 ternary resolvents (0 bin, 6 trn)
c [ternres-9] fully completed ternary resolution
c [decomp-35] removed 2 variables
c [basicprobe-5] limit 7650536 penalty 0 = 0 + 0
c [basicprobe-5-0] 338 sched 12%, 62 failed, 2 lifted, 2576 hbrs
c [decomp-36] removed 74 variables
c [basicprobe-5-1] 764 sched 29%, 41 failed, 2 lifted, 4459 hbrs
c [decomp-37] removed 51 variables
c [basicprobe-5-2] 572 probes remain 22% after last round
c [basicprobe-5-2] 110 units = 106 failed (96%) + 4 lifted (4%)
c [basicprobe-5-2] removed 128 variables, found 7488 hbrs
c [bate-3] eliminated 45 asymmetric tautologies during probing
c [unhide-13] limit 306021 with penalty 0 = 0 + 0
c [unhide-13-16] 0 units, 2 failed, 964 tauts, 0 hbrs, 16540 literals
c [transred-9] limit 1530107 with penalty 0 = 0 + 0
c [transred-9] removed 489 transitive binary clauses
c [cce-9] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-9-1] eliminated 2 clauses out of 11 (18%) of length 8
c [cce-9-1] eliminated 1 clauses out of 32 (3%) of length 7
c [cce-9-1] eliminated 5 clauses out of 285 (2%) of length 5
c [cce-9-1] eliminated 15 clauses out of 795 (2%) of length 4
c [cce-9-1] completed large round (ACCE)
c [cce-9-1] eliminated 23 large clauses in 1803569 steps
c [cce-9-1] allowing another 901784 steps for small clauses
c [cce-9-1] scheduling 10359 clauses = 8562 binary + 1797 ternary
c [cce-9-1] tried to eliminate 10359 small clauses 100%
c [cce-9-1] eliminated 415 binary clauses 5%
c [cce-9-1] eliminated 74 ternary clauses 4%
c [cce-9-1] eliminated 489 small clauses 5%
c [cce-9-1] eliminated 494 small clauses in 21879944 steps
c [cce-9-1] completed small round (ACCE)
c [cce-9-1] completed small and large (ACCE)
c [cce-9-1] eliminated 517 covered clauses in round 1
c [cce-9-2] eliminated 1 clauses out of 31 (3%) of length 7
c [cce-9-2] eliminated 3 clauses out of 280 (1%) of length 5
c [cce-9-2] eliminated 5 clauses out of 780 (1%) of length 4
c [cce-9-2] completed large round (ACCE)
c [cce-9-2] eliminated 9 large clauses in 1688028 steps
c [cce-9-2] allowing another 844014 steps for small clauses
c [cce-9-2] scheduling 9870 clauses = 8147 binary + 1723 ternary
c [cce-9-2] tried to eliminate 3687 small clauses 37%
c [cce-9-2] eliminated 5 binary clauses 0%
c [cce-9-2] eliminated 2 ternary clauses 0%
c [cce-9-2] eliminated 7 small clauses 0%
c [cce-9-2] eliminated 7 small clauses in 8120058 steps
c [cce-9-2] incomplete small round (ACCE)
c [cce-9-2] eliminated 16 covered clauses in round 2
c [cce-9] eliminated 533 covered clauses in TOTAL during 2 rounds
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 2659 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 164 variables 6% in round 1 in 767476 steps
c [elim-13-1] backward subsumption/strengthening limit 767400
c [elim-13-1-1] backward checking 824 touched variables 31%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 1 and strengthened 3 clauses in 81478 steps
c [elim-13-1] rescheduled 14 variables 1% by backward subsumption
c [elim-13-2] no variable eliminated in round 2 in 4032 steps
c [elim-13] fully completed in 2 rounds
c [elim-13] transition to [ all 0 rem 0 ] state
c [elim-13] eliminated 164 = 6% variables out of 2659 scheduled
c [bca-9] limit of 10000000 steps and 26602 added (scaled 2)
c [bca-9] 2825 out of 4992 literals actually usable 57%
c [bca-9] added 17 blocked clauses in 18132 steps
c [sweep-9] limit 1000000 penalty 0 = 0 + 0
c [sweep-9-1] 270 pos 17.3% + 1289 neg 82.7% = 1559 sched 62.5% ret 936
c [sweep-9-1] 1028099 steps 22 queries 169.36 avg class size
c [sweep-9-1] 743 decisions 21 SAT calls 137.76 avg env size
c [sweep-9-1] 1242 variables remain 50% (1253 retained 50%)
c [sweep-9-1] removed 0 vars (0 failed, 0 eqs, 1 impls)
c [sweep-9] removed 0 vars in TOTAL (1 rounds, 21 queries)
c [score-distribution-13] 1746 pos 69.98%, 384 min 15.39%, 365 zero 14.63%
c [score-distribution-13] 1164 different 46.65% out of total 2495 variables
c [simplification-13] removed 293 variables 10.5% (2495 remain 2%)
c [simplification-13] removed 1721 irredundant clauses 11.7% (13035 remain 2%)
c [simplification-13] maximum reduction of 12% = max (11%, 12%)
c [simplification-13] large reduction 12% >= 5% limit
c [simplification-13] next conflict interval 2000 = 2000/1
c [simplification-13] penalized conflict interval 2000 = 1 * 2000
c [simplification-13] hard conflict limit 36154 (soft 26154 + delta 10000)
c [simplification-13] new conflict limit 26154 (hard 36154)
c 
c [simplification-14] limit 26154 conflicts (hard 36154) hit after 26154 conflicts
c [ternres-10] limit 4000000 with penalty 0 = 0 + 0
c [ternres-10] all 2495 free variables schedulable
c [ternres-10] 9 ternary resolvents (0 bin, 9 trn)
c [ternres-10] fully completed ternary resolution
c [simpleprobe-6] all 2495 free variables schedulable
c [simpleprobe-6] limit 6533539 penalty 0 = 0 + 0
c [simpleprobe-6] fully completed simple probing
c [simpleprobe-6] removed 0 variables, found 719 hbrs, 0 units
c [unhide-14] limit 326676 with penalty 0 = 0 + 0
c [unhide-14-18] 0 units, 0 failed, 720 tauts, 0 hbrs, 7921 literals
c [transred-10] limit 1633384 with penalty 0 = 0 + 0
c [transred-10] removed 429 transitive binary clauses
c [transred-10] found 2 units
c [block-4] scheduling all variables this time
c [block-4] scheduled 2493 variables 100%
c [block-4] limit of 6250000 steps penalty 3 = 3 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 17 blocked clauses
c [block-4] 17 < 1/100 * 13009 = 130 considered unsuccessful
c [cce-10] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-10-1] eliminated 1 clauses out of 16 (6%) of length 8
c [cce-10-1] eliminated 3 clauses out of 309 (1%) of length 5
c [cce-10-1] eliminated 7 clauses out of 818 (1%) of length 4
c [cce-10-1] completed large round (ATE)
c [cce-10-1] eliminated 11 large clauses in 1908721 steps
c [cce-10-1] allowing another 954360 steps for small clauses
c [cce-10-1] scheduling 9979 clauses = 7860 binary + 2119 ternary
c [cce-10-1] tried to eliminate 9979 small clauses 100%
c [cce-10-1] eliminated 43 binary clauses 1%
c [cce-10-1] eliminated 55 ternary clauses 3%
c [cce-10-1] eliminated 98 small clauses 1%
c [cce-10-1] eliminated 98 small clauses in 19735786 steps
c [cce-10-1] completed small round (ATE)
c [cce-10-1] eliminated 109 covered clauses in round 1
c [cce-10-2] completed large round (ATE)
c [cce-10-2] allowing another 944823 steps for small clauses
c [cce-10-2] scheduling 9881 clauses = 7817 binary + 2064 ternary
c [cce-10-2] tried to eliminate 4919 small clauses 50%
c [cce-10-2] incomplete small round (ATE)
c [cce-10-2] eliminated 0 covered clauses in round 2
c [cce-10] eliminated 109 covered clauses in TOTAL during 2 rounds
c [cce-10] 109 < 1/100 * 12976 = 129 considered unsuccessful
c [elim-14] scheduling all variables this time
c [elim-14] scheduled 2493 variables 100%
c [elim-14] limit of 32667695 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 18 variables 1% in round 1 in 742990 steps
c [elim-14-1] backward subsumption/strengthening limit 742900
c [elim-14-1-1] backward checking 150 touched variables 6%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 1 and strengthened 0 clauses in 16625 steps
c [elim-14-1] rescheduled 5 variables 0% by backward subsumption
c [elim-14-2] eliminated 1 variables 0% in round 2 in 1817 steps
c [elim-14-2] backward subsumption/strengthening limit 1800
c [elim-14-2-1] backward checking 8 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 0 and strengthened 0 clauses in 1801 steps
c [elim-14-2] fully rescheduled 2474 variables 99%
c [elim-14-3] no variable eliminated in round 3 in 740727 steps
c [elim-14] fully completed in 3 rounds
c [elim-14] transition to [ all 0 rem 0 ] state
c [elim-14] eliminated 19 = 1% variables out of 2493 scheduled
c [elim-14] 19 < 1/100 * 2493 = 24 considered unsuccessful
c [bca-10] limit of 10000000 steps and 26244 added (scaled 2)
c [bca-10] 2705 out of 4950 literals actually usable 55%
c [bca-10] added 8 blocked clauses in 19780 steps
c [score-distribution-14] 1741 pos 70.37%, 377 min 15.24%, 356 zero 14.39%
c [score-distribution-14] 1208 different 48.83% out of total 2474 variables
c [simplification-14] removed 21 variables 0.8% (2474 remain 2%)
c [simplification-14] removed 183 irredundant clauses 1.4% (12852 remain 2%)
c [simplification-14] maximum reduction of 1% = max (1%, 1%)
c [simplification-14] geometric conflict interval increment 10000 = 20000 / 2
c [simplification-14] new conflict interval 15000
c [simplification-14] penalized conflict interval 15000 = 1 * 15000
c [simplification-14] hard conflict limit 51154 (soft 41154 + delta 10000)
c [simplification-14] new conflict limit 41154 (hard 51154)
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   26.3    2473    12852     32003   19134    419 11590   33    65   17  50%    153   37   35   14  258%
c 
c [simplification-15] limit 41154 conflicts (hard 51154) hit after 41155 conflicts
c [quatres-9] found 1040 quaternary clauses 37% in total
c [quatres-9-1] removed 2 duplicate quaternary clauses
c [quatres-9-2] added 1 single-self-subsuming ternary resolvents
c [quatres-9-2] added 7 quaternary resolvents
c [ternres-11] limit 4000000 with penalty 0 = 0 + 0
c [ternres-11] all 2473 free variables schedulable
c [ternres-11] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-11] fully completed ternary resolution
c [card-5] limit 125000 penalty 4 = 4 + 0
c [card-5] found 327 at-most-one constraints of average size 3.7
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 125000 for elimination
c [card-5] 327 out of 327 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-41] removed 2 variables
c [treelook-6] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 4944 literals 100%
c [treelook-6] scheduling used 127644 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 302243 steps
c [treelook-6] 4889 literals remain 99%
c [treelook-6] 2472 variables remain to probed next time 100%
c [treelook-6] removed 0 variables, found 1010 hbrs
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 331 transitive binary clauses
c [bca-11] limit of 10000000 steps and 26234 added (scaled 2)
c [bca-11] 2434 out of 4946 literals actually usable 49%
c [bca-11] added 7 blocked clauses in 33499 steps
c [sweep-10] limit 500000 penalty 1 = 1 + 0
c [sweep-10-1] 237 pos 19.3% + 992 neg 80.7% = 1229 sched 49.7% ret 1243
c [sweep-10-1] 522806 steps 18 queries 188.61 avg class size
c [sweep-10-1] 414 decisions 17 SAT calls 103.65 avg env size
c [sweep-10-1] 1098 variables remain 44% (1373 retained 56%)
c [decomp-43] removed 1 variables
c [sweep-10-1] removed 1 vars (0 failed, 0 eqs, 0 impls)
c [sweep-10] 1 < 1/1000 * 2472 = 2 considered unsuccessful
c [sweep-10] removed 1 vars in TOTAL (1 rounds, 17 queries)
c [score-distribution-15] 1637 pos 66.25%, 515 min 20.84%, 319 zero 12.91%
c [score-distribution-15] 1170 different 47.35% out of total 2471 variables
c [simplification-15] removed 2 variables 0.1% (2471 remain 2%)
c [simplification-15] removed 14 irredundant clauses 0.1% (12838 remain 2%)
c [simplification-15] maximum reduction of 0% = max (0%, 0%)
c [simplification-15] full geometric conflict interval increment 20000
c [simplification-15] new conflict interval 35000
c [simplification-15] penalized conflict interval 35000 = 1 * 35000
c [simplification-15] hard conflict limit 93655 (soft 76155 + delta 17500)
c [simplification-15] new conflict limit 76155 (hard 93655)
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   35.8    2470    12838     64095   49785    480 12278   37    62   29  59%    376   20   30   23  132%
c -   36.7    2470    12838     66644   16923    485 12278   38    63   20  60%    -47   20   41   23  174%
c 
c [simplification-16] limit 76155 conflicts (hard 93655) hit after 79271 conflicts
c [quatres-10] found 1141 quaternary clauses 33% in total
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 1 quaternary resolvents
c [ternres-12] limit 5405813 with penalty 0 = 0 + 0
c [ternres-12] all 2470 free variables schedulable
c [ternres-12] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-12] fully completed ternary resolution
c [gauss-6] limit 250000 penalty 3 = 3 + 0
c [gauss-6] extracted 10 xors of average arity 3.0
c [gauss-6] connected 30 occurrences of 18 variables (average 1.7)
c [gauss-6] limit 250000 penalty 3 = 3 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-6] limit 27029066 penalty 0 = 0 + 0
c [basicprobe-6-0] 618 sched 25%, 41 failed, 0 lifted, 1180 hbrs
c [decomp-45] removed 54 variables
c [basicprobe-6-1] 735 sched 31%, 18 failed, 0 lifted, 1385 hbrs
c [decomp-46] removed 22 variables
c [basicprobe-6-2] 727 sched 30%, 5 failed, 0 lifted, 656 hbrs
c [decomp-47] removed 10 variables
c [basicprobe-6-3] 718 sched 30%, 1 failed, 0 lifted, 100 hbrs
c [decomp-48] removed 1 variables
c [basicprobe-6-4] 719 sched 30%, 0 failed, 0 lifted, 18 hbrs
c [basicprobe-6-5] 70 probes remain 3% after last round
c [basicprobe-6-5] 65 units = 65 failed (100%) + 0 lifted (0%)
c [basicprobe-6-5] removed 87 variables, found 3344 hbrs
c [bate-4] eliminated 22 asymmetric tautologies during probing
c [unhide-15] limit 540581 with penalty 1 = 1 + 0
c [unhide-15-20] 0 units, 0 failed, 707 tauts, 0 hbrs, 22013 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 352 transitive binary clauses
c [cce-11] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-11-1] eliminated 3 clauses out of 13 (23%) of length 8
c [cce-11-1] eliminated 4 clauses out of 83 (5%) of length 6
c [cce-11-1] eliminated 8 clauses out of 269 (3%) of length 5
c [cce-11-1] eliminated 27 clauses out of 771 (4%) of length 4
c [cce-11-1] completed large round (ACCE)
c [cce-11-1] eliminated 42 large clauses in 1727953 steps
c [cce-11-1] allowing another 863976 steps for small clauses
c [cce-11-1] scheduling 9065 clauses = 7480 binary + 1585 ternary
c [cce-11-1] tried to eliminate 7951 small clauses 88%
c [cce-11-1] eliminated 214 binary clauses 3%
c [cce-11-1] eliminated 40 ternary clauses 3%
c [cce-11-1] eliminated 254 small clauses 3%
c [cce-11-1] eliminated 254 small clauses in 15000005 steps
c [cce-11-1] incomplete small round (ACCE)
c [cce-11-1] eliminated 296 covered clauses in round 1
c [cce-11] eliminated 296 covered clauses in TOTAL during 1 rounds
c [elim-15] scheduling all variables this time
c [elim-15] scheduled 2383 variables 100%
c [elim-15] limit of 54058132 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 99 variables 4% in round 1 in 690006 steps
c [elim-15-1] backward subsumption/strengthening limit 690000
c [elim-15-1-1] backward checking 567 touched variables 24%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 0 and strengthened 0 clauses in 58127 steps
c [elim-15] fully completed in 1 rounds
c [elim-15] transition to [ all 0 rem 0 ] state
c [elim-15] eliminated 99 = 4% variables out of 2383 scheduled
c [bca-12] limit of 10000000 steps and 24066 added (scaled 2)
c [bca-12] 2513 out of 4570 literals actually usable 55%
c [bca-12] added 12 blocked clauses in 29206 steps
c [score-distribution-16] 1533 pos 67.12%, 506 min 22.15%, 245 zero 10.73%
c [score-distribution-16] 961 different 42.08% out of total 2284 variables
c [simplification-16] removed 186 variables 7.5% (2284 remain 2%)
c [simplification-16] removed 1079 irredundant clauses 8.4% (11759 remain 2%)
c [simplification-16] maximum reduction of 8% = max (8%, 8%)
c [simplification-16] large reduction 8% >= 5% limit
c [simplification-16] next conflict interval 2000 = 2000/1
c [simplification-16] penalized conflict interval 2000 = 1 * 2000
c [simplification-16] hard conflict limit 91271 (soft 81271 + delta 10000)
c [simplification-16] new conflict limit 81271 (hard 91271)
c 
c [simplification-17] limit 81271 conflicts (hard 91271) hit after 81274 conflicts
c [quatres-11] found 1097 quaternary clauses 33% in total
c [quatres-11-1] removed 2 duplicate quaternary clauses
c [quatres-11-2] added 1 single-self-subsuming ternary resolvents
c [quatres-11-2] added 10 quaternary resolvents
c [ternres-13] limit 5529863 with penalty 0 = 0 + 0
c [ternres-13] all 2284 free variables schedulable
c [ternres-13] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-13] fully completed ternary resolution
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 216 transitive binary clauses
c [cce-12] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-12-1] eliminated 4 clauses out of 301 (1%) of length 5
c [cce-12-1] eliminated 4 clauses out of 787 (1%) of length 4
c [cce-12-1] completed large round (ATE)
c [cce-12-1] eliminated 8 large clauses in 1870465 steps
c [cce-12-1] allowing another 935232 steps for small clauses
c [cce-12-1] scheduling 8973 clauses = 7059 binary + 1914 ternary
c [cce-12-1] tried to eliminate 8973 small clauses 100%
c [cce-12-1] eliminated 34 binary clauses 0%
c [cce-12-1] eliminated 19 ternary clauses 1%
c [cce-12-1] eliminated 53 small clauses 1%
c [cce-12-1] eliminated 53 small clauses in 16503421 steps
c [cce-12-1] completed small round (ATE)
c [cce-12-1] eliminated 61 covered clauses in round 1
c [cce-12-2] completed large round (ATE)
c [cce-12-2] allowing another 929770 steps for small clauses
c [cce-12-2] scheduling 8920 clauses = 7025 binary + 1895 ternary
c [cce-12-2] tried to eliminate 7273 small clauses 82%
c [cce-12-2] incomplete small round (ATE)
c [cce-12-2] eliminated 0 covered clauses in round 2
c [cce-12] eliminated 61 covered clauses in TOTAL during 2 rounds
c [cce-12] 61 < 1/100 * 11752 = 117 considered unsuccessful
c [elim-16] scheduling all variables this time
c [elim-16] scheduled 2284 variables 100%
c [elim-16] limit of 110597266 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 5 variables 0% in round 1 in 673875 steps
c [elim-16-1] backward subsumption/strengthening limit 673800
c [elim-16-1-1] backward checking 68 touched variables 3%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 0 and strengthened 1 clauses in 8386 steps
c [elim-16-1] rescheduled 5 variables 0% by backward subsumption
c [elim-16-2] eliminated 1 variables 0% in round 2 in 7925 steps
c [elim-16-2] backward subsumption/strengthening limit 7900
c [elim-16-2-1] backward checking 9 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 0 and strengthened 0 clauses in 2020 steps
c [elim-16] fully completed in 2 rounds
c [elim-16] transition to [ all 0 rem 0 ] state
c [elim-16] eliminated 6 = 0% variables out of 2284 scheduled
c [elim-16] 6 < 1/100 * 2284 = 22 considered unsuccessful
c [bca-13] limit of 10000000 steps and 23922 added (scaled 2)
c [bca-13] 2476 out of 4558 literals actually usable 54%
c [bca-13] added 10 blocked clauses in 30993 steps
c [score-distribution-17] 1481 pos 65.01%, 554 min 24.32%, 243 zero 10.67%
c [score-distribution-17] 1018 different 44.69% out of total 2278 variables
c [simplification-17] removed 6 variables 0.3% (2278 remain 2%)
c [simplification-17] removed 75 irredundant clauses 0.6% (11684 remain 2%)
c [simplification-17] maximum reduction of 1% = max (0%, 1%)
c [simplification-17] geometric conflict interval increment 17500 = 35000 / 2
c [simplification-17] new conflict interval 52500
c [simplification-17] penalized conflict interval 52500 = 1 * 52500
c [simplification-17] hard conflict limit 160024 (soft 133774 + delta 26250)
c [simplification-17] new conflict limit 133774 (hard 160024)
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.8    2278    11684    113365   26037    486 11234   17    22   16  77%    478  -15   14   22   64%
c i   51.8    2277    11684    131441   41565    511 11238   14    20   21  73%    610  -13   23   20  115%
c i   52.4    2273    11684    134372   44288    516 11239   22    33   23  65%   -333    0   39   21  187%
c -   55.0    2272    11684    146137   26494    526 11240   36    57   23  64%   -200   21   34   23  147%
c 
c [simplification-18] limit 133774 conflicts (hard 160024) hit after 157831 conflicts
c [quatres-12] found 1194 quaternary clauses 29% in total
c [quatres-12-2] added 26 quaternary resolvents
c [ternres-14] limit 10950946 with penalty 0 = 0 + 0
c [ternres-14] all 2272 free variables schedulable
c [ternres-14] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-14] fully completed ternary resolution
c [decomp-51] removed 6 variables
c [simpleprobe-7] all 2272 free variables schedulable
c [simpleprobe-7] limit 21901893 penalty 1 = 1 + 0
c [simpleprobe-7] fully completed simple probing
c [simpleprobe-7] removed 0 variables, found 518 hbrs, 0 units
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 449 transitive binary clauses
c [bca-14] limit of 10000000 steps and 23821 added (scaled 2)
c [bca-14] 2348 out of 4546 literals actually usable 52%
c [bca-14] added 11 blocked clauses in 42819 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 8213210 penalty 2 = 2 + 0
c [sweep-11-1] 168 pos 16.3% + 864 neg 83.7% = 1032 sched 45.4% ret 1240
c [sweep-11-1] 5339219 steps 278 queries 7.67 avg class size
c [sweep-11-1] 3380 decisions 275 SAT calls 48.95 avg env size
c [sweep-11-1] fully completed sweeping round
c [decomp-53] removed 1 variables
c [sweep-11-1] removed 1 vars (0 failed, 2 eqs, 2 impls)
c [sweep-11-2] 299 pos 13.2% + 1972 neg 86.8% = 2271 sched 100.0% ret 0
c [sweep-11-2] 2895247 steps 50 queries 89.46 avg class size
c [sweep-11-2] 1395 decisions 49 SAT calls 109.61 avg env size
c [sweep-11-2] 907 variables remain 40% (1364 retained 60%)
c [sweep-11-2] removed 0 vars (0 failed, 0 eqs, 2 impls)
c [sweep-11] 1 < 1/1000 * 2272 = 2 considered unsuccessful
c [sweep-11] removed 1 vars in TOTAL (2 rounds, 326 queries)
c [score-distribution-18] 1540 pos 67.81%, 510 min 22.46%, 221 zero 9.73%
c [score-distribution-18] 998 different 43.95% out of total 2271 variables
c [simplification-18] removed 1 variables 0.0% (2271 remain 2%)
c [simplification-18] removed 55 irredundant clauses 0.5% (11629 remain 2%)
c [simplification-18] maximum reduction of 0% = max (0%, 0%)
c [simplification-18] full geometric conflict interval increment 52500
c [simplification-18] new conflict interval 105000
c [simplification-18] penalized conflict interval 105000 = 1 * 105000
c [simplification-18] hard conflict limit 315331 (soft 262831 + delta 52500)
c [simplification-18] new conflict limit 262831 (hard 315331)
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   60.6    2270    11629    169895   48593    587 11505   20    28   22  70%    172  -13    8   26   33%
c -   62.9    2252    11629    178844   25850    593 11507   38    58   18  66%   -211   17   45   27  164%
c -   70.4    2252    11629    214804   27184    625 11512   23    30   19  77%    311  -13   19   28   66%
c -   77.4    2252    11629    251977   28763    668 11519   14    19   19  76%    619  -20   11   26   42%
c i   78.0    2251    11629    255697   32061    674 11522   25    36   22  69%    642   -3   32   26  122%
c i   83.9    2250    11629    282791   56761    707 11533   28    41   29  69%   -130   -1    7   29   23%
c -   84.8    2250    11629    287831   28945    709 11533   29    42   19  70%   -439    0   44   29  152%
c 
c [simplification-19] limit 262831 conflicts (hard 315331) hit after 311969 conflicts
c [quatres-13] found 1460 quaternary clauses 29% in total
c [quatres-13-1] removed 1 duplicate quaternary clauses
c [quatres-13-2] added 4 single-self-subsuming ternary resolvents
c [quatres-13-2] added 1 quaternary resolvents
c [ternres-15] limit 22114384 with penalty 0 = 0 + 0
c [ternres-15] all 2250 free variables schedulable
c [ternres-15] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-55] removed 27 variables
c [unhide-16] limit 1105719 with penalty 2 = 2 + 0
c [unhide-16-22] 2 units, 0 failed, 1245 tauts, 0 hbrs, 39009 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 296 transitive binary clauses
c [transred-15] found 1 units
c [block-5] scheduling all variables this time
c [block-5] scheduled 2241 variables 100%
c [block-5] limit of 13821490 steps penalty 4 = 4 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 2 blocked clauses
c [block-5] 2 < 1/100 * 11453 = 114 considered unsuccessful
c [cce-13] boosting limit by 10
c [cce-13] limit of 552859610 steps penalty 1 = 1 + 0
c [cce-13-1] eliminated 1 clauses out of 4 (25%) of length 15
c [cce-13-1] eliminated 1 clauses out of 6 (17%) of length 9
c [cce-13-1] eliminated 1 clauses out of 80 (1%) of length 6
c [cce-13-1] eliminated 1 clauses out of 283 (0%) of length 5
c [cce-13-1] eliminated 24 clauses out of 750 (3%) of length 4
c [cce-13-1] completed large round (ACCE)
c [cce-13-1] eliminated 28 large clauses in 1894437 steps
c [cce-13-1] allowing another 947218 steps for small clauses
c [cce-13-1] scheduling 8445 clauses = 6986 binary + 1459 ternary
c [cce-13-1] tried to eliminate 8445 small clauses 100%
c [cce-13-1] eliminated 86 binary clauses 1%
c [cce-13-1] eliminated 36 ternary clauses 2%
c [cce-13-1] eliminated 122 small clauses 1%
c [cce-13-1] eliminated 122 small clauses in 16598629 steps
c [cce-13-1] completed small round (ACCE)
c [cce-13-1] eliminated 150 covered clauses in round 1
c [cce-13-2] eliminated 1 clauses out of 79 (1%) of length 6
c [cce-13-2] eliminated 1 clauses out of 282 (0%) of length 5
c [cce-13-2] eliminated 4 clauses out of 726 (1%) of length 4
c [cce-13-2] completed large round (ACCE)
c [cce-13-2] eliminated 6 large clauses in 1794716 steps
c [cce-13-2] allowing another 897358 steps for small clauses
c [cce-13-2] scheduling 8323 clauses = 6900 binary + 1423 ternary
c [cce-13-2] tried to eliminate 8323 small clauses 100%
c [cce-13-2] eliminated 2 binary clauses 0%
c [cce-13-2] eliminated 2 small clauses 0%
c [cce-13-2] eliminated 2 small clauses in 16148514 steps
c [cce-13-2] completed small round (ACCE)
c [cce-13-2] eliminated 8 covered clauses in round 2
c [cce-13-3] eliminated 1 clauses out of 27 (4%) of length 7
c [cce-13-3] eliminated 2 clauses out of 722 (0%) of length 4
c [cce-13-3] completed large round (ACCE)
c [cce-13-3] eliminated 3 large clauses in 1783747 steps
c [cce-13-3] allowing another 891873 steps for small clauses
c [cce-13-3] scheduling 8321 clauses = 6898 binary + 1423 ternary
c [cce-13-3] tried to eliminate 8321 small clauses 100%
c [cce-13-3] eliminated 2 binary clauses 0%
c [cce-13-3] eliminated 1 ternary clauses 0%
c [cce-13-3] eliminated 3 small clauses 0%
c [cce-13-3] eliminated 3 small clauses in 16103663 steps
c [cce-13-3] completed small round (ACCE)
c [cce-13-3] eliminated 6 covered clauses in round 3
c [cce-13] eliminated 164 covered clauses in TOTAL during 3 rounds
c [elim-17] scheduling all variables this time
c [elim-17] scheduled 2241 variables 100%
c [elim-17] limit of 221143844 steps penalty 1 = 1 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 31 variables 1% in round 1 in 643087 steps
c [elim-17-1] backward subsumption/strengthening limit 643000
c [elim-17-1-1] backward checking 197 touched variables 9%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 0 and strengthened 0 clauses in 18891 steps
c [elim-17] fully completed in 1 rounds
c [elim-17] transition to [ all 0 rem 0 ] state
c [elim-17] eliminated 31 = 1% variables out of 2241 scheduled
c [bca-15] limit of 10000000 steps and 23086 added (scaled 2)
c [bca-15] 2325 out of 4422 literals actually usable 53%
c [bca-15] added 16 blocked clauses in 51408 steps
c [score-distribution-19] 1445 pos 65.38%, 558 min 25.25%, 207 zero 9.37%
c [score-distribution-19] 940 different 42.53% out of total 2210 variables
c [simplification-19] removed 40 variables 1.8% (2210 remain 2%)
c [simplification-19] removed 368 irredundant clauses 3.2% (11261 remain 2%)
c [simplification-19] maximum reduction of 3% = max (2%, 3%)
c [simplification-19] geometric conflict interval increment 26250 = 105000 / 4
c [simplification-19] new conflict interval 131250
c [simplification-19] penalized conflict interval 131250 = 1 * 131250
c [simplification-19] hard conflict limit 508844 (soft 443219 + delta 65625)
c [simplification-19] new conflict limit 443219 (hard 508844)
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   95.8    2209    11261    324235   57066    699 10271   34    48   32  70%    183    6   19   29   66%
c -   97.0    2208    11261    329616   29358    702 10271   26    34   20  76%   -354   -7   24   29   84%
c -  103.9    2208    11261    368050   31424    712 10274   22    29   21  77%    256   -9   25   27   91%
c -  112.0    2208    11261    404430   30841    741 10279   31    43   20  71%    583    4   40   28  142%
c i  113.8    2207    11261    414403   39330    771 10283   20    27   25  74%    645  -12   11   28   38%
c i  114.3    2174    11261    418307   42621    782 10290   15    20   25  74%   -650  -19    8   27   31%
c -  119.9    2153    11261    445745   32890    793 10294   24    31   31  77%   -139   -5   24   27   90%
c 
c [simplification-20] limit 443219 conflicts (hard 508844) hit after 459017 conflicts
c [quatres-14] found 1434 quaternary clauses 31% in total
c [quatres-14-1] removed 13 duplicate quaternary clauses
c [quatres-14-1] added 1 double-self-subsuming ternary resolvents
c [quatres-14-2] added 3 single-self-subsuming ternary resolvents
c [quatres-14-2] added 4 quaternary resolvents
c [ternres-16] limit 32937616 with penalty 0 = 0 + 0
c [ternres-16] all 2153 free variables schedulable
c [ternres-16] 7 ternary resolvents (0 bin, 7 trn)
c [ternres-16] fully completed ternary resolution
c [decomp-56] removed 64 variables
c [treelook-7] limit 1646880 penalty 1 = 1 + 0 boost 1
c [treelook-7] scheduled 4292 literals 100%
c [treelook-7] scheduling used 148353 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 1646880 penalty 1 = 1 + 0 boost 1
c [treelook-7] used 1647385 steps
c [treelook-7] 3900 literals remain 92%
c [treelook-7] 2126 variables remain to probed next time 100%
c [decomp-57] removed 1 variables
c [treelook-7] removed 21 variables, found 10555 hbrs
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 988 transitive binary clauses
c [transred-16] found 4 units
c [cce-14] limit of 164688081 steps penalty 0 = 0 + 0
c [cce-14-1] eliminated 1 clauses out of 68 (1%) of length 6
c [cce-14-1] eliminated 11 clauses out of 245 (4%) of length 5
c [cce-14-1] eliminated 33 clauses out of 725 (5%) of length 4
c [cce-14-1] completed large round (ATE)
c [cce-14-1] eliminated 45 large clauses in 1465593 steps
c [cce-14-1] allowing another 732796 steps for small clauses
c [cce-14-1] scheduling 7870 clauses = 6688 binary + 1182 ternary
c [cce-14-1] tried to eliminate 7870 small clauses 100%
c [cce-14-1] eliminated 168 binary clauses 3%
c [cce-14-1] eliminated 24 ternary clauses 2%
c [cce-14-1] eliminated 192 small clauses 2%
c [cce-14-1] eliminated 218 small clauses in 14000586 steps
c [cce-14-1] completed small round (ATE)
c [cce-14-1] eliminated 263 covered clauses in round 1
c [cce-14-2] completed large round (ATE)
c [cce-14-2] allowing another 701308 steps for small clauses
c [cce-14-2] scheduling 7678 clauses = 6520 binary + 1158 ternary
c [cce-14-2] tried to eliminate 7678 small clauses 100%
c [cce-14-2] completed small round (ATE)
c [cce-14-2] eliminated 0 covered clauses in round 2
c [cce-14] eliminated 263 covered clauses in TOTAL during 2 rounds
c [elim-18] scheduling all variables this time
c [elim-18] scheduled 2121 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 13175046540 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 82 variables 4% in round 1 in 588520 steps
c [elim-18-1] backward subsumption/strengthening limit 588500
c [elim-18-1-1] backward checking 428 touched variables 20%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 1 and strengthened 1 clauses in 37985 steps
c [elim-18-1] rescheduled 9 variables 0% by backward subsumption
c [elim-18-2] eliminated 1 variables 0% in round 2 in 3714 steps
c [elim-18-2] backward subsumption/strengthening limit 3700
c [elim-18-2-1] backward checking 8 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 0 and strengthened 0 clauses in 2985 steps
c [elim-18] fully completed in 2 rounds
c [elim-18] transition to [ all 0 rem 0 ] state
c [elim-18] eliminated 83 = 4% variables out of 2121 scheduled
c [bca-16] limit of 10000000 steps and 21076 added (scaled 2)
c [bca-16] 2235 out of 4078 literals actually usable 55%
c [bca-16] added 13 blocked clauses in 36719 steps
c [score-distribution-20] 1254 pos 61.53%, 643 min 31.55%, 141 zero 6.92%
c [score-distribution-20] 832 different 40.82% out of total 2038 variables
c [simplification-20] removed 115 variables 5.3% (2038 remain 2%)
c [simplification-20] removed 1009 irredundant clauses 9.0% (10252 remain 2%)
c [simplification-20] maximum reduction of 9% = max (5%, 9%)
c [simplification-20] large reduction 9% >= 5% limit
c [simplification-20] next conflict interval 4590 = min (459017/100, 131250)
c [simplification-20] penalized conflict interval 4590 = 1 * 4590
c [simplification-20] hard conflict limit 473607 (soft 463607 + delta 10000)
c [simplification-20] new conflict limit 463607 (hard 473607)
c 
c [simplification-21] limit 463607 conflicts (hard 473607) hit after 467822 conflicts
c [quatres-15] found 1799 quaternary clauses 30% in total
c [quatres-15-1] removed 5 duplicate quaternary clauses
c [quatres-15-2] added 4 single-self-subsuming ternary resolvents
c [quatres-15-2] added 4 quaternary resolvents
c [ternres-17] limit 33438308 with penalty 0 = 0 + 0
c [ternres-17] all 2038 free variables schedulable
c [ternres-17] 10 ternary resolvents (0 bin, 10 trn)
c [ternres-17] fully completed ternary resolution
c [card-6] limit 1044947 penalty 4 = 4 + 0
c [card-6] found 1037 at-most-one constraints of average size 3.6
c [card-6] found 13 at-most-two constraints of average size 4.1
c [card-6] using previous limit 1044947 for elimination
c [card-6] 1049 out of 1050 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] generated 1433 at-most-one constraints, 1243 used 87%
c [card-6] exported 10062 binary clauses, 8.1 per/constraint
c [gauss-7] limit 417978 penalty 4 = 4 + 0
c [gauss-7] extracted 4 xors of average arity 3.0
c [gauss-7] connected 12 occurrences of 6 variables (average 2.0)
c [gauss-7] limit 417978 penalty 4 = 4 + 0
c [gauss-7] fully completed
c [gauss-7] exported 0 unary, 0 binary and 0 ternary equations
c [basicprobe-7] limit 167191541 penalty 0 = 0 + 0
c [basicprobe-7-0] 148 sched 7%, 8 failed, 0 lifted, 372 hbrs
c [decomp-59] removed 11 variables
c [basicprobe-7-1] 649 sched 33%, 38 failed, 3 lifted, 896 hbrs
c [decomp-60] removed 51 variables
c [basicprobe-7-2] 614 sched 31%, 5 failed, 0 lifted, 716 hbrs
c [decomp-61] removed 6 variables
c [basicprobe-7-3] 603 sched 31%, 1 failed, 0 lifted, 81 hbrs
c [decomp-62] removed 1 variables
c [basicprobe-7-4] 603 sched 31%, 0 failed, 0 lifted, 37 hbrs
c [basicprobe-7-5] 603 sched 31%, 0 failed, 0 lifted, 17 hbrs
c [basicprobe-7-6] 603 sched 31%, 0 failed, 0 lifted, 3 hbrs
c [basicprobe-7-7] 603 sched 31%, 0 failed, 0 lifted, 5 hbrs
c [basicprobe-7-8] 603 sched 31%, 0 failed, 0 lifted, 0 hbrs
c [basicprobe-7-8] round limit 8 hit
c [basicprobe-7-8] 55 units = 52 failed (95%) + 3 lifted (5%)
c [basicprobe-7-8] removed 69 variables, found 2127 hbrs
c [bate-5] eliminated 25 asymmetric tautologies during probing
c [unhide-17] limit 3343830 with penalty 1 = 1 + 0
c [unhide-17-28] 0 units, 0 failed, 9153 tauts, 0 hbrs, 66746 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 594 transitive binary clauses
c [cce-15] limit of 167191541 steps penalty 0 = 0 + 0
c [cce-15-1] eliminated 2 clauses out of 78 (3%) of length 6
c [cce-15-1] eliminated 4 clauses out of 228 (2%) of length 5
c [cce-15-1] eliminated 13 clauses out of 677 (2%) of length 4
c [cce-15-1] completed large round (ACCE)
c [cce-15-1] eliminated 19 large clauses in 1462787 steps
c [cce-15-1] allowing another 731393 steps for small clauses
c [cce-15-1] scheduling 7662 clauses = 6234 binary + 1428 ternary
c [cce-15-1] tried to eliminate 7662 small clauses 100%
c [cce-15-1] eliminated 116 binary clauses 2%
c [cce-15-1] eliminated 106 ternary clauses 7%
c [cce-15-1] eliminated 222 small clauses 3%
c [cce-15-1] eliminated 222 small clauses in 13021368 steps
c [cce-15-1] completed small round (ACCE)
c [cce-15-1] eliminated 241 covered clauses in round 1
c [cce-15-2] eliminated 1 clauses out of 76 (1%) of length 6
c [cce-15-2] eliminated 3 clauses out of 224 (1%) of length 5
c [cce-15-2] eliminated 2 clauses out of 664 (0%) of length 4
c [cce-15-2] completed large round (ACCE)
c [cce-15-2] eliminated 6 large clauses in 1411503 steps
c [cce-15-2] allowing another 705751 steps for small clauses
c [cce-15-2] scheduling 7440 clauses = 6118 binary + 1322 ternary
c [cce-15-2] tried to eliminate 7440 small clauses 100%
c [cce-15-2] eliminated 15 binary clauses 0%
c [cce-15-2] eliminated 15 ternary clauses 1%
c [cce-15-2] eliminated 30 small clauses 0%
c [cce-15-2] eliminated 30 small clauses in 12432594 steps
c [cce-15-2] completed small round (ACCE)
c [cce-15-2] eliminated 36 covered clauses in round 2
c [cce-15-3] eliminated 1 clauses out of 75 (1%) of length 6
c [cce-15-3] completed large round (ACCE)
c [cce-15-3] eliminated 1 large clauses in 1400456 steps
c [cce-15-3] allowing another 700228 steps for small clauses
c [cce-15-3] scheduling 7410 clauses = 6103 binary + 1307 ternary
c [cce-15-3] tried to eliminate 7410 small clauses 100%
c [cce-15-3] eliminated 1 binary clauses 0%
c [cce-15-3] eliminated 1 small clauses 0%
c [cce-15-3] eliminated 1 small clauses in 12366531 steps
c [cce-15-3] completed small round (ACCE)
c [cce-15-3] eliminated 2 covered clauses in round 3
c [cce-15] eliminated 279 covered clauses in TOTAL during 3 rounds
c [elim-19] scheduling all variables this time
c [elim-19] scheduled 1969 variables 100%
c [elim-19] limit of 668766167 steps penalty 0 = 0 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 79 variables 4% in round 1 in 544295 steps
c [elim-19-1] backward subsumption/strengthening limit 544200
c [elim-19-1-1] backward checking 442 touched variables 22%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 0 and strengthened 3 clauses in 38196 steps
c [elim-19-1] rescheduled 12 variables 1% by backward subsumption
c [elim-19-2] no variable eliminated in round 2 in 3298 steps
c [elim-19] fully completed in 2 rounds
c [elim-19] transition to [ all 0 rem 0 ] state
c [elim-19] eliminated 79 = 4% variables out of 1969 scheduled
c [bca-17] limit of 10000000 steps and 19463 added (scaled 2)
c [bca-17] 2021 out of 3782 literals actually usable 53%
c [bca-17] added 20 blocked clauses in 43378 steps
c [score-distribution-21] 1165 pos 61.64%, 619 min 32.75%, 106 zero 5.61%
c [score-distribution-21] 818 different 43.28% out of total 1890 variables
c [simplification-21] removed 148 variables 7.3% (1890 remain 1%)
c [simplification-21] removed 810 irredundant clauses 7.9% (9442 remain 2%)
c [simplification-21] maximum reduction of 8% = max (7%, 8%)
c [simplification-21] large reduction 8% >= 5% limit
c [simplification-21] next conflict interval 4678 = min (467822/100, 131250)
c [simplification-21] penalized conflict interval 4678 = 1 * 4678
c [simplification-21] hard conflict limit 482500 (soft 472500 + delta 10000)
c [simplification-21] new conflict limit 472500 (hard 482500)
c 
c [simplification-22] limit 472500 conflicts (hard 482500) hit after 472500 conflicts
c [quatres-16] found 1720 quaternary clauses 30% in total
c [quatres-16-1] removed 12 duplicate quaternary clauses
c [quatres-16-2] added 2 quaternary resolvents
c [ternres-18] limit 33765479 with penalty 0 = 0 + 0
c [ternres-18] all 1890 free variables schedulable
c [ternres-18] 4 ternary resolvents (0 bin, 4 trn)
c [ternres-18] fully completed ternary resolution
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 428 transitive binary clauses
c [cce-16] limit of 168827397 steps penalty 0 = 0 + 0
c [cce-16-1] eliminated 5 clauses out of 27 (19%) of length 7
c [cce-16-1] eliminated 8 clauses out of 703 (1%) of length 4
c [cce-16-1] completed large round (ATE)
c [cce-16-1] eliminated 13 large clauses in 1558134 steps
c [cce-16-1] allowing another 779067 steps for small clauses
c [cce-16-1] scheduling 7042 clauses = 5946 binary + 1096 ternary
c [cce-16-1] tried to eliminate 7042 small clauses 100%
c [cce-16-1] eliminated 14 binary clauses 0%
c [cce-16-1] eliminated 10 ternary clauses 1%
c [cce-16-1] eliminated 24 small clauses 0%
c [cce-16-1] eliminated 24 small clauses in 12331142 steps
c [cce-16-1] completed small round (ATE)
c [cce-16-1] eliminated 37 covered clauses in round 1
c [cce-16-2] completed large round (ATE)
c [cce-16-2] allowing another 774442 steps for small clauses
c [cce-16-2] scheduling 7018 clauses = 5932 binary + 1086 ternary
c [cce-16-2] tried to eliminate 7018 small clauses 100%
c [cce-16-2] completed small round (ATE)
c [cce-16-2] eliminated 0 covered clauses in round 2
c [cce-16] eliminated 37 covered clauses in TOTAL during 2 rounds
c [cce-16] 37 < 1/100 * 9436 = 94 considered unsuccessful
c [elim-20] scheduling all variables this time
c [elim-20] scheduled 1890 variables 100%
c [elim-20] limit of 675309588 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 5 variables 0% in round 1 in 535352 steps
c [elim-20-1] backward subsumption/strengthening limit 535300
c [elim-20-1-1] backward checking 78 touched variables 4%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 0 and strengthened 0 clauses in 8357 steps
c [elim-20] fully completed in 1 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 5 = 0% variables out of 1890 scheduled
c [elim-20] 5 < 1/100 * 1890 = 18 considered unsuccessful
c [bca-18] limit of 10000000 steps and 19375 added (scaled 2)
c [bca-18] 1980 out of 3772 literals actually usable 52%
c [bca-18] added 3 blocked clauses in 47492 steps
c [sweep-12] limit 1266205 penalty 3 = 3 + 0
c [sweep-12-1] 124 pos 16.9% + 610 neg 83.1% = 734 sched 38.9% ret 1151
c [sweep-12-1] 1532583 steps 31 queries 58.90 avg class size
c [sweep-12-1] 865 decisions 30 SAT calls 107.43 avg env size
c [sweep-12-1] 493 variables remain 26% (1392 retained 74%)
c [sweep-12-1] removed 0 vars (0 failed, 0 eqs, 0 impls)
c [sweep-12] removed 0 vars in TOTAL (1 rounds, 30 queries)
c [score-distribution-22] 1167 pos 61.91%, 612 min 32.47%, 106 zero 5.62%
c [score-distribution-22] 846 different 44.88% out of total 1885 variables
c [simplification-22] removed 5 variables 0.3% (1885 remain 1%)
c [simplification-22] removed 49 irredundant clauses 0.5% (9393 remain 2%)
c [simplification-22] maximum reduction of 1% = max (0%, 1%)
c [simplification-22] geometric conflict interval increment 65625 = 131250 / 2
c [simplification-22] new conflict interval 196875
c [simplification-22] penalized conflict interval 196875 = 1 * 196875
c [simplification-22] hard conflict limit 767812 (soft 669375 + delta 98437)
c [simplification-22] new conflict limit 669375 (hard 767812)
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 -  136.8    1885     9393    499057   30625    879 15764   37    50   20  75%    509    9   46   30  152%
c i  144.7    1884     9393    540581   66399    902 15773   14    17   39  83%    750  -18   13   26   53%
c -  145.2    1884     9393    541949   34155    902 15773   23    29   21  77%   -635   -6   47   26  183%
c i  149.2    1883     9393    560968   51190    926 15777   35    48   29  74%   -598    8   20   30   67%
c -  154.2    1863     9393    581453   32918    939 15778   30    40   31  76%   -400   -1   35   30  115%
c i  154.6    1862     9393    583843   35051    942 15779   30    40   35  75%   -349   -1   30   30   98%
c -  164.1    1862     9393    624597   34070    957 15781   34    43   31  78%     92    0   22   32   70%
c -  173.3    1862     9393    667285   34777    975 15784   40    50   21  78%    538    7   49   33  147%
c 
c [simplification-23] limit 669375 conflicts (hard 767812) hit after 669379 conflicts
c [quatres-17] found 1850 quaternary clauses 27% in total
c [quatres-17-2] added 2 single-self-subsuming ternary resolvents
c [ternres-19] limit 49453125 with penalty 0 = 0 + 0
c [ternres-19] all 1862 free variables schedulable
c [ternres-19] 3 ternary resolvents (0 bin, 3 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-69] removed 23 variables
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 362 transitive binary clauses
c [bca-19] limit of 10000000 steps and 19008 added (scaled 2)
c [bca-19] 1957 out of 3726 literals actually usable 53%
c [bca-19] added 6 blocked clauses in 40787 steps
c [score-distribution-23] 1130 pos 60.69%, 642 min 34.48%, 90 zero 4.83%
c [score-distribution-23] 765 different 41.08% out of total 1862 variables
c [simplification-23] removed 0 variables 0.0% (1862 remain 1%)
c [simplification-23] removed 184 irredundant clauses 2.0% (9209 remain 1%)
c [simplification-23] maximum reduction of 2% = max (0%, 2%)
c [simplification-23] geometric conflict interval increment 65625 = 196875 / 3
c [simplification-23] new conflict interval 262500
c [simplification-23] penalized conflict interval 262500 = 1 * 262500
c [simplification-23] hard conflict limit 1063129 (soft 931879 + delta 131250)
c [simplification-23] new conflict limit 931879 (hard 1063129)
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  182.7    1861     9209    708247   68911    945 15272   21    26   31  81%    764  -15   10   31   31%
c -  184.1    1813     9209    712544   35995    949 15272   37    46   19  81%  -1039    4   43   32  132%
c -  194.1    1813     9209    756042   37236    962 15275   22    27   29  80%    -54  -14   16   31   53%
c -  204.9    1813     9209    802254   37479    987 15281   36    46   28  80%    492    6   26   31   83%
c i  209.1    1812     9209    824799   56282   1001 15284   19    23   38  83%    647  -14   11   29   38%
c i  210.1    1811     9209    828660   59541   1013 15293   34    42   38  80%  -1033    4   33   30  109%
c -  215.8    1811     9209    848893   38474   1016 15293   38    45   15  83%   -563    6   49   31  156%
c i  216.7    1810     9209    853963   42500   1029 15298   22    27   19  83%   -445  -12   10   30   34%
c i  223.5    1809     9209    882223   63997   1055 15315   19    22   30  85%   -191  -15    9   29   30%
c i  223.5    1123     9209    882262   64025   1055 15315   19    22   30  85%   -207  -15    8   29   28%
c i  223.5    1119     9209    882452   64152   1067 15316   18    22   30  85%   -276  -15    9   29   33%
c i  223.5    1116     9209    882561   64211   1068 15318   18    21   30  85%   -309  -15    9   29   31%
c i  223.6    1104     9209    882660   64277   1073 15322   18    21   30  85%   -337  -15    8   29   27%
c i  223.6    1100     9209    882873   64383   1085 15324   17    20   30  85%   -388  -16    8   29   26%
c i  223.6    1045     9209    882884   64380   1087 15327   17    20   30  85%   -390  -16    7   29   25%
c i  223.6     996     9209    882885   64380   1087 15327   17    20   30  85%   -390  -16    7   29   25%
c i  223.6     995     9209    882919   64405   1088 15328   17    20   30  85%   -398  -16    7   29   25%
c i  223.6     739     9209    882920   64405   1088 15328   17    20   30  85%   -398  -16    7   29   25%
c i  223.6     534     9209    882922   64404   1089 15328   17    20   30  85%   -398  -16    7   29   25%
c i  223.6     413     9209    882923   64404   1089 15328   17    20   30  85%   -398  -16    7   29   25%
c 0  223.6     371     9209    882923   64404   1089 15328   17    20   30  85%   -399  -16    7   29   25%
c 
c  seconds         irredundant          redundant clauses       height      sat         jl' fast slow fast/
c          variables clauses conflicts large ternary binary glue        MB         it"      glue glue  slow
c 
s UNSATISFIABLE
c
c bate: 223 basic ate = 200 trn 90% + 23 lrg 10% in 5 updates
c bcas: 19 count, 187 added (27 skipped), 538842 steps
c bkwd: tried 172514 clauses, 344531 lits, 2.00 lits/clause
c bkwd: checked 3759369 occs, 21.79 occs/clause, 10.91 occs/lit
c bkwd: subsumed 100 binary, 137 ternary, 136 large
c bkwd: strengthened 20 binary, 3 ternary (100% self), 435 large (0% self)
c blkd: 5 bces, 748 removed, 381630 resolutions, 1036742 steps
c blkd: 1709 blocking literals 1%, 20 pure
c bump: 882902 bumped seen, 109103516 lits 123.6 on average
c card: 6 count, 0 units, 12235 am1, 14331398 steps
c card: 62 rescheduled, 584 eliminated, 7031 resolved, 69098 subsumed
c card: 19723 at-most-one constraints found, average size 4.41
c card: 19723 at-most-one constraints used 100%, average size 4.41
c card: 13 at-most-two constraints found, average size 4.08
c card: 12 at-most-two constraints used 92%, average size 4.08
c cces: 16 cces, 14006 eliminated, 12878 ate 92%, 1128 abce 8%
c cces: 0 probed, 0 lifted, 0 failed
c cces: 0 cached, 0 rsz, 0 cols 0%, 0 srch, 0 hits 0%
c clls: 1 sat, 0 simp, 0 freeze, 0 melt
c clls: 2059333 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 179 gcs, 0 rescored clauses, 464 rescored vars
c dcps: 69 decompositions, 41710 equivalent 29%
c deco: 905 decision-only clauses 0%, 48% reduction
c decs: 2603469 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c dsch: 5644001 push, 5502571 pop (5502571 dec 100%)
c dsch: 123247747 swaps, 0 down, 72814558 up
c elms: 20 elims, 13566 eliminated 10%, 48 pure 0%
c elms: 58 rounds, 2.9 rounds/bve
c elms: 12895 small 95%, 603 large 4%
c elms: 43137 tried small, 12897 succeeded 30%, 30240 failed 70%
c elms: 3833 subsumed, 5622 strengthened, 256 blocked
c elms: 2418865 copies, 2202309 resolutions, 1324293 ipos
c elms: 406792 subchks, 294519 strchks
c gaus: 7 extractions, 1124 extracted, 2.3 size, 4 max
c gaus: exported 2 units, 5 binary and 3 ternary equations
c gaus: 0 gc, 9972236 steps, 4986118 extr 50%, 34644 elim 0%
c glue: 29.6 orig avg, 29.6 real avg, 5.1 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 98128 = 15235 simple 16% + 70901 trn 72% + 11992 lrg 12%, 973 sub 1%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 882902 clauses, 59.0 length
c lrnd: 52130315 lits = 77158852 orig - 25028537 removed 32%
c lrnd: 298406 uips 34%, 534406 flips 61%
c mins: 877186 mins 99%, 217 bin 0%, 4551 size 1%
c mins: 85609535 poisoned searches, 16314525 hits, 19% hit rate
c mins: 145223051 used twice searches, 20561815 hits, 14% hit rate
c move: moved 13004, 9738 bin 75%, 3266 trn 25%
c otfs: 2049 driving 27%, 5628 restarting 73%
c otfs: str 7677, 7656 red 100%, 21 irr 0%
c otfs: str 7677, 0 bin 0%, 21 trn 0%, 7656 lrg 100%
c otfs: sub 40, 40 red 100%, 0 irr 0%
c otfs: sub 40, 0 bin 0%, 0 trn 0%, 40 lrg 100%
c phas: 2 computed, 14149 set, 0 pos (0%), 14149 neg (100%)
c prbs: 7 basic, 22667 probed, 640 failed, 53 lifted
c prbs: 7 simple, 185518 probed, 1245 failed, 18460 eqs
c prbs: 7 treelook, 555 probed, 40 failed, 0 lifted
c prom: 171376 locked 9% out of 1893994 tried
c prps: 245752664 props, 91 props/dec
c prps: 97% srch, 3% simp, 0% lkhd
c quat: 17 count, 71 quat, 19 self1, 1 self2, 43 dup
c redc: 4761 clauses 18%, 26900 tried 3%, 9 sat 0%
c redc: 12965 lits 4%, 315181 tried 0%, 9 sat 0%
c redc: 726 times jump level reduced, 6.0 levels on average
c reds: 20 count, 44146.2 conflicts per reduce
c reds: 0 memlim 0%, 20 arith 100%
c reds: 595110 collected 88%, 79354 retired 12%
c rmbd: 3673 removed, 857 red 23%
c rsts: 18998 restarts 100%, 21 skipped 0%
c rsts: 21 saturating 100%, 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: 23 count, 22 confs 96%, 0 vars 0%
c simp: 1 its 4%, 0 bin 0%, 0 trns 0%
c subl: 882902 count (777327 tried 0.9), 105181 sub out of 881234 (11.9%)
c swps: 12 count, 15 rounds, 1606 queries (107.1/round)
c swps: 1538 sat calls, 34 unsat (1.3% success rate)
c swps: 21465 decisions 14.0, 2028 conflicts 1.3
c swps; 45.7 avg class size, 59.1 avg environment size
c swps: 0 failed, 111 impls, 94 equivs
c swp0: 531 type 0 queries, 223 unsat (42.0%), 506 sat (95.3%)
c swp1: 1075 type 1 queries, 544 unsat (50.6%), 1006 sat (93.6%)
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: 6974291 calls to obtain time
c tops: 86213 fixed 61%, 158 its, 5588.12 confs/it
c trds: 19 transitive reductions, 8356 removed, 72 failed
c trds: 56316 nodes, 160722 edges, 27941998 steps
c trim: 1147885 words, 4.4 MB
c trnr: 19 count, 1 bin, 591 trn, 12729692 steps
c unhd: 17 count, 28 rounds, 11357134 steps
c unhd: 206 non-trivial sccs of average size 2.2
c unhd: 25 units, 24 bin, 1 trn, 0 lrg
c unhd: 1741 failed, 1733 stamp, 0 lits, 7 bin, 1 trn, 0 lrg
c unhd: 38984 tauts, 3130 bin 8%, 1051 trn 3%, 1311 lrg 3%
c unhd: 38984 tauts, 33492 stamp 86%, 28694 red 74%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 219186 str, 24 bin 0%, 492 trn 0%, 218670 lrg 100%, 216752 red 99%
c vars: 371 remaining 0% and 141489 removed 100% out of 141860
c vars: 86213 fixed 61%, 13566 eliminated 10%, 41710 equivalent 29%
c vsts: 6898309766 visits, 99% srch, 1% simp, 0% lkhd
c vsts: 28.7 search visits per propagation, 7707.2 per conflict
c wchs: 3110083666 pushed, 7957821 enlarged, 276 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         881305        595110         79354      27429467       7190536        433595
c 
c  0 0         15062   2      2359   0         0   0   7954529  29   1386563  19     35267   8     0.4
c  1 5          9733   1      4912   1      1291   2   2249411   8    488296   7     16886   4     0.2
c  2 6         41102   5     25015   4      3970   5   3792051  14<   954694  13     44410  10     0.9
c  3 9        102315  12     67605  11      8684  11   5207745  19   1464770  20<    81126  19     2.5
c  4 14       162173  18    113537  19     10908  14   3377858  12   1126115  16     82817  19<    4.1
c  5 21       191775  22<   138099  23<    12735  16   2317381   8    815843  11     71178  16     3.9
c  6 30       155545  18    110092  18     12908  16<  1276365   5    533483   7     51990  12     3.3
c  7 41       100912  11     69020  12     12463  16    661921   2    248592   3     29654   7     2.5
c  8 54        63124   7     41362   7      9454  12    402672   1    110926   2     13277   3     2.1
c  9 69        30529   3     18927   3      5238   7    141688   1     42688   1      5324   1     1.4
c 10 86         8110   1      4110   1      1617   2     43625   0     17031   0      1440   0     0.9
c 11 126         907   0        72   0        86   0      4196   0      1524   0       226   0     0.3
c 12 230          18   0         0   0         0   0        25   0        11   0         0   0     0.0
c 
c avg                  5.1           5.2           5.6           2.5           3.0           4.0
c std                  1.9           1.8           2.1           2.2           2.2           2.1
c 
c   14.719   7% cce
c    4.496   2% probe
c    4.122   2% unhide
c    3.322   1% bump
c    2.323   1% elim
c    1.970   1% decide
c    1.636   1% transred
c 
c    2.923 < 1% rest (below)
c 
c    1.501   1% sweep
c    0.373   0% bca
c    0.341   0% gauss
c    0.289   0% card
c    0.191   0% block
c    0.082   0% quatres
c    0.077   0% ternres
c    0.069   0% rescore
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    1.256   1% preprocessing     4%
c   30.296  14% inprocessing     96%
c ==================================
c   31.552  14% simplifying
c  192.067  86% search
c ==================================
c  223.622 100% all
c 
c        882923 conflicts,        3948.3 confs/sec
c           909 ternaries,         971.3 confs/ternary
c           394 binaries,         2240.9 confs/binary
c           158 iterations,       5588.1 confs/iteration
c 
c            20 reductions,          0.1 redus/sec,  44146.2 confs/reduction
c         18998 restarts,           85.0 rests/sec,     46.5 confs/restart
c       2603469 decisions,       11642.3 decis/sec,      2.9 decis/conflict
c     245752664 propagations,  1098963.6 props/sec,     94.4 props/decision
c 
c 223.6 seconds, 57.5 MB
c launch: done
