c launch: /data/cnf/sc2014/app/UTI-20-10p1.cnf.bz2
c host: atom03
c Lingeling SAT Solver
c 
c Version b7ztzu 7b29300825af9bcc1c8b2c5ebcf65fa1cb101cad
c 
c Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c All rights reserved.
c 
c released Sun Apr 26 19:26:13 CEST 2015
c compiled Sun Apr 26 19:26:13 CEST 2015
c 
c gcc (Ubuntu 4.8.2-19ubuntu1) 4.8.2
c -Wall -O3 -I../yalsat -I../druplig -DNLGLOG -DNDEBUG -DNCHKSOL
c Linux cluster2 3.13.0-45-generic x86_64
c 
c piping '/data/cnf/sc2014/app/UTI-20-10p1.cnf.bz2' through 'bzcat'
c reading input file /data/cnf/sc2014/app/UTI-20-10p1.cnf.bz2
c no embedded options
c found 'p cnf 260342 1391257' header
c read 260342 variables, 1391257 clauses, 3358569 literals in 0.00 seconds
c
c --abstime=0
c --bate=1
c --batewait=2
c --bca=1
c --bcaddlimldscale=2
c --bcamaxeff=10000000
c --bcaminuse=100
c --bcawait=2
c --bkwdscale=100
c --bkwdroundlim=7
c --bkwdresched=1
c --blkboost=10
c --blkboostvlim=10000000
c --blkclslim=1000000
c --blklarge=1
c --blkmaxeff=800000000
c --blkmineff=50000000
c --blkocclim1=100000
c --blkocclim=1000000
c --blkocclim2=10000
c --blkreleff=100
c --blkresched=1
c --blkrtc=0
c --blksmall=1
c --blksuccessmaxwortc=6
c --blksuccessrat=100
c --block=1
c --blockwait=1
c --boost=1
c --bumpsimp=1
c --card=1
c --cardcut=2
c --cardexpam1=3
c --cardglue=0
c --cardignused=0
c --cardmaxeff=300000000
c --cardmaxlen=1000
c --cardmineff=2000000
c --cardminlen=3
c --cardocclim1=300
c --cardocclim2=15
c --cardreleff=5
c --cardreschedint=10
c --carduse=2
c --cardwait=0
c --cce2wait=1
c --cce=3
c --cceateint=2
c --cceboost=10
c --cceboostdel=3
c --cceboostint=5
c --cceboostvlim=10000000
c --cce3wait=2
c --ccemaxround=3
c --ccemaxeff=2147483647
c --ccemineff=30000000
c --ccereleff=50
c --ccertc=0
c --ccertcint=15
c --ccertcintvlim=2000000
c --ccesuccessrat=100
c --ccewait=2
c --clim=-1
c --compact=0
c --deco=1
c --decolim=100
c --deco1opt=1
c --decompose=1
c --defragfree=50
c --defragint=10000000
c --delmax=10
c --dlim=-1
c --druplig=0
c --drupligcheck=0
c --drupligtrace=0
c --drupligtraceorig=0
c --elim=1
c --elmaxeff=800000000
c --elmblk=1
c --elmblkwait=1
c --elmboost=20
c --elmboostdel=3
c --elmboostint=5
c --elmboostvlim=4000000
c --elmclslim=1000000
c --elmfull=0
c --elmineff=20000000
c --elmlitslim=200
c --elmocclim1=1000
c --elmocclim=1000000
c --elmocclim2=100
c --elmoccsumforced=0
c --elmreleff=200
c --elmresched=0
c --elmroundlim=3
c --elmrtc=0
c --elmrtcint=10
c --elmrtcintvlim=500000
c --elmsuccessmaxwortc=4
c --elmsuccessrat=100
c --exitonabort=0
c --factmax=100000
c --factor=3
c --gauss=1
c --gaussexptrn=1
c --gaussextrall=1
c --gaussmaxeff=50000000
c --gaussmaxor=20
c --gaussmineff=2000000
c --gaussreleff=2
c --gausswait=2
c --gluekeep=4
c --gluekeepsize=15
c --gluescale=4
c --hbrdom=2
c --import=1
c --incredcint=1
c --incredconfslim=0
c --incsavevisits=0
c --inprocessing=1
c --irrlim=1
c --jwhred=1
c --keepmaxglue=1
c --keepmaxglueint=100
c --lhbr=1
c --lkhd=2
c --locs=0
c --locsbanner=0
c --locsclim=1000000
c --locsboost=2
c --locscint=10000
c --locset=2
c --locsexport=1
c --locsmaxeff=100000
c --locsmineff=1000
c --locsred=0
c --locsreleff=5
c --locsrtc=0
c --locsvared=100
c --locswait=2
c --maxscaledglue=15
c --memlim=-1
c --minimize=2
c --minlocalgluelim=200
c --minlocalsizelim=3000
c --minrecgluelim=100
c --minrecsizelim=1000
c --norestartsatlimlo=85
c --move=2
c --otfs=1
c --penmax=4
c --phase=0
c --phaseluckfactor=200
c --phaselucklim=100
c --phaseluckmaxround=10
c --phasesave=1
c --plain=0
c --plim=-1
c --poison=1
c --prbasic=1
c --prbasicmaxeff=400000000
c --prbasicmineff=1000000
c --prbasicreleff=50
c --prbasicroundlim=8
c --prbasicrtc=0
c --prbrtc=0
c --prbsimple=2
c --prbsimpleboost=10
c --prbsimpleliftdepth=2
c --prbsimplemaxeff=200000000
c --prbsimplemineff=2000000
c --prbsimplereleff=40
c --prbsimplertc=0
c --probe=1
c --promote=1
c --promotegluelim=8
c --pure=1
c --quatres=1
c --quatreswait=2
c --queuesort=1
c --queuesortjwh=0
c --randec=0
c --randecint=1000
c --redcls=1
c --redclsglue=6
c --redclsmaxdec=5
c --redclsmaxdepth=10
c --redclsmaxlrg=10
c --redclsmaxprops=100
c --redclsatlimlo=0
c --redclsatlimhi=100
c --redclsize=30
c --redclstype=4
c --reducefixed=0
c --reduceinc=1000
c --reduceinit=50000
c --reduce=1
c --restart=4
c --restartglcint=10
c --restartglclim=115
c --restartinit=0
c --restartint=5
c --restartpen=1
c --retirenb=1
c --retireint=4
c --retiremin=1
c --reusetrail=0
c --rmincpen=4
c --rstinoutinc=110
c --satlimdelay=10000
c --scincinc=200
c --scincincsatlimhi=100
c --scincincdelta=10
c --scincincincint=100000
c --scincincmin=200
c --scincincmode=1
c --score=4
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 247193 free variables 0%
c [limits] no decision limit
c [limits] no conflict limit
c [limits] no propagation limit
c [limits] simplification not delayed since 'simpdelay' zero
c [set-maximum-score] maximum score limit 1.000000d+500
c [set-minimum-score] minimum score limit 1.000000d-500
c [score-type] VSIDS (--score=4) decay interval 256 (--vsidsdint=256)
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  247193  1377238         0       0      0     0    0     0   58   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 6497 at-most-one constraints of average size 5.7
c [card-1] no at-most-two constraint found
c [card-1] using previous limit 2000000 for elimination
c [card-1] 6497 out of 6497 constraints (100%) meet size limits
c [card-1] no units found
c [card-1] no at-most-one constraints generated
c [decomp-1] removed 62800 variables
c [simpleprobe-1] all 197542 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 1569 variables
c [simpleprobe-1] 20928 variables remain 11% (175045 retained 89%)
c [simpleprobe-1] removed 1569 variables, found 21725 hbrs, 357 units
c [unhide-1] limit 65541 based on 1048664 irredundant clauses
c [unhide-1-1] 0 units, 4657 failed, 11362 tauts, 0 hbrs, 11424 literals
c [elim-1] scheduling all variables this time
c [elim-1] scheduled 194552 variables 100%
c [elim-1] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-1] rescheduling of touched variables disabled
c [elim-1] incomplete 60670 not tried 31% in round 1
c [elim-1] transition to [ all 1 rem 1 ] state
c [elim-1] eliminated 74772 = 38% variables out of 194552 scheduled
c [elim-1] considered successful since not run to completion yet
c [phase-count-1] 866695 negative 99.3% of 873213 except 6518 0.7%
c [phase-count-1] 702151 positive 80.4% of 873213 except 171062 19.6%
c [phase-count-1] less non-negative clauses 6518 than limit 87300 (10.0%)
c [phase-count-1] non-pos/non-neg = 171062/6518 = 26.24 >= 2.00 = 200/100
c [lucky-phase-1] forcing lucky phase -1
c [phase-1] phase bias: 0 positive 0%, 119780 negative 100%
c [sort-queue-1] sorted 119780 enqueued variables after 0 conflicts
c [score-dist-1] active 0 (0%), one 0 (0%), zero 119780 (100%)
c [score-dist-1] max exp 0, different 1 (100%)
c [score-dist-1] median active exp 0, avg 0.0
c [simplification-1] removed 83984 variables 41.2% (119780 remain 48%)
c [simplification-1] removed 504025 irredundant clauses 36.6% (873213 remain 63%)
c [simplification-1] maximum reduction of 41% = max (41%, 37%)
c [simplification-1] large reduction 41% >= 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    5.2  119779   873213        47      31      4 15337    0     6   58   5%      0    6    5    0 24081%
c i    5.4  119685   873213       140     104     16 15341    0    16   58   3%      0   16    6    0 18325%
c i    5.4  119513   873213       141     104     16 15341    0    16   58   3%      0   16    6    0 18254%
c i    5.5  119504   873213       151     106     17 15346    0    16   58   3%      0   16    6    0 17701%
c i    5.5  119496   873213       152     106     17 15346    0    16   58   3%      0   16    6    0 17632%
c i    5.5  119482   873213       191     138     18 15347    1    17   58   4%      0   17    7    0 16942%
c i    5.6  119476   873213       287     221     22 15349    1    20   58   5%      0   20   11    0 15831%
c i    5.6  119442   873213       303     233     25 15349    1    21   58   5%      0   21   11    0 15050%
c i    5.6  119430   873213       304     233     25 15349    1    21   58   5%      0   21   11    0 14991%
c i    6.0  119421   873213       430     333     34 15362    1    35   58   4%      0   35   11    0 12216%
c 
c [simplification-2] limit of 10 iterations hit after 10 iterations
c [decomp-3] removed 373 variables
c [simpleprobe-2] 19539 schedulable variables 16%
c [simpleprobe-2] limit 2000000 penalty 0 = 0 + 0
c [simpleprobe-2] 22768 variables remain 19% (96639 retained 81%)
c [simpleprobe-2] removed 0 variables, found 3975 hbrs, 0 units
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] scheduled 70696 literals 30%
c [treelook-1] scheduling used 300670 steps
c [treelook-1] not fully scheduled
c [treelook-1] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-1] used 413858 steps
c [treelook-1] 70677 literals remain 30%
c [treelook-1] 68102 variables remain to probed next time 57%
c [decomp-5] removed 2 variables
c [treelook-1] removed 14 variables, found 2347 hbrs
c [basicprobe-1] limit 6965896 based on 870737 irredundant clauses
c [basicprobe-1-0] 42879 probes remain 38% after last round
c [basicprobe-1-0] 39 units = 39 failed (100%) + 0 lifted (0%)
c [basicprobe-1-0] removed 7172 variables, found 18301 hbrs
c [unhide-2] limit 54421 based on 870737 irredundant clauses
c [unhide-2-2] 1 units, 2880 failed, 5034 tauts, 0 hbrs, 1525 literals
c [elim-2] 58007 variables 52% will be scheduled this time
c [elim-2] scheduled 58007 variables 52%
c [elim-2] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-2] rescheduling of touched variables disabled
c [elim-2] incomplete 23239 not tried 21% in round 1
c [elim-2] transition to [ all 0 rem 1 ] state
c [elim-2] eliminated 51 = 0% variables out of 58007 scheduled
c [elim-2] considered successful since not run to completion yet
c [phase-count-2] 786561 negative 99.2% of 793078 except 6517 0.8%
c [phase-count-2] 636714 positive 80.3% of 793078 except 156364 19.7%
c [phase-count-2] less non-negative clauses 6517 than limit 79300 (10.0%)
c [phase-count-2] non-pos/non-neg = 156364/6517 = 23.99 >= 2.00 = 200/100
c [lucky-phase-2] forcing lucky phase -1
c [phase-2] phase bias: 0 positive 0%, 5924 negative 100%
c [sort-queue-2] sorted 89834 enqueued variables after 430 conflicts
c [score-dist-2] active 20774 (19%), one 0 (0%), zero 89834 (81%)
c [score-dist-2] max exp 506, different 7 (1%)
c [score-dist-2] median active exp 503, avg 502.6
c [simplification-2] removed 8806 variables 7.4% (110608 remain 45%)
c [simplification-2] removed 80135 irredundant clauses 9.2% (793078 remain 58%)
c [simplification-2] maximum reduction of 9% = max (7%, 9%)
c [simplification-2] forced so keeping old conflict interval 0
c [simplification-2] conflict limit remains at 1031 (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    9.4  110607   793078       447     327     34 28486    1    38   53   4%      0   38   12    0 12124%
c i    9.5  110597   793078       464     342     34 28487    2    40   53   4%      0   39   12    0 11803%
c i    9.5  110587   793078       479     352     35 28490    2    41   53   4%      0   41   12    0 11494%
c i    9.8  110575   793078       580     422     52 28503    2    51   53   4%      0   51   13    0 10075%
c i    9.8  110565   793078       581     422     52 28503    2    51   53   4%      0   51   13    0 10036%
c i    9.8  110550   793078       582     422     52 28503    2    51   53   4%      0   51   13    0 9997%
c i   10.0  110540   793078       637     466     55 28510    2    59   53   3%      0   59   11    0 8586%
c i   10.1  110527   793078       664     489     55 28512    2    63   53   3%      0   62   11    0 8177%
c i   10.1  110516   793078       665     489     55 28512    2    63   53   3%      0   62   11    0 8145%
c i   10.1  110502   793078       666     489     55 28512    2    63   53   3%      0   62   11    0 8113%
c i   10.1  110490   793078       668     490     55 28512    2    63   53   3%      0   62   11    0 8097%
c i   10.1  110477   793078       669     490     55 28512    2    63   53   3%      0   62   11    0 8065%
c i   10.1  110466   793078       671     491     55 28512    2    63   53   3%      0   62   12    0 8313%
c i   10.1  110453   793078       673     492     55 28512    2    63   53   3%      0   62   12    0 8495%
c i   10.1  110445   793078       675     493     55 28512    2    63   53   3%      0   63   13    0 8722%
c i   10.1  110434   793078       677     494     55 28512    2    63   53   3%      0   63   13    0 8939%
c i   10.1  110425   793078       679     495     55 28512    2    63   53   4%      0   63   14    0 9145%
c i   10.1  110413   793078       682     497     55 28512    2    63   53   4%      0   63   14    0 9318%
c i   10.1  110401   793078       685     499     55 28512    2    63   53   4%      0   63   15    0 9562%
c i   10.1  110388   793078       687     500     55 28512    2    63   53   4%      0   63   15    0 9632%
c i   10.1  110375   793078       690     502     55 28512    2    63   53   4%      0   63   15    0 9757%
c i   10.1  110366   793078       692     503     55 28512    2    63   53   4%      0   63   16    0 9804%
c i   10.2  110353   793078       719     520     56 28520    2    64   53   4%      0   64   15    0 8991%
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   10.3  110216   793078       731     530     57 28520    2    65   53   4%      0   64   14    0 8702%
c i   10.3  110205   793078       738     535     57 28521    2    65   53   4%      0   65   14    0 8550%
c i   10.5  109692   793078       801     572     58 28540    3    70   53   4%      0   70   13    0 7709%
c i   10.9  109558   793078       960     707     66 28546    4    90   54   4%      0   89   27    0 9806%
c i   10.9  109548   793078       994     738     66 28546    5    94   54   5%      0   93   32    0 10389%
c i   11.2  109540   793078      1109     831     70 28558    6   109   54   6%      0  108   42    0 10198%
c i   11.2  109530   793078      1128     846     71 28560    6   111   54   6%      0  110   42    0 9813%
c i   11.2  109520   793078      1130     847     71 28560    6   111   54   6%      0  110   42    0 9751%
c 
c [simplification-3] limit 1136 conflicts (hard 11000) hit after 1136 conflicts
c [card-2] limit 1000000 penalty 1 = 1 + 0
c [card-2] found 3917 at-most-one constraints of average size 4.7
c [card-2] no at-most-two constraint found
c [card-2] using previous limit 1000000 for elimination
c [card-2] 3917 out of 3917 constraints (100%) meet size limits
c [card-2] no units found
c [card-2] no at-most-one constraints generated
c [decomp-6] removed 1333 variables
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] scheduled 66874 literals 31%
c [treelook-2] scheduling used 300633 steps
c [treelook-2] not fully scheduled
c [treelook-2] limit 300000 penalty 0 = 0 + 0 boost 1
c [treelook-2] used 345070 steps
c [treelook-2] 66867 literals remain 31%
c [treelook-2] 52002 variables remain to probed next time 48%
c [treelook-2] removed 0 variables, found 2433 hbrs
c [unhide-3] limit 87079 with penalty 1 = 0 + 1
c [unhide-3-3] 1 units, 2128 failed, 15147 tauts, 0 hbrs, 1365 literals
c [elim-3] scheduling all variables this time
c [elim-3] scheduled 107979 variables 100%
c [elim-3] limit of 20000000 steps penalty 0 = 0 + 0
c [elim-3] rescheduling of touched variables disabled
c [elim-3] incomplete 30869 not tried 29% in round 1
c [elim-3] transition to [ all 1 rem 1 ] state
c [elim-3] eliminated 3307 = 3% variables out of 107979 scheduled
c [elim-3] considered successful since not run to completion yet
c [phase-count-3] 746472 negative 99.1% of 752933 except 6461 0.9%
c [phase-count-3] 603746 positive 80.2% of 752933 except 149187 19.8%
c [phase-count-3] less non-negative clauses 6461 than limit 75200 (10.0%)
c [phase-count-3] non-pos/non-neg = 149187/6461 = 23.09 >= 2.00 = 200/100
c [lucky-phase-3] forcing lucky phase -1
c [phase-3] phase bias: 0 positive 0%, 1560 negative 100%
c [sort-queue-3] sorted 71500 enqueued variables after 1136 conflicts
c [score-dist-3] active 33172 (32%), one 0 (0%), zero 71500 (68%)
c [score-dist-3] max exp 507, different 11 (2%)
c [score-dist-3] median active exp 501, avg 501.1
c [simplification-3] removed 4836 variables 4.4% (104672 remain 42%)
c [simplification-3] removed 40145 irredundant clauses 5.1% (752933 remain 55%)
c [simplification-3] maximum reduction of 5% = max (4%, 5%)
c [simplification-3] large reduction 5% >= 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 13136 (soft 3136 + delta 10000)
c [simplification-3] new conflict limit 3136 (hard 13136)
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   14.1  104671   752933      1150     823     69 26840    6   113   52   6%      0  112   40    0 9186%
c i   14.4  104662   752933      1287     931     79 26848    7   141   52   5%      1  140   35    0 7109%
c i   14.5  104653   752933      1297     940     79 26848    7   142   52   5%      1  141   35    0 7077%
c i   14.5  104645   752933      1299     941     79 26848    7   142   52   5%      1  141   35    0 7025%
c i   14.6  104638   752933      1321     958     81 26850    7   146   52   5%      1  145   38    1 7333%
c i   14.6  104625   752933      1322     958     81 26850    7   146   52   5%      1  145   38    1 7305%
c i   14.8  104612   752933      1416    1036     86 26857    8   162   52   5%      1  161   39    1 6782%
c i   15.7  104611   752933      1676    1220    109 26899    9   201   52   4%      1  199   27    1 4029%
c i   15.7  104556   752933      1677    1220    109 26899    9   201   52   4%      1  199   27    1 4013%
c i   15.7  104342   752933      1687    1227    110 26900    9   202   52   4%      1  200   26    1 3899%
c i   15.9  104334   752933      1799    1297    121 26925    9   204   52   4%      1  201   21    1 3034%
c i   15.9  104240   752933      1803    1299    121 26926    9   204   52   4%      1  201   20    1 3000%
c i   15.9  104076   752933      1824    1315    123 26927    9   204   52   5%      1  201   21    1 2983%
c i   16.0  104044   752933      1858    1329    130 26935    9   203   52   5%      1  200   19    1 2750%
c 
c [simplification-4] limit of 212 binary hit after 212 binaries
c [decomp-8] removed 733 variables
c [basicprobe-2] limit 7372329 penalty 0 = 0 + 0
c [basicprobe-2-0] 38082 probes remain 37% after last round
c [basicprobe-2-0] 43 units = 43 failed (100%) + 0 lifted (0%)
c [basicprobe-2-0] removed 1992 variables, found 25319 hbrs
c [unhide-4] limit 147446 with penalty 1 = 0 + 1
c [unhide-4-4] 1 units, 1031 failed, 4052 tauts, 0 hbrs, 1373 literals
c [elim-4] 22768 variables 23% will be scheduled this time
c [elim-4] scheduled 22768 variables 23%
c [elim-4] boosting limit by 20
c [elim-4] limit of 589786360 steps penalty 0 = 0 + 0
c [elim-4] rescheduling of touched variables disabled
c [elim-4-1] no variable eliminated in round 1 in 46287977 steps
c [elim-4] fully completed in 1 rounds
c [elim-4] transition to [ all 0 rem 0 ] state
c [elim-4] eliminated 0 = 0% variables out of 22768 scheduled
c [phase-count-4] 715036 negative 99.1% of 721505 except 6469 0.9%
c [phase-count-4] 580185 positive 80.4% of 721505 except 141320 19.6%
c [phase-count-4] less non-negative clauses 6469 than limit 72100 (10.0%)
c [phase-count-4] non-pos/non-neg = 141320/6469 = 21.85 >= 2.00 = 200/100
c [lucky-phase-4] forcing lucky phase -1
c [phase-4] phase bias: 0 positive 0%, 745 negative 100%
c [sort-queue-4] sorted 60719 enqueued variables after 1883 conflicts
c [score-dist-4] active 40105 (40%), one 0 (0%), zero 60719 (60%)
c [score-dist-4] max exp 507, different 14 (3%)
c [score-dist-4] median active exp 500, avg 499.9
c [simplification-4] removed 3129 variables 3.0% (100824 remain 41%)
c [simplification-4] removed 31428 irredundant clauses 4.2% (721505 remain 52%)
c [simplification-4] maximum reduction of 4% = max (3%, 4%)
c [simplification-4] forced so keeping old conflict interval 0
c [simplification-4] conflict limit remains at 3165 (hard 13136)
c [simplification-4] new binary interval 1000
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.4  100823   721505      1910    1346    127 44928    9   201   51   5%      1  198   17    1 2441%
c i   18.5  100814   721505      1965    1379    139 44935    9   203   51   4%      1  199   15    1 2120%
c i   18.6  100813   721505      1977    1385    140 44937    9   203   51   4%      1  200   15    1 2158%
c i   18.6  100775   721505      2006    1402    146 44941    9   206   51   4%      1  202   15    1 2084%
c i   18.7  100736   721505      2038    1425    149 44944    9   208   51   4%      1  205   14    1 1972%
c i   18.8  100682   721505      2052    1435    151 44945    9   209   51   4%      1  206   14    1 1929%
c i   18.9  100241   721505      2136    1483    164 44961    9   210   51   4%      1  206   14    1 1892%
c i   19.2  100232   721505      2247    1566    179 44970    9   216   51   4%      1  212   16    1 2063%
c i   19.3  100226   721505      2264    1579    179 44973    9   217   51   4%      1  213   15    1 1990%
c i   19.3  100213   721505      2266    1579    179 44974    9   217   51   4%      1  213   15    1 1975%
c i   19.7  100204   721505      2425    1672    194 45012   10   218   51   4%      1  213   14    1 1730%
c i   19.8   99990   721505      2480    1716    199 45015   10   218   51   4%      1  213   16    1 1930%
c i   19.8   99980   721505      2481    1716    199 45015   10   218   51   4%      1  213   16    1 1923%
c i   20.0   99796   721505      2565    1782    200 45021   10   219   51   5%      1  214   23    1 2686%
c i   20.2   99787   721505      2655    1852    209 45030   10   223   51   5%      1  217   19    1 2139%
c i   20.2   99651   721505      2656    1852    209 45030   10   223   51   5%      1  217   19    1 2131%
c i   20.2   99617   721505      2668    1854    213 45034   10   223   51   5%      1  218   18    1 2041%
c i   20.5   99582   721505      2783    1943    218 45047   11   227   51   5%      1  221   21    1 2266%
c i   20.7   99446   721505      2863    1992    229 45064   11   230   51   5%      1  224   18    1 1889%
c i   21.5   99093   721505      3159    2254    237 45079   15   268   52   5%      1  261   59    1 4809%
c i   21.5   99085   721505      3161    2255    237 45079   15   268   52   5%      1  261   59    1 4776%
c i   21.5   99077   721505      3162    2255    237 45079   15   268   52   5%      1  261   58    1 4757%
c i   21.5   99068   721505      3163    2255    237 45079   15   268   52   5%      1  261   58    1 4739%
c 
c [simplification-5] limit 3215 conflicts (hard 13136) hit after 3215 conflicts
c [quatres-1] found 34043 quaternary clauses 34% in total
c [ternres-1] boosting ternary resolution limit by 5
c [ternres-1] limit 20000000 with penalty 0 = 0 + 0
c [ternres-1] all 99060 free variables schedulable
c [ternres-1] 12 ternary resolvents (1 bin, 11 trn)
c [ternres-1] fully completed ternary resolution
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] extracted 503 xors of average arity 2.1
c [gauss-1] connected 1075 occurrences of 452 variables (average 2.4)
c [gauss-1] limit 2000000 penalty 0 = 0 + 0
c [gauss-1] fully completed
c [gauss-1] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-9] removed 616 variables
c [unhide-5] limit 479689 with penalty 0 = 0 + 0
c [unhide-5-5] 0 units, 323 failed, 14089 tauts, 0 hbrs, 5345 literals
c [transred-1] limit 2000000 with penalty 0 = 0 + 0
c [transred-1] removed 159 transitive binary clauses
c [block-1] scheduling all variables this time
c [block-1] scheduled 97920 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 11333 blocked clauses
c [cce-1] limit of 30000000 steps penalty 0 = 0 + 0
c [cce-1-1] eliminated 10 clauses out of 418 (2%) of length 10
c [cce-1-1] eliminated 103 clauses out of 2169 (5%) of length 9
c [cce-1-1] eliminated 44 clauses out of 522 (8%) of length 8
c [cce-1-1] incomplete large round (ATE)
c [cce-1-1] eliminated 157 large clauses in 30000004 steps
c [cce-1-1] allowing another 15000002 steps for small clauses
c [cce-1-1] scheduling 345071 clauses = 325145 binary + 19926 ternary
c [cce-1-1] tried to eliminate 412 small clauses 0%
c [cce-1-1] eliminated 155 binary clauses 0%
c [cce-1-1] eliminated 14 ternary clauses 0%
c [cce-1-1] eliminated 169 small clauses 0%
c [cce-1-1] eliminated 169 small clauses in 30000009 steps
c [cce-1-1] incomplete small round (ATE)
c [cce-1-1] eliminated 326 covered clauses in round 1
c [cce-1] eliminated 326 covered clauses in TOTAL during 1 rounds
c [cce-1] 326 < 1/100 * 673969 = 6739 considered unsuccessful
c [bca-1] limit of 10000000 steps and 1347786 added (scaled 2)
c [bca-1] 175952 out of 195842 literals actually usable 90%
c [bca-1] added 189 blocked clauses in 518197 steps
c [sweep-1] limit 1347286 based on 673643 irredundant clauses
c [sweep-1-1] 9530 pos 9.7% + 88390 neg 90.3% = 97920 sched 100.0% ret 0
c [sweep-1-1] 1379606 steps 17 queries 28722.53 avg class size
c [sweep-1-1] 192 decisions 16 SAT calls 68.38 avg env size
c [sweep-1-1] 97830 variables remain 100% (80 retained 0%)
c [decomp-10] removed 21 variables
c [sweep-1-1] removed 21 vars (0 failed, 0 eqs, 3 impls)
c [sweep-1] considered successful since not run to completion yet
c [sweep-1] removed 21 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-5] 667112 negative 99.0% of 673530 except 6418 1.0%
c [phase-count-5] 550192 positive 81.7% of 673530 except 123338 18.3%
c [phase-count-5] less non-negative clauses 6418 than limit 67300 (10.0%)
c [phase-count-5] non-pos/non-neg = 123338/6418 = 19.22 >= 2.00 = 200/100
c [lucky-phase-5] forcing lucky phase -1
c [phase-5] phase bias: 0 positive 0%, 497 negative 100%
c [sort-queue-5] sorted 48873 enqueued variables after 3215 conflicts
c [score-dist-5] active 49026 (50%), one 0 (0%), zero 48873 (50%)
c [score-dist-5] max exp 507, different 19 (4%)
c [score-dist-5] median active exp 500, avg 499.1
c [simplification-5] removed 1161 variables 1.2% (97899 remain 40%)
c [simplification-5] removed 47975 irredundant clauses 6.6% (673530 remain 49%)
c [simplification-5] maximum reduction of 7% = max (1%, 7%)
c [simplification-5] large reduction 7% >= 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 15215 (soft 5215 + delta 10000)
c [simplification-5] new conflict limit 5215 (hard 15215)
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.4   97898   673530      3646    2657    271 59105   26   367   51   7%      2  358  117    2 5750%
c i   26.5   97762   673530      3650    2659    271 59105   26   368   51   7%      2  358  116    2 5673%
c i   26.5   97721   673530      3652    2660    271 59105   26   368   51   7%      2  358  115    2 5629%
c i   27.0   97615   673530      3829    2811    277 59111   27   401   51   7%      2  390   83    2 3850%
c i   27.0   97606   673530      3845    2823    279 59112   27   403   51   7%      2  393   82    2 3747%
c i   27.0   97603   673530      3846    2823    279 59112   27   403   51   7%      2  393   81    2 3733%
c i   27.1   97600   673530      3872    2845    279 59114   27   407   51   7%      2  396   83    2 3740%
c i   27.1   97551   673530      3876    2844    279 59114   27   407   51   7%      2  396   83    2 3732%
c i   27.3   97391   673530      3978    2920    280 59120   27   404   51   7%      2  393   66    2 2895%
c i   27.5   97384   673530      4052    2962    290 59138   27   408   51   7%      2  396   53    2 2315%
c i   27.6   97382   673530      4099    2995    295 59143   27   409   51   7%      2  397   54    2 2342%
c i   27.8   97268   673530      4225    3101    299 59153   31   406   51   8%      2  394   90    3 3457%
c i   28.5   97235   673530      4490    3340    302 59163   31   421   51   7%      2  406   50    3 1863%
c i   28.7   97230   673530      4565    3392    304 59179   30   430   51   7%      2  415   42    3 1539%
c i   28.7   97223   673530      4567    3392    304 59180   30   430   51   7%      2  415   41    3 1527%
c i   28.7   97215   673530      4569    3392    304 59181   30   430   51   7%      2  415   41    3 1515%
c i   28.7   97203   673530      4571    3392    304 59182   30   430   51   7%      2  415   41    3 1504%
c i   28.8   97195   673530      4573    3392    304 59183   30   430   51   7%      2  415   40    3 1492%
c i   28.8   97189   673530      4574    3392    304 59183   30   430   51   7%      2  415   40    3 1486%
c i   28.8   97182   673530      4575    3392    304 59183   30   429   51   7%      2  415   40    3 1481%
c i   28.8   97174   673530      4576    3392    304 59183   30   429   51   7%      2  414   40    3 1475%
c i   29.1   97171   673530      4677    3477    308 59192   31   445   51   7%      2  429   47    3 1670%
c i   29.4   97163   673530      4835    3607    317 59203   32   452   52   7%      1  435   53    3 1820%
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   29.4   97155   673530      4864    3632    318 59204   33   451   52   7%      1  434   66    3 2195%
c i   29.8   97154   673530      4995    3750    321 59209   33   455   52   7%      1  438   58    3 1870%
c i   30.3   97017   673530      5251    3957    336 59230   36   475   52   8%      2  456   77    3 2272%
c i   30.3   96752   673530      5257    3958    336 59234   36   475   52   8%      2  456   75    3 2222%
c 
c [simplification-6] limit 5285 conflicts (hard 15215) hit after 5285 conflicts
c [ternres-2] limit 4000000 with penalty 0 = 0 + 0
c [ternres-2] all 96734 free variables schedulable
c [ternres-2] 0 ternary resolvents (0 bin, 0 trn)
c [ternres-2] 70105 variables remain 72% (26629 retained 28%)
c [card-3] limit 500000 penalty 2 = 2 + 0
c [card-3] found 2120 at-most-one constraints of average size 4.2
c [card-3] no at-most-two constraint found
c [card-3] using previous limit 500000 for elimination
c [card-3] 2120 out of 2120 constraints (100%) meet size limits
c [card-3] no units found
c [card-3] no at-most-one constraints generated
c [decomp-11] removed 1466 variables
c [simpleprobe-3] 19263 schedulable variables 20%
c [simpleprobe-3] limit 7488740 penalty 1 = 1 + 0
c [decomp-12] removed 102 variables
c [simpleprobe-3] 25339 variables remain 26% (70992 retained 74%)
c [simpleprobe-3] removed 102 variables, found 16505 hbrs, 41 units
c [unhide-6] limit 748874 with penalty 0 = 0 + 0
c [unhide-6-6] 1 units, 758 failed, 5299 tauts, 0 hbrs, 10746 literals
c [transred-2] limit 2000000 with penalty 0 = 0 + 0
c [transred-2] removed 236 transitive binary clauses
c [block-2] scheduling all variables this time
c [block-2] scheduled 95281 variables 100%
c [block-2] limit of 50000000 steps penalty 0 = 0 + 0
c [block-2] fully completed
c [block-2] transition to [ all 0 rem 0 ] state
c [block-2] eliminated 954 blocked clauses
c [block-2] 954 < 1/100 * 663085 = 6630 considered unsuccessful
c [elim-5] scheduling all variables this time
c [elim-5] scheduled 95280 variables 100%
c [elim-5] limit of 37443704 steps penalty 1 = 1 + 0
c [elim-5] rescheduling of touched variables disabled
c [elim-5] incomplete 10746 not tried 11% in round 1
c [elim-5] transition to [ all 1 rem 1 ] state
c [elim-5] eliminated 2840 = 3% variables out of 95280 scheduled
c [bca-2] limit of 10000000 steps and 1297420 added (scaled 2)
c [bca-2] 163788 out of 184882 literals actually usable 89%
c [bca-2] added 130 blocked clauses in 480708 steps
c [sweep-2] limit 1296826 based on 648413 irredundant clauses
c [sweep-2-1] 9332 pos 10.1% + 83033 neg 89.9% = 92365 sched 99.9% ret 75
c [sweep-2-1] 2059191 steps 12 queries 20219.58 avg class size
c [sweep-2-1] 339 decisions 9 SAT calls 316.22 avg env size
c [sweep-2-1] 91742 variables remain 100% (108 retained 0%)
c [decomp-13] removed 593 variables
c [sweep-2-1] removed 593 vars (0 failed, 3 eqs, 4 impls)
c [sweep-2] considered successful since not run to completion yet
c [sweep-2] removed 593 vars in TOTAL (1 rounds, 11 queries)
c [phase-count-6] 635660 negative 99.1% of 641439 except 5779 0.9%
c [phase-count-6] 522394 positive 81.4% of 641439 except 119045 18.6%
c [phase-count-6] less non-negative clauses 5779 than limit 64100 (10.0%)
c [phase-count-6] non-pos/non-neg = 119045/5779 = 20.60 >= 2.00 = 200/100
c [lucky-phase-6] forcing lucky phase -1
c [phase-6] phase bias: 0 positive 0%, 185 negative 100%
c [sort-queue-6] sorted 40043 enqueued variables after 5285 conflicts
c [score-dist-6] active 51804 (56%), one 0 (0%), zero 40043 (44%)
c [score-dist-6] max exp 508, different 28 (6%)
c [score-dist-6] median active exp 499, avg 497.4
c [simplification-6] removed 4887 variables 5.1% (91847 remain 37%)
c [simplification-6] removed 32091 irredundant clauses 4.8% (641439 remain 47%)
c [simplification-6] maximum reduction of 5% = max (5%, 5%)
c [simplification-6] large reduction 5% >= 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 17285 (soft 7285 + delta 10000)
c [simplification-6] new conflict limit 7285 (hard 17285)
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   34.7   91846   641439      5305    3447    310 70045   36   480   50   8%      1  460   71    3 2071%
c i   34.7   91836   641439      5307    3447    310 70046   36   479   50   8%      1  460   70    3 2055%
c i   35.1   91821   641439      5626    3728    322 70055   38   503   51   8%      2  481   56    4 1526%
c i   35.3   91637   641439      5812    3882    328 70067   40   500   51   8%      2  477   61    4 1583%
c i   35.6   91636   641439      6111    4111    341 70098   39   481   51   8%      2  456   36    4  888%
c i   36.6   91606   641439      6947    4695    395 70142   41   437   51   9%      5  407   41    5  905%
c i   36.7   91581   641439      6998    4729    404 70149   40   437   51   9%      5  405   36    5  782%
c 
c [simplification-7] limit 7290 conflicts (hard 17285) hit after 7290 conflicts
c [quatres-2] found 36314 quaternary clauses 37% in total
c [quatres-2-2] added 1 single-self-subsuming ternary resolvents
c [quatres-2-2] added 5 quaternary resolvents
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] extracted 18 xors of average arity 2.9
c [gauss-2] connected 52 occurrences of 44 variables (average 1.2)
c [gauss-2] limit 1000000 penalty 1 = 1 + 0
c [gauss-2] fully completed
c [gauss-2] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-14] removed 19 variables
c [unhide-7] limit 902100 with penalty 0 = 0 + 0
c [unhide-7-7] 0 units, 175 failed, 9698 tauts, 0 hbrs, 10736 literals
c [transred-3] limit 2000000 with penalty 0 = 0 + 0
c [transred-3] removed 224 transitive binary clauses
c [transred-3] found 3 units
c [cce-2] limit of 15000000 steps penalty 1 = 1 + 0
c [cce-2-1] incomplete large round (ATE)
c [cce-2-1] allowing another 7500000 steps for small clauses
c [cce-2-1] scheduling 511011 clauses = 303421 binary + 207590 ternary
c [cce-2-1] tried to eliminate 148 small clauses 0%
c [cce-2-1] eliminated 43 binary clauses 0%
c [cce-2-1] eliminated 19 ternary clauses 0%
c [cce-2-1] eliminated 62 small clauses 0%
c [cce-2-1] eliminated 1746 small clauses in 15000014 steps
c [cce-2-1] incomplete small round (ATE)
c [cce-2-1] eliminated 1746 covered clauses in round 1
c [cce-2] eliminated 1746 covered clauses in TOTAL during 1 rounds
c [cce-2] 1746 < 1/100 * 631093 = 6310 considered unsuccessful
c [elim-6] 10723 variables 12% will be scheduled this time
c [elim-6] scheduled 10723 variables 12%
c [elim-6] limit of 90210009 steps penalty 0 = 0 + 0
c [elim-6] rescheduling of touched variables disabled
c [elim-6-1] no variable eliminated in round 1 in 23902773 steps
c [elim-6] fully completed in 1 rounds
c [elim-6] transition to [ all 0 rem 0 ] state
c [elim-6] eliminated 0 = 0% variables out of 10723 scheduled
c [bca-3] limit of 10000000 steps and 1258355 added (scaled 2)
c [bca-3] 158174 out of 182786 literals actually usable 87%
c [bca-3] added 69 blocked clauses in 453967 steps
c [sweep-3] limit 1353150 penalty 0 = 0 + 0
c [sweep-3-1] 9858 pos 10.8% + 81431 neg 89.2% = 91289 sched 99.9% ret 103
c [sweep-3-1] 1391839 steps 17 queries 21425.35 avg class size
c [sweep-3-1] 238 decisions 14 SAT calls 88.07 avg env size
c [sweep-3-1] 91227 variables remain 100% (163 retained 0%)
c [decomp-15] removed 4 variables
c [sweep-3-1] removed 4 vars (0 failed, 2 eqs, 4 impls)
c [sweep-3] considered successful since not run to completion yet
c [sweep-3] removed 4 vars in TOTAL (1 rounds, 16 queries)
c [phase-count-7] 623050 negative 99.1% of 628823 except 5773 0.9%
c [phase-count-7] 512869 positive 81.6% of 628823 except 115954 18.4%
c [phase-count-7] less non-negative clauses 5773 than limit 62800 (10.0%)
c [phase-count-7] non-pos/non-neg = 115954/5773 = 20.09 >= 2.00 = 200/100
c [lucky-phase-7] forcing lucky phase -1
c [phase-7] phase bias: 0 positive 0%, 158 negative 100%
c [sort-queue-7] sorted 35561 enqueued variables after 7290 conflicts
c [score-dist-7] active 55827 (61%), one 0 (0%), zero 35561 (39%)
c [score-dist-7] max exp 507, different 35 (7%)
c [score-dist-7] median active exp 495, avg 494.1
c [simplification-7] removed 193 variables 0.2% (91388 remain 37%)
c [simplification-7] removed 12616 irredundant clauses 2.0% (628823 remain 46%)
c [simplification-7] maximum reduction of 2% = max (0%, 2%)
c [simplification-7] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-7] new conflict interval 6666
c [simplification-7] penalized conflict interval 6666 = 1 * 6666
c [simplification-7] hard conflict limit 23956 (soft 13956 + delta 10000)
c [simplification-7] new conflict limit 13956 (hard 23956)
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   42.9   91387   628823      8279    5856    463 69714   49   574   52   9%     10  534   94    6 1601%
c i   43.3   91379   628823      8403    5943    472 69735   49   581   52   8%      9  540   73    6 1226%
c i   43.3   91378   628823      8426    5959    473 69735   49   580   52   9%      8  539   73    6 1217%
c i   44.0   91373   628823      8792    6282    486 69744   55   606   52   9%      7  562  115    7 1766%
c i   44.2   91372   628823      8869    6355    487 69744   55   613   52   9%      6  568   98    7 1482%
c i   44.5   91147   628823      8965    6439    488 69750   54   620   52   9%      6  574   83    7 1245%
c i   44.9   91090   628823      9227    6683    491 69753   64   657   53  10%      5  609  183    7 2448%
c i   45.2   91081   628823      9357    6793    497 69757   74   680   53  11%      4  631  254    8 3105%
c i   45.2   91074   628823      9358    6793    497 69757   74   680   53  11%      4  630  253    8 3093%
c i   45.5   91067   628823      9553    6948    500 69766   91   701   54  13%      4  650  358    9 3779%
c i   45.7   91062   628823      9684    7051    509 69771   98   709   54  14%      3  656  350   10 3472%
c i   46.3   91052   628823     10333    7620    528 69778  101   674   54  15%      4  615  106   11  948%
c i   46.4   90775   628823     10343    7629    528 69778  101   674   54  15%      4  615  103   11  918%
c i   47.9   90747   628823     11073    8267    547 69798  102   734   55  14%      5  668  106   12  869%
c i   48.7   90746   628823     11440    8577    558 69819  102   750   57  14%      4  680   83   13  652%
c i   48.7   90743   628823     11441    8577    558 69819  102   749   57  14%      4  680   83   13  650%
c i   49.1   90717   628823     11763    8796    561 69825  111   722   57  15%      4  650  163   14 1185%
c i   49.1   90709   628823     11764    8796    561 69825  111   722   57  15%      4  650  162   14 1181%
c i   49.1   90701   628823     11765    8796    561 69825  111   722   57  15%      4  649  161   14 1176%
c i   49.1   90695   628823     11768    8798    561 69825  111   722   57  15%      4  649  160   14 1164%
c i   49.4   90493   628823     11929    8927    571 69840  108   712   57  15%      3  638  101   14  731%
c i   50.4   90489   628823     12316    9243    593 69871  101   723   58  14%      3  645   55   14  397%
c i   50.4   90486   628823     12317    9243    593 69871  101   723   58  14%      3  645   55   14  396%
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   50.9   90479   628823     12707    9576    604 69881  121   739   58  16%      3  657  311   16 1982%
c i   51.1   90478   628823     12898    9743    605 69881  137   747   58  18%      3  663  411   17 2418%
c i   51.5   90469   628823     13271   10073    614 69895  137   754   58  18%      3  666  166   18  939%
c i   51.9   90467   628823     13496   10250    619 69919  132   759   58  17%      2  669  101   18  566%
c i   52.4   90457   628823     13858   10514    628 69974  129   783   58  17%      2  690  112   18  614%
c 
c [simplification-8] limit 14010 conflicts (hard 23956) hit after 14014 conflicts
c [quatres-3] found 34881 quaternary clauses 37% in total
c [quatres-3-1] removed 2 duplicate quaternary clauses
c [quatres-3-2] added 1 single-self-subsuming ternary resolvents
c [ternres-3] limit 3840687 with penalty 1 = 1 + 0
c [ternres-3] 65495 schedulable variables 72%
c [ternres-3] 8 ternary resolvents (0 bin, 8 trn)
c [ternres-3] 38810 variables remain 43% (51612 retained 57%)
c [decomp-16] removed 999 variables
c [treelook-3] limit 384068 penalty 1 = 1 + 0 boost 1
c [treelook-3] scheduled 70697 literals 39%
c [treelook-3] scheduling used 384603 steps
c [treelook-3] not fully scheduled
c [treelook-3] limit 384068 penalty 1 = 1 + 0 boost 1
c [treelook-3] used 416526 steps
c [treelook-3] 70685 literals remain 39%
c [treelook-3] 38067 variables remain to probed next time 42%
c [treelook-3] removed 3 variables, found 1582 hbrs
c [unhide-8] limit 768137 with penalty 1 = 0 + 1
c [unhide-8-8] 2 units, 309 failed, 2867 tauts, 0 hbrs, 136968 literals
c [transred-4] limit 2000000 with penalty 0 = 0 + 0
c [transred-4] removed 223 transitive binary clauses
c [transred-4] found 3 units
c [block-3] scheduling all variables this time
c [block-3] scheduled 89791 variables 100%
c [block-3] limit of 38406877 steps penalty 1 = 1 + 0
c [block-3] fully completed
c [block-3] transition to [ all 0 rem 0 ] state
c [block-3] eliminated 16 blocked clauses
c [block-3] 16 < 1/100 * 618141 = 6181 considered unsuccessful
c [bca-4] limit of 10000000 steps and 1229236 added (scaled 2)
c [bca-4] 144444 out of 179584 literals actually usable 80%
c [bca-4] added 49 blocked clauses in 393380 steps
c [sweep-4] limit 2304412 penalty 0 = 0 + 0
c [sweep-4-1] 8626 pos 9.6% + 81012 neg 90.4% = 89638 sched 99.8% ret 153
c [sweep-4-1] 2567806 steps 14 queries 24652.57 avg class size
c [sweep-4-1] 280 decisions 13 SAT calls 224.23 avg env size
c [sweep-4-1] 89583 variables remain 100% (203 retained 0%)
c [decomp-18] removed 132 variables
c [sweep-4-1] removed 132 vars (0 failed, 0 eqs, 1 impls)
c [sweep-4] considered successful since not run to completion yet
c [sweep-4] removed 132 vars in TOTAL (1 rounds, 13 queries)
c [phase-count-8] 607807 negative 99.1% of 613579 except 5772 0.9%
c [phase-count-8] 496041 positive 80.8% of 613579 except 117538 19.2%
c [phase-count-8] less non-negative clauses 5772 than limit 61300 (10.0%)
c [phase-count-8] non-pos/non-neg = 117538/5772 = 20.36 >= 2.00 = 200/100
c [lucky-phase-8] forcing lucky phase -1
c [phase-8] phase bias: 0 positive 0%, 20 negative 100%
c [sort-queue-8] sorted 26264 enqueued variables after 14014 conflicts
c [score-dist-8] active 63395 (71%), one 0 (0%), zero 26264 (29%)
c [score-dist-8] max exp 508, different 62 (12%)
c [score-dist-8] median active exp 494, avg 489.8
c [simplification-8] removed 763 variables 0.8% (89659 remain 36%)
c [simplification-8] removed 15244 irredundant clauses 2.4% (613579 remain 45%)
c [simplification-8] maximum reduction of 2% = max (1%, 2%)
c [simplification-8] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-8] new conflict interval 13332
c [simplification-8] penalized conflict interval 13332 = 1 * 13332
c [simplification-8] hard conflict limit 37346 (soft 27346 + delta 10000)
c [simplification-8] new conflict limit 27346 (hard 37346)
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   56.4   89658   613579     14490   10799    673 70200  119   783   60  15%      3  683   53   19  285%
c i   56.7   89650   613579     14733   10969    709 70222  115   770   60  15%      3  667   43   19  230%
c i   56.7   89496   613579     14734   10969    709 70222  115   770   60  15%      3  667   43   19  229%
c i   57.1   88943   613579     14926   11110    715 70256  111   768   60  14%      3  664   35   19  185%
c i   57.1   88939   613579     14927   11110    715 70256  111   768   60  14%      3  663   34   19  184%
c i   57.1   88935   613579     14932   11113    715 70257  111   768   60  14%      3  663   34   19  181%
c i   57.4   88926   613579     15027   11185    723 70268  108   768   60  14%      2  662   30   19  158%
c i   58.1   88917   613579     15305   11409    745 70283  103   788   60  13%      2  680   27   19  143%
c i   58.9   88909   613579     15721   11778    754 70297  102   830   60  12%      2  717   73   19  382%
c i   59.2   88908   613579     15849   11896    754 70301  103   845   61  12%      2  731   98   19  507%
c i   59.5   88907   613579     16078   12094    758 70305  109   833   61  13%      2  717  172   20  859%
c i   60.2   88900   613579     16476   12435    766 70313  108   830   61  13%      2  709  110   21  537%
c i   60.2   88897   613579     16477   12435    766 70313  108   830   61  13%      2  709  110   21  535%
c i   60.8   88893   613579     16922   12830    769 70316  121   833   61  14%      2  708  208   22  949%
c i   60.8   88858   613579     16934   12839    769 70316  121   832   61  15%      2  707  208   22  950%
c i   60.8   88849   613579     16961   12857    771 70318  121   829   61  15%      2  703  203   22  923%
c i   60.9   88846   613579     17069   12950    771 70321  121   815   61  15%      2  689  174   22  787%
c i   61.0   88845   613579     17112   12984    772 70324  120   810   61  15%      2  683  155   22  700%
c i   61.0   88834   613579     17116   12986    772 70325  120   809   61  15%      2  682  153   22  690%
c i   61.1   88825   613579     17142   13009    772 70325  120   808   61  15%      2  680  142   22  641%
c i   61.2   88819   613579     17210   13055    779 70335  118   802   61  15%      2  674  114   22  513%
c i   61.4   88649   613579     17321   13151    782 70342  116   792   61  15%      2  663   94   22  423%
c i   61.5   88641   613579     17366   13192    784 70342  116   788   61  15%      2  659   91   22  409%
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   62.4   88629   613579     18052   13779    811 70364  133   784   61  17%      3  648  218   24  894%
c i   62.5   88621   613579     18089   13805    814 70369  132   786   61  17%      3  650  192   24  787%
c i   63.0   88508   613579     18366   14025    827 70393  126   804   61  16%      3  665   89   24  366%
c i   63.1   88500   613579     18407   14060    831 70393  125   808   61  16%      3  668   88   24  360%
c i   63.2   88499   613579     18412   14064    831 70393  125   808   61  16%      3  668   87   24  355%
c i   63.2   88498   613579     18414   14065    831 70393  125   808   61  16%      3  668   87   24  358%
c i   63.6   88497   613579     18593   14216    837 70401  124   834   61  15%      2  692   90   25  364%
c i   64.0   88494   613579     18801   14387    844 70410  123   860   61  14%      2  715   99   25  398%
c i   64.1   88483   613579     18834   14418    844 70411  124   860   61  14%      2  716  117   25  468%
c i   64.1   88475   613579     18835   14418    844 70411  124   860   61  14%      2  715  117   25  466%
c i   64.3   88468   613579     19012   14575    848 70416  130   849   61  15%      2  703  195   26  762%
c i   64.3   88466   613579     19033   14593    849 70416  131   848   61  15%      2  701  206   26  800%
c i   64.4   88465   613579     19128   14674    853 70419  132   840   61  16%      2  693  196   26  756%
c i   65.4   88461   613579     19692   15111    869 70468  138   835   61  17%      3  682  207   27  760%
c i   65.4   88433   613579     19710   15123    870 70468  138   835   61  16%      3  681  198   27  727%
c i   65.5   88431   613579     19711   15123    870 70468  138   835   61  16%      3  681  197   27  724%
c i   65.5   88428   613579     19712   15123    870 70468  138   835   61  16%      3  681  197   27  721%
c i   65.5   88425   613579     19713   15123    870 70468  138   834   61  16%      3  681  196   27  718%
c i   65.5   88422   613579     19714   15123    870 70468  137   834   61  16%      3  680  195   27  716%
c i   66.0   88420   613579     20064   15423    873 70477  143   854   61  17%      2  697  185   28  656%
c i   66.1   88411   613579     20078   15434    873 70479  143   857   61  17%      2  700  178   28  631%
c i   66.4   88405   613579     20225   15561    879 70484  141   890   61  16%      2  731  150   28  527%
c i   67.1   88352   613579     20527   15807    886 70521  143   942   68  15%      2  780  153   29  527%
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   67.2   88349   613579     20610   15869    892 70529  143   939   68  15%      2  775  154   29  526%
c i   67.2   88348   613579     20614   15870    892 70531  143   938   68  15%      2  775  152   29  519%
c i   67.4   88347   613579     20698   15932    893 70542  142   932   68  15%      2  767  139   29  475%
c i   69.2   88346   613579     21519   16606    927 70606  137   912   68  15%      4  739  122   30  404%
c i   70.0   88341   613579     21836   16881    937 70628  131   927   68  14%      4  750   79   30  260%
c i   70.1   88047   613579     21877   16916    939 70628  132   927   68  14%      3  749   93   31  304%
c i   70.1   88046   613579     21878   16916    939 70628  132   927   68  14%      3  749   92   31  303%
c i   70.1   88045   613579     21894   16929    939 70629  131   927   68  14%      3  749   90   31  296%
c i   73.1   88042   613579     23315   18182    953 70651  153   958   73  16%     10  764  199   34  582%
c i   74.1   88039   613579     24041   18864    956 70658  167   990   73  17%      8  787  202   37  553%
c i   74.1   88030   613579     24076   18895    956 70660  169   992   73  17%      7  789  230   37  626%
c i   74.1   88022   613579     24077   18895    956 70660  169   991   73  17%      7  788  229   37  623%
c i   74.2   88016   613579     24101   18917    956 70661  169   993   73  17%      7  790  218   37  592%
c i   74.3   88010   613579     24154   18967    957 70662  170   996   73  17%      7  792  223   37  604%
c i   74.5   88005   613579     24334   19133    957 70662  172   993   73  17%      6  787  219   37  586%
c i   76.0   88004   613579     25483   20136    972 70673  185   910   74  20%      8  691  133   41  327%
c i   76.4   87636   613579     25680   20297    974 70682  180   896   74  20%      7  676  100   41  244%
c i   78.3   87632   613579     26913   21293    984 70698  189   862   74  22%      9  629  251   44  572%
c i   78.5   87631   613579     27010   21378    985 70700  187   857   74  22%      8  623  215   44  489%
c 
c [simplification-9] limit 27459 conflicts (hard 37346) hit after 27460 conflicts
c [quatres-4] found 34309 quaternary clauses 39% in total
c [quatres-4-1] removed 2 duplicate quaternary clauses
c [ternres-4] limit 13676292 with penalty 0 = 0 + 0
c [ternres-4] 37575 schedulable variables 42%
c [ternres-4] 21 ternary resolvents (0 bin, 21 trn)
c [ternres-4] fully completed ternary resolution
c [decomp-19] removed 2120 variables
c [basicprobe-3] limit 68381461 penalty 0 = 0 + 0
c [basicprobe-3-0] 28928 probes remain 34% after last round
c [basicprobe-3-0] 311 units = 308 failed (99%) + 3 lifted (1%)
c [basicprobe-3-0] removed 1304 variables, found 246040 hbrs
c [bate-1] eliminated 138 asymmetric tautologies during probing
c [unhide-9] limit 683814 with penalty 2 = 0 + 2
c [unhide-9-9] 1 units, 209 failed, 13617 tauts, 0 hbrs, 354104 literals
c [transred-5] limit 2000000 with penalty 0 = 0 + 0
c [transred-5] removed 177 transitive binary clauses
c [transred-5] found 1 units
c [elim-7] scheduling all variables this time
c [elim-7] scheduled 85972 variables 100%
c [elim-7] limit of 136762922 steps penalty 1 = 1 + 0
c [elim-7] rescheduling of touched variables disabled
c [elim-7-1] eliminated 2463 variables 3% in round 1 in 52287585 steps
c [elim-7-1] backward subsumption/strengthening limit 52287500
c [elim-7-1-1] backward checking 8522 touched variables 10%
c [elim-7-1-1] fully completed backward checking in 1 rounds
c [elim-7-1] subsumed 2 and strengthened 255 clauses in 2748189 steps
c [elim-7-1] rescheduled 599 variables 1% by backward subsumption
c [elim-7-2] eliminated 84 variables 0% in round 2 in 628031 steps
c [elim-7-2] backward subsumption/strengthening limit 628000
c [elim-7-2-1] backward checking 642 touched variables 1%
c [elim-7-2-1] fully completed backward checking in 1 rounds
c [elim-7-2] subsumed 0 and strengthened 4 clauses in 344928 steps
c [elim-7-2] rescheduled 16 variables 0% by backward subsumption
c [elim-7-3] eliminated 2 variables 0% in round 3 in 18189 steps
c [elim-7-3] backward subsumption/strengthening limit 18100
c [elim-7-3-1] backward checking 20 touched variables 0%
c [elim-7-3-1] incomplete backward checking 0 remain 0%
c [elim-7-3] subsumed 0 and strengthened 4 clauses in 18101 steps
c [elim-7] incomplete 16 not tried 0% in round 3
c [elim-7] transition to [ all 1 rem 1 ] state
c [elim-7] eliminated 2557 = 3% variables out of 85972 scheduled
c [bca-5] limit of 10000000 steps and 1143128 added (scaled 2)
c [bca-5] 130925 out of 166832 literals actually usable 78%
c [bca-5] added 59 blocked clauses in 356755 steps
c [sweep-5] boosting sweeping limit by 10
c [sweep-5] limit 41028870 penalty 0 = 0 + 0
c [sweep-5-1] 8982 pos 10.8% + 74258 neg 89.2% = 83240 sched 99.8% ret 175
c [sweep-5-1] 41121430 steps 374 queries 1647.72 avg class size
c [sweep-5-1] 6049 decisions 315 SAT calls 154.91 avg env size
c [sweep-5-1] 70502 variables remain 85% (12616 retained 15%)
c [decomp-20] removed 531 variables
c [sweep-5-1] removed 531 vars (0 failed, 63 eqs, 119 impls)
c [sweep-5] considered successful since not run to completion yet
c [sweep-5] removed 531 vars in TOTAL (1 rounds, 373 queries)
c [phase-count-9] 562896 negative 99.0% of 568468 except 5572 1.0%
c [phase-count-9] 458734 positive 80.7% of 568468 except 109734 19.3%
c [phase-count-9] less non-negative clauses 5572 than limit 56800 (10.0%)
c [phase-count-9] non-pos/non-neg = 109734/5572 = 19.69 >= 2.00 = 200/100
c [lucky-phase-9] forcing lucky phase -1
c [phase-9] phase bias: 0 positive 0%, 9 negative 100%
c [sort-queue-9] sorted 20170 enqueued variables after 27460 conflicts
c [score-dist-9] active 62714 (76%), one 0 (0%), zero 20170 (24%)
c [score-dist-9] max exp 509, different 115 (23%)
c [score-dist-9] median active exp 486, avg 479.8
c [simplification-9] removed 4747 variables 5.4% (82884 remain 34%)
c [simplification-9] removed 45111 irredundant clauses 7.4% (568468 remain 41%)
c [simplification-9] maximum reduction of 7% = max (5%, 7%)
c [simplification-9] large reduction 7% >= 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 39460 (soft 29460 + delta 10000)
c [simplification-9] new conflict limit 29460 (hard 39460)
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   90.6   82883   568468     27462   15553    955 333844  192   831   60  23%      6  593  214   45  472%
c i   90.9   82882   568468     27670   15741    957 333849  187   829   69  23%      5  589  156   45  343%
c i   90.9   82878   568468     27671   15741    957 333849  187   829   69  23%      5  589  155   45  342%
c i   90.9   82876   568468     27672   15741    957 333849  187   829   69  23%      5  589  155   45  341%
c i   90.9   82875   568468     27673   15741    957 333849  187   829   69  23%      5  589  154   45  339%
c i   92.3   82873   568468     28438   16380    968 333862  171   753   69  23%      5  506   79   46  173%
c i   93.3   82872   568468     29112   16912    975 333869  161   678   69  24%      5  427   91   47  196%
c i   93.5   82871   568468     29317   17066    981 333876  160   663   69  24%      4  411  123   47  261%
c 
c [simplification-10] limit 29490 conflicts (hard 39460) hit after 29494 conflicts
c [ternres-5] limit 14523473 with penalty 0 = 0 + 0
c [ternres-5] all 82871 free variables schedulable
c [ternres-5] 76 ternary resolvents (0 bin, 76 trn)
c [ternres-5] 323 variables remain 0% (82548 retained 100%)
c [card-4] limit 907717 penalty 3 = 3 + 0
c [card-4] found 1947 at-most-one constraints of average size 4.1
c [card-4] no at-most-two constraint found
c [card-4] using previous limit 907717 for elimination
c [card-4] 1947 out of 1947 constraints (100%) meet size limits
c [card-4] no units found
c [card-4] no at-most-one constraints generated
c [gauss-3] limit 726173 penalty 2 = 2 + 0
c [gauss-3] extracted 9 xors of average arity 3.0
c [gauss-3] connected 27 occurrences of 21 variables (average 1.3)
c [gauss-3] limit 726173 penalty 2 = 2 + 0
c [gauss-3] fully completed
c [gauss-3] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-21] removed 1 variables
c [simpleprobe-4] 23029 schedulable variables 28%
c [simpleprobe-4] limit 58093893 penalty 0 = 0 + 0
c [decomp-22] removed 2151 variables
c [simpleprobe-4] 11133 variables remain 14% (69586 retained 86%)
c [simpleprobe-4] removed 2151 variables, found 99689 hbrs, 1048 units
c [unhide-10] limit 1452347 with penalty 1 = 0 + 1
c [unhide-10-10] 4 units, 449 failed, 44337 tauts, 0 hbrs, 44988 literals
c [transred-6] limit 2000000 with penalty 0 = 0 + 0
c [transred-6] removed 251 transitive binary clauses
c [transred-6] found 1 units
c [cce-3] limit of 18154341 steps penalty 2 = 2 + 0
c [cce-3-1] eliminated 4 clauses out of 1254 (0%) of length 9
c [cce-3-1] eliminated 6 clauses out of 515 (1%) of length 8
c [cce-3-1] eliminated 37 clauses out of 789 (5%) of length 7
c [cce-3-1] incomplete large round (ACCE)
c [cce-3-1] eliminated 47 large clauses in 18154341 steps
c [cce-3-1] allowing another 9077170 steps for small clauses
c [cce-3-1] scheduling 440609 clauses = 275693 binary + 164916 ternary
c [cce-3-1] tried to eliminate 173 small clauses 0%
c [cce-3-1] eliminated 35 binary clauses 0%
c [cce-3-1] eliminated 19 ternary clauses 0%
c [cce-3-1] eliminated 54 small clauses 0%
c [cce-3-1] eliminated 3530 small clauses in 18154344 steps
c [cce-3-1] incomplete small round (ACCE)
c [cce-3-1] eliminated 3577 covered clauses in round 1
c [cce-3] eliminated 3577 covered clauses in TOTAL during 1 rounds
c [cce-3] 3577 < 1/100 * 547087 = 5470 considered unsuccessful
c [elim-8] no untried remaining variables left
c [elim-8] scheduled 80315 variables 100%
c [elim-8] boosting limit by 20
c [elim-8] limit of 5809389300 steps penalty 0 = 0 + 0
c [elim-8] rescheduling of touched variables disabled
c [elim-8-1] eliminated 1608 variables 2% in round 1 in 50893430 steps
c [elim-8-1] backward subsumption/strengthening limit 50893400
c [elim-8-1-1] backward checking 5770 touched variables 7%
c [elim-8-1-1] fully completed backward checking in 1 rounds
c [elim-8-1] subsumed 15 and strengthened 153 clauses in 3786126 steps
c [elim-8-1] rescheduled 371 variables 0% by backward subsumption
c [elim-8-2] eliminated 46 variables 0% in round 2 in 2363168 steps
c [elim-8-2] backward subsumption/strengthening limit 2363100
c [elim-8-2-1] backward checking 362 touched variables 0%
c [elim-8-2-1] fully completed backward checking in 1 rounds
c [elim-8-2] subsumed 0 and strengthened 2 clauses in 308331 steps
c [elim-8-2] rescheduled 8 variables 0% by backward subsumption
c [elim-8-3] eliminated 1 variables 0% in round 3 in 9020 steps
c [elim-8-3] backward subsumption/strengthening limit 9000
c [elim-8-3-1] backward checking 10 touched variables 0%
c [elim-8-3-1] incomplete backward checking 3 remain 30%
c [elim-8-3] subsumed 0 and strengthened 2 clauses in 9030 steps
c [elim-8] incomplete 8 not tried 0% in round 3
c [elim-8] transition to [ all 1 rem 1 ] state
c [elim-8] eliminated 1660 = 2% variables out of 80315 scheduled
c [bca-6] limit of 10000000 steps and 1077306 added (scaled 2)
c [bca-6] 121647 out of 157312 literals actually usable 77%
c [bca-6] added 202 blocked clauses in 326365 steps
c [sweep-6] limit 4357041 penalty 0 = 0 + 0
c [sweep-6-1] 8462 pos 12.5% + 59302 neg 87.5% = 67764 sched 86.2% ret 10891
c [sweep-6-1] 4362881 steps 50 queries 7322.84 avg class size
c [sweep-6-1] 735 decisions 45 SAT calls 152.87 avg env size
c [sweep-6-1] 67281 variables remain 86% (11356 retained 14%)
c [decomp-23] removed 25 variables
c [sweep-6-1] removed 25 vars (0 failed, 6 eqs, 11 impls)
c [sweep-6] considered successful since not run to completion yet
c [sweep-6] removed 25 vars in TOTAL (1 rounds, 49 queries)
c [phase-count-10] 532784 negative 99.0% of 538066 except 5282 1.0%
c [phase-count-10] 429996 positive 79.9% of 538066 except 108070 20.1%
c [phase-count-10] less non-negative clauses 5282 than limit 53800 (10.0%)
c [phase-count-10] non-pos/non-neg = 108070/5282 = 20.46 >= 2.00 = 200/100
c [lucky-phase-10] forcing lucky phase -1
c [phase-10] phase bias: 0 positive 0%, 9 negative 100%
c [sort-queue-10] sorted 16970 enqueued variables after 29494 conflicts
c [score-dist-10] active 61660 (78%), one 0 (0%), zero 16970 (22%)
c [score-dist-10] max exp 508, different 122 (24%)
c [score-dist-10] median active exp 492, avg 477.8
c [simplification-10] removed 4241 variables 5.1% (78630 remain 32%)
c [simplification-10] removed 30402 irredundant clauses 5.3% (538066 remain 39%)
c [simplification-10] maximum reduction of 5% = max (5%, 5%)
c [simplification-10] large reduction 5% >= 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 41494 (soft 31494 + delta 10000)
c [simplification-10] new conflict limit 31494 (hard 41494)
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  101.3   78629   538066     29743   14883   1009 345447  151   653   63  23%      3  398   81   47  172%
c i  101.3   78580   538066     29768   14905   1011 345447  151   652   63  23%      3  396   83   47  176%
c i  101.7   78579   538066     30053   15126   1013 345454  147   621   63  24%      3  365   80   47  170%
c i  101.9   78490   538066     30126   15195   1013 345454  144   616   63  23%      2  359   64   47  135%
c i  101.9   78486   538066     30128   15196   1013 345454  144   616   63  23%      2  359   63   47  134%
c i  102.3   78484   538066     30823   15827   1026 345459  125   559   63  22%      3  299   21   47   45%
c i  102.4   78482   538066     30904   15899   1027 345459  124   565   63  22%      3  304   31   47   65%
c i  102.5   78481   538066     31060   16024   1030 345466  121   566   63  21%      3  304   42   47   89%
c i  102.5   78480   538066     31089   16049   1031 345467  121   565   63  21%      2  303   47   47  100%
c i  102.6   78468   538066     31200   16139   1035 345474  120   558   63  21%      2  295   56   47  119%
c i  102.7   78170   538066     31248   16171   1035 345479  120   556   63  22%      2  293   67   47  142%
c 
c [simplification-11] limit 31499 conflicts (hard 41494) hit after 31501 conflicts
c [quatres-5] found 34723 quaternary clauses 42% in total
c [quatres-5-1] removed 1 duplicate quaternary clauses
c [quatres-5-2] added 2 single-self-subsuming ternary resolvents
c [quatres-5-2] added 8 quaternary resolvents
c [ternres-6] limit 15098345 with penalty 0 = 0 + 0
c [ternres-6] 289 schedulable variables 0%
c [ternres-6] 11 ternary resolvents (0 bin, 11 trn)
c [ternres-6] fully completed ternary resolution
c [decomp-24] removed 548 variables
c [treelook-4] limit 1509834 penalty 0 = 0 + 0 boost 1
c [treelook-4] scheduled 119497 literals 77%
c [treelook-4] scheduling used 1509843 steps
c [treelook-4] not fully scheduled
c [treelook-4] limit 1509834 penalty 0 = 0 + 0 boost 1
c [treelook-4] used 1920638 steps
c [treelook-4] 119480 literals remain 77%
c [treelook-4] 31220 variables remain to probed next time 40%
c [decomp-25] removed 1 variables
c [treelook-4] removed 2 variables, found 4521 hbrs
c [unhide-11] limit 1509834 with penalty 1 = 0 + 1
c [unhide-11-11] 4 units, 31 failed, 7907 tauts, 0 hbrs, 26117 literals
c [transred-7] limit 2000000 with penalty 0 = 0 + 0
c [transred-7] removed 250 transitive binary clauses
c [block-4] scheduling all variables this time
c [block-4] scheduled 78020 variables 100%
c [block-4] limit of 37745863 steps penalty 2 = 2 + 0
c [block-4] fully completed
c [block-4] transition to [ all 0 rem 0 ] state
c [block-4] eliminated 202 blocked clauses
c [block-4] 202 < 1/100 * 527622 = 5276 considered unsuccessful
c [elim-9] no untried remaining variables left
c [elim-9] scheduled 78019 variables 100%
c [elim-9] limit of 301966910 steps penalty 0 = 0 + 0
c [elim-9] rescheduling of touched variables disabled
c [elim-9-1] eliminated 478 variables 1% in round 1 in 48785479 steps
c [elim-9-1] backward subsumption/strengthening limit 48785400
c [elim-9-1-1] backward checking 2099 touched variables 3%
c [elim-9-1-1] fully completed backward checking in 1 rounds
c [elim-9-1] subsumed 3 and strengthened 19 clauses in 838573 steps
c [elim-9-1] rescheduled 62 variables 0% by backward subsumption
c [elim-9-2] eliminated 6 variables 0% in round 2 in 60705 steps
c [elim-9-2] backward subsumption/strengthening limit 60700
c [elim-9-2-1] backward checking 56 touched variables 0%
c [elim-9-2-1] incomplete backward checking 0 remain 0%
c [elim-9-2] subsumed 0 and strengthened 0 clauses in 60701 steps
c [elim-9-2] fully rescheduled 77535 variables 99%
c [elim-9-3] eliminated 4 variables 0% in round 3 in 48687650 steps
c [elim-9-3] backward subsumption/strengthening limit 48687600
c [elim-9-3-1] backward checking 36 touched variables 0%
c [elim-9-3-1] fully completed backward checking in 1 rounds
c [elim-9-3] subsumed 0 and strengthened 1 clauses in 99222 steps
c [elim-9] incomplete 4 not tried 0% in round 3
c [elim-9] transition to [ all 1 rem 1 ] state
c [elim-9] eliminated 488 = 1% variables out of 78019 scheduled
c [elim-9] 488 < 1/100 * 78019 = 780 considered unsuccessful
c [bca-7] limit of 10000000 steps and 1052195 added (scaled 2)
c [bca-7] 119250 out of 155064 literals actually usable 77%
c [bca-7] added 39 blocked clauses in 317975 steps
c [sweep-7] limit 4529503 penalty 0 = 0 + 0
c [sweep-7-1] 8483 pos 12.8% + 57886 neg 87.2% = 66369 sched 85.6% ret 11162
c [sweep-7-1] 4532691 steps 64 queries 7795.80 avg class size
c [sweep-7-1] 944 decisions 55 SAT calls 117.75 avg env size
c [sweep-7-1] 65592 variables remain 85% (11894 retained 15%)
c [decomp-26] removed 78 variables
c [sweep-7-1] removed 78 vars (0 failed, 8 eqs, 17 impls)
c [sweep-7] removed 78 vars in TOTAL (1 rounds, 63 queries)
c [phase-count-11] 520251 negative 99.0% of 525251 except 5000 1.0%
c [phase-count-11] 421032 positive 80.2% of 525251 except 104219 19.8%
c [phase-count-11] skipping relative phase luck test
c [phase-11] phase bias: 3 positive 100%, 0 negative 0%
c [sort-queue-11] sorted 16356 enqueued variables after 31501 conflicts
c [score-dist-11] active 61097 (79%), one 0 (0%), zero 16356 (21%)
c [score-dist-11] max exp 507, different 129 (25%)
c [score-dist-11] median active exp 494, avg 481.7
c [simplification-11] removed 631 variables 0.8% (77453 remain 31%)
c [simplification-11] removed 12815 irredundant clauses 2.4% (525251 remain 38%)
c [simplification-11] maximum reduction of 2% = max (1%, 2%)
c [simplification-11] geometric conflict interval increment 6666 = 20000 / 3
c [simplification-11] new conflict interval 19998
c [simplification-11] penalized conflict interval 19998 = 1 * 19998
c [simplification-11] hard conflict limit 61499 (soft 51499 + delta 10000)
c [simplification-11] new conflict limit 51499 (hard 61499)
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  110.5   77452   525251     32399   15514   1076 344567  106   643   61  17%      7  374   68   47  144%
c i  110.6   77451   525251     32450   15554   1077 344567  107   650   61  16%      6  381   80   47  168%
c i  110.7   77447   525251     32496   15593   1077 344567  107   650   61  16%      6  381   87   47  182%
c i  111.5   77446   525251     32886   15942   1082 344581  105   697   61  15%      5  426   88   48  185%
c i  112.0   77445   525251     33092   16137   1085 344584  106   743   61  14%      4  471  107   48  223%
c i  112.7   77438   525251     33495   16506   1086 344589  119   815   62  15%      3  540  283   49  577%
c i  112.7   77437   525251     33522   16518   1087 344589  122   815   62  15%      3  539  306   49  620%
c i  112.9   77436   525251     33652   16622   1088 344590  130   812   62  16%      2  534  334   50  668%
c i  113.0   77435   525251     33694   16660   1088 344592  129   811   62  16%      2  534  292   50  584%
c i  113.0   77434   525251     33711   16670   1088 344594  130   811   62  16%      2  533  287   50  574%
c i  113.0   77433   525251     33712   16670   1088 344594  130   810   62  16%      2  533  286   50  572%
c i  113.0   77432   525251     33719   16675   1088 344595  130   810   62  16%      2  532  286   50  572%
c i  113.0   77431   525251     33721   16676   1088 344595  130   810   62  16%      2  532  285   50  568%
c i  113.0   77430   525251     33722   16676   1088 344595  130   809   62  16%      2  532  284   50  566%
c i  113.0   77426   525251     33723   16676   1088 344595  130   809   62  16%      2  531  282   50  564%
c i  113.0   77425   525251     33725   16677   1088 344595  130   809   62  16%      2  531  281   50  560%
c i  113.0   77424   525251     33727   16678   1088 344595  130   809   62  16%      2  531  279   50  557%
c i  113.0   77423   525251     33729   16679   1088 344595  130   809   62  16%      2  531  279   50  557%
c i  113.0   77422   525251     33734   16683   1088 344595  130   808   62  16%      2  530  278   50  554%
c i  113.1   77421   525251     33736   16684   1088 344595  130   808   62  16%      2  530  278   50  554%
c i  113.1   77420   525251     33746   16690   1088 344597  130   807   62  16%      2  529  272   50  543%
c i  113.1   77419   525251     33748   16691   1088 344597  130   807   62  16%      2  529  272   50  543%
c i  113.1   77418   525251     33750   16692   1088 344597  130   807   62  16%      2  529  272   50  543%
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  113.1   77417   525251     33789   16722   1088 344598  131   805   62  16%      2  526  265   50  528%
c i  113.5   77414   525251     33955   16872   1091 344602  128   816   62  16%      2  536  163   50  324%
c i  113.6   77413   525251     33978   16892   1092 344602  127   816   62  16%      2  537  152   50  304%
c i  113.6   77412   525251     33999   16904   1092 344605  127   817   62  16%      1  537  142   50  284%
c i  113.6   77411   525251     34000   16904   1092 344605  127   817   62  16%      1  537  142   50  283%
c i  113.6   77410   525251     34001   16904   1092 344605  127   816   62  16%      1  536  141   50  281%
c i  113.6   77409   525251     34002   16904   1092 344605  127   816   62  16%      1  536  141   50  280%
c i  113.6   77408   525251     34005   16906   1092 344605  127   816   62  16%      1  536  139   50  277%
c i  113.7   77407   525251     34009   16908   1092 344605  127   816   62  16%      1  535  137   50  273%
c i  113.7   77406   525251     34012   16909   1093 344605  126   815   62  16%      1  535  136   50  270%
c i  113.7   77405   525251     34013   16909   1093 344605  126   815   62  16%      1  535  135   50  269%
c i  113.7   77404   525251     34019   16914   1093 344605  126   815   62  16%      1  534  132   50  263%
c i  113.9   77403   525251     34168   17025   1093 344609  131   810   62  16%      1  529  190   51  374%
c i  114.0   77402   525251     34185   17036   1095 344609  131   809   62  16%      1  527  190   51  374%
c i  114.0   77401   525251     34191   17039   1095 344611  131   808   62  16%      1  527  185   51  366%
c i  114.0   77400   525251     34192   17039   1095 344611  131   808   62  16%      1  527  185   51  364%
c i  114.0   77399   525251     34203   17040   1095 344614  131   807   62  16%      1  526  189   51  372%
c i  114.0   77398   525251     34212   17041   1095 344616  131   806   62  16%      1  525  194   51  382%
c i  114.1   77397   525251     34214   17042   1095 344616  131   806   62  16%      1  524  193   51  379%
c i  114.1   77396   525251     34215   17042   1095 344616  131   806   62  16%      1  524  192   51  378%
c i  114.1   77392   525251     34216   17042   1095 344616  131   806   62  16%      1  524  191   51  376%
c i  114.1   77391   525251     34229   17050   1095 344617  131   804   62  16%      1  522  191   51  376%
c i  114.1   77389   525251     34230   17050   1095 344617  131   804   62  16%      1  522  190   51  375%
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  114.1   77386   525251     34231   17050   1095 344617  131   804   62  16%      1  522  190   51  373%
c i  114.1   77383   525251     34233   17051   1095 344617  131   804   62  16%      1  522  188   51  370%
c i  114.1   77380   525251     34234   17051   1095 344617  131   803   62  16%      1  521  187   51  369%
c i  114.7   77378   525251     34618   17352   1102 344627  128   762   62  17%      1  477  112   51  219%
c i  117.0   77375   525251     35793   18414   1121 344645  126   855   62  15%      7  561  116   52  223%
c i  117.1   77374   525251     35819   18437   1122 344645  126   856   62  15%      6  562  117   52  223%
c i  117.1   77114   525251     35822   18439   1122 344645  127   856   62  15%      6  562  118   52  226%
c i  117.1   77110   525251     35847   18459   1122 344645  127   857   62  15%      6  562  125   52  239%
c i  117.2   77109   525251     35861   18471   1122 344645  127   857   62  15%      6  562  126   52  240%
c i  117.6   77108   525251     36177   18729   1126 344654  123   831   62  15%      5  534   99   52  189%
c i  117.8   77104   525251     36254   18797   1127 344658  125   835   62  15%      4  537  124   53  235%
c i  118.3   77102   525251     36515   19012   1127 344664  130   854   64  15%      3  554  198   53  372%
c i  119.1   77101   525251     36915   19367   1133 344669  129   880   66  15%      3  576  123   54  230%
c i  119.1   77100   525251     36917   19368   1133 344669  129   879   66  15%      3  576  123   54  229%
c i  119.2   77099   525251     36981   19421   1136 344670  129   874   66  15%      2  570  123   54  229%
c i  119.9   77098   525251     37337   19730   1139 344673  130   866   66  15%      2  559  151   54  277%
c i  120.8   77097   525251     37776   20124   1152 344684  136   907   69  15%      2  597  217   55  393%
c i  122.5   77096   525251     38540   20732   1158 344703  170   901   69  19%      3  584  386   58  661%
c i  122.5   77095   525251     38550   20739   1158 344703  171   900   69  19%      3  583  383   58  656%
c i  122.5   77094   525251     38553   20741   1158 344703  171   900   69  19%      3  582  378   58  648%
c i  122.5   77093   525251     38555   20742   1158 344703  171   899   69  19%      3  582  375   58  644%
c i  123.6   77092   525251     39211   21299   1162 344707  174   852   71  20%      4  529  230   60  386%
c i  123.6   77091   525251     39215   21302   1162 344707  174   852   71  20%      3  528  228   60  382%
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  123.6   77090   525251     39216   21302   1162 344707  174   851   71  20%      3  528  227   60  380%
c i  123.6   77089   525251     39219   21304   1162 344707  174   851   71  20%      3  528  225   60  377%
c i  123.6   77088   525251     39222   21306   1162 344707  174   851   71  20%      3  528  222   60  373%
c i  123.9   77087   525251     39438   21474   1164 344713  179   839   71  21%      3  514  255   60  422%
c i  124.0   77086   525251     39456   21486   1164 344713  179   839   71  21%      3  513  259   60  429%
c i  124.4   77085   525251     39854   21787   1168 344724  188   812   71  23%      2  484  273   62  443%
c i  124.4   77081   525251     39855   21787   1168 344724  188   812   71  23%      2  484  272   62  441%
c i  124.4   77077   525251     39860   21791   1168 344724  188   811   71  23%      2  483  268   62  435%
c i  124.4   77074   525251     39861   21791   1168 344724  188   811   71  23%      2  483  267   62  433%
c i  125.0   77071   525251     40608   22338   1171 344724  209   764   71  27%      3  431  305   65  472%
c i  125.4   77070   525251     40832   22538   1176 344729  201   758   71  27%      3  423  155   65  240%
c i  126.7   77069   525251     41635   23246   1186 344741  195   809   71  24%      4  469  243   66  369%
c i  127.1   77068   525251     41826   23396   1191 344744  217   835   71  26%      3  493  467   67  693%
c i  128.1   77062   525251     42226   23742   1196 344748  234   855   76  27%      3  511  412   69  593%
c i  128.6   77053   525251     42561   24027   1203 344751  239   850   76  28%      2  503  342   71  483%
c i  128.8   77051   525251     42610   24075   1203 344751  238   844   76  28%      2  497  305   71  431%
c i  128.8   77050   525251     42662   24114   1203 344752  240   840   76  29%      2  492  318   71  448%
c i  130.8   77049   525251     43965   25145   1214 344768  228   756   84  30%      8  400  221   73  301%
c i  131.0   77048   525251     44036   25182   1218 344780  229   754   84  30%      7  397  231   74  314%
c i  131.0   77047   525251     44041   25183   1221 344780  229   754   84  30%      7  397  227   74  308%
c i  131.0   77046   525251     44044   25185   1221 344780  229   753   84  30%      7  396  224   74  304%
c i  131.0   77045   525251     44047   25186   1221 344780  229   753   84  30%      7  396  224   74  304%
c i  131.2   77044   525251     44143   25253   1222 344786  228   746   84  31%      6  388  218   74  296%
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  131.8   77041   525251     44749   25719   1227 344795  211   680   85  31%      5  318   98   74  132%
c i  131.9   77014   525251     44762   25730   1227 344796  210   678   86  31%      5  317   95   74  128%
c i  132.2   77008   525251     44988   25924   1234 344800  205   664   86  31%      4  302  106   74  143%
c i  132.4   77001   525251     45172   26065   1237 344804  204   656   86  31%      3  293  150   75  201%
c i  132.4   76993   525251     45173   26065   1237 344804  204   655   86  31%      3  292  149   75  200%
c i  132.4   76992   525251     45178   26069   1237 344804  204   655   86  31%      3  292  148   75  198%
c i  132.4   76991   525251     45193   26080   1238 344805  204   654   86  31%      3  291  147   75  197%
c i  132.4   76990   525251     45202   26086   1239 344805  204   653   86  31%      3  290  148   75  199%
c 
c [simplification-12] limit of 324 iterations hit after 324 iterations
c [quatres-6] found 34618 quaternary clauses 42% in total
c [quatres-6-2] added 1 quaternary resolvents
c [ternres-7] limit 20662876 with penalty 0 = 0 + 0
c [ternres-7] all 76990 free variables schedulable
c [ternres-7] 88 ternary resolvents (0 bin, 88 trn)
c [ternres-7] fully completed ternary resolution
c [decomp-27] removed 484 variables
c [basicprobe-4] limit 103314382 penalty 0 = 0 + 0
c [basicprobe-4-0] 23797 probes remain 31% after last round
c [basicprobe-4-0] 579 units = 563 failed (97%) + 16 lifted (3%)
c [basicprobe-4-0] removed 1396 variables, found 324691 hbrs
c [bate-2] eliminated 210 asymmetric tautologies during probing
c [unhide-12] limit 1033143 with penalty 2 = 0 + 2
c [unhide-12-12] 9 units, 355 failed, 47668 tauts, 0 hbrs, 315134 literals
c [transred-8] limit 2000000 with penalty 0 = 0 + 0
c [transred-8] removed 187 transitive binary clauses
c [transred-8] found 1 units
c [bca-8] limit of 10000000 steps and 1018146 added (scaled 2)
c [bca-8] 107823 out of 150590 literals actually usable 72%
c [bca-8] added 25 blocked clauses in 284614 steps
c [sweep-8] limit 6198862 penalty 0 = 0 + 0
c [sweep-8-1] 8303 pos 13.0% + 55655 neg 87.0% = 63958 sched 84.9% ret 11336
c [sweep-8-1] 6277780 steps 83 queries 5681.12 avg class size
c [sweep-8-1] 1203 decisions 75 SAT calls 169.17 avg env size
c [sweep-8-1] 62633 variables remain 83% (12657 retained 17%)
c [decomp-28] removed 223 variables
c [sweep-8-1] removed 223 vars (0 failed, 8 eqs, 24 impls)
c [sweep-8] removed 223 vars in TOTAL (1 rounds, 82 queries)
c [phase-count-12] 502836 negative 99.0% of 507825 except 4989 1.0%
c [phase-count-12] 404118 positive 79.6% of 507825 except 103707 20.4%
c [phase-count-12] skipping relative phase luck test
c [phase-12] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-12] sorted 14706 enqueued variables after 45202 conflicts
c [score-dist-12] active 60365 (80%), one 0 (0%), zero 14706 (20%)
c [score-dist-12] max exp 509, different 184 (36%)
c [score-dist-12] median active exp 490, avg 476.0
c [simplification-12] removed 1919 variables 2.5% (75071 remain 30%)
c [simplification-12] removed 17426 irredundant clauses 3.3% (507825 remain 37%)
c [simplification-12] maximum reduction of 3% = max (2%, 3%)
c [simplification-12] forced so keeping old conflict interval 19998
c [simplification-12] conflict limit remains at 51767 (hard 61499)
c [simplification-12] new iteration interval 1000
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  142.0   75070   507825     45207   25863   1371 606572  204   653   81  31%      3  289  149   75  199%
c i  142.0   75069   507825     45214   25865   1371 606572  204   652   82  31%      3  289  149   75  200%
c i  142.0   75068   507825     45249   25895   1371 606572  203   648   84  31%      3  285  146   75  196%
c i  142.3   75067   507825     45486   26050   1375 606582  198   628   87  32%      2  263  116   75  155%
c i  142.5   75066   507825     45594   26145   1376 606582  194   627   87  31%      2  263   91   75  122%
c i  142.8   75065   507825     45877   26400   1388 606586  184   633   87  29%      1  267   57   75   77%
c i  143.0   74985   507825     46087   26555   1413 606610  178   635   87  28%      1  268   62   75   83%
c i  143.4   74984   507825     46811   27128   1454 606663  160   668   90  24%      2  298   46   74   61%
c i  143.7   74983   507825     47052   27332   1465 606674  154   656   90  23%      2  285   53   74   71%
c i  144.8   74982   507825     48715   28806   1483 606694  121   863   90  14%     12  483   46   74   63%
c i  145.6   74981   507825     49268   29330   1489 606698  130   941   90  14%      8  556  215   75  288%
c i  146.9   74980   507825     50017   29993   1494 606704  154   950   90  16%      6  559  255   77  330%
c i  147.3   74979   507825     50298   30206   1506 606709  158   939   90  17%      4  546  230   78  296%
c i  147.8   74978   507825     50592   30368   1507 606722  167   911   90  18%      3  515  272   79  345%
c i  148.9   74977   507825     51611   31272   1529 606753  158   903   90  17%      5  500  135   79  171%
c 
c [simplification-13] limit 51770 conflicts (hard 61499) hit after 51772 conflicts
c [quatres-7] found 32989 quaternary clauses 42% in total
c [quatres-7-1] removed 1 duplicate quaternary clauses
c [quatres-7-2] added 1 single-self-subsuming ternary resolvents
c [quatres-7-2] added 1 quaternary resolvents
c [ternres-8] limit 22368686 with penalty 0 = 0 + 0
c [ternres-8] all 74977 free variables schedulable
c [ternres-8] 33 ternary resolvents (0 bin, 33 trn)
c [ternres-8] fully completed ternary resolution
c [decomp-29] removed 98 variables
c [simpleprobe-5] 10641 schedulable variables 14%
c [simpleprobe-5] limit 89474746 penalty 0 = 0 + 0
c [decomp-30] removed 1589 variables
c [simpleprobe-5] 125 variables remain 0% (73259 retained 100%)
c [simpleprobe-5] removed 1589 variables, found 66821 hbrs, 1015 units
c [unhide-13] limit 1118434 with penalty 2 = 0 + 2
c [unhide-13-13] 3 units, 7 failed, 7214 tauts, 0 hbrs, 311240 literals
c [transred-9] limit 2000000 with penalty 0 = 0 + 0
c [transred-9] removed 297 transitive binary clauses
c [elim-10] no untried remaining variables left
c [elim-10] scheduled 73149 variables 100%
c [elim-10] limit of 223686866 steps penalty 1 = 1 + 0
c [elim-10] rescheduling of touched variables disabled
c [elim-10-1] eliminated 1775 variables 2% in round 1 in 42883375 steps
c [elim-10-1] backward subsumption/strengthening limit 42883300
c [elim-10-1-1] backward checking 6634 touched variables 9%
c [elim-10-1-1] fully completed backward checking in 1 rounds
c [elim-10-1] subsumed 39 and strengthened 251 clauses in 2086092 steps
c [elim-10-1] rescheduled 669 variables 1% by backward subsumption
c [elim-10-2] eliminated 88 variables 0% in round 2 in 673689 steps
c [elim-10-2] backward subsumption/strengthening limit 673600
c [elim-10-2-1] backward checking 690 touched variables 1%
c [elim-10-2-1] fully completed backward checking in 1 rounds
c [elim-10-2] subsumed 8 and strengthened 14 clauses in 396330 steps
c [elim-10-2] rescheduled 67 variables 0% by backward subsumption
c [elim-10-3] eliminated 10 variables 0% in round 3 in 151055 steps
c [elim-10-3] backward subsumption/strengthening limit 151000
c [elim-10-3-1] backward checking 91 touched variables 0%
c [elim-10-3-1] incomplete backward checking 0 remain 0%
c [elim-10-3] subsumed 2 and strengthened 10 clauses in 151001 steps
c [elim-10] incomplete 44 not tried 0% in round 3
c [elim-10] transition to [ all 1 rem 1 ] state
c [elim-10] eliminated 1874 = 3% variables out of 73149 scheduled
c [bca-9] limit of 10000000 steps and 950703 added (scaled 2)
c [bca-9] 103609 out of 142552 literals actually usable 73%
c [bca-9] added 45 blocked clauses in 276920 steps
c [sweep-9] limit 6710605 penalty 0 = 0 + 0
c [sweep-9-1] 8855 pos 14.8% + 51115 neg 85.2% = 59970 sched 84.1% ret 11305
c [sweep-9-1] 6874477 steps 98 queries 5216.14 avg class size
c [sweep-9-1] 1364 decisions 71 SAT calls 197.63 avg env size
c [sweep-9-1] 59110 variables remain 83% (12080 retained 17%)
c [decomp-31] removed 115 variables
c [sweep-9-1] removed 115 vars (0 failed, 31 eqs, 49 impls)
c [sweep-9] removed 115 vars in TOTAL (1 rounds, 97 queries)
c [phase-count-13] 469718 negative 99.0% of 474446 except 4728 1.0%
c [phase-count-13] 373822 positive 78.8% of 474446 except 100624 21.2%
c [phase-count-13] skipping relative phase luck test
c [phase-13] phase bias: 0 positive 0%, 0 negative 0%
c [sort-queue-13] sorted 12693 enqueued variables after 51772 conflicts
c [score-dist-13] active 58467 (82%), one 0 (0%), zero 12693 (18%)
c [score-dist-13] max exp 508, different 207 (41%)
c [score-dist-13] median active exp 491, avg 476.3
c [simplification-13] removed 3817 variables 5.1% (71160 remain 29%)
c [simplification-13] removed 33379 irredundant clauses 6.6% (474446 remain 34%)
c [simplification-13] maximum reduction of 7% = max (5%, 7%)
c [simplification-13] large reduction 7% >= 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 63772 (soft 53772 + delta 10000)
c [simplification-13] new conflict limit 53772 (hard 63772)
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  157.1   71159   474446     51938   21577   1448 591791  169   939   71  18%      4  533  216   80  269%
c i  157.1   71156   474446     51939   21577   1448 591791  169   939   71  18%      4  533  215   80  268%
c i  158.3   71155   474446     52715   22150   1465 591814  178   870   72  20%      4  458  142   82  173%
c i  158.3   71154   474446     52792   22195   1467 591821  175   862   72  20%      4  449  118   82  144%
c i  158.5   71153   474446     52891   22282   1470 591821  172   850   72  20%      3  437   90   82  110%
c 
c [simplification-14] limit 53782 conflicts (hard 63772) hit after 53782 conflicts
c [quatres-8] found 31862 quaternary clauses 42% in total
c [quatres-8-2] added 5 quaternary resolvents
c [ternres-9] limit 23012537 with penalty 0 = 0 + 0
c [ternres-9] all 71153 free variables schedulable
c [ternres-9] 253 ternary resolvents (0 bin, 253 trn)
c [ternres-9] fully completed ternary resolution
c [gauss-4] limit 575313 penalty 3 = 3 + 0
c [gauss-4] extracted 8 xors of average arity 3.0
c [gauss-4] connected 24 occurrences of 21 variables (average 1.1)
c [gauss-4] limit 575313 penalty 3 = 3 + 0
c [gauss-4] fully completed
c [gauss-4] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-32] removed 2 variables
c [treelook-5] limit 2301253 penalty 0 = 0 + 0 boost 1
c [treelook-5] scheduled 109466 literals 77%
c [treelook-5] scheduling used 1832499 steps
c [treelook-5] scheduled completely
c [treelook-5] limit 2301253 penalty 0 = 0 + 0 boost 1
c [treelook-5] used 2401091 steps
c [treelook-5] 109431 literals remain 77%
c [treelook-5] 27718 variables remain to probed next time 39%
c [decomp-33] removed 1 variables
c [treelook-5] removed 2 variables, found 12031 hbrs
c [unhide-14] limit 2301253 with penalty 1 = 0 + 1
c [unhide-14-14] 1 units, 93 failed, 40831 tauts, 0 hbrs, 60183 literals
c [transred-10] limit 2000000 with penalty 0 = 0 + 0
c [transred-10] removed 215 transitive binary clauses
c [cce-4] boosting limit by 10
c [cce-4] limit of 143828356 steps penalty 3 = 3 + 0
c [cce-4-1] eliminated 1 clauses out of 495 (0%) of length 8
c [cce-4-1] eliminated 17 clauses out of 709 (2%) of length 7
c [cce-4-1] eliminated 2791 clauses out of 5291 (53%) of length 6
c [cce-4-1] eliminated 13954 clauses out of 33976 (41%) of length 5
c [cce-4-1] incomplete large round (ATE)
c [cce-4-1] eliminated 16763 large clauses in 143828361 steps
c [cce-4-1] allowing another 71914180 steps for small clauses
c [cce-4-1] scheduling 267101 clauses = 246189 binary + 20912 ternary
c [cce-4-1] tried to eliminate 4281 small clauses 2%
c [cce-4-1] eliminated 1062 binary clauses 0%
c [cce-4-1] eliminated 132 ternary clauses 1%
c [cce-4-1] eliminated 1194 small clauses 0%
c [cce-4-1] eliminated 3786 small clauses in 143828366 steps
c [cce-4-1] incomplete small round (ATE)
c [cce-4-1] eliminated 20549 covered clauses in round 1
c [cce-4] eliminated 20549 covered clauses in TOTAL during 1 rounds
c [elim-11] no untried remaining variables left
c [elim-11] scheduled 70992 variables 100%
c [elim-11] limit of 460250741 steps penalty 0 = 0 + 0
c [elim-11] rescheduling of touched variables disabled
c [elim-11-1] eliminated 9049 variables 13% in round 1 in 39471658 steps
c [elim-11-1] backward subsumption/strengthening limit 39471600
c [elim-11-1-1] backward checking 22364 touched variables 32%
c [elim-11-1-1] fully completed backward checking in 1 rounds
c [elim-11-1] subsumed 2 and strengthened 14 clauses in 4046845 steps
c [elim-11-1] rescheduled 59 variables 0% by backward subsumption
c [elim-11-2] eliminated 3 variables 0% in round 2 in 35410 steps
c [elim-11-2] backward subsumption/strengthening limit 35400
c [elim-11-2-1] backward checking 40 touched variables 0%
c [elim-11-2-1] incomplete backward checking 0 remain 0%
c [elim-11-2] subsumed 2 and strengthened 4 clauses in 35401 steps
c [elim-11-2] rescheduled 20 variables 0% by backward subsumption
c [elim-11-3] eliminated 2 variables 0% in round 3 in 22842 steps
c [elim-11-3] backward subsumption/strengthening limit 22800
c [elim-11-3-1] backward checking 20 touched variables 0%
c [elim-11-3-1] incomplete backward checking 0 remain 0%
c [elim-11-3] subsumed 0 and strengthened 4 clauses in 22801 steps
c [elim-11] incomplete 16 not tried 0% in round 3
c [elim-11] transition to [ all 1 rem 1 ] state
c [elim-11] eliminated 9055 = 13% variables out of 70992 scheduled
c [bca-10] limit of 10000000 steps and 863053 added (scaled 2)
c [bca-10] 104598 out of 123876 literals actually usable 84%
c [bca-10] added 348 blocked clauses in 271537 steps
c [sweep-10] limit 6903761 penalty 0 = 0 + 0
c [sweep-10-1] 7954 pos 15.2% + 44332 neg 84.8% = 52286 sched 84.4% ret 9651
c [sweep-10-1] 7086610 steps 112 queries 4721.91 avg class size
c [sweep-10-1] 1358 decisions 100 SAT calls 129.25 avg env size
c [sweep-10-1] 50918 variables remain 82% (10975 retained 18%)
c [decomp-34] removed 79 variables
c [sweep-10-1] removed 79 vars (0 failed, 13 eqs, 23 impls)
c [sweep-10] removed 79 vars in TOTAL (1 rounds, 111 queries)
c [phase-count-14] 429636 negative 99.7% of 430730 except 1094 0.3%
c [phase-count-14] 330489 positive 76.7% of 430730 except 100241 23.3%
c [phase-count-14] skipping relative phase luck test
c [phase-14] phase bias: 0 positive 0%, 2 negative 100%
c [sort-queue-14] sorted 11479 enqueued variables after 53782 conflicts
c [score-dist-14] active 50379 (81%), one 0 (0%), zero 11479 (19%)
c [score-dist-14] max exp 508, different 215 (42%)
c [score-dist-14] median active exp 496, avg 475.9
c [simplification-14] removed 9295 variables 13.1% (61858 remain 25%)
c [simplification-14] removed 43716 irredundant clauses 9.2% (430730 remain 31%)
c [simplification-14] maximum reduction of 13% = max (13%, 9%)
c [simplification-14] large reduction 13% >= 5% limit
c [simplification-14] next conflict interval 2000 = 2000/1
c [simplification-14] penalized conflict interval 2000 = 1 * 2000
c [simplification-14] hard conflict limit 65782 (soft 55782 + delta 10000)
c [simplification-14] new conflict limit 55782 (hard 65782)
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  168.9   61857   430730     53791    6129   1699 527870  160   828   47  19%      4  410  133   82  162%
c i  169.1   61854   430730     53973    6287   1704 527875  156   857   48  18%      3  437  104   82  126%
c i  169.3   61853   430730     54134    6426   1709 527883  153   865   48  18%      3  444   89   82  109%
c i  170.0   61852   430730     55536    7680   1727 527900  125   804   49  16%      9  375   67   82   82%
c i  170.3   61850   430730     55776    7904   1728 527900  125   795   49  16%      7  364  103   82  126%
c 
c [simplification-15] limit 55782 conflicts (hard 65782) hit after 55783 conflicts
c [quatres-9] found 36414 quaternary clauses 58% in total
c [quatres-9-1] removed 1 duplicate quaternary clauses
c [quatres-9-2] added 1 single-self-subsuming ternary resolvents
c [quatres-9-2] added 2 quaternary resolvents
c [ternres-10] limit 23406145 with penalty 0 = 0 + 0
c [ternres-10] all 61850 free variables schedulable
c [ternres-10] 103 ternary resolvents (1 bin, 102 trn)
c [ternres-10] fully completed ternary resolution
c [card-5] limit 731442 penalty 4 = 4 + 0
c [card-5] found 1147 at-most-one constraints of average size 4.0
c [card-5] no at-most-two constraint found
c [card-5] using previous limit 731442 for elimination
c [card-5] 1147 out of 1147 constraints (100%) meet size limits
c [card-5] no units found
c [card-5] no at-most-one constraints generated
c [decomp-35] removed 10 variables
c [basicprobe-5] limit 117030725 penalty 0 = 0 + 0
c [basicprobe-5-0] 14043 probes remain 23% after last round
c [basicprobe-5-0] 788 units = 782 failed (99%) + 6 lifted (1%)
c [basicprobe-5-0] removed 1178 variables, found 437071 hbrs
c [bate-3] eliminated 370 asymmetric tautologies during probing
c [unhide-15] limit 4681229 with penalty 0 = 0 + 0
c [unhide-15-16] 3 units, 93 failed, 59185 tauts, 0 hbrs, 24298 literals
c [transred-11] limit 2000000 with penalty 0 = 0 + 0
c [transred-11] removed 112 transitive binary clauses
c [block-5] scheduling all variables this time
c [block-5] scheduled 60590 variables 100%
c [block-5] limit of 29257681 steps penalty 3 = 3 + 0
c [block-5] fully completed
c [block-5] transition to [ all 0 rem 0 ] state
c [block-5] eliminated 155 blocked clauses
c [block-5] 155 < 1/100 * 416334 = 4163 considered unsuccessful
c [elim-12] no untried remaining variables left
c [elim-12] scheduled 60587 variables 100%
c [elim-12] limit of 468122901 steps penalty 0 = 0 + 0
c [elim-12] rescheduling of touched variables disabled
c [elim-12-1] eliminated 818 variables 1% in round 1 in 35488795 steps
c [elim-12-1] backward subsumption/strengthening limit 35488700
c [elim-12-1-1] backward checking 4113 touched variables 7%
c [elim-12-1-1] fully completed backward checking in 1 rounds
c [elim-12-1] subsumed 17 and strengthened 56 clauses in 1259630 steps
c [elim-12-1] rescheduled 161 variables 0% by backward subsumption
c [elim-12-2] eliminated 21 variables 0% in round 2 in 147856 steps
c [elim-12-2] backward subsumption/strengthening limit 147800
c [elim-12-2-1] backward checking 217 touched variables 0%
c [elim-12-2-1] incomplete backward checking 0 remain 0%
c [elim-12-2] subsumed 5 and strengthened 4 clauses in 147801 steps
c [elim-12-2] rescheduled 25 variables 0% by backward subsumption
c [elim-12-3] eliminated 5 variables 0% in round 3 in 34836 steps
c [elim-12-3] backward subsumption/strengthening limit 34800
c [elim-12-3-1] backward checking 102 touched variables 0%
c [elim-12-3-1] incomplete backward checking 39 remain 38%
c [elim-12-3] subsumed 0 and strengthened 0 clauses in 34841 steps
c [elim-12] fully completed in 3 rounds
c [elim-12] transition to [ all 0 rem 0 ] state
c [elim-12] eliminated 847 = 1% variables out of 60587 scheduled
c [bca-11] limit of 10000000 steps and 826739 added (scaled 2)
c [bca-11] 98971 out of 119482 literals actually usable 83%
c [bca-11] added 77 blocked clauses in 251172 steps
c [sweep-11] boosting sweeping limit by 10
c [sweep-11] limit 70218430 penalty 0 = 0 + 0
c [sweep-11-1] 8067 pos 16.3% + 41400 neg 83.7% = 49467 sched 82.8% ret 10273
c [sweep-11-1] 70223294 steps 1422 queries 296.49 avg class size
c [sweep-11-1] 13174 decisions 1266 SAT calls 85.69 avg env size
c [sweep-11-1] 28399 variables remain 48% (31231 retained 52%)
c [decomp-36] removed 679 variables
c [sweep-11-1] removed 679 vars (0 failed, 184 eqs, 276 impls)
c [sweep-11] removed 679 vars in TOTAL (1 rounds, 1421 queries)
c [sort-queue-15] sorted 9956 enqueued variables after 55783 conflicts
c [score-dist-15] active 49105 (83%), one 0 (0%), zero 9956 (17%)
c [score-dist-15] max exp 508, different 221 (43%)
c [score-dist-15] median active exp 502, avg 484.6
c [simplification-15] removed 2789 variables 4.5% (59061 remain 24%)
c [simplification-15] removed 19688 irredundant clauses 4.6% (411042 remain 30%)
c [simplification-15] maximum reduction of 5% = max (5%, 5%)
c [simplification-15] large reduction 5% >= 5% limit
c [simplification-15] next conflict interval 2000 = 2000/1
c [simplification-15] penalized conflict interval 2000 = 1 * 2000
c [simplification-15] hard conflict limit 67783 (soft 57783 + delta 10000)
c [simplification-15] new conflict limit 57783 (hard 67783)
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  185.6   59060   411042     56199    8240   1905 881504  119   776   56  15%      5  343   62   82   75%
c i  185.8   59058   411042     56629    8624   1908 881514  113   776   56  15%      3  342   52   82   63%
c 
c [simplification-16] limit 57783 conflicts (hard 67783) hit after 57783 conflicts
c [quatres-10] found 33721 quaternary clauses 58% in total
c [quatres-10-2] added 1 single-self-subsuming ternary resolvents
c [quatres-10-2] added 4 quaternary resolvents
c [ternres-11] limit 23687150 with penalty 0 = 0 + 0
c [ternres-11] all 59056 free variables schedulable
c [ternres-11] 266 ternary resolvents (0 bin, 266 trn)
c [ternres-11] fully completed ternary resolution
c [decomp-37] removed 7 variables
c [simpleprobe-6] 118 schedulable variables 0%
c [simpleprobe-6] limit 94748600 penalty 0 = 0 + 0
c [decomp-38] removed 273 variables
c [simpleprobe-6] 2583 variables remain 4% (56198 retained 96%)
c [simpleprobe-6] removed 273 variables, found 62045 hbrs, 209 units
c [unhide-16] limit 4737430 with penalty 0 = 0 + 0
c [unhide-16-18] 6 units, 70 failed, 54875 tauts, 0 hbrs, 31293 literals
c [transred-12] limit 2000000 with penalty 0 = 0 + 0
c [transred-12] removed 134 transitive binary clauses
c [cce-5] limit of 29608937 steps penalty 2 = 2 + 0
c [cce-5-1] eliminated 1 clauses out of 31 (3%) of length 10
c [cce-5-1] eliminated 9 clauses out of 285 (3%) of length 7
c [cce-5-1] eliminated 40 clauses out of 3070 (1%) of length 6
c [cce-5-1] incomplete large round (ACCE)
c [cce-5-1] eliminated 50 large clauses in 29608943 steps
c [cce-5-1] allowing another 14804471 steps for small clauses
c [cce-5-1] scheduling 327911 clauses = 204874 binary + 123037 ternary
c [cce-5-1] tried to eliminate 666 small clauses 0%
c [cce-5-1] eliminated 100 binary clauses 0%
c [cce-5-1] eliminated 54 ternary clauses 0%
c [cce-5-1] eliminated 154 small clauses 0%
c [cce-5-1] eliminated 277 small clauses in 29608945 steps
c [cce-5-1] incomplete small round (ACCE)
c [cce-5-1] eliminated 327 covered clauses in round 1
c [cce-5] eliminated 327 covered clauses in TOTAL during 1 rounds
c [cce-5] 327 < 1/100 * 403553 = 4035 considered unsuccessful
c [elim-13] scheduling all variables this time
c [elim-13] scheduled 58687 variables 100%
c [elim-13] almost no limit of 100000000000 steps
c [elim-13] rescheduling of touched variables disabled
c [elim-13-1] eliminated 919 variables 2% in round 1 in 35197306 steps
c [elim-13-1] backward subsumption/strengthening limit 35197300
c [elim-13-1-1] backward checking 4196 touched variables 7%
c [elim-13-1-1] fully completed backward checking in 1 rounds
c [elim-13-1] subsumed 11 and strengthened 48 clauses in 1339604 steps
c [elim-13-1] rescheduled 163 variables 0% by backward subsumption
c [elim-13-2] eliminated 19 variables 0% in round 2 in 223825 steps
c [elim-13-2] backward subsumption/strengthening limit 223800
c [elim-13-2-1] backward checking 171 touched variables 0%
c [elim-13-2-1] fully completed backward checking in 1 rounds
c [elim-13-2] subsumed 0 and strengthened 9 clauses in 146374 steps
c [elim-13-2] rescheduled 34 variables 0% by backward subsumption
c [elim-13-3] eliminated 4 variables 0% in round 3 in 28054 steps
c [elim-13-3] backward subsumption/strengthening limit 28000
c [elim-13-3-1] backward checking 40 touched variables 0%
c [elim-13-3-1] incomplete backward checking 0 remain 0%
c [elim-13-3] subsumed 1 and strengthened 8 clauses in 28001 steps
c [elim-13] incomplete 31 not tried 0% in round 3
c [elim-13] transition to [ all 1 rem 1 ] state
c [elim-13] eliminated 945 = 2% variables out of 58687 scheduled
c [bca-12] limit of 10000000 steps and 801694 added (scaled 2)
c [bca-12] 93981 out of 115486 literals actually usable 81%
c [bca-12] added 107 blocked clauses in 236592 steps
c [sweep-12] limit 7106145 penalty 0 = 0 + 0
c [sweep-12-1] 5632 pos 20.4% + 21936 neg 79.6% = 27568 sched 47.7% ret 30174
c [sweep-12-1] 7167360 steps 140 queries 2348.08 avg class size
c [sweep-12-1] 1623 decisions 126 SAT calls 99.11 avg env size
c [sweep-12-1] 26910 variables remain 47% (30823 retained 53%)
c [decomp-39] removed 96 variables
c [sweep-12-1] removed 96 vars (0 failed, 15 eqs, 26 impls)
c [sweep-12] removed 96 vars in TOTAL (1 rounds, 139 queries)
c [sort-queue-16] sorted 9557 enqueued variables after 57783 conflicts
c [score-dist-16] active 48089 (83%), one 0 (0%), zero 9557 (17%)
c [score-dist-16] max exp 509, different 230 (45%)
c [score-dist-16] median active exp 495, avg 480.5
c [simplification-16] removed 1410 variables 2.4% (57646 remain 23%)
c [simplification-16] removed 10909 irredundant clauses 2.7% (400133 remain 29%)
c [simplification-16] maximum reduction of 3% = max (2%, 3%)
c [simplification-16] geometric conflict interval increment 5000 = 20000 / 4
c [simplification-16] new conflict interval 24998
c [simplification-16] penalized conflict interval 24998 = 1 * 24998
c [simplification-16] hard conflict limit 95280 (soft 82781 + delta 12499)
c [simplification-16] new conflict limit 82781 (hard 95280)
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  193.7   57645   400133     58350    8850   2052 852522   97   792   56  12%     12  348   62   81   76%
c i  193.9   57644   400133     58744    9209   2061 852522   94   789   56  12%      8  343   59   81   72%
c i  194.2   57637   400133     59592    9939   2071 852527   88   702   56  13%      6  253   70   81   87%
c i  194.7   57633   400133     60487   10692   2083 852543   85   622   57  14%      5  170   65   81   80%
c i  195.1   57632   400133     61151   11211   2107 852581   80   570   58  14%      4  116   48   81   60%
c i  195.1   57631   400133     61159   11218   2107 852581   80   570   58  14%      4  116   47   81   58%
c i  195.4   57630   400133     62011   11964   2118 852588   72   540   59  13%      4   85   36   80   45%
c i  196.0   57561   400133     63084   12903   2145 852614   69   502   60  14%      6   46   94   80  118%
c i  198.2   57557   400133     67083   16373   2220 852683   70   494   64  14%     43   36   70   79   89%
c i  199.4   57556   400133     68588   17714   2261 852699   95   559   66  17%     17   99  240   81  297%
c i  199.4   57555   400133     68590   17715   2261 852699   95   559   66  17%     17   98  239   81  295%
c i  199.4   57554   400133     68669   17766   2264 852701   99   560   68  18%     15  100  255   81  315%
c i  199.7   57553   400133     68924   17969   2265 852704  107   559   68  19%     11   98  222   82  272%
c i  199.9   57552   400133     69094   18124   2265 852709  105   550   69  19%      9   89  148   82  182%
c i  199.9   57551   400133     69126   18151   2265 852709  105   548   69  19%      8   87  141   82  173%
c i  200.5   57487   400133     69722   18693   2278 852717  105   548   69  19%      5   86  128   82  157%
c i  200.6   57480   400133     69931   18896   2278 852717  105   550   69  19%      3   88  123   82  150%
c i  200.6   57477   400133     69961   18923   2278 852717  105   549   69  19%      3   87  121   82  148%
c i  200.7   57476   400133     70330   19244   2283 852720  107   532   69  20%      1   69  116   82  142%
c i  201.1   57475   400133     71196   19969   2302 852725   92   456   69  20%      2   -7   27   81   33%
c i  201.5   57474   400133     71812   20508   2308 852733   94   463   69  20%      1   -0  126   82  154%
c i  201.6   57473   400133     71889   20573   2309 852733   95   464   69  21%      1    2  134   82  164%
c i  201.8   57471   400133     72060   20725   2312 852738   95   465   69  20%      0    2  112   82  138%
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  204.9   57470   400133     76422   23563   2397 852795  104   288   73  36%     46 -167  157   83  189%
c i  206.4   57468   400133     78246   24986   2428 852812  131   386   78  34%     17  -66  129   86  150%
c i  206.4   57466   400133     78248   24986   2428 852812  131   386   78  34%     17  -66  129   86  150%
c i  206.4   57464   400133     78249   24986   2428 852812  131   386   78  34%     17  -66  128   86  150%
c i  206.4   57462   400133     78300   25033   2428 852812  130   387   78  34%     16  -65  119   86  139%
c i  207.8   57461   400133     79802   26305   2441 852827  146   458   79  32%      9    7  264   88  301%
c i  210.2   57415   400133     81911   27716   2459 852835  217   515   81  42%     14   63  400   95  422%
c 
c [simplification-17] limit 82802 conflicts (hard 95280) hit after 82802 conflicts
c [quatres-11] found 32015 quaternary clauses 56% in total
c [quatres-11-2] added 5 quaternary resolvents
c [ternres-12] limit 28463769 with penalty 0 = 0 + 0
c [ternres-12] all 57408 free variables schedulable
c [ternres-12] 226 ternary resolvents (3 bin, 223 trn)
c [ternres-12] fully completed ternary resolution
c [decomp-40] removed 266 variables
c [treelook-6] limit 2846376 penalty 0 = 0 + 0 boost 1
c [treelook-6] scheduled 81927 literals 71%
c [treelook-6] scheduling used 1845501 steps
c [treelook-6] scheduled completely
c [treelook-6] limit 2846376 penalty 0 = 0 + 0 boost 1
c [treelook-6] used 2857240 steps
c [treelook-6] 81872 literals remain 71%
c [treelook-6] 17783 variables remain to probed next time 31%
c [treelook-6] removed 3 variables, found 21684 hbrs
c [unhide-17] limit 2846376 with penalty 1 = 0 + 1
c [unhide-17-20] 12 units, 80 failed, 27010 tauts, 0 hbrs, 459818 literals
c [transred-13] limit 2000000 with penalty 0 = 0 + 0
c [transred-13] removed 149 transitive binary clauses
c [transred-13] found 1 units
c [elim-14] no untried remaining variables left
c [elim-14] scheduled 57257 variables 100%
c [elim-14] limit of 569275389 steps penalty 0 = 0 + 0
c [elim-14] rescheduling of touched variables disabled
c [elim-14-1] eliminated 354 variables 1% in round 1 in 34921483 steps
c [elim-14-1] backward subsumption/strengthening limit 34921400
c [elim-14-1-1] backward checking 1760 touched variables 3%
c [elim-14-1-1] fully completed backward checking in 1 rounds
c [elim-14-1] subsumed 4 and strengthened 14 clauses in 556397 steps
c [elim-14-1] rescheduled 64 variables 0% by backward subsumption
c [elim-14-2] eliminated 7 variables 0% in round 2 in 61499 steps
c [elim-14-2] backward subsumption/strengthening limit 61400
c [elim-14-2-1] backward checking 82 touched variables 0%
c [elim-14-2-1] incomplete backward checking 0 remain 0%
c [elim-14-2] subsumed 4 and strengthened 6 clauses in 61401 steps
c [elim-14-2] rescheduled 30 variables 0% by backward subsumption
c [elim-14-3] eliminated 3 variables 0% in round 3 in 39464 steps
c [elim-14-3] backward subsumption/strengthening limit 39400
c [elim-14-3-1] backward checking 33 touched variables 0%
c [elim-14-3-1] incomplete backward checking 0 remain 0%
c [elim-14-3] subsumed 0 and strengthened 4 clauses in 39401 steps
c [elim-14] incomplete 16 not tried 0% in round 3
c [elim-14] transition to [ all 1 rem 1 ] state
c [elim-14] eliminated 364 = 1% variables out of 57257 scheduled
c [elim-14] 364 < 1/100 * 57257 = 572 considered unsuccessful
c [bca-13] limit of 10000000 steps and 789933 added (scaled 2)
c [bca-13] 83677 out of 113788 literals actually usable 74%
c [bca-13] added 48 blocked clauses in 224966 steps
c [sweep-13] limit 8539130 penalty 0 = 0 + 0
c [sweep-13-1] 5779 pos 21.9% + 20602 neg 78.1% = 26381 sched 46.4% ret 30512
c [sweep-13-1] 8738682 steps 158 queries 1194.26 avg class size
c [sweep-13-1] 2123 decisions 146 SAT calls 120.93 avg env size
c [sweep-13-1] 25473 variables remain 45% (31372 retained 55%)
c [decomp-42] removed 92 variables
c [sweep-13-1] removed 92 vars (0 failed, 14 eqs, 23 impls)
c [sweep-13] removed 92 vars in TOTAL (1 rounds, 157 queries)
c [sort-queue-17] sorted 8987 enqueued variables after 82802 conflicts
c [score-dist-17] active 47814 (84%), one 0 (0%), zero 8987 (16%)
c [score-dist-17] max exp 509, different 319 (63%)
c [score-dist-17] median active exp 467, avg 441.1
c [simplification-17] removed 607 variables 1.1% (56801 remain 23%)
c [simplification-17] removed 6264 irredundant clauses 1.6% (393869 remain 29%)
c [simplification-17] maximum reduction of 2% = max (1%, 2%)
c [simplification-17] geometric conflict interval increment 8332 = 24998 / 3
c [simplification-17] new conflict interval 33330
c [simplification-17] penalized conflict interval 33330 = 1 * 33330
c [simplification-17] hard conflict limit 132797 (soft 116132 + delta 16665)
c [simplification-17] new conflict limit 116132 (hard 132797)
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  218.0   56800   393869     83044   26602   2522 836001  226   542   79  42%      6   89  296   97  303%
c i  218.8   56798   393869     83994   27361   2528 836010  214   498   80  43%      3   43  159   98  161%
c i  218.8   56796   393869     83996   27362   2528 836010  214   498   80  43%      3   43  158   98  160%
c i  218.9   56793   393869     84001   27366   2528 836010  214   497   80  43%      3   43  155   98  158%
c i  219.0   56789   393869     84160   27486   2529 836012  216   497   80  43%      2   43  211   99  213%
c i  219.2   56788   393869     84336   27628   2529 836015  217   498   80  44%      0   43  225   99  227%
c i  221.3   56775   393869     86870   29606   2556 836036  185   469   80  40%     18   13  165  101  163%
c i  223.9   56774   393869     89299   31481   2582 836038  218   570   88  38%     18  113  325  107  305%
c i  224.2   56773   393869     89700   31777   2588 836038  214   572   88  37%     10  114  164  107  153%
c i  225.5   56723   393869     91628   33394   2635 836064  177   574   88  31%     11  113  183  107  171%
c i  225.5   56722   393869     91629   33394   2635 836064  177   574   88  31%     11  113  182  107  170%
c i  225.5   56719   393869     91630   33394   2635 836064  177   574   88  31%     11  112  181  107  169%
c i  225.5   56718   393869     91632   33395   2635 836064  177   574   88  31%     11  112  180  107  168%
c i  225.5   56717   393869     91633   33395   2635 836064  177   573   88  31%     11  112  179  107  167%
c i  227.1   56716   393869     93155   34638   2660 836075  185   640   88  29%      7  176  142  109  129%
c i  227.1   56715   393869     93166   34647   2660 836075  184   639   88  29%      7  174  137  109  125%
c i  230.3   56714   393869     96475   37414   2686 836093  225   699   97  32%     28  225  284  116  244%
c i  230.7   56571   393869     96778   37645   2686 836093  232   695   97  33%     19  220  326  117  278%
c i  237.8   56560   393869    102873   41769   2726 836119  244   560  112  44%     67   73  398  129  308%
c i  242.1   56433   393869    106328   44051   2751 836138  271   554  121  49%     28   63  222  138  161%
c i  242.3   56432   393869    106704   44365   2751 836139  265   541  121  49%     16   50  217  138  157%
c i  242.8   56431   393869    107621   45102   2755 836143  245   489  121  50%      3   -3  149  138  108%
c i  242.9   56430   393869    107919   45312   2756 836144  239   473  121  50%     -0  -19  155  139  112%
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  243.5   56429   393869    109456   46397   2761 836152  196   393  123  50%      1  -97   60  138   43%
c i  244.8   56428   393869    111401   48065   2787 836179  161   494  126  33%      5    6  160  137  117%
c i  245.1   56427   393869    111955   48503   2787 836180  164   470  126  35%     -0  -17  184  137  135%
c i  245.3   56425   393869    112536   48959   2800 836184  157   439  126  36%     -4  -49   96  137   70%
c 
c [simplification-18] limit 116174 conflicts (hard 132797) hit after 116176 conflicts
c [quatres-12] found 31096 quaternary clauses 56% in total
c [quatres-12-2] added 6 single-self-subsuming ternary resolvents
c [quatres-12-2] added 7 quaternary resolvents
c [ternres-13] limit 36063266 with penalty 0 = 0 + 0
c [ternres-13] all 56423 free variables schedulable
c [ternres-13] 161 ternary resolvents (0 bin, 161 trn)
c [ternres-13] fully completed ternary resolution
c [decomp-43] removed 452 variables
c [basicprobe-6] limit 180316334 penalty 0 = 0 + 0
c [basicprobe-6-0] 7312 probes remain 13% after last round
c [basicprobe-6-0] 1120 units = 1113 failed (99%) + 7 lifted (1%)
c [basicprobe-6-0] removed 1512 variables, found 553076 hbrs
c [bate-4] eliminated 430 asymmetric tautologies during probing
c [unhide-18] limit 1803163 with penalty 2 = 0 + 2
c [unhide-18-21] 3 units, 83 failed, 75500 tauts, 0 hbrs, 753259 literals
c [transred-14] limit 2000000 with penalty 0 = 0 + 0
c [transred-14] removed 171 transitive binary clauses
c [transred-14] found 1 units
c [bca-14] limit of 10000000 steps and 753197 added (scaled 2)
c [bca-14] 76005 out of 109548 literals actually usable 69%
c [bca-14] added 29 blocked clauses in 227955 steps
c [sweep-14] limit 10818980 penalty 0 = 0 + 0
c [sweep-14-1] 5397 pos 21.9% + 19239 neg 78.1% = 24636 sched 45.0% ret 30137
c [sweep-14-1] 10823869 steps 194 queries 1391.16 avg class size
c [sweep-14-1] 5823 decisions 176 SAT calls 251.36 avg env size
c [sweep-14-1] 23435 variables remain 43% (31324 retained 57%)
c [decomp-44] removed 161 variables
c [sweep-14-1] removed 161 vars (0 failed, 20 eqs, 36 impls)
c [sweep-14] removed 161 vars in TOTAL (1 rounds, 193 queries)
c [sort-queue-18] sorted 8077 enqueued variables after 116176 conflicts
c [score-dist-18] active 46535 (85%), one 0 (0%), zero 8077 (15%)
c [score-dist-18] max exp 509, different 431 (85%)
c [score-dist-18] median active exp 486, avg 406.8
c [simplification-18] removed 1811 variables 3.2% (54612 remain 22%)
c [simplification-18] removed 18241 irredundant clauses 4.6% (375628 remain 27%)
c [simplification-18] maximum reduction of 5% = max (3%, 5%)
c [simplification-18] large reduction 5% >= 5% limit
c [simplification-18] next conflict interval 2000 = 2000/1
c [simplification-18] penalized conflict interval 2000 = 1 * 2000
c [simplification-18] hard conflict limit 128176 (soft 118176 + delta 10000)
c [simplification-18] new conflict limit 118176 (hard 128176)
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  265.2   54611   375628    116647   51720   3081 1214340  197   523  137  38%     35   38  258  140  184%
c i  266.7   54610   375628    117764   52591   3084 1214350  211   544  137  39%      9   58  235  142  165%
c 
c [simplification-19] limit 118176 conflicts (hard 128176) hit after 118178 conflicts
c [quatres-13] found 30468 quaternary clauses 57% in total
c [quatres-13-1] removed 3 duplicate quaternary clauses
c [quatres-13-2] added 1 single-self-subsuming ternary resolvents
c [quatres-13-2] added 23 quaternary resolvents
c [ternres-14] limit 36676690 with penalty 0 = 0 + 0
c [ternres-14] all 54610 free variables schedulable
c [ternres-14] 67 ternary resolvents (3 bin, 64 trn)
c [ternres-14] fully completed ternary resolution
c [gauss-5] limit 458458 penalty 4 = 4 + 0
c [gauss-5] extracted 9 xors of average arity 3.0
c [gauss-5] connected 27 occurrences of 24 variables (average 1.1)
c [gauss-5] limit 458458 penalty 4 = 4 + 0
c [gauss-5] fully completed
c [gauss-5] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-45] removed 4 variables
c [simpleprobe-7] 2466 schedulable variables 5%
c [simpleprobe-7] limit 146706761 penalty 0 = 0 + 0
c [decomp-46] removed 163 variables
c [simpleprobe-7] 2794 variables remain 5% (51649 retained 95%)
c [simpleprobe-7] removed 163 variables, found 94576 hbrs, 100 units
c [unhide-19] limit 1833834 with penalty 2 = 0 + 2
c [unhide-19-22] 1 units, 10 failed, 4921 tauts, 0 hbrs, 269602 literals
c [transred-15] limit 2000000 with penalty 0 = 0 + 0
c [transred-15] removed 175 transitive binary clauses
c [cce-6] limit of 22922931 steps penalty 3 = 3 + 0
c [cce-6-1] eliminated 1 clauses out of 1 (100%) of length 19
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 18
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 17
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 16
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 15
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 14
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 13
c [cce-6-1] eliminated 2 clauses out of 2 (100%) of length 12
c [cce-6-1] eliminated 1 clauses out of 2 (50%) of length 11
c [cce-6-1] eliminated 3 clauses out of 31 (10%) of length 10
c [cce-6-1] eliminated 1 clauses out of 155 (1%) of length 9
c [cce-6-1] eliminated 2 clauses out of 157 (1%) of length 8
c [cce-6-1] eliminated 2 clauses out of 229 (1%) of length 7
c [cce-6-1] eliminated 18 clauses out of 2829 (1%) of length 6
c [cce-6-1] eliminated 291 clauses out of 15328 (2%) of length 5
c [cce-6-1] incomplete large round (ATE)
c [cce-6-1] eliminated 330 large clauses in 22922937 steps
c [cce-6-1] allowing another 11461468 steps for small clauses
c [cce-6-1] scheduling 301793 clauses = 192678 binary + 109115 ternary
c [cce-6-1] tried to eliminate 620 small clauses 0%
c [cce-6-1] eliminated 103 binary clauses 0%
c [cce-6-1] eliminated 48 ternary clauses 0%
c [cce-6-1] eliminated 151 small clauses 0%
c [cce-6-1] eliminated 362 small clauses in 22922936 steps
c [cce-6-1] incomplete small round (ATE)
c [cce-6-1] eliminated 692 covered clauses in round 1
c [cce-6] eliminated 692 covered clauses in TOTAL during 1 rounds
c [cce-6] 692 < 1/100 * 370637 = 3706 considered unsuccessful
c [elim-15] no untried remaining variables left
c [elim-15] scheduled 54401 variables 100%
c [elim-15] limit of 366766904 steps penalty 1 = 1 + 0
c [elim-15] rescheduling of touched variables disabled
c [elim-15-1] eliminated 1184 variables 2% in round 1 in 32839418 steps
c [elim-15-1] backward subsumption/strengthening limit 32839400
c [elim-15-1-1] backward checking 5996 touched variables 11%
c [elim-15-1-1] fully completed backward checking in 1 rounds
c [elim-15-1] subsumed 20 and strengthened 33 clauses in 1659126 steps
c [elim-15-1] rescheduled 172 variables 0% by backward subsumption
c [elim-15-2] eliminated 20 variables 0% in round 2 in 345715 steps
c [elim-15-2] backward subsumption/strengthening limit 345700
c [elim-15-2-1] backward checking 253 touched variables 0%
c [elim-15-2-1] fully completed backward checking in 1 rounds
c [elim-15-2] subsumed 12 and strengthened 17 clauses in 253268 steps
c [elim-15-2] rescheduled 72 variables 0% by backward subsumption
c [elim-15-3] eliminated 3 variables 0% in round 3 in 121539 steps
c [elim-15-3] backward subsumption/strengthening limit 121500
c [elim-15-3-1] backward checking 39 touched variables 0%
c [elim-15-3-1] fully completed backward checking in 1 rounds
c [elim-15-3] subsumed 0 and strengthened 5 clauses in 111078 steps
c [elim-15] incomplete 20 not tried 0% in round 3
c [elim-15] transition to [ all 1 rem 1 ] state
c [elim-15] eliminated 1207 = 2% variables out of 54401 scheduled
c [bca-15] limit of 10000000 steps and 734016 added (scaled 2)
c [bca-15] 75641 out of 106390 literals actually usable 71%
c [bca-15] added 28 blocked clauses in 210871 steps
c [sweep-15] limit 11003007 penalty 0 = 0 + 0
c [sweep-15-1] 5172 pos 22.6% + 17686 neg 77.4% = 22858 sched 43.0% ret 30336
c [sweep-15-1] 11043896 steps 223 queries 1156.11 avg class size
c [sweep-15-1] 4348 decisions 196 SAT calls 124.38 avg env size
c [sweep-15-1] 21720 variables remain 41% (31355 retained 59%)
c [decomp-47] removed 208 variables
c [sweep-15-1] removed 208 vars (0 failed, 30 eqs, 40 impls)
c [sweep-15] removed 208 vars in TOTAL (1 rounds, 222 queries)
c [sort-queue-19] sorted 7621 enqueued variables after 118178 conflicts
c [score-dist-19] active 45365 (86%), one 0 (0%), zero 7621 (14%)
c [score-dist-19] max exp 509, different 434 (85%)
c [score-dist-19] median active exp 486, avg 406.3
c [simplification-19] removed 1624 variables 3.0% (52986 remain 21%)
c [simplification-19] removed 10303 irredundant clauses 2.7% (365325 remain 27%)
c [simplification-19] maximum reduction of 3% = max (3%, 3%)
c [simplification-19] geometric conflict interval increment 8332 = 33330 / 4
c [simplification-19] new conflict interval 41662
c [simplification-19] penalized conflict interval 41662 = 1 * 41662
c [simplification-19] hard conflict limit 180671 (soft 159840 + delta 20831)
c [simplification-19] new conflict limit 159840 (hard 180671)
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  278.3   52985   365325    118766   35029   2844 1174564  222   541   91  41%      0   54  280  144  194%
c i  280.0   52982   365325    120613   36484   2872 1174573  199   542   91  37%      4   54  156  145  108%
c i  280.0   52789   365325    120625   36494   2872 1174573  199   541   91  37%      3   53  158  145  109%
c i  281.5   52783   365325    123865   39323   2902 1174585  134   565   91  24%     21   74  106  142   75%
c i  281.5   52782   365325    123901   39350   2902 1174587  134   565   91  24%     20   74  103  142   72%
c i  281.5   52778   365325    123916   39360   2902 1174587  133   565   91  24%     20   75  102  141   72%
c i  282.2   52738   365325    125063   40293   2922 1174601  125   549   91  23%      4   57   95  141   68%
c i  283.2   52737   365325    126057   41117   2930 1174614  157   581   93  27%     -2   88  377  143  265%
c i  283.4   52736   365325    126296   41309   2934 1174623  169   585   93  29%     -4   92  374  143  261%
c i  284.9   52735   365325    127496   42191   2944 1174626  252   687  103  37%     -4  191  535  150  358%
c i  289.6   52734   365325    131763   45611   2982 1174648  311   806  111  39%     36  290  328  162  202%
c i  289.7   52733   365325    131820   45645   2982 1174648  311   801  111  39%     33  285  327  162  202%
c i  290.0   52732   365325    132110   45877   2988 1174651  304   770  111  39%     22  253  236  163  145%
c i  290.5   52730   365325    132737   46418   2997 1174656  289   748  111  39%      7  229  201  163  124%
c i  291.1   52729   365325    133319   46861   2999 1174656  294   737  111  40%     -1  216  315  164  192%
c i  291.7   52728   365325    133947   47349   3004 1174658  298   721  111  41%     -5  198  344  166  208%
c i  292.1   52717   365325    134181   47507   3004 1174659  304   714  111  43%     -7  190  387  167  233%
c i  292.4   52716   365325    134523   47786   3006 1174662  296   690  111  43%     -8  166  235  167  141%
c i  294.6   52711   365325    136449   49291   3035 1174665  304   690  116  44%      2  161  345  171  202%
c i  295.7   52710   365325    137184   49763   3039 1174665  327   708  116  46%     -3  177  417  174  240%
c -  306.7   52710   365325    145993   25077   3088 1174708  390   753   66  52%    101  193  423  200  212%
c i  307.3   52709   365325    146518   25487   3090 1174708  389   755   73  52%    108  193  407  201  202%
c i  307.6   52708   365325    146695   25611   3091 1174708  388   750   74  52%     88  187  381  202  189%
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  307.9   52706   365325    147032   25853   3093 1174709  384   740   75  52%     58  176  355  202  176%
c i  309.7   52705   365325    148520   26770   3098 1174717  366   697   76  53%      7  130  382  205  187%
c i  311.1   52696   365325    149601   27510   3100 1174722  386   725   81  53%     -6  155  528  209  253%
c i  314.4   52661   365325    152683   29369   3119 1174739  314   577   87  54%     11    4  296  211  140%
c i  315.3   52658   365325    153577   29927   3124 1174744  305   559   87  55%     -4  -14  277  212  131%
c i  316.7   52657   365325    155295   30803   3146 1174758  273   472   88  58%     -5 -100  148  212   70%
c i  317.0   52602   365325    156309   31533   3154 1174764  237   426   88  56%    -10 -143  134  210   64%
c i  317.1   52554   365325    156465   31682   3156 1174764  229   424   88  54%    -11 -145   82  210   39%
c i  319.3   52548   365325    162717   36534   3197 1174781  142   358  100  40%     58 -196  175  202   87%
c i  319.6   52547   365325    163476   36999   3197 1174781  134   323  100  42%     19 -230   83  200   41%
c i  320.7   52546   365325    166544   39251   3244 1174829   88   261  104  34%     11 -278   26  194   13%
c i  320.9   52545   365325    166950   39454   3245 1174830   93   256  104  36%      1 -281  119  193   62%
c i  324.6   52543   365325    171984   43073   3273 1174868  165   415  109  40%     38 -105  256  192  133%
c i  325.5   52512   365325    173518   44362   3300 1174870  156   437  109  36%      1  -81  104  191   55%
c i  326.5   52510   365325    174638   45151   3313 1174877  139   388  109  36%     -9 -128   64  189   34%
c i  326.5   52507   365325    174653   45162   3313 1174877  139   388  109  36%    -10 -128   67  189   36%
c i  326.5   52504   365325    174661   45169   3313 1174877  139   388  109  36%    -10 -128   69  189   37%
c 
c [simplification-20] limit 159841 conflicts (hard 180671) hit after 177051 conflicts
c [quatres-14] found 28586 quaternary clauses 55% in total
c [quatres-14-2] added 4 single-self-subsuming ternary resolvents
c [quatres-14-2] added 1 quaternary resolvents
c [ternres-15] limit 48949882 with penalty 0 = 0 + 0
c [ternres-15] all 52504 free variables schedulable
c [ternres-15] 267 ternary resolvents (1 bin, 266 trn)
c [ternres-15] fully completed ternary resolution
c [decomp-48] removed 566 variables
c [treelook-7] limit 4894988 penalty 0 = 0 + 0 boost 1
c [treelook-7] scheduled 73893 literals 70%
c [treelook-7] scheduling used 2112442 steps
c [treelook-7] scheduled completely
c [treelook-7] limit 4894988 penalty 0 = 0 + 0 boost 1
c [treelook-7] used 4921577 steps
c [treelook-7] 73799 literals remain 70%
c [treelook-7] 15405 variables remain to probed next time 29%
c [decomp-49] removed 2 variables
c [treelook-7] removed 11 variables, found 18725 hbrs
c [unhide-20] limit 2447494 with penalty 2 = 0 + 2
c [unhide-20-23] 0 units, 35 failed, 63974 tauts, 0 hbrs, 555343 literals
c [transred-16] limit 2000000 with penalty 0 = 0 + 0
c [transred-16] removed 97 transitive binary clauses
c [block-6] scheduling all variables this time
c [block-6] scheduled 52364 variables 100%
c [block-6] limit of 30593676 steps penalty 4 = 4 + 0
c [block-6] fully completed
c [block-6] transition to [ all 0 rem 0 ] state
c [block-6] eliminated 58 blocked clauses
c [block-6] 58 < 1/100 * 361402 = 3614 considered unsuccessful
c [elim-16] no untried remaining variables left
c [elim-16] scheduled 52361 variables 100%
c [elim-16] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-16] rescheduling of touched variables disabled
c [elim-16-1] eliminated 535 variables 1% in round 1 in 32460974 steps
c [elim-16-1] backward subsumption/strengthening limit 32460900
c [elim-16-1-1] backward checking 2575 touched variables 5%
c [elim-16-1-1] fully completed backward checking in 1 rounds
c [elim-16-1] subsumed 6 and strengthened 35 clauses in 812756 steps
c [elim-16-1] rescheduled 98 variables 0% by backward subsumption
c [elim-16-2] eliminated 9 variables 0% in round 2 in 295542 steps
c [elim-16-2] backward subsumption/strengthening limit 295500
c [elim-16-2-1] backward checking 108 touched variables 0%
c [elim-16-2-1] fully completed backward checking in 1 rounds
c [elim-16-2] subsumed 7 and strengthened 11 clauses in 159653 steps
c [elim-16-2] rescheduled 47 variables 0% by backward subsumption
c [elim-16-3] eliminated 1 variables 0% in round 3 in 240367 steps
c [elim-16-3] backward subsumption/strengthening limit 240300
c [elim-16-3-1] backward checking 21 touched variables 0%
c [elim-16-3-1] fully completed backward checking in 1 rounds
c [elim-16-3] subsumed 0 and strengthened 2 clauses in 96868 steps
c [elim-16] incomplete 8 not tried 0% in round 3
c [elim-16] transition to [ all 1 rem 1 ] state
c [elim-16] eliminated 549 = 1% variables out of 52361 scheduled
c [bca-16] limit of 10000000 steps and 720864 added (scaled 2)
c [bca-16] 70531 out of 103626 literals actually usable 68%
c [bca-16] added 19 blocked clauses in 201195 steps
c [sweep-16] limit 14684964 penalty 0 = 0 + 0
c [sweep-16-1] 5451 pos 26.1% + 15424 neg 73.9% = 20875 sched 40.3% ret 30937
c [sweep-16-1] 14736854 steps 278 queries 661.37 avg class size
c [sweep-16-1] 4765 decisions 257 SAT calls 116.83 avg env size
c [sweep-16-1] 19324 variables remain 37% (32380 retained 63%)
c [decomp-50] removed 143 variables
c [sweep-16-1] removed 143 vars (0 failed, 21 eqs, 35 impls)
c [sweep-16] removed 143 vars in TOTAL (1 rounds, 277 queries)
c [sort-queue-20] sorted 9090 enqueued variables after 177051 conflicts
c [score-dist-20] active 42579 (82%), one 2012 (4%), zero 7078 (14%)
c [score-dist-20] max exp 509, different 464 (91%)
c [score-dist-20] median active exp 476, avg 440.3
c [simplification-20] removed 835 variables 1.6% (51669 remain 21%)
c [simplification-20] removed 6164 irredundant clauses 1.7% (359161 remain 26%)
c [simplification-20] maximum reduction of 2% = max (2%, 2%)
c [simplification-20] geometric conflict interval increment 13887 = 41662 / 3
c [simplification-20] new conflict interval 55549
c [simplification-20] penalized conflict interval 55549 = 1 * 55549
c [simplification-20] hard conflict limit 260374 (soft 232600 + delta 27774)
c [simplification-20] new conflict limit 232600 (hard 260374)
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  336.8   51668   359161    177764   41270   3293 1090478  224   570   97  39%     10   55  425  194  219%
c i  342.7   51666   359161    184305   45608   3332 1090511  257   591  100  43%     60   78  458  199  231%
c i  343.2   51664   359161    184701   45937   3332 1090513  283   640  107  44%     33  126  495  201  247%
c i  343.9   51663   359161    185387   46549   3334 1090515  292   733  113  40%      7  218  392  202  194%
c i  344.4   51662   359161    185833   46945   3334 1090515  295   783  113  38%     -4  266  342  203  168%
c i  349.6   51661   359161    190859   50724   3354 1090551  299   697  114  43%     36  157  224  213  105%
c i  349.8   51659   359161    190963   50759   3359 1090553  301   692  114  43%     30  152  282  213  132%
c i  350.6   51658   359161    191370   50949   3359 1090554  304   669  114  45%     12  129  328  214  154%
c i  355.3   51657   359161    197220   54987   3390 1090583  239   653  144  37%     47  105  245  216  113%
c i  355.5   51656   359161    197484   55206   3394 1090584  241   673  144  36%     30  125  272  216  126%
c i  355.5   51655   359161    197533   55252   3394 1090584  241   677  144  36%     28  129  265  216  123%
c i  355.7   51654   359161    197698   55395   3396 1090585  237   674  152  35%     19  125  207  216   96%
c i  356.5   51652   359161    198928   56371   3411 1090593  223   637  152  35%     -6   86  242  215  112%
c -  358.0   51652   359161    201534   28857   3439 1090615  178   449   64  40%     -0 -102   50  212   24%
c i  358.2   51651   359161    202326   29514   3445 1090618  153   395   72  39%     10 -154   46  210   22%
c i  364.5   51650   359161    214466   38507   3532 1090750  166   451   84  37%    136  -73  174  199   87%
c i  366.4   51649   359161    216802   40227   3540 1090761  191   492   87  39%      1  -29  234  200  117%
c i  366.4   51648   359161    216826   40249   3540 1090761  190   490   87  39%     -0  -30  220  200  110%
c i  366.4   51647   359161    216827   40249   3540 1090761  190   490   87  39%     -0  -31  220  200  110%
c i  366.5   51646   359161    216830   40251   3540 1090761  190   490   87  39%     -1  -31  218  200  109%
c i  367.7   51645   359161    218651   41679   3553 1090767  181   499   91  36%    -17  -21  117  199   59%
c i  367.7   51644   359161    218653   41680   3553 1090767  181   499   91  36%    -17  -21  116  199   58%
c i  369.1   51643   359161    220886   43467   3569 1090781  181   564   93  32%    -15   44  273  198  138%
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  369.8   51642   359161    221563   43988   3580 1090781  188   563  101  33%    -23   44  177  198   89%
c i  370.0   51641   359161    221855   44241   3581 1090786  188   574  101  33%    -26   55  191  198   96%
c i  373.5   51640   359161    224484   45790   3594 1090829  204   496  101  41%    -10  -25  146  200   73%
c i  384.0   51639   359161    231834   49540   3622 1090850  206   363  123  57%     61 -146  140  201   70%
c i  401.8   51637   359161    243544   54741   3651 1090891  171   244  137  70%    121 -227  169  195   87%
c i  404.5   51636   359161    245441   55809   3656 1090899  202   302  137  67%     -5 -164  314  197  159%
c i  406.5   51635   359161    246865   56531   3669 1090907  186   282  137  66%    -26 -180  151  196   77%
c i  406.5   51634   359161    246867   56532   3669 1090907  186   282  137  66%    -26 -180  150  196   76%
c i  407.1   51633   359161    248012   57377   3675 1090912  182   318  137  57%    -32 -141  117  196   60%
c -  409.7   51633   359161    251421   31020   3692 1090919  207   428   65  48%     -7  -25  303  196  154%
c 
c [simplification-21] limit 232623 conflicts (hard 260374) hit after 251863 conflicts
c [quatres-15] found 28355 quaternary clauses 53% in total
c [quatres-15-2] added 3 quaternary resolvents
c [ternres-16] limit 67210313 with penalty 0 = 0 + 0
c [ternres-16] all 51633 free variables schedulable
c [ternres-16] 205 ternary resolvents (0 bin, 205 trn)
c [ternres-16] fully completed ternary resolution
c [card-6] limit 2100322 penalty 4 = 4 + 0
c [card-6] found 1451 at-most-one constraints of average size 3.9
c [card-6] no at-most-two constraint found
c [card-6] using previous limit 2100322 for elimination
c [card-6] 1451 out of 1451 constraints (100%) meet size limits
c [card-6] no units found
c [card-6] no at-most-one constraints generated
c [decomp-51] removed 68 variables
c [basicprobe-7] limit 336051566 penalty 0 = 0 + 0
c [basicprobe-7-0] 7725 sched 15%, 1126 failed, 14 lifted, 565569 hbrs
c [decomp-52] removed 1483 variables
c [basicprobe-7-1] 8808 probes remain 18% after last round
c [basicprobe-7-1] 1385 units = 1371 failed (99%) + 14 lifted (1%)
c [basicprobe-7-1] removed 1985 variables, found 777320 hbrs
c [bate-5] eliminated 520 asymmetric tautologies during probing
c [unhide-21] limit 6721031 with penalty 1 = 0 + 1
c [unhide-21-25] 1 units, 22 failed, 121504 tauts, 0 hbrs, 80510 literals
c [transred-17] limit 2000000 with penalty 0 = 0 + 0
c [transred-17] removed 115 transitive binary clauses
c [elim-17] no untried remaining variables left
c [elim-17] scheduled 49595 variables 100%
c [elim-17] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-17] rescheduling of touched variables disabled
c [elim-17-1] eliminated 936 variables 2% in round 1 in 30414023 steps
c [elim-17-1] backward subsumption/strengthening limit 30414000
c [elim-17-1-1] backward checking 5409 touched variables 11%
c [elim-17-1-1] fully completed backward checking in 1 rounds
c [elim-17-1] subsumed 11 and strengthened 40 clauses in 1519074 steps
c [elim-17-1] rescheduled 143 variables 0% by backward subsumption
c [elim-17-2] eliminated 11 variables 0% in round 2 in 201391 steps
c [elim-17-2] backward subsumption/strengthening limit 201300
c [elim-17-2-1] backward checking 127 touched variables 0%
c [elim-17-2-1] fully completed backward checking in 1 rounds
c [elim-17-2] subsumed 0 and strengthened 8 clauses in 135516 steps
c [elim-17-2] rescheduled 32 variables 0% by backward subsumption
c [elim-17-3] eliminated 4 variables 0% in round 3 in 34881 steps
c [elim-17-3] backward subsumption/strengthening limit 34800
c [elim-17-3-1] backward checking 40 touched variables 0%
c [elim-17-3-1] incomplete backward checking 0 remain 0%
c [elim-17-3] subsumed 0 and strengthened 8 clauses in 34801 steps
c [elim-17] incomplete 32 not tried 0% in round 3
c [elim-17] transition to [ all 1 rem 1 ] state
c [elim-17] eliminated 951 = 2% variables out of 49595 scheduled
c [bca-17] limit of 10000000 steps and 670889 added (scaled 2)
c [bca-17] 67871 out of 97290 literals actually usable 70%
c [bca-17] added 26 blocked clauses in 181669 steps
c [sweep-17] limit 20163094 penalty 0 = 0 + 0
c [sweep-17-1] 4586 pos 24.8% + 13918 neg 75.2% = 18504 sched 38.0% ret 30140
c [sweep-17-1] 20208763 steps 549 queries 495.39 avg class size
c [sweep-17-1] 6295 decisions 503 SAT calls 79.85 avg env size
c [sweep-17-1] 15810 variables remain 33% (32729 retained 67%)
c [decomp-53] removed 197 variables
c [sweep-17-1] removed 197 vars (0 failed, 48 eqs, 83 impls)
c [sweep-17] removed 197 vars in TOTAL (1 rounds, 548 queries)
c [sort-queue-21] sorted 9375 enqueued variables after 251863 conflicts
c [score-dist-21] active 39072 (81%), one 3635 (8%), zero 5740 (12%)
c [score-dist-21] max exp 510, different 433 (85%)
c [score-dist-21] median active exp 497, avg 423.5
c [simplification-21] removed 3186 variables 6.2% (48447 remain 20%)
c [simplification-21] removed 25920 irredundant clauses 7.2% (333241 remain 24%)
c [simplification-21] maximum reduction of 7% = max (6%, 7%)
c [simplification-21] large reduction 7% >= 5% limit
c [simplification-21] next conflict interval 2518 = min (251863/100, 55549)
c [simplification-21] penalized conflict interval 2518 = 1 * 2518
c [simplification-21] hard conflict limit 264381 (soft 254381 + delta 10000)
c [simplification-21] new conflict limit 254381 (hard 264381)
c 
c [simplification-22] limit 254381 conflicts (hard 264381) hit after 254381 conflicts
c [quatres-16] found 30048 quaternary clauses 57% in total
c [quatres-16-2] added 3 quaternary resolvents
c [ternres-17] limit 67833774 with penalty 0 = 0 + 0
c [ternres-17] all 48447 free variables schedulable
c [ternres-17] 368 ternary resolvents (1 bin, 367 trn)
c [ternres-17] fully completed ternary resolution
c [simpleprobe-8] 2236 schedulable variables 5%
c [simpleprobe-8] limit 200000000 penalty 0 = 0 + 0
c [decomp-55] removed 57 variables
c [simpleprobe-8] 1388 variables remain 3% (47002 retained 97%)
c [simpleprobe-8] removed 57 variables, found 79850 hbrs, 32 units
c [unhide-22] limit 6783377 with penalty 1 = 0 + 1
c [unhide-22-27] 0 units, 6 failed, 80074 tauts, 0 hbrs, 151754 literals
c [transred-18] limit 2000000 with penalty 0 = 0 + 0
c [transred-18] removed 105 transitive binary clauses
c [elim-18] no untried remaining variables left
c [elim-18] scheduled 48379 variables 100%
c [elim-18] boosting limit by 20
c [elim-18] limit of 16000000000 steps penalty 0 = 0 + 0
c [elim-18] rescheduling of touched variables disabled
c [elim-18-1] eliminated 187 variables 0% in round 1 in 30806399 steps
c [elim-18-1] backward subsumption/strengthening limit 30806300
c [elim-18-1-1] backward checking 1162 touched variables 2%
c [elim-18-1-1] fully completed backward checking in 1 rounds
c [elim-18-1] subsumed 5 and strengthened 20 clauses in 394463 steps
c [elim-18-1] rescheduled 77 variables 0% by backward subsumption
c [elim-18-2] eliminated 7 variables 0% in round 2 in 95840 steps
c [elim-18-2] backward subsumption/strengthening limit 95800
c [elim-18-2-1] backward checking 80 touched variables 0%
c [elim-18-2-1] fully completed backward checking in 1 rounds
c [elim-18-2] subsumed 0 and strengthened 3 clauses in 81753 steps
c [elim-18-2] rescheduled 12 variables 0% by backward subsumption
c [elim-18-3] eliminated 1 variables 0% in round 3 in 20634 steps
c [elim-18-3] backward subsumption/strengthening limit 20600
c [elim-18-3-1] backward checking 10 touched variables 0%
c [elim-18-3-1] incomplete backward checking 0 remain 0%
c [elim-18-3] subsumed 0 and strengthened 2 clauses in 20601 steps
c [elim-18] incomplete 8 not tried 0% in round 3
c [elim-18] transition to [ all 1 rem 1 ] state
c [elim-18] eliminated 195 = 0% variables out of 48379 scheduled
c [elim-18] 195 < 1/100 * 48379 = 483 considered unsuccessful
c [bca-18] limit of 10000000 steps and 660888 added (scaled 2)
c [bca-18] 67495 out of 96370 literals actually usable 70%
c [bca-18] added 29 blocked clauses in 181087 steps
c [sweep-18] almost no limit of 4000000000 steps
c [sweep-18-1] 3754 pos 23.9% + 11934 neg 76.1% = 15688 sched 32.6% ret 32496
c [sweep-18-1] 144013607 steps 5342 queries 30.05 avg class size
c [sweep-18-1] 36422 decisions 4561 SAT calls 56.92 avg env size
c [sweep-18-1] fully completed sweeping round
c [decomp-56] removed 902 variables
c [sweep-18-1] removed 902 vars (1 failed, 786 eqs, 1022 impls)
c [sweep-18-2] 7750 pos 16.4% + 39532 neg 83.6% = 47282 sched 100.0% ret 0
c [sweep-18-2] 217497253 steps 6113 queries 43.93 avg class size
c [sweep-18-2] 55918 decisions 5879 SAT calls 79.33 avg env size
c [sweep-18-2] fully completed sweeping round
c [decomp-57] removed 274 variables
c [sweep-18-2] removed 274 vars (0 failed, 239 eqs, 667 impls)
c [sweep-18-3] 7738 pos 16.5% + 39270 neg 83.5% = 47008 sched 100.0% ret 0
c [sweep-18-3] 225705998 steps 5951 queries 49.72 avg class size
c [sweep-18-3] 58189 decisions 5839 SAT calls 81.93 avg env size
c [sweep-18-3] fully completed sweeping round
c [decomp-58] removed 141 variables
c [sweep-18-3] removed 141 vars (0 failed, 130 eqs, 484 impls)
c [sweep-18] removed 1317 vars in TOTAL (3 rounds, 17403 queries)
c [sort-queue-22] sorted 8147 enqueued variables after 254381 conflicts
c [score-dist-22] active 38720 (83%), one 2836 (6%), zero 5311 (11%)
c [score-dist-22] max exp 511, different 389 (76%)
c [score-dist-22] median active exp 503, avg 465.9
c [simplification-22] removed 1580 variables 3.3% (46867 remain 19%)
c [simplification-22] removed 6095 irredundant clauses 1.8% (327146 remain 24%)
c [simplification-22] maximum reduction of 3% = max (3%, 2%)
c [simplification-22] geometric conflict interval increment 13887 = 55549 / 4
c [simplification-22] new conflict interval 69436
c [simplification-22] penalized conflict interval 69436 = 1 * 69436
c [simplification-22] hard conflict limit 358535 (soft 323817 + delta 34718)
c [simplification-22] new conflict limit 323817 (hard 358535)
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  469.5   46866   327146    255942   31824   3815 1482495  314   669   84  47%     61  209  528  206  256%
c i  470.3   46865   327146    256820   32443   3823 1482497  329   706   84  47%      3  244  252  209  121%
c i  470.5   46856   327146    257248   32795   3823 1482498  311   726   84  43%    -13  262  179  208   86%
c i  471.1   46855   327146    257731   33065   3823 1482500  339   744   84  46%    -24  279  445  211  211%
c i  472.0   46853   327146    258464   33587   3828 1482503  348   747   89  47%    -32  278  311  213  146%
c i  472.0   46852   327146    258473   33594   3828 1482503  348   746   89  47%    -32  277  306  213  144%
c i  472.0   46851   327146    258482   33602   3828 1482503  347   745   89  47%    -32  277  299  213  141%
c i  472.2   46850   327146    258717   33799   3830 1482504  331   723   89  46%    -35  253  153  212   72%
c i  473.7   46848   327146    261388   36076   3848 1482507  267   714   94  37%    -17  234  149  212   70%
c i  473.8   46847   327146    261393   36080   3848 1482507  267   714   94  37%    -18  234  147  212   69%
c i  473.9   46840   327146    261782   36405   3850 1482511  259   709   94  37%    -25  228  173  211   82%
c i  473.9   46839   327146    261784   36406   3850 1482511  259   709   94  37%    -25  228  171  211   81%
c i  473.9   46838   327146    261785   36406   3850 1482511  259   709   94  37%    -25  228  171  211   81%
c i  476.0   46837   327146    265085   38505   3861 1482513  212   507  100  42%     -7   21  179  209   86%
c i  476.8   46836   327146    266318   39227   3863 1482514  214   477  100  45%    -24   -9  238  210  113%
c i  476.9   46835   327146    266402   39302   3863 1482517  212   479  100  44%    -26   -8  191  209   91%
c i  476.9   46834   327146    266424   39321   3863 1482517  211   479  100  44%    -26   -8  190  209   90%
c i  476.9   46833   327146    266502   39393   3863 1482517  210   479  100  44%    -27   -8  181  209   86%
c i  477.3   46832   327146    267099   39839   3870 1482523  210   480  101  44%    -32   -6  212  209  101%
c i  477.3   46831   327146    267248   39949   3873 1482523  208   472  101  44%    -33  -15  176  209   84%
c i  478.1   46830   327146    268160   40540   3875 1482524  195   432  102  45%    -34  -54  159  208   76%
c i  482.8   46829   327146    275323   46012   3932 1482572  219   584  115  37%     53  102  360  206  175%
c i  483.6   46826   327146    275928   46481   3939 1482573  232   608  115  38%     12  124  310  207  150%
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  484.2   46825   327146    276437   46896   3940 1482576  237   622  119  38%     -8  138  249  207  120%
c i  491.1   46824   327146    283525   52122   3967 1482607  339   741  132  46%     51  241  268  220  122%
c i  495.8   46823   327146    288319   55256   3978 1482622  290   561  132  52%     16   47  141  226   62%
c i  496.1   46821   327146    288660   55480   3978 1482622  285   548  132  52%      0   34  219  226   97%
c i  496.1   46820   327146    288662   55481   3978 1482622  285   548  132  52%     -0   34  220  226   98%
c i  497.6   46819   327146    289824   56320   3981 1482623  318   612  157  52%    -22   97  458  229  200%
c i  497.6   46818   327146    289826   56321   3981 1482623  318   612  157  52%    -22   97  456  229  199%
c i  497.6   46817   327146    289827   56321   3981 1482623  318   612  157  52%    -22   96  454  229  198%
c i  500.6   46816   327146    292362   57919   3986 1482627  369   661  157  56%    -16  142  563  236  239%
c i  503.3   46815   327146    294037   59014   3988 1482628  425   752  157  56%    -23  228  423  243  174%
c i  509.1   46814   327146    298508   61302   3990 1482633  380   627  176  61%     13   93  353  251  140%
c i  509.3   46813   327146    298722   61476   3992 1482634  375   633  176  59%      4   99  311  252  124%
c i  509.3   46812   327146    298723   61476   3992 1482634  375   633  176  59%      3   99  310  252  123%
c i  509.3   46811   327146    298724   61476   3992 1482634  375   633  176  59%      3   99  309  252  123%
c i  511.5   46810   327146    300625   62664   4001 1482634  397   672  184  59%    -17  135  326  257  127%
c i  511.9   46809   327146    300914   62889   4002 1482635  397   682  184  58%    -22  144  395  257  153%
c -  512.3   46809   327146    301119   31857   4002 1482635  404   680   71  59%    -25  142  478  258  185%
c i  515.2   46808   327146    304324   33757   4027 1482651  270   465   80  58%     -1  -76   45  254   18%
c i  516.6   46807   327146    305930   34675   4031 1482653  223   382   83  58%    -19 -156   97  251   39%
c 
c [simplification-23] limit 323876 conflicts (hard 358535) hit after 337606 conflicts
c [quatres-17] found 29965 quaternary clauses 55% in total
c [quatres-17-2] added 6 single-self-subsuming ternary resolvents
c [quatres-17-2] added 6 quaternary resolvents
c [ternres-18] limit 85394748 with penalty 0 = 0 + 0
c [ternres-18] all 46807 free variables schedulable
c [ternres-18] 182 ternary resolvents (1 bin, 181 trn)
c [ternres-18] fully completed ternary resolution
c [decomp-59] removed 66 variables
c [treelook-8] limit 8539474 penalty 0 = 0 + 0 boost 1
c [treelook-8] scheduled 66234 literals 71%
c [treelook-8] scheduling used 2425833 steps
c [treelook-8] scheduled completely
c [treelook-8] limit 8539474 penalty 0 = 0 + 0 boost 1
c [treelook-8] used 8569210 steps
c [treelook-8] 66015 literals remain 71%
c [treelook-8] 13563 variables remain to probed next time 29%
c [treelook-8] removed 2 variables, found 24637 hbrs
c [unhide-23] limit 4269737 with penalty 2 = 0 + 2
c [unhide-23-29] 3 units, 47 failed, 117201 tauts, 0 hbrs, 1318470 literals
c [transred-19] limit 2000000 with penalty 0 = 0 + 0
c [transred-19] removed 119 transitive binary clauses
c [cce-7] limit of 26685858 steps penalty 4 = 4 + 0
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 102
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 101
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 100
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 99
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 98
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 97
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 96
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 95
c [cce-7-1] eliminated 1 clauses out of 1 (100%) of length 94
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 93
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 92
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 91
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 90
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 89
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 88
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 87
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 86
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 85
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 84
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 83
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 82
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 81
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 80
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 79
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 78
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 77
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 76
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 75
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 74
c [cce-7-1] eliminated 2 clauses out of 2 (100%) of length 73
c [cce-7-1] eliminated 1 clauses out of 2 (50%) of length 72
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 71
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 70
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 69
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 68
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 67
c [cce-7-1] eliminated 2 clauses out of 3 (67%) of length 66
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 65
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 64
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 63
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 62
c [cce-7-1] eliminated 4 clauses out of 5 (80%) of length 61
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 60
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 59
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 58
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 57
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 56
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 55
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 54
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 53
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 52
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 51
c [cce-7-1] eliminated 2 clauses out of 5 (40%) of length 50
c [cce-7-1] eliminated 4 clauses out of 4 (100%) of length 49
c [cce-7-1] eliminated 2 clauses out of 4 (50%) of length 48
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 47
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 46
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 45
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 44
c [cce-7-1] eliminated 5 clauses out of 6 (83%) of length 43
c [cce-7-1] eliminated 4 clauses out of 6 (67%) of length 42
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 41
c [cce-7-1] eliminated 5 clauses out of 7 (71%) of length 40
c [cce-7-1] eliminated 6 clauses out of 7 (86%) of length 39
c [cce-7-1] eliminated 6 clauses out of 9 (67%) of length 38
c [cce-7-1] eliminated 8 clauses out of 10 (80%) of length 37
c [cce-7-1] eliminated 7 clauses out of 11 (64%) of length 36
c [cce-7-1] eliminated 9 clauses out of 11 (82%) of length 35
c [cce-7-1] eliminated 9 clauses out of 14 (64%) of length 34
c [cce-7-1] eliminated 13 clauses out of 16 (81%) of length 33
c [cce-7-1] eliminated 11 clauses out of 16 (69%) of length 32
c [cce-7-1] eliminated 12 clauses out of 15 (80%) of length 31
c [cce-7-1] eliminated 11 clauses out of 15 (73%) of length 30
c [cce-7-1] eliminated 13 clauses out of 18 (72%) of length 29
c [cce-7-1] eliminated 13 clauses out of 17 (76%) of length 28
c [cce-7-1] eliminated 13 clauses out of 17 (76%) of length 27
c [cce-7-1] eliminated 11 clauses out of 16 (69%) of length 26
c [cce-7-1] eliminated 16 clauses out of 18 (89%) of length 25
c [cce-7-1] eliminated 11 clauses out of 18 (61%) of length 24
c [cce-7-1] eliminated 14 clauses out of 19 (74%) of length 23
c [cce-7-1] eliminated 14 clauses out of 19 (74%) of length 22
c [cce-7-1] eliminated 16 clauses out of 20 (80%) of length 21
c [cce-7-1] eliminated 14 clauses out of 20 (70%) of length 20
c [cce-7-1] eliminated 15 clauses out of 19 (79%) of length 19
c [cce-7-1] eliminated 13 clauses out of 18 (72%) of length 18
c [cce-7-1] eliminated 15 clauses out of 20 (75%) of length 17
c [cce-7-1] eliminated 13 clauses out of 19 (68%) of length 16
c [cce-7-1] eliminated 15 clauses out of 20 (75%) of length 15
c [cce-7-1] eliminated 15 clauses out of 21 (71%) of length 14
c [cce-7-1] eliminated 17 clauses out of 27 (63%) of length 13
c [cce-7-1] eliminated 24 clauses out of 28 (86%) of length 12
c [cce-7-1] eliminated 19 clauses out of 29 (66%) of length 11
c [cce-7-1] eliminated 25 clauses out of 59 (42%) of length 10
c [cce-7-1] eliminated 72 clauses out of 126 (57%) of length 9
c [cce-7-1] eliminated 44 clauses out of 110 (40%) of length 8
c [cce-7-1] eliminated 42 clauses out of 145 (29%) of length 7
c [cce-7-1] eliminated 16 clauses out of 2717 (1%) of length 6
c [cce-7-1] incomplete large round (ACCE)
c [cce-7-1] eliminated 725 large clauses in 26685878 steps
c [cce-7-1] allowing another 13342939 steps for small clauses
c [cce-7-1] scheduling 262421 clauses = 175066 binary + 87355 ternary
c [cce-7-1] tried to eliminate 761 small clauses 0%
c [cce-7-1] eliminated 108 binary clauses 0%
c [cce-7-1] eliminated 16 ternary clauses 0%
c [cce-7-1] eliminated 124 small clauses 0%
c [cce-7-1] eliminated 280 small clauses in 26685860 steps
c [cce-7-1] incomplete small round (ACCE)
c [cce-7-1] eliminated 1005 covered clauses in round 1
c [cce-7] eliminated 1005 covered clauses in TOTAL during 1 rounds
c [cce-7] 1005 < 1/100 * 322146 = 3221 considered unsuccessful
c [bca-19] limit of 10000000 steps and 643541 added (scaled 2)
c [bca-19] 60471 out of 93558 literals actually usable 65%
c [bca-19] added 13 blocked clauses in 184128 steps
c [sweep-19] limit 25618424 penalty 0 = 0 + 0
c [sweep-19-1] 7882 pos 16.8% + 38896 neg 83.2% = 46778 sched 100.0% ret 0
c [sweep-19-1] 25685993 steps 402 queries 659.58 avg class size
c [sweep-19-1] 12050 decisions 389 SAT calls 210.39 avg env size
c [sweep-19-1] 33240 variables remain 71% (13530 retained 29%)
c [decomp-61] removed 31 variables
c [sweep-19-1] removed 31 vars (0 failed, 14 eqs, 25 impls)
c [sweep-19] 31 < 1/1000 * 46778 = 46 considered unsuccessful
c [sweep-19] removed 31 vars in TOTAL (1 rounds, 401 queries)
c [sort-queue-23] sorted 11220 enqueued variables after 337606 conflicts
c [score-dist-23] active 35527 (76%), one 6032 (13%), zero 5188 (11%)
c [score-dist-23] max exp 510, different 425 (83%)
c [score-dist-23] median active exp 490, avg 398.1
c [simplification-23] removed 60 variables 0.1% (46747 remain 19%)
c [simplification-23] removed 6158 irredundant clauses 1.9% (320988 remain 23%)
c [simplification-23] maximum reduction of 2% = max (0%, 2%)
c [simplification-23] geometric conflict interval increment 23145 = 69436 / 3
c [simplification-23] new conflict interval 92581
c [simplification-23] penalized conflict interval 92581 = 1 * 92581
c [simplification-23] hard conflict limit 476477 (soft 430187 + delta 46290)
c [simplification-23] new conflict limit 430187 (hard 476477)
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  565.1   46746   320988    356013   64670   4252 1385270  193   474  140  41%    521    8  133  225   59%
c -  565.4   46746   320988    356438   33846   4255 1385271  179   439   70  41%    259  -28   58  223   26%
c i  565.4   46745   320988    356661   34040   4256 1385273  171   419   75  41%    161  -47   36  223   16%
c i  576.3   46744   320988    367187   41126   4301 1385297  245   429   96  57%    -79  -41  152  228   67%
c i  580.9   46743   320988    372706   44732   4336 1385299  257   472  105  54%   -143    4  213  230   93%
c i  581.2   46742   320988    373024   44932   4336 1385299  259   473  106  55%   -160    5  271  230  118%
c i  588.8   46741   320988    380393   49633   4358 1385310  259   484  119  54%    -97   11  267  235  114%
c i  605.5   46740   320988    395359   58898   4402 1385342  296   491  152  60%     39   -6  157  256   61%
c i  606.1   46739   320988    395867   59189   4403 1385350  300   497  152  60%    -45    0  324  257  126%
c i  611.6   46738   320988    400408   62017   4418 1385368  302   514  153  59%   -114   17  349  260  134%
c -  620.7   46738   320988    408563   34955   4438 1385376  268   445   72  60%    -46  -48  257  260   99%
c i  620.9   46737   320988    408740   35091   4438 1385376  267   443   77  60%    -43  -50  254  260   98%
c i  636.9   46736   320988    421583   40796   4491 1385408  248   360  100  69%     38 -112  277  258  107%
c i  638.7   46735   320988    424480   42938   4508 1385421  168   424  102  40%   -102  -42   60  251   24%
c 
c [simplification-24] limit 430187 conflicts (hard 476477) hit after 434001 conflicts
c [quatres-18] found 28656 quaternary clauses 54% in total
c [quatres-18-1] removed 1 duplicate quaternary clauses
c [ternres-19] limit 108802061 with penalty 0 = 0 + 0
c [ternres-19] all 46735 free variables schedulable
c [ternres-19] 82 ternary resolvents (0 bin, 82 trn)
c [ternres-19] fully completed ternary resolution
c [decomp-62] removed 12 variables
c [basicprobe-8] limit 400000000 penalty 0 = 0 + 0
c [basicprobe-8-0] 8837 sched 19%, 354 failed, 2 lifted, 186593 hbrs
c [decomp-63] removed 473 variables
c [basicprobe-8-1] 3416 probes remain 7% after last round
c [basicprobe-8-1] 464 units = 462 failed (100%) + 2 lifted (0%)
c [basicprobe-8-1] removed 700 variables, found 252472 hbrs
c [bate-6] eliminated 179 asymmetric tautologies during probing
c [unhide-24] limit 5000000 with penalty 2 = 0 + 2
c [unhide-24-30] 0 units, 18 failed, 86990 tauts, 0 hbrs, 289242 literals
c [transred-20] limit 2000000 with penalty 0 = 0 + 0
c [transred-20] removed 110 transitive binary clauses
c [elim-19] no untried remaining variables left
c [elim-19] scheduled 46033 variables 100%
c [elim-19] limit of 400000000 steps penalty 1 = 1 + 0
c [elim-19] rescheduling of touched variables disabled
c [elim-19-1] eliminated 1484 variables 3% in round 1 in 26630534 steps
c [elim-19-1] backward subsumption/strengthening limit 26630500
c [elim-19-1-1] backward checking 6647 touched variables 14%
c [elim-19-1-1] fully completed backward checking in 1 rounds
c [elim-19-1] subsumed 8 and strengthened 78 clauses in 1610069 steps
c [elim-19-1] rescheduled 230 variables 0% by backward subsumption
c [elim-19-2] eliminated 25 variables 0% in round 2 in 224858 steps
c [elim-19-2] backward subsumption/strengthening limit 224800
c [elim-19-2-1] backward checking 232 touched variables 1%
c [elim-19-2-1] fully completed backward checking in 1 rounds
c [elim-19-2] subsumed 0 and strengthened 5 clauses in 150615 steps
c [elim-19-2] rescheduled 20 variables 0% by backward subsumption
c [elim-19-3] eliminated 2 variables 0% in round 3 in 20235 steps
c [elim-19-3] backward subsumption/strengthening limit 20200
c [elim-19-3-1] backward checking 23 touched variables 0%
c [elim-19-3-1] incomplete backward checking 0 remain 0%
c [elim-19-3] subsumed 0 and strengthened 2 clauses in 20201 steps
c [elim-19] incomplete 8 not tried 0% in round 3
c [elim-19] transition to [ all 1 rem 1 ] state
c [elim-19] eliminated 1511 = 3% variables out of 46033 scheduled
c [bca-20] limit of 10000000 steps and 620927 added (scaled 2)
c [bca-20] 60869 out of 89046 literals actually usable 68%
c [bca-20] added 504 blocked clauses in 162994 steps
c [sort-queue-24] sorted 12318 enqueued variables after 434001 conflicts
c [score-dist-24] active 32204 (72%), one 7770 (17%), zero 4548 (10%)
c [score-dist-24] max exp 510, different 418 (82%)
c [score-dist-24] median active exp 491, avg 464.6
c [simplification-24] removed 2213 variables 4.7% (44522 remain 18%)
c [simplification-24] removed 11157 irredundant clauses 3.5% (309831 remain 22%)
c [simplification-24] maximum reduction of 5% = max (5%, 3%)
c [simplification-24] large reduction 5% >= 5% limit
c [simplification-24] next conflict interval 4340 = min (434001/100, 92581)
c [simplification-24] penalized conflict interval 4340 = 1 * 4340
c [simplification-24] hard conflict limit 448341 (soft 438341 + delta 10000)
c [simplification-24] new conflict limit 438341 (hard 448341)
c 
c [simplification-25] limit 438341 conflicts (hard 448341) hit after 445847 conflicts
c [ternres-20] limit 110589875 with penalty 0 = 0 + 0
c [ternres-20] all 44522 free variables schedulable
c [ternres-20] 246 ternary resolvents (0 bin, 246 trn)
c [ternres-20] fully completed ternary resolution
c [gauss-6] limit 1382373 penalty 4 = 4 + 0
c [gauss-6] extracted 23 xors of average arity 2.9
c [gauss-6] connected 67 occurrences of 50 variables (average 1.3)
c [gauss-6] limit 1382373 penalty 4 = 4 + 0
c [gauss-6] fully completed
c [gauss-6] exported 0 unary, 0 binary and 0 ternary equations
c [decomp-64] removed 1 variables
c [simpleprobe-9] 1222 schedulable variables 3%
c [simpleprobe-9] limit 200000000 penalty 0 = 0 + 0
c [decomp-65] removed 5 variables
c [simpleprobe-9] 1708 variables remain 4% (42808 retained 96%)
c [simpleprobe-9] removed 5 variables, found 71244 hbrs, 2 units
c [unhide-25] limit 10000000 with penalty 1 = 0 + 1
c [unhide-25-34] 0 units, 1 failed, 100884 tauts, 0 hbrs, 359132 literals
c [transred-21] limit 2000000 with penalty 0 = 0 + 0
c [transred-21] removed 80 transitive binary clauses
c [elim-20] no untried remaining variables left
c [elim-20] scheduled 44515 variables 100%
c [elim-20] limit of 800000000 steps penalty 0 = 0 + 0
c [elim-20] rescheduling of touched variables disabled
c [elim-20-1] eliminated 80 variables 0% in round 1 in 26188818 steps
c [elim-20-1] backward subsumption/strengthening limit 26188800
c [elim-20-1-1] backward checking 745 touched variables 2%
c [elim-20-1-1] fully completed backward checking in 1 rounds
c [elim-20-1] subsumed 0 and strengthened 3 clauses in 234717 steps
c [elim-20-1] rescheduled 14 variables 0% by backward subsumption
c [elim-20-2] eliminated 1 variables 0% in round 2 in 8304 steps
c [elim-20-2] backward subsumption/strengthening limit 8300
c [elim-20-2-1] backward checking 10 touched variables 0%
c [elim-20-2-1] incomplete backward checking 0 remain 0%
c [elim-20-2] subsumed 0 and strengthened 1 clauses in 8301 steps
c [elim-20-2] rescheduled 4 variables 0% by backward subsumption
c [elim-20-3] no variable eliminated in round 3 in 1264 steps
c [elim-20] fully completed in 3 rounds
c [elim-20] transition to [ all 0 rem 0 ] state
c [elim-20] eliminated 81 = 0% variables out of 44515 scheduled
c [elim-20] 81 < 1/100 * 44515 = 445 considered unsuccessful
c [bca-21] limit of 10000000 steps and 614251 added (scaled 2)
c [bca-21] 59685 out of 88870 literals actually usable 67%
c [bca-21] added 19 blocked clauses in 166284 steps
c [sweep-20] limit 16588481 penalty 1 = 1 + 0
c [sweep-20-1] 7040 pos 22.0% + 24929 neg 78.0% = 31969 sched 71.9% ret 12465
c [sweep-20-1] 16649373 steps 339 queries 754.83 avg class size
c [sweep-20-1] 6804 decisions 329 SAT calls 151.49 avg env size
c [sweep-20-1] 26225 variables remain 59% (18208 retained 41%)
c [decomp-66] removed 13 variables
c [sweep-20-1] removed 13 vars (0 failed, 9 eqs, 20 impls)
c [sweep-20] 13 < 1/1000 * 44434 = 44 considered unsuccessful
c [sweep-20] removed 13 vars in TOTAL (1 rounds, 338 queries)
c [sort-queue-25] sorted 11928 enqueued variables after 445847 conflicts
c [score-dist-25] active 32493 (73%), one 7398 (17%), zero 4530 (10%)
c [score-dist-25] max exp 510, different 422 (83%)
c [score-dist-25] median active exp 499, avg 457.1
c [simplification-25] removed 101 variables 0.2% (44421 remain 18%)
c [simplification-25] removed 3562 irredundant clauses 1.1% (306269 remain 22%)
c [simplification-25] maximum reduction of 1% = max (0%, 1%)
c [simplification-25] geometric conflict interval increment 46290 = 92581 / 2
c [simplification-25] new conflict interval 138871
c [simplification-25] penalized conflict interval 138871 = 1 * 138871
c [simplification-25] hard conflict limit 654153 (soft 584718 + delta 69435)
c [simplification-25] new conflict limit 584718 (hard 654153)
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 -  728.3   44421   306269    506958   35298   4534 1288002  145   207   67  70%    688 -149  130  196   66%
c i  735.0   44420   306269    516903   42877   4591 1288023  191   510   89  37%    735  158  348  193  180%
c -  770.4   44420   306269    562634   37402   4734 1288120  120   275   68  44%    150  -76   66  189   35%
c i  775.3   44419   306269    571593   43911   4781 1288163   87   544   83  16%    262  196   76  177   43%
c 
c [simplification-26] limit 584718 conflicts (hard 654153) hit after 602073 conflicts
c [quatres-19] found 30457 quaternary clauses 55% in total
c [quatres-19-1] removed 3 duplicate quaternary clauses
c [ternres-21] limit 140100481 with penalty 0 = 0 + 0
c [ternres-21] all 44419 free variables schedulable
c [ternres-21] 79 ternary resolvents (0 bin, 79 trn)
c [ternres-21] fully completed ternary resolution
c [decomp-67] removed 2 variables
c [treelook-9] limit 14010048 penalty 0 = 0 + 0 boost 1
c [treelook-9] scheduled 62505 literals 70%
c [treelook-9] scheduling used 2197839 steps
c [treelook-9] scheduled completely
c [treelook-9] limit 14010048 penalty 0 = 0 + 0 boost 1
c [treelook-9] used 14011968 steps
c [treelook-9] 62236 literals remain 70%
c [treelook-9] 12630 variables remain to probed next time 28%
c [treelook-9] removed 0 variables, found 28791 hbrs
c [unhide-26] limit 5000000 with penalty 2 = 0 + 2
c [unhide-26-35] 0 units, 0 failed, 23963 tauts, 0 hbrs, 1008708 literals
c [transred-22] limit 2000000 with penalty 0 = 0 + 0
c [transred-22] removed 90 transitive binary clauses
c [block-7] scheduling all variables this time
c [block-7] scheduled 44419 variables 100%
c [block-7] limit of 50000000 steps penalty 4 = 4 + 0
c [block-7] fully completed
c [block-7] transition to [ all 0 rem 0 ] state
c [block-7] eliminated 2 blocked clauses
c [block-7] 2 < 1/100 * 306196 = 3061 considered unsuccessful
c [bca-22] limit of 10000000 steps and 613915 added (scaled 2)
c [bca-22] 55511 out of 88840 literals actually usable 62%
c [bca-22] added 9 blocked clauses in 185599 steps
c [sort-queue-26] sorted 11316 enqueued variables after 602073 conflicts
c [score-dist-26] active 33103 (75%), one 6858 (15%), zero 4458 (10%)
c [score-dist-26] max exp 510, different 420 (82%)
c [score-dist-26] median active exp 484, avg 449.4
c [simplification-26] removed 0 variables 0.0% (44419 remain 18%)
c [simplification-26] removed 75 irredundant clauses 0.0% (306194 remain 22%)
c [simplification-26] maximum reduction of 0% = max (0%, 0%)
c [simplification-26] full geometric conflict interval increment 138871
c [simplification-26] new conflict interval 277742
c [simplification-26] penalized conflict interval 277742 = 1 * 277742
c [simplification-26] hard conflict limit 1018686 (soft 879815 + delta 138871)
c [simplification-26] new conflict limit 879815 (hard 1018686)
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 -  816.2   44419   306194    611397   39347   4979 1292689  140  1027   71  14%    136  537  131  211   62%
c i  817.1   44418   306194    613155   40628   4986 1292701  149   820   82  18%    159  318  120  210   57%
c -  847.6   44418   306194    658463   39447   5188 1292823  188   385   69  49%    260 -131  238  205  116%
c -  894.1   44418   306194    716739   41076   5317 1292919  149   496   69  30%    710   79  218  187  117%
c -  951.9   44418   306194    780036   41482   5415 1292978  245   414   70  59%    905   67  391  186  210%
c i  982.6   44417   306194    817343   65834   5511 1293038  121   264  136  46%    956  -78   97  174   56%
c
c CAUGHT SIGNAL 15 SIGTERM
c
c s UNKNOWN
c bate: 1847 basic ate = 1721 trn 93% + 126 lrg 7% in 6 updates
c bcas: 22 count, 2063 added (326 skipped), 6094930 steps
c bkwd: tried 512664 clauses, 1024887 lits, 2.00 lits/clause
c bkwd: checked 17271526 occs, 33.69 occs/clause, 16.85 occs/lit
c bkwd: subsumed 12 binary, 123 ternary, 49 large
c bkwd: strengthened 0 binary, 0 ternary (0% self), 1159 large (0% self)
c blkd: 7 bces, 12720 removed, 11773498 resolutions, 32675340 steps
c blkd: 14192 blocking literals 3%, 8 pure
c bump: 832864 bumped seen, 612320830 lits 735.2 on average
c card: 6 count, 0 units, 0 am1, 488856826 steps
c card: 0 rescheduled, 0 eliminated, 0 resolved, 73421 subsumed
c card: 17079 at-most-one constraints found, average size 4.83
c card: 17079 at-most-one constraints used 100%, average size 4.83
c card: 0 at-most-two constraints found, average size 0.00
c card: 0 at-most-two constraints used 0%, average size 0.00
c cces: 7 cces, 19980 eliminated, 19854 ate 99%, 126 abce 1%
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: 4749826 add, 0 assume, 0 deref, 0 failed
c clls: 0 lkhd, 0 cassume, 0 mosat
c coll: 190 gcs, 0 rescored clauses, 3230 rescored vars
c dcps: 68 decompositions, 11215 equivalent 4%
c deco: 262888 decision-only clauses 32%, 64% reduction
c decs: 17829899 total, 0 rnd 0.000%, 0 heap 0.000%, %lld queue 0.000%
c elms: 20 elims, 103237 eliminated 40%, 30 pure 0%
c elms: 61 rounds, 3.0 rounds/bve
c elms: 82914 small 80%, 20285 large 20%
c elms: 274010 tried small, 82914 succeeded 30%, 191096 failed 70%
c elms: 59029 subsumed, 68254 strengthened, 1533 blocked
c elms: 30808981 copies, 30031439 resolutions, 8175470 ipos
c elms: 8740532 subchks, 5419160 strchks
c gaus: 6 extractions, 570 extracted, 2.2 size, 3 max
c gaus: exported 0 units, 0 binary and 0 ternary equations
c gaus: 0 gc, 12286970 steps, 6143485 extr 50%, 20044 elim 0%
c glue: 202.4 orig avg, 202.4 real avg, 9.0 scaled avg
c glue: 0 maxscaledglue=15 (0%), 0 kept 0%
c hbrs: 3653201 = 516430 simple 14% + 3085163 trn 84% + 51608 lrg 1%, 7533 sub 0%
c ints: 0 luby (0 steps), 0 inout (0 steps)
c locs: 0 count, 0 flips, 0 mems, 2147483647 minimun
c lrnd: 832864 clauses, 315.8 length
c lrnd: 263058099 lits = 457406297 orig - 194348198 removed 42%
c lrnd: 410739 uips 49%, 349581 flips 42%
c mins: 456760 mins 62%, 3729 bin 1%, 10357 size 1%
c mins: 211176208 poisoned searches, 43500334 hits, 21% hit rate
c mins: 262640813 used twice searches, 24295441 hits, 9% hit rate
c move: moved 22688, 13886 bin 61%, 8802 trn 39%
c otfs: 8454 driving 30%, 19597 restarting 70%
c otfs: str 28051, 27962 red 100%, 89 irr 0%
c otfs: str 28051, 0 bin 0%, 137 trn 0%, 27914 lrg 100%
c otfs: sub 102, 102 red 100%, 0 irr 0%
c otfs: sub 102, 0 bin 0%, 2 trn 2%, 100 lrg 98%
c phas: 14 computed, 128892 set, 3 pos (0%), 128889 neg (100%)
c prbs: 8 basic, 94043 probed, 4681 failed, 48 lifted
c prbs: 9 simple, 810787 probed, 2804 failed, 834 eqs
c prbs: 9 treelook, 700 probed, 20 failed, 0 lifted
c prom: 74083 locked 3% out of 2265934 tried
c prps: 2359596489 props, 123 props/dec
c prps: 93% srch, 7% simp, 0% lkhd
c quat: 19 count, 74 quat, 24 self1, 0 self2, 3717 dup
c queu: 26 sorted, 17829899 next (119627 steps 0.01)
c queu: 736809420 enq (1331001067 steps 1.81), 612320830 deq 83%
c redc: 8363 clauses 30%, 27808 tried 3%, 100 sat 0%
c redc: 22137 lits 8%, 292274 tried 0%, 100 sat 0%
c redc: 977 times jump level reduced, 73.4 levels on average
c reds: 12 count, 69658.8 conflicts per reduce
c reds: 0 memlim 0%, 12 arith 100%
c reds: 333131 collected 87%, 48179 retired 13%
c rmbd: 66184 removed, 18455 red 28%
c rsts: 16935 restarts 100%, 0 skipped 0%
c rsts: 0 saturating 0%, 0 reuse 0%
c rsts: 0 kept 0.0% average 0.0%
c scnc: 0 count, 1.000 min (0/1000), 1.000 max (0/1000)
c simp: 26 count, 23 confs 88%, 0 vars 0%
c simp: 2 its 8%, 1 bin 4%, 0 trns 0%
c subl: 832864 count (963818 tried 1.2), 266811 sub out of 821320 (32.5%)
c swps: 20 count, 22 rounds, 21930 queries (996.8/round)
c swps: 20380 sat calls, 150 unsat (0.3% success rate)
c swps: 220236 decisions 10.8, 5413 conflicts 0.3
c swps; 346.6 avg class size, 84.6 avg environment size
c swps: 1 failed, 2992 impls, 1644 equivs
c swp0: 7302 type 0 queries, 3563 unsat (48.8%), 6804 sat (93.2%)
c swp1: 14628 type 1 queries, 7956 unsat (54.4%), 13482 sat (92.2%)
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: 37333016 calls to obtain time
c tops: 101473 fixed 39%, 537 its, 1556.62 confs/it
c trds: 22 transitive reductions, 3676 removed, 11 failed
c trds: 17058 nodes, 52650 edges, 44033648 steps
c trim: 4776763 words, 18.2 MB
c trnr: 21 count, 11 bin, 2743 trn, 292885385 steps
c unhd: 26 count, 35 rounds, 139624096 steps
c unhd: 1790 non-trivial sccs of average size 2.1
c unhd: 57 units, 56 bin, 0 trn, 1 lrg
c unhd: 13870 failed, 13711 stamp, 0 lits, 126 bin, 15 trn, 1 lrg
c unhd: 1045203 tauts, 15188 bin 1%, 14734 trn 1%, 765 lrg 0%
c unhd: 1045203 tauts, 1014516 stamp 97%, 955888 red 91%
c unhd: 0 hbrs, 0 trn 0%, 0 lrg 0%, 0 red 0%
c unhd: 6592677 str, 56 bin 0%, 2939 trn 0%, 6589682 lrg 100%, 6573153 red 100%
c vars: 44417 remaining 17% and 215925 removed 83% out of 260342
c vars: 101473 fixed 39%, 103237 eliminated 40%, 11215 equivalent 4%
c vsts: 19894924123 visits, 93% srch, 7% simp, 0% lkhd
c vsts: 8.4 search visits per propagation, 22136.2 per conflict
c wchs: 1432625833 pushed, 70420640 enlarged, 284 defrags
c 
c scaled glue      added       reduced       retired       forcing      resolved     conflicts   maxmb
c 
c all         821394        333131         48179      73916041      12654779        385057
c 
c  0 0         26917   3      3226   1         0   0  27910968  38   3097265  24     45819  12     1.0
c  1 5          7936   1      2167   1      1281   3   4429542   6    593062   5     10434   3     0.3
c  2 6         19232   2      6092   2      2376   5   8134154  11   1165951   9     25019   6     1.0
c  3 9         27664   3     10610   3      2710   6   7756496  10<  1283212  10     30644   8     1.8
c  4 14        33845   4     15452   5      3088   6   6792275   9   1321433  10<    31653   8     2.5
c  5 21        39913   5     21314   6      3091   6   5623344   8   1199151   9     33502   9     3.1
c  6 30        41837   5     26430   8      2636   5   3470419   5    851948   7     29377   8<    3.3
c  7 41        44666   5     29759   9      2708   6   2555780   3    638814   5     23276   6     3.6
c  8 54        46030   6     30737   9      2640   5   1781943   2    509064   4     21265   6     4.8
c  9 69        45696   6<    30446   9<     2479   5<  1305822   2    412295   3     20214   5     6.8
c 10 86        68607   8     44377  13      4121   9   1532674   2    534582   4     28851   7     8.4
c 11 126      132547  16     50451  15      6449  13   1583259   2    542282   4     33441   9    15.1
c 12 230      215243  26     46517  14      9718  20    858149   1    416929   3     42445  11    34.0
c 13 534       71261   9     15553   5      4882  10    181216   0     88791   1      9117   2    33.6
c 
c avg                  9.1           8.6           8.6           2.8           4.2           6.3
c std                  3.6           3.0           3.7           3.1           3.7           4.0
c 
c  120.968  12% bump
c   82.890   8% probe
c   47.738   5% sweep
c   37.970   4% unhide
c   27.490   3% elim
c   15.989   2% rescore
c   11.239   1% decide
c   10.128   1% cce
c    5.523   1% bca
c 
c   11.953 < 1% rest (below)
c 
c    3.739   0% block
c    2.686   0% transred
c    2.050   0% gauss
c    1.779   0% ternres
c    1.299   0% quatres
c    0.401   0% card
c    0.000   0% locs
c    0.000   0% queuesort
c ==================================
c    5.051   1% preprocessing     2%
c  236.358  24% inprocessing     98%
c ==================================
c  241.410  24% simplifying
c  757.874  76% search
c ==================================
c  999.288 100% all
c 
c        835905 conflicts,         836.5 confs/sec
c          5089 ternaries,         164.3 confs/ternary
c          4678 binaries,          178.7 confs/binary
c           537 iterations,       1556.6 confs/iteration
c 
c            12 reductions,          0.0 redus/sec,  69658.8 confs/reduction
c         16935 restarts,           16.9 rests/sec,     49.4 confs/restart
c      17829899 decisions,       17842.6 decis/sec,     21.3 decis/conflict
c    2359596489 propagations,  2361278.1 props/sec,    132.3 props/decision
c 
c 999.3 seconds, 184.9 MB
c
c CAUGHT SIGNAL 15 SIGTERM
c
c launch: done
